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

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
> >
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080328/320637e8/attachment.htm