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

Hugo Pacheco:

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

You can't check this easily (for the general case). Given type family G a b type FList a x = G a x type instance F [a] = FList a Does FList ignore its second argument? Depends on the type instances of G. Manuel

On Fri, Mar 28, 2008 at 12:04 AM, Manuel M T Chakravarty

...

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