<div dir="ltr"><div>Does merely type checking this cause the stack overflow? If so, there's not much excuse, because nothing in your example is executing the bad code. So the stack overflow must be a bug checking this example. Perhaps the termination checker itself is spinning?<br>
</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Sep 4, 2013 at 10:25 AM, Dan Piponi <span dir="ltr"><<a href="mailto:dpiponi@gmail.com" target="_blank">dpiponi@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>This short piece of code causes a stack overflow in 2.3.2.1 (sometimes after a long wait):</div><div>
<br></div><div>{-# OPTIONS --without-K --type-in-type #-}</div><div><br></div><div>module bug where</div>
<div><br></div><div> open import Data.Nat</div><div><br></div><div> infix 3 _≡_</div><div><br></div><div> data _≡_ {A : Set} : A → A → Set where</div><div> refl : {a : A} → a ≡ a</div><div><br></div><div> infixr 14 _■_</div>
<div> _■_ : {A : Set} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)</div><div> refl ■ refl = refl</div><div><br></div><div> f : ℕ → ℕ ≡ ℕ</div><div> f zero = refl</div><div> f (suc n) = f (suc n) ■ refl</div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>