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 <e...@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_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
