[Agda] Size Issue when Modelling Effectful Data Structures and Computations

[jonas.hoefer at stud.htwk-leipzig.de]

Hello

> Note that the last example works fine:

Your code only seems works with the current Agda version from the Master
branch
not Agda version 2.6.1 (or 2.6.1.1). I don't think the last example should
work.
It fails in version 2.6.1 with the error message "Set (suc a) is not less or
equal than Set a".

> foo bar : Free (Op a) (Listᴹ (Op a) Bool)
> foo = pure nil
> bar = op foo

Op a produces a container of level suc a. Free and Listᴹ both use
the level of
their container i.e. suc a. op expects an argument of level a (not suc a,
because the stored type is smaller), but passing foo seems to work.

> op : {A : Set a} → Free (Op a) A → Free (Op a) A
> op {A = A} ma = impure (opˢ A , λ { (inj₁ tt) →
ma; (inj₂ x) → pure x })

Replacing Set a with Set (suc a) in the definition of op fails with the same
error, but the following works.

> op′ : {a : Level} {A : Set (suc a)} → Free (Op a) A →
Free (Op a) A
> op′ {a} {A} ma = op {a} ma

Passing {A} directly as an argument to op also yields the error, but omitting
it works. I think this behavior is a bug in the current version, because the
following implementation of Russel's paradox type checks with my build of the
latest version (commit 832057961873856915c41745c37e055ff4b2c583).

  {-# OPTIONS --cumulativity #-}

  open import Data.Bool
  open import Data.Empty
  open import Data.Product
  open import Data.Sum
  open import Data.Unit
  open import Data.Maybe

  open import Function
  open import Level

  open import Relation.Binary.PropositionalEquality

  private
    variable
      a : Level

  record Container a : Set (suc a) where
    constructor _◁_/_
    field
      Shape : Set a
      Pos   : Shape → Set a
      Ctx   : (s : Shape) → Pos s → Maybe {a = suc a} (Set a)

  open Container public

  ⟦_⟧ : Container a → (Set a → Set a) →
Set a → Set a
  ⟦ S ◁ P / C ⟧ F A = Σ[ s ∈ S ] ((p : P s)
→ F (fromMaybe A (C s p)))

  data Free {a : Level} (C : Container a) (A : Set a) : Set a where
    pure   : A                → Free C A
    impure : ⟦ C ⟧ (λ A → Free C A) A →
Free C A

  data Listᴹ (C : Container a) (A : Set a) : Set a where
    nil : Listᴹ C A
    cons : Free C A → Free C (Listᴹ C A) → Listᴹ C A

  ROp : ∀ a → Container (suc a)
  ROp a = Set a ◁ id / λ _ _ → nothing

  rop : {a : Level} {A : Set a} → Free (ROp a) A
  rop {_} {A} = impure (A , pure)

  rop′ : {a : Level} {A : Set (suc a)} → Free (ROp a) A
  rop′ = rop

  rop₁ : {A : Set₁} → Free (ROp 0ℓ) A
  rop₁ = rop′

  _bind_ : {A B : Set (suc a)} → Free (ROp a) A → (A →
Free (ROp a) B)
    → Free (ROp a) B
  pure x bind k = k x
  impure (X , pf) bind k = impure (X , λ p → pf p bind k)

  M : Set₁
  M = Free (ROp 0ℓ) ⊥

  m : (I : Set₁) → (I → M) → M
  m I pf = rop₁ {I} bind pf

  -- Now we can follow some implementation of Russell's Paradox
  -- http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html

  _∈_ : M → M → Set₁
  a ∈ (impure (I , f)) = ∃[ i ] (a ≡ f i)

  _∉_ : M → M → Set₁
  x ∉ y = x ∈ y → ⊥

  R : M
  R = m (Σ M λ s → s ∉ s) proj₁

  lem-1 : {X : M} → X ∈ R → X ∉ X
  lem-1 ((s , s∉s) , p) = subst₂ _∉_ p' p' s∉s
where p' = sym p

  lem-2 : {X : M} →  X ∉ X → X ∈ R
  lem-2 {X} X∉X = ((X , X∉X) , refl)

  lem-3 : R ∉ R
  lem-3 R∈R = lem-1 R∈R R∈R

  contr : ⊥
  contr = lem-3 (lem-2 {R} lem-3)

Jonas