SystemF.agda

open import Data.List
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to mapSum)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality

Con : Set → Set
Con = List

data Var {A : Set} (t : A) : Con A → Set where
  here : ∀ {Γ : Con A} → Var t (t ∷ Γ)
  there : ∀ {t′} {Γ : Con A} → (v : Var t Γ) → Var t (t′ ∷ Γ)

data _⊆_ {A : Set} : Con A -> Con A -> Set where
  stop : [] ⊆ []
  skip : ∀ {Γ Δ a} -> Γ ⊆ Δ ->      Γ  ⊆ (a ∷ Δ)
  keep : ∀ {Γ Δ a} -> Γ ⊆ Δ -> (a ∷ Γ) ⊆ (a ∷ Δ)

⊆-refl : ∀ {A} {Γ : Con A} → Γ ⊆ Γ
⊆-refl {Γ = []} = stop
⊆-refl {Γ = x ∷ Γ} = keep ⊆-refl

⊆-trans : ∀ {A} {Γ₁ Γ₂ Γ₃ : Con A} → Γ₁ ⊆ Γ₂ → Γ₂ ⊆ Γ₃ → Γ₁ ⊆ Γ₃
⊆-trans σ₁ stop = σ₁
⊆-trans σ₁ (skip σ₂) = skip (⊆-trans σ₁ σ₂)
⊆-trans (skip σ₁) (keep σ₂) = skip (⊆-trans σ₁ σ₂)
⊆-trans (keep σ₁) (keep σ₂) = keep (⊆-trans σ₁ σ₂)

⊆-trans-idʳ : ∀ {A} {Γ Γ′ : Con A} → (σ : Γ ⊆ Γ′) → ⊆-trans σ ⊆-refl ≡ σ
⊆-trans-idʳ stop = refl
⊆-trans-idʳ (skip σ) = cong skip (⊆-trans-idʳ σ)
⊆-trans-idʳ (keep σ) = cong keep (⊆-trans-idʳ σ)

⊆-trans-idˡ : ∀ {A} {Γ Γ′ : Con A} → (σ : Γ ⊆ Γ′) → ⊆-trans ⊆-refl σ ≡ σ
⊆-trans-idˡ stop = refl
⊆-trans-idˡ (skip σ) = cong skip (⊆-trans-idˡ σ)
⊆-trans-idˡ (keep σ) = cong keep (⊆-trans-idˡ σ)

top : ∀ {A a} {Γ : Con A} -> Γ ⊆ (a ∷ Γ)
top = skip ⊆-refl

renᵛ : ∀ {A a} {Γ Δ : Con A} -> Γ ⊆ Δ -> Var a Γ → Var a Δ
renᵛ stop    ()
renᵛ (skip σ) v         = there (renᵛ σ v)
renᵛ (keep σ) here      = here
renᵛ (keep σ) (there v) = there (renᵛ σ v)

renᵛ-compose : ∀ {A a} {Γ₁ Γ₂ Γ₃ : Con A} (σ₁ : Γ₁ ⊆ Γ₂) (σ₂ : Γ₂ ⊆ Γ₃)
             → renᵛ {a = a} σ₂ ∘ renᵛ σ₁ ≗ renᵛ (⊆-trans σ₁ σ₂)
renᵛ-compose () stop here
renᵛ-compose () stop (there v)
renᵛ-compose σ₁ (skip σ₂) v = cong there (renᵛ-compose σ₁ σ₂ v)
renᵛ-compose (skip σ₁) (keep σ₂) v = cong there (renᵛ-compose σ₁ σ₂ v)
renᵛ-compose (keep σ₁) (keep σ₂) here = refl
renᵛ-compose (keep σ₁) (keep σ₂) (there v) = cong there (renᵛ-compose σ₁ σ₂ v)

data Env {A} (_⊢_ : Con A → A → Set) (Δ : Con A) : Con A → Set where
  [] : Env _⊢_ Δ []
  _∷_ : ∀ {Γ t} → (Δ ⊢ t) → Env _⊢_ Δ Γ → Env _⊢_ Δ (t ∷ Γ)

lookup : ∀ {A _⊢_ a} {Γ Δ : Con A} → Env _⊢_ Δ Γ → Var a Γ → Δ ⊢ a
lookup (x ∷ ρ) here = x
lookup (x ∷ ρ) (there v) = lookup ρ v

data Kind : Set where
  ⋆ : Kind

KCon : Set
KCon = Con Kind

mutual
  Ty : KCon → Set
  Ty Γ = Γ ⊢ₖ ⋆

  data _⊢ₖ_ (Γ : KCon) : Kind → Set where
    TyVar : ∀ {κ} → (α : Var κ Γ) → Γ ⊢ₖ κ
    _⟶_ : (t₁ t₂ : Ty Γ) → Ty Γ
    Forall : ∀ {κ′} → (κ : Kind) → (t : (κ ∷ Γ) ⊢ₖ κ′) → Γ ⊢ₖ κ′

