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

[Vlad Rusu]

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