I think instead you should have: - abandoned FunDeps - embraced Overlapping more!
Well, using TypeCast to emulate all FunDeps was demonstrated three years later after HList (or even sooner -- I don't remember when exactly the code was written):
Yes, I see the same idiom. I'll use it below in the definition of the TypeEq predicate.
So here's my conjecture: 1. We don't need FunDeps, except to define TypeCast. (And GHC now has equality constraints, which are prettier.) 2. Without FunDeps, overlapping works fine. ...
I agree on point 1 but not on point 2. The example of incoherence described in Sec `7.6.3.4. Overlapping instances' of the GHC User Guide has nothing to do with functional dependencies.
The question a couple of months ago was: do we need Type-level TypeRep? And you had made a case before that for the TTypeable approach. And TTypeable started life as 'A representation-based equality predicate', Section 9 of the HList paper. And the justification for it was 'Overlapping banned', Section 6. So three questions in light of the approach of abandoning FunDeps and therefore not getting interference with overlapping: A. Does TTypeable need to be so complicated? B. Is TTypeable needed at all? C. Does the 'simplistic' version of type equality testing suffer possible IncoherentInstances? A. I conjecture that TTypeable does not need the TC_code family, nor the phantom type to drive it, nor the NAT encoding. Instead let each type stand for itself, then we just need TYPEOF: type instance TYPEOF () = ( (), NIL ) type instance TYPEOF [a] = ( [()], (TYPEOF a) :/ NIL ) type instance TYPEOF (IO a) = ( IO (), (TYPEOF a) :/ NIL ) -- etc -- I guess TH could generate those instances? Then for testing type equality, we can use a simple overlapping test: type family TypeEq a b :: Bool where { TypeEq a a = True ; TypeEq _ _ = False } This uses the proposed NewAxiom style of type function. Equivalently with a class: instance (TypeCast p TTrue) => TypeEq a a p -- works in Hugs 2002! instance (TypeCast p TFalse) => TypeEq a b p No risk of incoherent instances because the arguments have to be instantiated via TYPEOF. The approach of putting unit as dummy argument to the type constructors means we can also test the 'shape' of the types. 2. But (apart from testing the shape) have we gained anything here over testing the types directly, rather than going via TYPEOF? If the type isn't grounded enough to test for equality (as observed in Section 9 'By chance or by design?'), then neither is it grounded enough to instantiate for TYPEOF. 3. The incoherent instances example in Sec 7.6.3.4 is because of instances defined in separate modules. The simplistic test for type equality declares its two instances together. Is there some way an incoherent instance could slip through? If not, what is the TTypeable mechanism gaining? And by the way, I couldn't help trying a bit of 'compiler archaeology'. I dug out Hugs version November 2002. My revised hDeleteMany works fine, as does my 'repair' to the example in 'Ended up in murky water'. So I can't see a need for TTypeable even back in 2004. AntC