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

[vlad]

> 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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201019/cc00f0d8/attachment.html>