I'd like to have type-level type representations to _implement_ overlapping type function equations. With type level Typeable, you would not need to do anything about point 2 therefore. The problem 2 will be solved.
There seems no reason in principle to disallow type instance F where F Int = Bool F a = [a]
I would implement this as follows:
type instance F x = F' (EQ (TYPEOF x) INT) x type family F' trep x type instance F' TRUE x = Bool type instance F' FALSE x = [x]
Thanks Oleg. I'm familiar with that style from HList, but it still seems cumbersome to me (compared to separate equations). I suppose a type-level if- then-else would be possible? Does this read any better? type instance F x = IF (EQ (TYPEOF x) INT) Bool [x] I note there by the way, that INT ~ (TYPEOF Int), is that upshifting the name going to work well for all Prelude types? How about (TYPEOF ()) or (TYPEOF [a])? The EQ seems somehow redundant. We can only test type (reps) for equality, or do you envisage inducing some ordering over typereps? How scalable is your approach with multi-argument type functions? Such as: module Mine where type family F a b data Mine = ... type instance F Mine Int = ... type instance F Mine y = ... -- overlap on 2nd arg module Yours where import Mine data Yours = ... type instance F Yours Bool = ... -- no overlap with F Mine b type instance F Yours y = ... -- overlap on 2nd arg We'd need a clan of helper functions F'Mine, F'Yours, etc. This multi-argument example also goes against closed type families, I think.
Finally, could GHC automatically derive instances of TTypeable, which maps types to TYPEREP: type family TTypeable (x :: *) :: TYPEREP
I can see that if we went the route of type-level Typeable, it would need compiler support. But do we need that? Would it be sufficient to have a compiler-supported if-then-else type equality? Perhaps IFEQ, like this: type instance F a = IFEQ a Int Bool [a] type instance F a = (a ?~ Int) Bool [a] -- over-exotic syntax? To be fair to the design you've put into TTypeable, we'd also need to handle polymorphic/partly-ground/higher-ranked types: type instance G a = IFEQ a (Maybe b) b () type instance IsFunction a = IFEQ a (_ -> _) TRUE FALSE -- the classic type instance IsNum a = IFEQ a (Num b => b) a Int And that last example is a worry: what we're calling a type equality test is really a test for unifiability. AntC