Ryan Ingram wrote:
But it doesn't generalize; you need to create a witness of inequality for every pair of types you care about.
One can do better, avoiding the quadratic explosion. One merely needs to establish a map from a type to a suitable, comparable representation -- for example, to a type level list of type level numerals. Comparing types for equality, inequality and even order is a simple matter of comparing their representations. The fact that types become totally ordered lets us even implement type-level maps: Data.Map on types. (We may need a Type.* module hierarchy.) That idea was described in the HList paper http://homepages.cwi.nl/~ralf/HList/paper.pdf Section 9. The code is still available, http://code.haskell.org/HList/examples/TTypeable.hs see also TypeEqExplosive.hs, TypeEqTTypeable.hs.
But given the use of UndecidableInstances and OverlappingInstances, I was hoping that type families could come a little cleaner.
Normally if the use of functional dependencies requires UndecidableInstances, type families would ask for them too. As to OverlappingInstances -- that is the key to generic inequality, isn't it? Given the set of pairs of types, the set of the elements representing non-equal types is the complement of the set of elements representing equal types (by equal I mean identical). Overlapping instances is the way to express set complementation. The most general instance is chosen when none of the more specific apply. The set of types chosen by that general instance is the complement for the set of types chosen by the specific instances.
Does "TypeEq a c HFalse" imply proof of inequality, or unprovability of equality?
We are all constructivists here... If 'a' and 'c' are type variables, (TypeEq a c HFalse) is the constraint -- proof obligation if you will -- making sure the variables will never be instantiated to identical types. Strictly speaking, the constraint is discharged if 'a' and 'c' are two ground, and syntactically distinct (non-identical) types. In reality, I think GHC is able to discharge the constraint if 'a' and 'c' are grounded ``sufficiently enough'' for the difference to become apparent (e.g., the head constructors are different).