<div dir="ltr"><div>Hi Vlad,</div><div><br></div><div>I just fixed issue #4995 this morning, this also means your example is no longer accepted by the development version of Agda:</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>Failed to solve the following constraints:<br>  Is empty: n ≡ suc (λ {_} → n) (blocked on _s_49)<br></div></blockquote><div><br></div><div>-- Jesper <br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Oct 17, 2020 at 11:39 PM Vlad Rusu <<a href="mailto:Vlad.Rusu@inria.fr">Vlad.Rusu@inria.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The following code shows how a slightly wrong use of sized types in a <br>
definition of natural numbers leads to a proof of  ⊥.<br>
<br>
--------------{-# OPTIONS --sized --safe  #-}<br>
open import Relation.Binary.PropositionalEquality as Eq<br>
open import Data.Empty using (⊥; ⊥-elim)<br>
open import Size<br>
<br>
<br>
-------------- auxiliary--------------<br>
→-elim : ∀ {A B : Set}  → (A → B)  → A  → B<br>
→-elim L M = L M<br>
-- a trick found on the Web_<br>
data [Size<_] (i : Size) : Set where<br>
   box : Size< i → [Size< i ]<br>
unbox : ∀ {i} → [Size< i ] → Size< i<br>
unbox (box j) = j<br>
<br>
--size eliminators<br>
size-elim :  (P : Size → Set) → (∀ i → ((j : [Size< i ]) → P (unbox j)) <br>
→ P i) →  ∀ i → P i<br>
size-elim P Hind i = Hind _ λ { (box j) → size-elim P Hind j }<br>
size-elimproved : (P : Size → Set) → (∀ i → ((j : (Size< i)) → P j ) → P <br>
i) →  ∀ i → P i<br>
size-elimproved P Hind i = →-elim (λ {Hind' → size-elim P Hind' i })<br>
                         λ {i' Hind' → Hind i' (λ { j' → Hind' (box j')  <br>
}) }<br>
------------ end auxiliary-----------<br>
<br>
-- one might think that the following is a definition natural numbers <br>
using some Size arguments<br>
data ℕ  {s : Size} :  Set where<br>
  zero :  ℕ<br>
  suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}<br>
<br>
-- the definition is slightly wrong ("suc" should not contain <br>
()-parentheses) and leads to a proof of ⊥<br>
<br>
-- introducing foo, a certain natural number<br>
foo : ℕ<br>
foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j } ) _<br>
<br>
-- foo is a successor to itself<br>
bar : foo ≡ suc foo<br>
bar = refl<br>
<br>
-- which is forbidden<br>
baz : ∀ (n : ℕ) → (n ≡ suc λ { _ } → n   ) → ⊥<br>
baz _ ()<br>
<br>
--hence...<br>
zut : ⊥<br>
zut = baz foo bar<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>