Repeated variables in type family instances

[AntC]

> Richard Eisenberg <eir <at> cis.upenn.edu> writes:

Hi Richard, I was hoping one of the type/class/family luminaries would 
pick this up, but I'll make a crack at moving it along.

>  
> It’s come to my attention that there is a tiny lurking potential hole in 
> GHC’s type safety around type families in the presence of 
> UndecidableInstances. ...

Hmm. Several things seem 'fishy' in your examples. I'll take the second 
one first:

> > type family G
> > type family G = [G]
>  
> This declarations are all valid in GHC 7.6.3.

G is 0-adic, so only one instance is allowed, so it should be like a 
simple type synonym. What about:

>    type G2 = [G2]

     ghc rejects "Cycle in type synonym declarations"

But I guess ghc doesn't want to make a special case of 0-adic type 
functions. Really that G instance is no different to:

>    type instance F Int Bool = [F Int Bool]

G's instance is degenerate because I can't declare a term of type G:

>    g :: G
>    g = undefined

ghc says "Occurs check: cannot construct the infinite type: uf0 = [uf0]"

This isn't unusual in the borderlands of UndecidableInstances: you can 
declare an instance but never use it.

Now to your main example:
>  
> > type family F a b
> > type instance F x x = Int
> > type instance F [x] x = Bool
> > 

I plain disagree that these are overlapping. That code compiles OK with 
OverlappingInstances switched off (at ghc 7.6.1). What's more, I can 
access both instances:

*Main> :t undefined :: F Int Int
undefined :: F Int Int :: Int
*Main> :t undefined :: F [Int] Int
undefined :: F [Int] Int :: Bool

For them to overlap would require the two arguments to be equal in the 
second instance. In other words: [x] ~ x

Let's try to do that with a class instance:

>    class F2 a b
>    instance ([x] ~ x) => F2 [x] x

ghc rejects "Couldn't match type `x' with `[x]'"


So you haven't yet convinced me that there's anything that needs 'fixing'. 
Especially if you're proposing a breaking change.

I make heavy use of repeated type vars in class instances (in combination 
with an overlapped instance with distinct type vars). I have been waiting 
patiently for overlapping instances to appear with type funs, so I can 
make my code easier to read (more functional ;-). 

I guess the key thing I'm looking for is a type-level test for type 
equality -- which needs repeated type vars(?) 


Anthony