Richard Eisenberg
writes: And, in response to your closing paragraph, having type-level equality is the prime motivator for a lot of this work, so we will indeed have it!
Thank you Richard, I'll take comfort in that. I'd beware this though: the Nonlinearity wikipage says "a medium-intensity search did not find any uses of nonlinear ... family instances in existing code, ..." That doesn't surprise me, but I wouldn't put much weight on it. The main purpose of repeated tyvars in a (class) instance is so that you can have a 'wider' overlapping instance with distinct tyvars (and a non-congruent result). Since family instances don't currently support non-congruent overlap, I guess there would be a pent-up demand to translate class instances to (branched?) family instances with repeated tyvars. Here's two example instance from HList that mirror your two instances for family F:
-- pattern of instance F x x class TypeEq a b c | a b -> c instance TypeEq x x HTrue instance (c ~ HFalse) => TypeEq x y c
-- pattern of instance F [x] x -- actually F x (HCons x ...) class Has e l -- constraint instance Has e (HCons e l') instance (Has e l') => Has e (HCons e' l')
I haven't, though, seen those two patterns appearing as instances of the same class. And given that those patterns are to be allowed only within branched instances, the 'cleaned up syntax' makes sense -- I'm glad I suggested it! (see http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage#Suggestio ns, under 'Idiom of a total function' ;-) It still seems mildly 'unfair' to ban repeated tyvars when really the cause of the problem is infinite types. I take you to be saying that as soon as we allow UndecidableInstances, it's just too hard to guard against infinite types appearing from chains of instances, possibly in 'distant' imports or recursive module references. So I understand it's not worth sacrificing type safety. AntC