Re: [Haskell-cafe] Equality constraints in type families

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 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