<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>Hi Jesper,<br>
    </p>
    <p>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. <br>
    </p>
    <p>Best regards,<br>
    </p>
    <p>- Vlad<br>
    </p>
    <div class="moz-cite-prefix">On 22/10/2020 13:36, Jesper Cockx
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAEm=bozoOppn9q-02b=aqp7+7HRB6H1CTWkXMjdFxiaU9v2NeQ@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <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"
            moz-do-not-send="true">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"
            moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
          <a href="https://lists.chalmers.se/mailman/listinfo/agda"
            rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
        </blockquote>
      </div>
    </blockquote>
  </body>
</html>