<div dir="ltr"><div>Specifing the sizes makes it work as expected</div><div><br></div><div>workaround : {ι : Size} → ListN {ι} → ℕ</div><div>workaround []n = 0</div><div>workaround (_∷n_ {i} x xs) with sized {i} xs | inspect (sized {i}) xs</div>
<div>... | n | [ fx≡n ] = { fx≡n }0 </div><div><br></div><div>It seems like in a sized function the sizes doesn't get resolved early enough for with to see that the two occurrences of (sized {_} xs) in the context are the same expression.</div>
<div><br></div><div><br></div><div>Cheers,</div><div>Andrea </div><div><br></div><div>I guess the</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Feb 27, 2014 at 12:12 PM, Ernesto Copello <span dir="ltr"><<a href="mailto:ecopello@gmail.com" target="_blank">ecopello@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><pre>Hi, Agda community.<br>I found the following problem with agda'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>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>