```------------------------------------------------------------------------
-- A type soundness result
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

open import Equality.Propositional
open import Prelude
open import Size

open import Function-universe equality-with-J
open import Maybe equality-with-J

open import Lambda.Syntax

open Closure Tm

-- If we can prove □ ∞ (WF-MV σ) (run x), then x does not "go wrong".

does-not-go-wrong : ∀ {σ} {x : M ∞ Value} →
□ ∞ (WF-MV σ) (run x) → ¬ x ≈M fail
does-not-go-wrong (now {x = nothing} ())
does-not-go-wrong (now {x = just x} x-wf) ()
does-not-go-wrong (later x-wf)            (laterˡ x↯) =
does-not-go-wrong (force x-wf) x↯

-- A "constructor" for □ i ∘ WF-MV.

_>>=-wf_ :
∀ {i σ τ} {x : M ∞ Value} {f : Value → M ∞ Value} →
□ i (WF-MV σ) (run x) →
(∀ {v} → WF-Value σ v → □ i (WF-MV τ) (run (f v))) →
□ i (WF-MV τ) (MaybeT.run (x >>= f))
x-wf >>=-wf f-wf =
□->>= x-wf λ { {nothing} ()
; {just v}  v-wf → f-wf v-wf
}

-- Well-typed programs do not "go wrong".

mutual

⟦⟧-wf : ∀ {i n Γ} (t : Tm n) {σ} → Γ ⊢ t ∈ σ →
∀ {ρ} → WF-Env Γ ρ →
□ i (WF-MV σ) (run (⟦ t ⟧ ρ))
⟦⟧-wf (con i)   con             ρ-wf = now con
⟦⟧-wf (var x)   var             ρ-wf = now (ρ-wf x)
⟦⟧-wf (ƛ t)     (ƛ t∈)          ρ-wf = now (ƛ t∈ ρ-wf)
⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) {ρ} ρ-wf =
⟦⟧-wf t₁ t₁∈ ρ-wf >>=-wf λ f-wf →
⟦⟧-wf t₂ t₂∈ ρ-wf >>=-wf λ v-wf →
∙-wf f-wf v-wf

∙-wf : ∀ {i σ τ f v} →
WF-Value (σ ⇾ τ) f → WF-Value (force σ) v →
□ i (WF-MV (force τ)) (run (f ∙ v))
∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf =
later λ { .force → ⟦⟧-wf _ t₁∈ (snoc-wf ρ₁-wf v₂-wf) }

type-soundness : ∀ {t : Tm 0} {σ} →
empty ⊢ t ∈ σ → ¬ ⟦ t ⟧ empty ≈M fail
type-soundness {t} {σ} =
empty ⊢ t ∈ σ                      ↝⟨ (λ t∈ → ⟦⟧-wf _ t∈ empty-wf) ⟩
□ ∞ (WF-MV σ) (run (⟦ t ⟧ empty))  ↝⟨ does-not-go-wrong ⟩□
¬ ⟦ t ⟧ empty ≈M fail              □
```