[Haskell-cafe] Equality constraints in type families
Hugo Pacheco
hpacheco at gmail.com
Thu Mar 27 12:45:22 EDT 2008
>
> 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/4806d385/attachment.htm
More information about the Haskell-Cafe
mailing list