[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Dan Doel:
> On Tuesday 11 March 2008, Tom Schrijvers wrote:
>> I think you've uncovered a bug in the type checker. We made the  
>> design
>> choice that type functions with a higher-kinded result type must be
>> injective with respect to the additional paramters. I.e. in your  
>> case:
>>
>> 		F x y ~ F u v <=> F x ~ F u /\ y ~ v
>>
>> So if we apply that to F d c ~ F a (c,a) we get:
>>
>> 	F d ~ F a /\ c ~ (c,a)
>>
>> where the latter clearly is an occurs-check error, i.e. there's no  
>> finite
>> type c such that c = (c,a). So the error in the second version is
>> justified. There should have been one in the latter, but the type  
>> checker
>> failed to do the decomposition: a bug.
>
> While I think I understand why this is (due to the difference  
> between index
> and non-index types), does this mean the following won't type check  
> (it does
> in 6.8, but I gather its type family implementation wasn't exactly  
> complete)?
>
>    type family D a :: *
>    type family E a :: *
>
>    type instance D Int  = Char
>    type instance D Char = Int
>
>    type instance E Char = Char
>    type instance E Int  = Int
>
>    type family F a :: * -> *
>
>    type instance F Int  = D
>    type instance F Char = E
>
>    foo :: F Int Int ~ F Char Char => a
>    foo = undefined
>
> Clearly, both F Int Int ~ Char and F Char Char ~ Char, but neither  
> Int ~ Char
> nor F Int ~ F Char.
>
> Then again, looking at that code, I guess it's an error to have D  
> and E
> partially applied like that?

Exactly.

> And one can't write, say:
>
>    type instance F Int a = D a
>
> correct? I suppose that clears up situations where one might be able  
> to
> construct a specific F X Y ~ F U V, but F X /~ F U \/ Y /~ V (at  
> least, I
> can't thing of any others off the top of my head).

Yes, this type instance is invalid.  However, early version of the  
type family implementation erroneously accepted such instances.

Manuel