[Agda] Circular proof causes stack overflow

[Wojciech Meyer]

It's not a bug in Agda, but the reason for that is that the recursion
is not terminating at all.

 f (suc n) = f (suc n) ■ refl
the argument is not structurally decreasing, after each recursive call.

You should write instead:
 f (suc n) = f n ■ refl

Wojciech



On Wed, Sep 4, 2013 at 3:25 PM, 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/32bcfe5d/attachment.html