[Agda] Sized types problem

[Roly Perera]

Hi,

I'm modelling pi calculus in Agda and having difficulty using sized types
in order to have the function ⊖ below pass the termination-checker. I'm
also getting an error message which looks a bit odd, so perhaps there's a
clue to what I'm doing wrong in there.

{-# OPTIONS --sized-types #-}

module Temp where

   open import Data.Product public hiding (swap)
   open import Relation.Binary.PropositionalEquality
   open import Size

   -- Processes.
   data Proc : Set where
      ν_ : Proc → Proc

   -- Actions.
   data ⟿ᵇ : Set where
      input : ⟿ᵇ
      boundOut : ⟿ᵇ

   data ⟿ᶜ : Set where
      out : ⟿ᶜ

   data ⟿ : Set where
      _ᵇ : ⟿ᵇ → ⟿
      _ᶜ : ⟿ᶜ → ⟿

   -- Renamings. Leave undefined for now.
   data Ren : Set where

   postulate
      push : Ren
      swap : Ren
      _ᴬ*_ : Ren → ⟿ᶜ →  ⟿ᶜ

   -- Transitions.
   data _—[_]→_ : {ι : Size} → Proc → (a : ⟿) → Proc → Set where
      ν•_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P (out ᶜ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (boundOut ᵇ) R
      νᵇ_ : ∀ {ι P R} {a : ⟿ᵇ} → _—[_]→_ {ι = ι} P (boundOut ᵇ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (a ᵇ) (ν R)
      νᶜ_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P ((push ᴬ* out) ᶜ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (out ᶜ) (ν R)

   infixl 0 _—[_]→_

   postulate
      _ᴾ*_ : Ren → Proc → Proc
      _ᵀ*_ : ∀ {ι} (ρ : Ren) {P R} {a : ⟿ᶜ} → _—[_]→_ {ι = ι} P (a ᶜ) R →
             _—[_]→_ {ι = ι} (ρ ᴾ* P) ((ρ ᴬ* a) ᶜ) (ρ ᴾ* R)
      swap-involutive : ∀ (P : Proc) → swap ᴾ* swap ᴾ* P ≡ P
      swap∘push : swap ᴬ* push ᴬ* out ≡ out

   infixr 8 _ᵀ*_ _ᴾ*_ _ᴬ*_

   -- Structural congruence.
   infix 4 _≅_
   data _≅_ : Proc → Proc → Set where
      νν-swap : ∀ P → ν (ν (swap ᴾ* P)) ≅ ν (ν P)

   -- "Residual" of a transition E after a structural congruence φ.
   ⊖ : ∀ {ι P P′} {a : ⟿} {R} (E : _—[_]→_ {ι = ι} P a R) (φ : P ≅ P′) →
       Σ[ R ∈ Proc ] _—[_]→_ {ι = ι} P′ a R
   ⊖ (ν•_ (νᶜ E)) (νν-swap P) with swap ᵀ* E
   ... | swap*E rewrite swap-involutive P | swap∘push =
      _ , {!!} -- νᵇ (ν• swap*E)
   ⊖ E φ = {!!}

(I can try to boil the code down further if that would help, but I wanted
to maintain some of the structure of my setting.)

In the first goal above, I'm matching on the situation where there are
adjacent ν binders, and showing that if I transpose the binders (by
applying the 'swap' renaming under the binders) then the associated steps
in the derivation also tranpose. Intuitively this preserves the size of the
transition derivation. And indeed, toggling hidden arguments reveals that
the goal has type _—[_]→_ {↑ (↑ .ι)}, so I expect to be able to apply two
constructors (νᵇ and ν• in this case) in return for two I eliminated (ν•
and νᶜ).

I can also see that E has type _—[_]→_ {.ι}. Since I've postulated that ᵀ*
is size-preserving, the variable swap*E also has this type. Naively, I
expect νᵇ (ν• swap*E) to therefore be size-consistent with the goal.
However Agda complains that the constraints are inconsistent.

Weirdly, if I use a "with" clause to introduce ν• swap*E into the context,
I get the following error:

.ι !=< P of type Size
when checking that the expression E has type
swap ᴾ* P —[ (push ᴬ* out) ᶜ ]→ .R

This is baffling because the appearance of meta-variable P in the error
message suggests that Agda is trying to match a size index against a
variable of type Proc, does it not?

Can anyone shed any light on what's going on here?

many thanks,
Roly


Roly Perera
LFCS, School of Informatics
University of Edinburgh
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140818/7b8c2928/attachment.html