[Agda] slightly wrong sized datatype definition leads to proof of False

[Andrea Vezzosi]

The issue here is only incidentally about sized types. but rather an
issue with the check for when an absurd pattern (i.e. "()") is
allowed:

https://github.com/agda/agda/issues/4995

Btw, the type you defined is more like co-natural numbers, i.e. with
an extra point at infinity, so it's quite natural to have a fix-point
for `suc`.

On Mon, Oct 19, 2020 at 1:44 PM vlad <Vlad.Rusu at inria.fr> wrote:
>
> Thanks for finding this. I guess this is in a longer tradition of
> problems with the sized types implementation, see e.g.
> https://github.com/agda/agda/issues/2820,
> https://github.com/agda/agda/issues/3026,
> https://github.com/agda/agda/issues/1428.
>
> I don't understand whether it has overlap with existing issues. You
> don't use the infinity size, nor equality. So maybe it's a new kind of
> issue, coming from interaction of sizes with inductive types?
>
> It is an elaboration on the bug about well-founded induction and sized types (https://github.com/agda/agda/issues/3026). The main difference with the latter is that, instead of importing the well-founded module of Agda's library, I am using an apparently innocent definition of a sized inductive type :
>
> data ℕ  {s : Size} :  Set where
>   zero :  ℕ
>   suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
>
> as an accessibility predicate for the relation between sized induced by the construction Size<. By using the "size-elimproved" construction (also an elaboration of code found here: https://github.com/agda/agda/issues/2820#issuecomment-339969286) I can then define a "natural number" for each size, including infinity (note that sizes are implicit arguments, so infinity does not show up in the code, but it's there all right). For size = infinity, the "natural number"
>
> foo : ℕ
> foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j } ) _
>
> is easily shown to be a successor of itself, which the definition of "natural numbers" forbids, hence the proof of False.
>
> Overall, I'm not sure it's worth a new bug report, as it is an elaboration of existing constructions. My main point in showing this is that one may easily "believe" that one is defining natural numbers with sizes e.g. for writing non-structural recursive functions over them (like integer division), while in effect writing something else, with unpleasant consequences.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda