<br><br><div class="gmail_quote">On Fri, Jan 29, 2010 at 8:56 AM, <span dir="ltr"><<a href="mailto:oleg@okmij.org">oleg@okmij.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
Here is a bit more simplified version of the example. The example has<br>
no value level recursion and no overt recursive types, and no impredicative<br>
polymorphism. The key is the observation, made earlier, that two types<br>
c (c ()) and R (c ())<br>
unify when c = R. Although the GADTs R c below is not recursive, when<br>
we instantiate c = R, it becomes recursive, with the negative<br>
occurrence. The trouble is imminent.<br>
<br>
We reach the conclusion that an instance of a non-recursive GADT<br>
can be a recursive type. GADT may harbor recursion, so to speak.<br>
<br>
The code below, when loaded into GHCi 6.10.4, diverges on<br>
type-checking. It type-checks when we comment-out absurd.<br>
<br>
<br>
{-# LANGUAGE GADTs, EmptyDataDecls #-}<br>
<br>
data False -- No constructors<br>
<br>
data R c where -- Not recursive<br>
R :: (c (c ()) -> False) -> R (c ())<br>
<br>
-- instantiate c to R, so (c (c ())) and R (c ()) coincide<br>
-- and we obtain a recursive type<br>
-- mu R. (R (R ()) -> False) -> R (R ())<br>
<br>
cond_false :: R (R ()) -> False<br>
cond_false x@(R f) = f x<br>
<br>
absurd :: False<br>
absurd = cond_false (R cond_false)<br>
<div><div></div><div class="h5"><br></div></div></blockquote><div><br>GHC (the compiler terminates)<br><br>The following variants terminate, either with GHCi or GHC,<br><br>absurd1 :: False<br>absurd1 = let x = (R cond_false)<br>
in cond_false x <br><br>absurd2 = R cond_false<br><br>absurd3 x = cond_false x<br><br>absurd4 :: False<br>absurd4 = absurd3 absurd2<br><br>This suggests there's a bug in the type checker.<br>If i scribble down the type equation, I can't see<br>
why the type checker should loop here.<br><br>-Martin<br><br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div><div class="h5">
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>