[Agda] nontermination and Sized types

[vlad]

Thank you very much for the information. IMO this bug and others 
(incompatibility of sized types with equality, ...) should be better 
documented.

Best regards,

  - Vlad

On 02/10/2020 15:52, Andrew M. Pitts wrote:
>> On 2 Oct 2020, at 13:36, vlad <Vlad.Rusu at inria.fr> wrote:
>>
>> Looking at (V2) one can notice that nonterminating'  looks like a well-founded induction principle for the _<_ relation on Size, defined by j < i iff (t : Size< i). Which is strange since _<_ is *not* well founded, as ∞ < ∞ holds. Indeed, if nonterminating' were accepted then it could be used to prove that _<_ is  well  founded: just take P s = "there is no infinite <-decreasing sequance starting at s". So, I believe the Agda termination checker rightfully rejects the definition (V2).
> I believe issue #3026 is still open and that at the moment (v2.6.1) Agda allows one to prove _<_ for Size is well-founded and hence derive a logical inconsistency. :-)
>
> Andy
>
>
>