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

[Manuel Bärenz]

You may be interested as well to join the discussion at AIM today. See
https://agda.zulipchat.com/#narrow/stream/257010-aim-xxxiii/topic/Sized.20types
if you want to join.

As far as I am aware the theoretical background is explained in
https://dl.acm.org/doi/10.1145/2500365.2500591 or
http://www.cse.chalmers.se/~abela/jfp15.pdf, but the implementation
doesn't follow the theory exactly, because there are workarounds
necessary when touching (co?)inductive types, or at least datatype
definitions, I believe. Someone who understands the problem and the
implementation better than me please speak up if I'm blathering nonsense
here.

On 19.10.20 11:23, Frédéric Blanqui wrote:
> Hello. I see many problems with sized types in Agda. Is it really just
> a matter of implementation? Some issues are several years old and
> haven't been fixed yet. I am curious: where are described the
> theoretical grounds of the current implementation?
>
> Le 19/10/2020 à 11:15, Manuel Bärenz a écrit :
>> 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?
>>
>> Anyways, I guess it makes sense to report at
>> https://github.com/agda/agda?
>>
>> On 17.10.20 23:38, Vlad Rusu wrote:
>>> The following code shows how a slightly wrong use of sized types in a
>>> definition of natural numbers leads to a proof of  ⊥.
>>>
>>> --------------{-# OPTIONS --sized --safe  #-}
>>> open import Relation.Binary.PropositionalEquality as Eq
>>> open import Data.Empty using (⊥; ⊥-elim)
>>> open import Size
>>>
>>>
>>> -------------- auxiliary--------------
>>> →-elim : ∀ {A B : Set}  → (A → B)  → A  → B
>>> →-elim L M = L M
>>> -- a trick found on the Web_
>>> data [Size<_] (i : Size) : Set where
>>>    box : Size< i → [Size< i ]
>>> unbox : ∀ {i} → [Size< i ] → Size< i
>>> unbox (box j) = j
>>>
>>> --size eliminators
>>> size-elim :  (P : Size → Set) → (∀ i → ((j : [Size< i ]) → P (unbox
>>> j)) → P i) →  ∀ i → P i
>>> size-elim P Hind i = Hind _ λ { (box j) → size-elim P Hind j }
>>> size-elimproved : (P : Size → Set) → (∀ i → ((j : (Size< i)) → P j ) →
>>> P i) →  ∀ i → P i
>>> size-elimproved P Hind i = →-elim (λ {Hind' → size-elim P Hind' i })
>>>                          λ {i' Hind' → Hind i' (λ { j' → Hind' (box
>>> j')  }) }
>>> ------------ end auxiliary-----------
>>>
>>> -- one might think that the following is a definition natural numbers
>>> using some Size arguments
>>> data ℕ  {s : Size} :  Set where
>>>   zero :  ℕ
>>>   suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}
>>>
>>> -- the definition is slightly wrong ("suc" should not contain
>>> ()-parentheses) and leads to a proof of ⊥
>>>
>>> -- introducing foo, a certain natural number
>>> foo : ℕ
>>> foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j } ) _
>>>
>>> -- foo is a successor to itself
>>> bar : foo ≡ suc foo
>>> bar = refl
>>>
>>> -- which is forbidden
>>> baz : ∀ (n : ℕ) → (n ≡ suc λ { _ } → n   ) → ⊥
>>> baz _ ()
>>>
>>> --hence...
>>> zut : ⊥
>>> zut = baz foo bar
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda