[Agda] Circular proof causes stack overflow

Dan Doel dan.doel at gmail.com
Wed Sep 4 17:39:45 CEST 2013


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?


On Wed, Sep 4, 2013 at 10:25 AM, Dan Piponi <dpiponi at gmail.com> wrote:

> This short piece of code causes a stack overflow in 2.3.2.1 (sometimes
> after a long wait):
>
> {-# OPTIONS --without-K --type-in-type #-}
>
> module bug where
>
>  open import Data.Nat
>
>  infix 3 _≡_
>
>  data _≡_ {A : Set} : A → A → Set where
>    refl : {a : A} → a ≡ a
>
>  infixr 14 _■_
>  _■_ : {A : Set} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
>  refl ■ refl = refl
>
>  f : ℕ → ℕ ≡ ℕ
>  f zero = refl
>  f (suc n) = f (suc n) ■ refl
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130904/36991b86/attachment-0001.html


More information about the Agda mailing list