[Haskell-cafe] Equality constraints in type families

[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? 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).

Thanks.
-- Dan