[Agda] Circular proof causes stack overflow

[Dan Piponi]

If I didn't make it clear: Agda itself is crashing on this example.


On Wed, Sep 4, 2013 at 8:39 AM, Dan Doel <dan.doel at gmail.com> wrote:

> 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/20b6efac/attachment.html