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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
