# [isabelle] Exhaustiveness of Pure.type

Hello!

`I've recently noticed an unexpected thing about the quite common type
``proxy ‹Pure.type›. My understanding is that it's convenient to use for
``defining type-dependent polymorphic constants, including type class
``members with no normal parameters (say, some abstract number ascribed to
``a type such as its assumed physical size). The thing is, I can't find
``any exhaustiveness theorem related to the constant ‹Pure.type› and its
``type ‹'a itself› e.g. "x ≡ Pure.type" or "(x ≡ Pure.type ⟹ P) ⟹ P".
``Analogous lemma exists for the unit type in HOL and the type itself
``looks similar enough to Haskell's Proxy datatype with a single Proxy
``constructor (which should imply exhaustiveness as with other datatypes).
``The non-exhaustiveness of ‹'a itself› causes a problem when one
``accidentally defines some class axiom with an extra term variable ‹t ::
``'a itself› in place of the ‹Pure.type› constant, sometimes the axiom
``then cannot be proved if the corresponding instance definition is
``specified using the ‹Pure.type› constant, since the definition in the
``goal can be neither unfolded nor refined using the exhaustiveness
``rewrite/elimination rule. Is this situation intentional due to some
``logical limitations I'm not aware of? Of course ‹Pure.type› is part of
``Pure and not even HOL, so it's not technically related to datatypes, but
``is such exhaustiveness axiom incompatible with something important?
`
Regards, Mikhail

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*