[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Claus Reinke:
>>>> type family F a :: * -> *
>> ..
>>> 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
>
> actually, i don't even understand the first part of that:-(
>
> why would F x and F u have to be the same functions?
> shouldn't it be sufficient for them to have the same result,
> when applied to y and v, respectively?

Oh, yes, that is sufficient and exactly what is meant by F x ~ F u.   
It means, the two can be unified modulo any type instances and local  
given equalities.

Manuel