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

[1]: http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf
[2]: https://ghc.haskell.org/trac/ghc/ticket/8162

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.

Richard

On Jul 2, 2014, at 4:19 AM, Brandon Moore <brandon_m_moore@yahoo.com> 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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users