<div dir="ltr"><pre>Hi, Agda community.<br>I found the following problem with agda&#39;s extension with sized types.<br><br>As I show in the error function below, it seems that the inspect idiom does not work inside a sized function, when used to remember the result of another sized function.<br>
<br>The other possible sized/not sized combinations seem to work, as tested in good1, good2 and good3 examples.<br><br>Thanks<br>Ernesto<br><br>---------------------------------------------------------------------------------<br>
{-# OPTIONS --sized-types #-}<br>module InspectSizedTypesProblem {A : Set} where<br><br>open import Data.Nat<br>open import Size<br>open import Relation.Binary.PropositionalEquality as PropEq <br><br>infixr 10 _∷n_<br>data ListN : {ι : Size} → Set where<br>
  []n : {ι : Size} → ListN {↑ ι}<br>  _∷n_ : {ι : Size} → A → ListN {ι} → ListN {↑ ι}<br><br>sized : {ι : Size} → ListN {ι} → ℕ <br>sized []n = 0<br>sized (x ∷n xs) = 1 <br><br>notSized : ListN → ℕ<br>notSized []n = 0<br>
notSized (x ∷n xs) = 1<br><br>-- sized/sized<br>error : {ι : Size} → ListN {ι} → ℕ<br>error []n = 0<br>error (x ∷n xs) with sized xs | inspect sized xs<br>... | n | [ fx≡n ] = {! fx≡n!}  -- fx≡n has type ¨sized xs ≡ sized xs¨, error ?<br>
<br>-- sized/not sized<br>good1 : {ι : Size} → ListN {ι} → ℕ<br>good1 []n = 0<br>good1 (x ∷n xs) with notSized xs | inspect notSized xs<br>... | n | [ fx≡n ] = {! fx≡n!}  -- fx≡n has type ¨notSized xs ≡ n¨, good<br><br>-- not sized/ sized<br>
good2 : ListN → ℕ<br>good2 []n = 0<br>good2 (x ∷n xs) with sized xs | inspect sized xs<br>... | n | [ fx≡n ] = {! fx≡n!} -- fx≡n has type ¨sized xs ≡ n¨, good<br><br>-- not sized/not sized<br>good3 : ListN → ℕ<br>good3 []n = 0<br>
good3 (x ∷n xs) with notSized xs | inspect notSized xs<br>... | n | [ fx≡n ] = {! fx≡n!} -- fx≡n has type ¨notsized xs ≡ n¨, good<br><br><br></pre></div>