<div dir="ltr"><pre>Hi, Agda community.<br><br>We have some problems working with Agda&#39;s sized types extension. <br><br>We are working with Agda&#39;s version 2.3.2.<br><br>We have been able to isolate the problems in the following reduced example.<br>
<br></pre><pre>Thanks,<br></pre><pre>Ernesto<br><br>-------------------------------------------------------------------------------<br><br>{-# OPTIONS --sized-types #-}<br>module problem where<br><br>open import Size<br>open import Data.Nat<br>
open import Relation.Binary<br>open import Relation.Binary.PropositionalEquality<br><br>data D : {ι : Size} → Set where<br>  d1 : {ι : Size} → ℕ → D {↑ ι}<br>  d2 : {ι : Size} → D {ι} → D {↑ ι}<br><br>-- d1 n, d2 (.. d2 (d1 n))<br>
<br>postulate<br>  op : {ι : Size} → D {ι} → D {ι}<br>  pr : {x : D} → op x ≡ x<br><br>-- Some reflexive binary relation<br>data R : D → D → Set where<br>  r1 : (n : ℕ) → R (d1 n) (d1 n)<br>  r2 : (d : D) → R (op d) (op d) → R (d2 d) (d2 d)<br>
<br>-- r1 (d1 n) (d1 n), r2 (r1 (d1 n) (d1 n))<br><br>good : D → D<br>good x with op x | pr {x}<br>... | .x | refl = x<br><br>-- We are not able to do the same as above with size information annotations, the following commented code does not compile:<br>
-- problem : {ι : Size} → D {ι} → D<br>-- problem x with op x | pr {x}<br>-- ... | .x | refl = {! !}<br><br>ρ-good : Reflexive R<br>ρ-good {x = d1 x} = r1 x<br>ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})<br><br>-- To pass the termination checking algorithm, we add size information to the type signature of the previous code, but another problem arises, and now the proofs do not pass type checking.<br>
ρ-problem : {ι : Size} → Reflexive {A = D {ι}} R<br>ρ-problem {x = d1 x} = {! r1 x!}<br>ρ-problem {x = d2 x} = {! r2 x (ρ-problem {x = op x})!}<br><br><br><br><br><br><br><br><br><br><br></pre></div>