24 Mar
2008
24 Mar
'08
12:18 a.m.
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