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 <brandon_m_mo...@yahoo.com> 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 <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
