Repeated variables in type family instances

[AntC]

> Richard Eisenberg <eir <at> cis.upenn.edu> 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