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

[Vlad Rusu]

Hi Jesper,

Thanks for the information. On issue less is good news. However, from 
what I understand from earlier exchanges on this list, the more serious 
issue with sized types is the inequality ∞<∞. When that is fixed I would 
be very interested to see the repercussions on existing code such as the 
codata definitions in the standard library and, much more modestly, on a 
development I did that uses sized types.

Best regards,

- Vlad

On 22/10/2020 13:36, Jesper Cockx wrote:
> Hi Vlad,
>
> I just fixed issue #4995 this morning, this also means your example is 
> no longer accepted by the development version of Agda:
>
>     Failed to solve the following constraints:
>       Is empty: n ≡ suc (λ {_} → n) (blocked on _s_49)
>
>
> -- Jesper
>
> On Sat, Oct 17, 2020 at 11:39 PM Vlad Rusu <Vlad.Rusu at inria.fr 
> <mailto:Vlad.Rusu at inria.fr>> 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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201022/156e310e/attachment.html>