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_mo...@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
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
