But you have just pushed the problem off to the definition of EQ. And your definition of EQ requires a finite enumeration of all types, I think. But * is open, so that's hard to do. What you want is type instance EQ where EQ a a = TRUE EQ _ _ = FALSE and now we are back where we started.
Not at all. In the first approximation, EQ is the _numerical_ equality, equality of two type-level naturals. Since Goedel numbering is no fun in practice, I agree on the second approximation, described in TTypeable.hs. I quote the beginning of that file for reference:
module TTypeable where {- It helps in understanding the code if we imagine Haskell had algebraic data kinds. We could then say
kind TyCon_name -- name associated with each (registered) type constructor
kind NAT -- Type-level natural numbers kind BOOL -- Type-level booleans
kind LIST a = NIL | a :/ LIST a
-- Type-level type representation kind TYPEREP = (TyCon_name, LIST TYPEREP) -}
-- Type-lever typeOf -- The more precise kind is * -> TYPEREP type family TYPEOF ty :: *
-- Auxiliary families
-- The more precise kind is TyCon_name -> NAT type family TC_code tycon :: *
-- Sample type reps (the rest should be derived, using TH, for example) -- Alternatively, it would be great if GHC could provide such instances -- automatically or by demand, e.g., -- deriving instance TYPEOF Foo
data TRN_unit type instance TC_code TRN_unit = Z type instance TYPEOF () = (TRN_unit, NIL)
data TRN_bool type instance TC_code TRN_bool = S Z type instance TYPEOF Bool = (TRN_bool, NIL)
I could write a TH function tderive to be used as follows. When the user defines a new data type data Foo = ... then $(tderive ''Foo) expands in
data TRN_package_name_module_name_Foo type instance TC_code TRN_package_name_module_name_Foo = <very long type-level numeral that spells package_name_module_name_Foo in unary> type instance TYPEOF Foo = (TRN_package_name_module_name_Foo, NIL)
I think I can write such tderive right now. So, the EQ (or, TREPEQ as I call it) is defined in closed form:
-- Comparison predicate on TYPEREP and its parts
-- TYPEREP -> TYPEREP -> BOOL type family TREPEQ x y :: *
type instance TREPEQ (tc1, targ1) (tc2, targ2) = AND (NatEq (TC_code tc1) (TC_code tc2)) (TREPEQL targ1 targ2)
-- LIST TYPEREP -> LIST TYPEREP -> BOOL type family TREPEQL xs ys :: *
type instance TREPEQL NIL NIL = HTrue type instance TREPEQL NIL (h :/ t) = HFalse type instance TREPEQL (h :/ t) NIL = HFalse type instance TREPEQL (h1 :/ t1) (h2 :/ t2) = AND (TREPEQ h1 h2) (TREPEQL t1 t2)
That is it. These are the all clauses. Again, I have already defined them, and it works in GHC 7.0. Certainly I would be grateful if GHC blessed them with a special attention so they run faster.