Re: Closed type families, apartness, and occurs check

But that would mean that `IsEq (F a) (F a)` (for some irreducible-for-now `F a`) is stuck, even when we're sure that it will eventually become True. Your approach is perhaps right, but it has negative consequences, too. Richard On Jul 2, 2014, at 9:58 AM, Brandon Moore wrote:

That was the only thing I worried about, but any examples I tried with families like that ended up with infinite type errors. Infinite types are not meant to be supported, which perhaps gives a solution - the other sensible answer is bottom, i.e. a type checker error or perhaps an infinite loop in the compiler. For instantating with a type family to solve an equation that fails the occurs check, the type family has to be able to already reduce (even if there are some variables), so just adopting the policy that type families be fully expanded before the check would seem to prevent IsEq (G a) [G a] from ever evaulating to true.

Brandon

On Wednesday, July 2, 2014 7:11 AM, Richard Eisenberg wrote:

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