Closed type families, apartness, and occurs check

[Brandon Moore]

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 <eir at cis.upenn.edu> 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 <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/7cef8782/attachment.html>