Closed type families, apartness, and occurs check

Richard Eisenberg eir at
Wed Jul 2 12:11:06 UTC 2014

Hi Brandon,

Yes, this is a dark corner of GHC wherein a proper dragon lurks.

In your second example, you're suggesting that, for all types `a`, `a` is never equal to `[a]`. The problem is: that's not true! Consider:

> type family G x where
>   G x = [G x]

This is a well-formed, although pathological, type family. What should the behavior of `IsEq (G Int) [G Int]` be? The only possible consistent answer is `True`. This is why `IsEq a [a]` correctly does not reduce.

For further information, see section 6 of [1] and for a practical example of how this can cause a program error (with open type families) see [2].


It is conceivable that some restrictions around UndecidableInstances (short of banning it in a whole program, including all importing modules) can mitigate this problem, but no one I know has gotten to the bottom of it.


On Jul 2, 2014, at 4:19 AM, Brandon Moore <brandon_m_moore at> wrote:

> From the user manual, it sounds like a clause of a closed type family should be rejected once no subsitution of the type could make it unify with the clause. If so, it doesn't seem to do an occurs check:
> type family IsEq a b :: Bool where
>   IsEq a a = True
>   IsEq a b = False
> > :kind! forall a . IsEq a a
> forall a . IsEq a a :: Bool
> = forall (a :: k). 'True
> > :kind! forall a . IsEq a [a]
> forall a . IsEq a [a] :: Bool
> = forall a. IsEq a [a]
> I came across this while trying to using Generics to find the immediate children of a term - this sort of non-reduction happens while comparing a type like (Term var) with a constructor argument of type var.
> Brandon
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Glasgow-haskell-users mailing list