Closed type families, apartness, and occurs check

[Richard Eisenberg]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140702/44482750/attachment.html>