renᵗʸ : ∀ {Γ Γ′ κ} → Γ ⊆ Γ′ → Γ ⊢ₖ κ → Γ′ ⊢ₖ κ
renᵗʸ σ (TyVar α) = TyVar (renᵛ σ α)
renᵗʸ σ (t₁ ⟶ t₂) = renᵗʸ σ t₁ ⟶ renᵗʸ σ t₂
renᵗʸ σ (Forall κ t) = Forall κ (renᵗʸ (keep σ) t)

renᵗʸ-compose : ∀ {Γ₁ Γ₂ Γ₃ κ} (σ₁ : Γ₁ ⊆ Γ₂) (σ₂ : Γ₂ ⊆ Γ₃) → renᵗʸ {κ = κ} σ₂ ∘ renᵗʸ σ₁ ≗ renᵗʸ (⊆-trans σ₁ σ₂)
renᵗʸ-compose σ₁ σ₂ (TyVar α) = cong TyVar (renᵛ-compose σ₁ σ₂ α)
renᵗʸ-compose σ₁ σ₂ (t₁ ⟶ t₂) = cong₂ _⟶_ (renᵗʸ-compose σ₁ σ₂ t₁) (renᵗʸ-compose σ₁ σ₂ t₂)
renᵗʸ-compose σ₁ σ₂ (Forall κ t) = cong (Forall κ) (renᵗʸ-compose (keep σ₁) (keep σ₂) t)

wkᵗʸ : ∀ {κ₀ Γ κ} → (Γ ⊢ₖ κ) → (κ₀ ∷ Γ) ⊢ₖ κ
wkᵗʸ = renᵗʸ top

KEnv : KCon → KCon → Set
KEnv = Env _⊢ₖ_

renᵗʸᴱ : ∀ {Γ Δ Ω : KCon} → Γ ⊆ Ω → KEnv Γ Δ → KEnv Ω Δ
renᵗʸᴱ σ [] = []
renᵗʸᴱ σ (t ∷ ρ) = (renᵗʸ σ t) ∷ (renᵗʸᴱ σ ρ)

keepᵗʸᴱ : ∀ {Γ Δ κ} → KEnv Γ Δ → KEnv (κ ∷ Γ) (κ ∷ Δ)
keepᵗʸᴱ ρ = TyVar here ∷ renᵗʸᴱ top ρ

reflᵗʸᴱ : ∀ {Γ : KCon} → KEnv Γ Γ
reflᵗʸᴱ {[]} = []
reflᵗʸᴱ {_ ∷ _} = keepᵗʸᴱ reflᵗʸᴱ

subᵗʸ : ∀ {Γ Γ′ κ} → KEnv Γ′ Γ → Γ ⊢ₖ κ → Γ′ ⊢ₖ κ
subᵗʸ ρ (TyVar α) = lookup ρ α
subᵗʸ ρ (t₁ ⟶ t₂) = subᵗʸ ρ t₁ ⟶ subᵗʸ ρ t₂
subᵗʸ ρ (Forall κ t) = Forall κ (subᵗʸ (keepᵗʸᴱ ρ) t)

_[_]ᵗʸ : ∀ {Γ κ κ′}
      → (κ′ ∷ Γ) ⊢ₖ κ
      → Γ ⊢ₖ κ′
      → Γ ⊢ₖ κ
t [ t′ ]ᵗʸ = subᵗʸ (t′ ∷ reflᵗʸᴱ) t

TyCon : (Γ : KCon) → Set
TyCon Γ = Con (Ty Γ)

⊆-wk : ∀ {Γ κ} {Σ Σ′ : TyCon Γ} → Σ ⊆ Σ′ → (map (wkᵗʸ {κ}) Σ) ⊆ (map wkᵗʸ Σ′)
⊆-wk stop = stop
⊆-wk (skip σ) = skip (⊆-wk σ)
⊆-wk (keep σ) = keep (⊆-wk σ)

data _,_⊢ₜ_ (Γ : KCon) (Σ : TyCon Γ) : Ty Γ → Set where
  var : ∀ {t} → Var t Σ → Γ , Σ ⊢ₜ t
  lam : ∀ t {t′} → (e : Γ , (t ∷ Σ) ⊢ₜ t′) → Γ , Σ ⊢ₜ (t ⟶ t′)
  _‿_ : ∀ {t₁ t₂} (e₁ : Γ , Σ ⊢ₜ (t₁ ⟶ t₂)) → (e₂ : Γ , Σ ⊢ₜ t₁) → Γ , Σ ⊢ₜ t₂
  Lam : ∀ (κ : Kind) {t} → (e : (κ ∷ Γ) , map wkᵗʸ Σ ⊢ₜ t) → Γ , Σ ⊢ₜ Forall κ t
  _&_ : ∀ {κ t₀} (e : Γ , Σ ⊢ₜ (Forall κ t₀)) → (t : Γ ⊢ₖ κ) → Γ , Σ ⊢ₜ (t₀ [ t ]ᵗʸ)

