[Agda] Circular proof causes stack overflow

[Dan Doel]

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