[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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 <chak at cse.unsw.edu.au 
> > 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 <hpacheco at gmail.com>
> > 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
> >
> >
>
>