[Haskell-cafe] Equality constraints in type families

Manuel M T Chakravarty chak at cse.unsw.edu.au
Mon Mar 24 00:18:25 EDT 2008

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.


More information about the Haskell-Cafe mailing list