renᵗⱽₜ : ∀ {Γ Γ′ t} {Σ : TyCon Γ}
       → (σ : Γ ⊆ Γ′)
       → Var t Σ
       → Var (renᵗʸ σ t) (map (renᵗʸ σ) Σ)
renᵗⱽₜ σ here = here
renᵗⱽₜ σ (there v) = there (renᵗⱽₜ σ v)

open import Data.List.Properties

wk-renᵛ : ∀ {Γ Γ′ κ Σ} {t : Ty (κ ∷ Γ)} (σ : Γ ⊆ Γ′)
        → Var t (map (wkᵗʸ {κ}) Σ)
        → Var (renᵗʸ (keep σ) t) (map (wkᵗʸ ∘ renᵗʸ σ) Σ)
wk-renᵛ {Σ = []} σ ()
wk-renᵛ {κ = κ} {t ∷ Σ} σ here rewrite
    renᵗʸ-compose (skip {a = κ} ⊆-refl) (keep σ) t | ⊆-trans-idˡ σ |
    map-cong (renᵗʸ-compose σ (top {a = κ})) (t ∷ Σ) | ⊆-trans-idʳ σ
  = here
wk-renᵛ {κ = κ} {t ∷ Σ} σ (there v) = there (wk-renᵛ σ v)

renᵗ : ∀ {Γ Σ Σ′ t}
     → (σ : Σ ⊆ Σ′)
     → Γ , Σ ⊢ₜ t
     → Γ , Σ′ ⊢ₜ t
renᵗ σ (var v) = var (renᵛ σ v)
renᵗ σ (lam t e) = lam t (renᵗ (keep σ) e)
renᵗ σ (e₁ ‿ e₂) = renᵗ σ e₁ ‿ renᵗ σ e₂
renᵗ σ (Lam κ e) = Lam κ (renᵗ (⊆-wk σ) e)
renᵗ σ (e & t) = renᵗ σ e & t

TyEnv : ∀ {Γ} → TyCon Γ → TyCon Γ → Set
TyEnv {Γ} = Env (λ Σ t → Γ , Σ ⊢ₜ t)

renᵗᴱ : ∀ {Γ} {Σ Σ′ Ω : TyCon Γ} → Σ ⊆ Ω → TyEnv Σ Σ′ → TyEnv Ω Σ′
renᵗᴱ σ [] = []
renᵗᴱ σ (e ∷ ρ) = (renᵗ σ e) ∷ (renᵗᴱ σ ρ)

keepᵗᴱ : ∀ {Γ} {Σ Σ′ : TyCon Γ} {t} → TyEnv Σ Σ′ → TyEnv (t ∷ Σ) (t ∷ Σ′)
keepᵗᴱ ρ = var here ∷ renᵗᴱ top ρ

reflᵗᴱ : ∀ {Γ} {Σ : TyCon Γ} → TyEnv Σ Σ
reflᵗᴱ {Σ = []} = []
reflᵗᴱ {Σ = _ ∷ _} = keepᵗᴱ reflᵗᴱ

wkᵗₜ : ∀ {Γ κ} {Σ : TyCon Γ} {t} → Γ , Σ ⊢ₜ t → (κ ∷ Γ) , map wkᵗʸ Σ ⊢ₜ wkᵗʸ t
wkᵗₜ (var v) = var (renᵗⱽₜ (skip ⊆-refl) v)
wkᵗₜ (lam t e) = lam (wkᵗʸ t) (wkᵗₜ e)
wkᵗₜ (e₁ ‿ e₂) = wkᵗₜ e₁ ‿ wkᵗₜ e₂
wkᵗₜ (Lam κ e) = Lam κ {!!}
wkᵗₜ (e & t) = wkᵗₜ {!e!} & wkᵗʸ t

wkᵗᴱ : ∀ {Γ κ} {Σ Σ′ : TyCon Γ} → TyEnv Σ Σ′ → TyEnv (map (wkᵗʸ {κ}) Σ) (map wkᵗʸ Σ′)
wkᵗᴱ [] = []
wkᵗᴱ (e ∷ ρ) = wkᵗₜ e ∷ wkᵗᴱ ρ

subᵗ : ∀ {Γ} {Σ Σ′ t} → TyEnv Σ′ Σ → Γ , Σ ⊢ₜ t → Γ , Σ′ ⊢ₜ t
subᵗ ρ (var v) = lookup ρ v
subᵗ ρ (lam t e) = lam t (subᵗ (keepᵗᴱ ρ) e)
subᵗ ρ (e₁ ‿ e₂) = subᵗ ρ e₁ ‿ subᵗ ρ e₂
subᵗ ρ (Lam κ e) = Lam κ (subᵗ (wkᵗᴱ ρ) e)
subᵗ ρ (e & t) = subᵗ ρ e & t

_[_]ᵗ : ∀ {Γ Σ t t′}
      → Γ , (t′ ∷ Σ) ⊢ₜ t
      → Γ , Σ ⊢ₜ t′
      → Γ , Σ ⊢ₜ t
e [ e′ ]ᵗ = subᵗ (e′ ∷ reflᵗᴱ) e