[Agda] Circular proof causes stack overflow

[Andreas Abel]

Dan,

In the darcs version of Agda (upcoming 2.3.4), there is no stack 
overflow, but just the expected complaint by the termination checker.

Seems like the bug you point to is fixed already in the development 
version.

Cheers,
Andreas

On 2013-09-04 17:44, Nils Anders Danielsson wrote:
> On 2013-09-04 16:25, Dan Piponi wrote:
>> This short piece of code causes a stack overflow in 2.3.2.1 
>> (sometimes
>> after a long wait):
>
> The release notes for Agda 2.3.4 (which is under development) 
> currently
> contains the following text:
>
>   Definitions which fail the termination checker are not unfolded any
>   longer to avoid loops or stack overflows in Agda.  However, the
>   termination checker for a mutual block is only invoked after
>   type-checking, so there can still be loops if you define a
>   non-terminating function.  But termination checking now happens
>   before the other supplementary checks: positivity, polarity,
>   injectivity and projection-likeness.
>   Note that with the pragma {-# NO_TERMINATION_CHECK #-} you can make
>   Agda treat any function as terminating.

-- 
Andreas Abel  <><     Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich 
http://www.tcs.informatik.uni-muenchen.de/~abel/