<html><body><div style="color:#000; background-color:#fff; font-family:HelveticaNeue, Helvetica Neue, Helvetica, Arial, Lucida Grande, sans-serif;font-size:12pt"><div><span>That was the only thing I worried about, but any examples I tried with families like that ended up with infinite type errors.</span></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: HelveticaNeue,Helvetica Neue,Helvetica,Arial,Lucida Grande,sans-serif; background-color: transparent; font-style: normal;"><span>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.<br></span></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: HelveticaNeue,Helvetica Neue,Helvetica,Arial,Lucida Grande,sans-serif; background-color: transparent; font-style: normal;"><br><span></span></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: HelveticaNeue,Helvetica Neue,Helvetica,Arial,Lucida Grande,sans-serif; background-color: transparent; font-style: normal;"><span>Brandon<br></span></div> <div class="qtdSeparateBR"><br><br></div><div style="display: block;" class="yahoo_quoted"> <div style="font-family: HelveticaNeue, Helvetica Neue, Helvetica, Arial, Lucida Grande, sans-serif; font-size: 12pt;"> <div style="font-family: HelveticaNeue, Helvetica Neue, Helvetica, Arial, Lucida Grande, sans-serif; font-size: 12pt;"> <div dir="ltr"> <font face="Arial" size="2"> On Wednesday, July 2, 2014 7:11 AM, Richard Eisenberg <eir@cis.upenn.edu> wrote:<br> </font>
</div> <blockquote style="border-left: 2px solid rgb(16, 16, 255); margin-left: 5px; margin-top: 5px; padding-left: 5px;"> <br><br> <div class="y_msg_container"><div id="yiv1069034502"><div><div>Hi Brandon,</div><div><br clear="none"></div><div>Yes, this is a dark corner of GHC wherein a proper dragon lurks.</div><div><br clear="none"></div><div>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:</div><div><br clear="none"></div><div>> type family G x where</div><div>> G x = [G x]</div><div><br clear="none"></div><div>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.</div><div><br clear="none"></div><div>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].</div><div><br clear="none"></div><div>[1]: <a rel="nofollow" shape="rect" target="_blank" href="http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf">http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf</a></div><div>[2]: <a rel="nofollow" shape="rect" target="_blank" href="https://ghc.haskell.org/trac/ghc/ticket/8162">https://ghc.haskell.org/trac/ghc/ticket/8162</a></div><div><br clear="none"></div><div>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.</div><div><br clear="none"></div><div>Richard</div><br clear="none"><div><div class="yiv1069034502yqt5413483431" id="yiv1069034502yqt77158"><div>On Jul 2, 2014, at 4:19 AM, Brandon Moore <<a rel="nofollow" shape="rect"
ymailto="mailto:brandon_m_moore@yahoo.com" target="_blank" href="mailto:brandon_m_moore@yahoo.com">brandon_m_moore@yahoo.com</a>> wrote:</div><br class="yiv1069034502Apple-interchange-newline" clear="none"><blockquote type="cite"><div><div style="background-color:rgb(255, 255, 255);font-family:HelveticaNeue, 'Helvetica Neue', Helvetica, Arial, 'Lucida Grande', sans-serif;font-size:12pt;"><div class="yiv1069034502" style="">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:<br clear="none"></div><br clear="none"><div class="yiv1069034502" style="font-size:16px;font-family:HelveticaNeue, 'Helvetica Neue', Helvetica, Arial, 'Lucida Grande', sans-serif;background-color:transparent;font-style:normal;">type family IsEq a b :: Bool where<br style="" clear="none"> IsEq a a = True<br
class="yiv1069034502" style="" clear="none"> IsEq a b = False<br class="yiv1069034502" style="" clear="none"></div><div class="yiv1069034502" style="font-size:16px;font-family:HelveticaNeue, 'Helvetica Neue', Helvetica, Arial, 'Lucida Grande', sans-serif;background-color:transparent;font-style:normal;"><br clear="none"></div><div class="yiv1069034502" style="font-size:16px;font-family:HelveticaNeue, 'Helvetica Neue', Helvetica, Arial, 'Lucida Grande', sans-serif;background-color:transparent;font-style:normal;">> :kind! forall a . IsEq a a<br class="yiv1069034502" style="" clear="none">forall a . IsEq a a :: Bool<br class="yiv1069034502" style="" clear="none">= forall (a :: k). 'True<br class="yiv1069034502" style="" clear="none">> :kind! forall a . IsEq a [a]<br class="yiv1069034502" style="" clear="none">forall a . IsEq a [a] :: Bool<br class="yiv1069034502" style="" clear="none">= forall a. IsEq a [a]<br class="yiv1069034502" style=""
clear="none"></div><div class="yiv1069034502" style=""><br clear="none"></div><div class="yiv1069034502" style="font-size:16px;font-family:HelveticaNeue, 'Helvetica Neue', Helvetica, Arial, 'Lucida Grande', sans-serif;background-color:transparent;font-style:normal;">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.<br clear="none"></div><div class="yiv1069034502" style="font-size:16px;font-family:HelveticaNeue, 'Helvetica Neue', Helvetica, Arial, 'Lucida Grande', sans-serif;background-color:transparent;font-style:normal;"><br clear="none"></div><div class="yiv1069034502" style="font-size:16px;font-family:HelveticaNeue, 'Helvetica Neue', Helvetica, Arial, 'Lucida Grande', sans-serif;background-color:transparent;font-style:normal;">Brandon<br class="yiv1069034502" style=""
clear="none"></div></div></div>_______________________________________________<br clear="none">Glasgow-haskell-users mailing list<br clear="none"><a rel="nofollow" shape="rect" ymailto="mailto:Glasgow-haskell-users@haskell.org" target="_blank" href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br clear="none">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users<br clear="none"></blockquote></div></div><br clear="none"></div></div><br><br></div> </blockquote> </div> </div> </div> </div></body></html>