[Haskell-cafe] Equality constraints in type families
Hugo Pacheco
hpacheco at gmail.com
Thu Mar 27 12:46:31 EDT 2008
Sorry, I meant
type FList a x = Either One (a,x)
type instance F [a] = FList a
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/20080327/b0d10751/attachment.htm
More information about the Haskell-Cafe
mailing list