[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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