Issue439.agda

{- This example goes through now that we allow instantiation of
   blocked terms #-}
module Issue439 where

record Σ (A : Set) (B : A → Set) : Set where
 constructor _,_
 field
   p₁ : A
   p₂ : B p₁

open Σ

record ⊤ : Set where

data Tree : Set where
 leaf : Tree
 node : Tree → Tree → Tree

mutual

 U : Tree → Set
 U leaf           = ⊤
 U (node tr₁ tr₂) = Σ (U tr₁) λ a → El a → U tr₂

 El : ∀ {tr} → U tr → Set
 El {leaf}         _       = ⊤
 El {node tr₁ tr₂} (a , b) = (x : El a) → El (b x)

mutual

 data C : Set where
   c : (Γ : C) → T Γ → C

 T : C → Set
 T Γ = Σ Tree (λ tr → E Γ → U tr)

 E : C → Set
 E (c Γ σ) = Σ (E Γ) λ γ → El (p₂ σ γ)

postulate
 e : C
 M : (Γ : C) → T Γ → Set
 z : ∀ {Γ σ} → M (c Γ σ) (p₁ σ , λ γ → p₂ σ (p₁ γ))
 l : ∀ {Γ} σ {τ} → M (c Γ σ) τ →
     M Γ (_ , λ γ → p₂ σ γ , λ v → p₂ τ (γ , v))
 a : ∀ {Γ tr₁ tr₂ σ} →
     M Γ (node tr₁ tr₂ , σ) → M Γ (tr₁ , λ γ → p₁ (σ γ)) →
     M Γ (leaf , _)
 s : ∀ {Γ} → M Γ (leaf , _)

t : ∀ {Γ σ} → M Γ σ → T Γ
t {σ = σ} _ = σ

foo : M (c e (leaf , _)) (leaf , _)
foo = a (l (t s) z) z