<div dir="ltr"><div>If I didn't make it clear: Agda itself is crashing on this example.</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Sep 4, 2013 at 8:39 AM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@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>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"><div><div class="h5">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>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><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></div></div><div class="im">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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></div></blockquote></div><br></div>
</blockquote></div><br></div></div>