> > The current implementation is wrong, as it permits > > type S a b = a > type family F a :: * -> * > type instance F a = S a > > Why do we need to forbid this type instance? Because it breaks the > confluence of equality constraint normalisation. Here are two > diverging normalisations: > > (1) > > F Int Bool ~ F Int Char > > ==> DECOMP > > F Int ~ F Int, Bool ~ Char > > ==> FAIL > > > (2) > > F Int Bool ~ F Int Char > > ==> TOP > > S Int Bool ~ S Int Char > > ==> (expand type synonym) > > Int ~ Int > > ==> TRIVIAL > > This does mean that a program such as
type FList a = Either One ((,) a) type instance F [a] = FList a will be disallowed in further versions? Doesn't this problem occur only for type synonyms that ignore one or more of the parameters? If so, this could be checked... hugo
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
