[Agda] (no subject)

[Ernesto Copello]

Hi, Agda community.

We have some problems working with Agda's sized types extension.

We are working with Agda's version 2.3.2.

We have been able to isolate the problems in the following reduced example.

Thanks,

Ernesto

-------------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}
module problem where

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

data D : {ι : Size} → Set where
  d1 : {ι : Size} → ℕ → D {↑ ι}
  d2 : {ι : Size} → D {ι} → D {↑ ι}

-- d1 n, d2 (.. d2 (d1 n))

postulate
  op : {ι : Size} → D {ι} → D {ι}
  pr : {x : D} → op x ≡ x

-- Some reflexive binary relation
data R : D → D → Set where
  r1 : (n : ℕ) → R (d1 n) (d1 n)
  r2 : (d : D) → R (op d) (op d) → R (d2 d) (d2 d)

-- r1 (d1 n) (d1 n), r2 (r1 (d1 n) (d1 n))

good : D → D
good x with op x | pr {x}
... | .x | refl = x

-- We are not able to do the same as above with size information
annotations, the following commented code does not compile:
-- problem : {ι : Size} → D {ι} → D
-- problem x with op x | pr {x}
-- ... | .x | refl = {! !}

ρ-good : Reflexive R
ρ-good {x = d1 x} = r1 x
ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})

-- 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.
ρ-problem : {ι : Size} → Reflexive {A = D {ι}} R
ρ-problem {x = d1 x} = {! r1 x!}
ρ-problem {x = d2 x} = {! r2 x (ρ-problem {x = op x})!}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140625/afec9dff/attachment.html