[Agda] Sized types and Inspect idiom problem

[Ernesto Copello]

Hi, Agda community.
I found the following problem with agda's extension with sized types.

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.

The other possible sized/not sized combinations seem to work, as
tested in good1, good2 and good3 examples.

Thanks
Ernesto

---------------------------------------------------------------------------------
{-# OPTIONS --sized-types #-}
module InspectSizedTypesProblem {A : Set} where

open import Data.Nat
open import Size
open import Relation.Binary.PropositionalEquality as PropEq

infixr 10 _∷n_
data ListN : {ι : Size} → Set where
  []n : {ι : Size} → ListN {↑ ι}
  _∷n_ : {ι : Size} → A → ListN {ι} → ListN {↑ ι}

sized : {ι : Size} → ListN {ι} → ℕ
sized []n = 0
sized (x ∷n xs) = 1

notSized : ListN → ℕ
notSized []n = 0
notSized (x ∷n xs) = 1

-- sized/sized
error : {ι : Size} → ListN {ι} → ℕ
error []n = 0
error (x ∷n xs) with sized xs | inspect sized xs
... | n | [ fx≡n ] = {! fx≡n!}  -- fx≡n has type ¨sized xs ≡ sized xs¨, error ?

-- sized/not sized
good1 : {ι : Size} → ListN {ι} → ℕ
good1 []n = 0
good1 (x ∷n xs) with notSized xs | inspect notSized xs
... | n | [ fx≡n ] = {! fx≡n!}  -- fx≡n has type ¨notSized xs ≡ n¨, good

-- not sized/ sized
good2 : ListN → ℕ
good2 []n = 0
good2 (x ∷n xs) with sized xs | inspect sized xs
... | n | [ fx≡n ] = {! fx≡n!} -- fx≡n has type ¨sized xs ≡ n¨, good

-- not sized/not sized
good3 : ListN → ℕ
good3 []n = 0
good3 (x ∷n xs) with notSized xs | inspect notSized xs
... | n | [ fx≡n ] = {! fx≡n!} -- fx≡n has type ¨notsized xs ≡ n¨, good
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140227/72e14df0/attachment.html