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
