Yes, but doesn't the confluence problem only occur for type synonyms that ignore one or more of the parameters? If so, this could be checked...
On Fri, Mar 28, 2008 at 12:04 AM, Manuel M T Chakravarty < [EMAIL PROTECTED]> wrote: > Hugo Pacheco: > > Sorry, I meant > > > > type FList a x = Either One (a,x) > > type instance F [a] = FList a > > We should not allow such programs. > > Manuel > > > > > > > On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco <[EMAIL PROTECTED]> > > wrote: > > > > > > 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
