HindleyMilner.agda

-- The algorithm here is based on the one in the paper "First-order unification by structural recursion" by Conor McBride.
-- There are some notes on the syntax in the McBride paper and how it
-- corresponds to the names here in some of the places where they differ.
--
-- The proofs are after the comment marking the beginning of the proofs.

open import Data.Nat hiding (_≤_)
import Data.Nat.Properties
import Data.Nat.Properties as ℕᵖ
open import Data.Product
open import Data.Sum
open import Relation.Unary hiding (_⇒_; ∅)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Bool renaming (Bool to Boolean; _≟_ to _B≟_) hiding (_≤_)
open import Data.Empty
open import Function
open import Data.Maybe

open ≡-Reasoning

module HindleyMilner where

data Ctx⋆ : Set where
  ∅⋆ : Ctx⋆
  S⋆_ : Ctx⋆ → Ctx⋆

data Ix⋆ : Ctx⋆ → ℕ → Set where
  here⋆ : ∀ {Φ} →
    Ix⋆ Φ 0

  there⋆ : ∀ {Φ} {i} →
    Ix⋆ Φ i →
    Ix⋆ (S⋆ Φ) (suc i)

data Mono-Ty (Φ : Ctx⋆) : Set where
  Bool :
    Mono-Ty Φ

  _⇒_ :
    Mono-Ty Φ → Mono-Ty Φ → Mono-Ty Φ

  Var : ∀ {i} →
    Ix⋆ Φ i →
    Mono-Ty Φ

data Ty : Set where
  Foralls : ∀ Φ →
    Mono-Ty Φ →
    Ty

Ix⋆-unique : ∀ {Φ} {i} (x y : Ix⋆ Φ i) →
  x ≡ y
Ix⋆-unique here⋆ here⋆ = refl
Ix⋆-unique (there⋆ x) (there⋆ y) rewrite Ix⋆-unique x y = refl

Renaming⋆ : Ctx⋆ → Ctx⋆ → Set
Renaming⋆ Φ Ψ =
  ∀ {i} →
  Ix⋆ Φ i →
  ∃[ j ] Ix⋆ Ψ j

Subst⋆ : Ctx⋆ → Ctx⋆ → Set
Subst⋆ Φ Ψ =
  ∀ {i} →
  Ix⋆ Φ i →
  Mono-Ty Ψ

lift⋆ : ∀ {Φ Ψ} →
  Renaming⋆ Φ Ψ →
  Renaming⋆ (S⋆ Φ) (S⋆ Ψ)
lift⋆ ρ here⋆ = 0 , here⋆
lift⋆ ρ (there⋆ x) =
  let i , y = ρ x
  in
  suc i , there⋆ y

apply-Renaming⋆ : ∀ {Φ Ψ} →
  Renaming⋆ Φ Ψ →
  Mono-Ty Φ →
  Mono-Ty Ψ
apply-Renaming⋆ ρ Bool = Bool
apply-Renaming⋆ ρ (a ⇒ b) = apply-Renaming⋆ ρ a ⇒ apply-Renaming⋆ ρ b
apply-Renaming⋆ ρ (Var x) = Var (proj₂ (ρ x))

weaken⋆ : ∀ {Φ} →
  Mono-Ty Φ →
  Mono-Ty (S⋆ Φ)
weaken⋆ = apply-Renaming⋆ λ { {i = i} x → suc i , there⋆ x }

lift-Subst⋆ : ∀ {Φ Ψ} →
  Subst⋆ Φ Ψ →
  Subst⋆ (S⋆ Φ) (S⋆ Ψ)
lift-Subst⋆ σ here⋆ = Var here⋆
lift-Subst⋆ σ (there⋆ x) = weaken⋆ (σ x)

apply-Subst⋆ : ∀ {Φ Ψ} →
  Subst⋆ Φ Ψ →
  Mono-Ty Φ →
  Mono-Ty Ψ
apply-Subst⋆ σ Bool = Bool
apply-Subst⋆ σ (a ⇒ b) = apply-Subst⋆ σ a ⇒ apply-Subst⋆ σ b
apply-Subst⋆ σ (Var x) = σ x

idSubst⋆ : ∀ {Φ} → Subst⋆ Φ Φ
idSubst⋆ {Φ} x = Var x

apply-idSubst⋆ : ∀ {Φ} a →
  apply-Subst⋆ {Φ} idSubst⋆ a ≡ a
apply-idSubst⋆ {_} Bool = refl
apply-idSubst⋆ {_} (a ⇒ b) rewrite apply-idSubst⋆ a | apply-idSubst⋆ b = refl
apply-idSubst⋆ {_} (Var x) = refl

_∘S_ : ∀ {Φ Ψ Ξ} → Subst⋆ Ψ Ξ → Subst⋆ Φ Ψ → Subst⋆ Φ Ξ
(τ ∘S σ) x = apply-Subst⋆ τ (σ x)

apply-Subst⋆-∘ :
  ∀ {Φ Ψ Ξ} (τ : Subst⋆ Ψ Ξ) (σ : Subst⋆ Φ Ψ) (t : Mono-Ty Φ) →
  apply-Subst⋆ (τ ∘S σ) t ≡ apply-Subst⋆ τ (apply-Subst⋆ σ t)
apply-Subst⋆-∘ τ σ Bool     = refl
apply-Subst⋆-∘ τ σ (u ⇒ v)  = cong₂ _⇒_ (apply-Subst⋆-∘ τ σ u) (apply-Subst⋆-∘ τ σ v)
apply-Subst⋆-∘ τ σ (Var x)  = refl

Mono-Ty-eq-dec : ∀ {Φ} (a b : Mono-Ty Φ) →
  Dec (a ≡ b)
Mono-Ty-eq-dec Bool Bool = yes refl
Mono-Ty-eq-dec Bool (b ⇒ b₁) = no λ ()
Mono-Ty-eq-dec Bool (Var x) = no λ ()
Mono-Ty-eq-dec (a ⇒ a₁) Bool = no λ ()
Mono-Ty-eq-dec (a ⇒ a₁) (Var x) = no λ ()
Mono-Ty-eq-dec (Var x) Bool = no λ ()
Mono-Ty-eq-dec (Var x) (b ⇒ b₁) = no λ ()
Mono-Ty-eq-dec (a ⇒ a₁) (b ⇒ b₁) with Mono-Ty-eq-dec a b | Mono-Ty-eq-dec a₁ b₁
... | no ¬p | no ¬q = no λ { refl → ¬q refl }
... | no ¬p | yes q = no λ { refl → ¬p refl }
... | yes p | no ¬q = no λ { refl → ¬q refl }
... | yes refl | yes refl = yes refl

Mono-Ty-eq-dec (Var {i = i} x) (Var {i = j} y) with i ≟ j
... | no ¬p = no λ { refl → ¬p refl }
... | yes refl rewrite Ix⋆-unique x y = yes refl

Ctx⋆-eq-dec : (Φ Ψ : Ctx⋆) →
  Dec (Φ ≡ Ψ)
Ctx⋆-eq-dec ∅⋆ ∅⋆ = yes refl
Ctx⋆-eq-dec ∅⋆ (S⋆ Ψ) = no λ ()
Ctx⋆-eq-dec (S⋆ Φ) ∅⋆ = no λ ()
Ctx⋆-eq-dec (S⋆ Φ) (S⋆ Ψ) with Ctx⋆-eq-dec Φ Ψ
... | no ¬p = no λ { refl → ¬p refl }
... | yes refl = yes refl

Ty-eq-dec : (a b : Ty) →
  Dec (a ≡ b)
Ty-eq-dec (Foralls Φ a) (Foralls Ψ b) with Ctx⋆-eq-dec Φ Ψ
Ty-eq-dec (Foralls Φ a) (Foralls Ψ b) | no ¬p = no λ { refl → ¬p refl }
Ty-eq-dec (Foralls Φ a) (Foralls Ψ b) | yes refl with Mono-Ty-eq-dec a b
Ty-eq-dec (Foralls Φ a) (Foralls Ψ b) | yes refl | no ¬q = no λ { refl → ¬q refl }
Ty-eq-dec (Foralls Φ a) (Foralls Φ b) | yes refl | yes refl = yes refl

data CtxEntry (Φ : Ctx⋆) : Set where
  mono : Mono-Ty Φ → CtxEntry Φ
  poly : Ty        → CtxEntry Φ

data Ctx (Φ : Ctx⋆) : Set where
  ∅ : Ctx Φ
  _,,_ : Ctx Φ → CtxEntry Φ → Ctx Φ

data Ix {Φ} : Ctx Φ → ℕ → CtxEntry Φ → Set where
  here : ∀ {Γ a} →
    Ix (Γ ,, a) 0 a

  there : ∀ {Γ i a b} →
    Ix Γ i a →
    Ix (Γ ,, b) (suc i) a

data Expr : Set where
  var : ℕ → Expr
  app : Expr → Expr → Expr
  lam : Expr → Expr
  true : Expr
  false : Expr

_◇_ : ∀ {Φ1 Φ2 Φ3} →
  Subst⋆ Φ2 Φ3 →
  Subst⋆ Φ1 Φ2 →
  Subst⋆ Φ1 Φ3
_◇_ σ σ′ x = apply-Subst⋆ σ (σ′ x)

thin-ℕ : ℕ → ℕ → ℕ
thin-ℕ zero y = suc y
thin-ℕ (suc x) zero = zero
thin-ℕ (suc x) (suc y) = suc (thin-ℕ x y)

thin : ∀ {Φ} {i j} →
  Ix⋆ (S⋆ Φ) i →
  Ix⋆ Φ j →
  Ix⋆ (S⋆ Φ) (thin-ℕ i j)
thin here⋆ y = there⋆ y
thin (there⋆ x) here⋆ = here⋆
thin (there⋆ x) (there⋆ y) = there⋆ (thin x y)

thick-ℕ :
  ℕ →
  ℕ →
  ℕ
thick-ℕ zero zero = zero
thick-ℕ zero (suc y) = y
thick-ℕ (suc x) zero = zero
thick-ℕ (suc x) (suc y) = suc (thick-ℕ x y)

thick : ∀ {Φ} {i j} →
  Ix⋆ (S⋆ Φ) i →
  Ix⋆ (S⋆ Φ) j →
  Maybe (Ix⋆ Φ (thick-ℕ i j))
thick here⋆ here⋆ = nothing
thick here⋆ (there⋆ y) = just y
thick (there⋆ x) here⋆ = just here⋆
thick {∅⋆} (there⋆ x) (there⋆ y) = nothing
thick {S⋆ Φ} (there⋆ x) (there⋆ y) with thick x y
... | just z = just (there⋆ z)
... | nothing = nothing

subst-there :
  ∀ {Φ i j} (e : j ≡ i) (y : Ix⋆ Φ i) →
  subst (λ n → Ix⋆ (S⋆ Φ) n) (sym (cong suc e)) (there⋆ y)
  ≡ there⋆ (subst (λ n → Ix⋆ Φ n) (sym e) y)
subst-there refl y = refl

inj-just : ∀ {A : Set} {x y : A} → just x ≡ just y → x ≡ y
inj-just refl = refl

-- *** McBride syntax: `occurs-check x t` === `check x t`
occurs-check : ∀ {Φ} {i} →
  (x : Ix⋆ (S⋆ Φ) i) →
  (a : Mono-Ty (S⋆ Φ)) →
  Maybe (Mono-Ty Φ)
occurs-check x Bool = just Bool
occurs-check x (a ⇒ b) with occurs-check x a | occurs-check x b
... | just a′ | just b′ = just (a′ ⇒ b′)
... | just x₁ | nothing = nothing
... | nothing | just x₁ = nothing
... | nothing | nothing = nothing
occurs-check x (Var y) with thick x y
... | just z = just (Var z)
... | nothing = nothing

-- *** McBride syntax: `thicken-except x a` === `a for x`
thicken-except : ∀ {Φ} {i} {j} →
  (x : Ix⋆ (S⋆ Φ) i) →
  (a : Mono-Ty Φ) →
  (y : Ix⋆ (S⋆ Φ) j) →
  Mono-Ty Φ
thicken-except x a y with thick x y
... | just z = Var z
... | nothing = a

data AList : Ctx⋆ → Ctx⋆ → Set where
  anil : ∀ {Φ} → AList Φ Φ
  asnoc : ∀ {Φ Φ′} {i} →
    AList Φ Φ′ →
    Mono-Ty Φ →
    Ix⋆ (S⋆ Φ) i →
    AList (S⋆ Φ) Φ′

-- *** McBride syntax: `AList-subst σ` === `sub σ`
AList-subst : ∀ {Φ Φ′} {i} →
  AList Φ Φ′ →
  Ix⋆ Φ i →
  Mono-Ty Φ′
AList-subst anil x = Var x
AList-subst (asnoc σ a y) x = (AList-subst σ ◇ thicken-except y a) x

_++_ : ∀ {Φ Φ′ Φ′′} →
  AList Φ′ Φ′′ →
  AList Φ Φ′ →
  AList Φ Φ′′
ρ ++ anil = ρ
ρ ++ asnoc σ a x = asnoc (ρ ++ σ) a x

_++′_ : ∀ {Φ Φ′ Φ′′} →
  AList Φ Φ′ →
  AList Φ′ Φ′′ →
  AList Φ Φ′′
_++′_ ρ σ = σ ++ ρ

flex-flex : ∀ {Φ} {i j} →
  (x : Ix⋆ Φ i) →
  (y : Ix⋆ Φ j) →
  ∃[ Φ′ ] AList Φ Φ′
flex-flex {∅⋆} x y = ∅⋆ , anil
flex-flex {S⋆ Φ} x y with thick x y
... | just y′ = Φ , asnoc anil (Var y′) x
... | nothing = S⋆ Φ , anil

flex-rigid : ∀ {Φ} {i} →
  Ix⋆ Φ i →
  Mono-Ty Φ →
  Maybe (∃[ Φ′ ] AList Φ Φ′)

flex-rigid {∅⋆} x a = nothing
flex-rigid {S⋆ Φ} x a with occurs-check x a
... | just b = just (Φ , asnoc anil b x)
... | nothing = nothing

amgu : ∀ {Φ} →
  (s t : Mono-Ty Φ) →
  (∃[ Φ′ ] AList Φ Φ′) →
  Maybe (∃[ Φ′′ ] AList Φ Φ′′)
amgu Bool Bool acc = just acc
amgu Bool (t ⇒ t₁) acc = nothing
amgu (s ⇒ s₁) Bool acc = nothing

amgu (Var x) (Var y) (Φ′ , anil) = just (flex-flex x y)

amgu a@Bool (Var x) (Φ′ , anil) = flex-rigid x a
amgu a@(a₀ ⇒ a₁) (Var x) (Φ′ , anil) = flex-rigid x a
amgu (Var x) a@Bool (Φ′ , anil) = flex-rigid x a
amgu (Var x) a@(a₀ ⇒ a₁) (Φ′ , anil) = flex-rigid x a

amgu (s ⇒ s₁) (t ⇒ t₁) acc with amgu s t acc
... | just acc′ = amgu s₁ t₁ acc′
... | nothing = nothing

amgu s@Bool t@(Var x) (Φ′ , asnoc σ z r)
  with amgu (apply-Subst⋆ (thicken-except r z) s) (apply-Subst⋆ (thicken-except r z) t) (Φ′ , σ)
... | just (Φ′′ , σ′) = just (Φ′′ , asnoc σ′ z r)
... | nothing = nothing
amgu s@(s₀ ⇒ s₁) t@(Var x) (Φ′ , asnoc σ z r)
  with amgu (apply-Subst⋆ (thicken-except r z) s) (apply-Subst⋆ (thicken-except r z) t) (Φ′ , σ)
... | just (Φ′′ , σ′) = just (Φ′′ , asnoc σ′ z r)
... | nothing = nothing
amgu s@(Var x) t@Bool (Φ′ , asnoc σ z r)
  with amgu (apply-Subst⋆ (thicken-except r z) s) (apply-Subst⋆ (thicken-except r z) t) (Φ′ , σ)
... | just (Φ′′ , σ′) = just (Φ′′ , asnoc σ′ z r)
... | nothing = nothing
amgu s@(Var x) t@(t₀ ⇒ t₁) (Φ′ , asnoc σ z r)
  with amgu (apply-Subst⋆ (thicken-except r z) s) (apply-Subst⋆ (thicken-except r z) t) (Φ′ , σ)
... | just (Φ′′ , σ′) = just (Φ′′ , asnoc σ′ z r)
... | nothing = nothing
amgu s@(Var x) t@(Var x₁) (Φ′ , asnoc σ z r)
  with amgu (apply-Subst⋆ (thicken-except r z) s) (apply-Subst⋆ (thicken-except r z) t) (Φ′ , σ)
... | just (Φ′′ , σ′) = just (Φ′′ , asnoc σ′ z r)
... | nothing = nothing

mgu : ∀ {Φ} →
  (s t : Mono-Ty Φ) →
  Maybe (∃[ Φ′ ] AList Φ Φ′)
mgu {Φ} s t = amgu s t (Φ , anil)

----------- Proofs start here -----------

thin-ℕ-suc : ∀ {i j k} →
  thin-ℕ i j ≡ k →
  thin-ℕ (suc i) (suc j) ≡ suc k
thin-ℕ-suc {zero} {j} {k} refl = refl
thin-ℕ-suc {suc i} {zero} {k} refl = refl
thin-ℕ-suc {suc i} {suc j} {k} refl = refl

suc-invert : ∀ {i j} →
  suc i ≡ suc j →
  i ≡ j
suc-invert refl = refl

thin-ℕ-unique : ∀ x y z →
  thin-ℕ x y ≡ thin-ℕ x z →
  y ≡ z
thin-ℕ-unique zero y z refl = refl
thin-ℕ-unique (suc x) zero zero eq = eq
thin-ℕ-unique (suc x) (suc y) (suc z) eq =
  cong suc (thin-ℕ-unique x y z (suc-invert eq))

thin-ℕ≢ : ∀ i j →
  thin-ℕ i j ≢ i
thin-ℕ≢ zero j = λ ()
thin-ℕ≢ (suc i) zero = λ ()
thin-ℕ≢ (suc i) (suc j) eq = thin-ℕ≢ i j (suc-invert eq)

thin-ℕ-coverage : ∀ x y →
  x ≢ y →
  ∃[ y′ ] thin-ℕ x y′ ≡ y
thin-ℕ-coverage zero zero x≢y = ⊥-elim (x≢y refl)
thin-ℕ-coverage zero (suc y) x≢y = y , refl
thin-ℕ-coverage (suc x) zero x≢y = zero , refl
thin-ℕ-coverage (suc x) (suc y) x≢y =
  let z , p = thin-ℕ-coverage x y λ e → x≢y (cong suc e)
  in
  suc z , thin-ℕ-suc p

Unifies : ∀ {Φ Ψ} → Subst⋆ Φ Ψ → Mono-Ty Φ → Mono-Ty Φ → Set
Unifies σ s t = apply-Subst⋆ σ s ≡ apply-Subst⋆ σ t

-- x never maps to anything under 'thick' with itself
thick-self-nothing :
  ∀ {Φ i} (x : Ix⋆ (S⋆ Φ) i) → thick x x ≡ nothing
thick-self-nothing here⋆ = refl
thick-self-nothing {∅⋆} (there⋆ x) = refl
thick-self-nothing {S⋆ Φ} (there⋆ x) rewrite thick-self-nothing x = refl

-- and therefore the "for" substitution returns the payload at x
thicken-except-self :
  ∀ {Φ i} (x : Ix⋆ (S⋆ Φ) i) (b : Mono-Ty Φ) →
  thicken-except x b x ≡ b
thicken-except-self x b rewrite thick-self-nothing x = refl

-- delete after insert on ℕ
thick-ℕ-thin-ℕ : ∀ i j → thick-ℕ i (thin-ℕ i j) ≡ j
thick-ℕ-thin-ℕ zero     j       = refl
thick-ℕ-thin-ℕ (suc i)  zero    = refl
thick-ℕ-thin-ℕ (suc i) (suc j)  = cong suc (thick-ℕ-thin-ℕ i j)

-- insert after delete when you didn't delete the inserted spot
thin-ℕ-thick-ℕ : ∀ i j → j ≢ i → thin-ℕ i (thick-ℕ i j) ≡ j
thin-ℕ-thick-ℕ zero    zero    j≢i = ⊥-elim (j≢i refl)
thin-ℕ-thick-ℕ zero   (suc j)  _   = refl
thin-ℕ-thick-ℕ (suc i) zero    _   = refl
thin-ℕ-thick-ℕ (suc i) (suc j) j≢i = cong suc (thin-ℕ-thick-ℕ i j (λ e → j≢i (cong suc e)))

-- thick ∘ thin is the identity *up to transport on the index*
thick-thin :
  ∀ {Φ i j} (ι : Ix⋆ (S⋆ Φ) i) (y : Ix⋆ Φ j) →
  thick ι (thin ι y) ≡
    just (subst (λ n → Ix⋆ Φ n) (sym (thick-ℕ-thin-ℕ i j)) y)
thick-thin here⋆ y = refl
thick-thin (there⋆ x) here⋆ = refl
thick-thin {S⋆ Φ} {i = suc i} {j = suc j} (there⋆ x) (there⋆ y) rewrite thick-thin x y =
  cong just (sym (subst-there (thick-ℕ-thin-ℕ i j) y))

occurs-check-β-irrel :
  ∀ {Φ i} (x : Ix⋆ (S⋆ Φ) i) (a : Mono-Ty (S⋆ Φ))
    {b c : Mono-Ty Φ} →
  occurs-check x a ≡ just b →
  apply-Subst⋆ (thicken-except x c) a ≡ b
-- Bool
occurs-check-β-irrel x Bool {b} {c} eq with inj-just eq
... | refl = refl
-- Var
occurs-check-β-irrel x (Var y) {b} {c} eq with thick x y
... | just z with inj-just eq
... | refl = refl                     -- LHS = Var z, RHS = Var z

-- Arrow
occurs-check-β-irrel x (u ⇒ v) {b} {c} eq
  with occurs-check x u in E | occurs-check x v in E′
... | just u′ | just v′ with inj-just eq
... | refl rewrite eq =
  cong₂ _⇒_ (occurs-check-β-irrel x u {b = u′} {c = c} E)
            (occurs-check-β-irrel x v {b = v′} {c = c} E′)

occurs-check-β-irrel x (u ⇒ v) {b} {c} () | nothing | just x₁
occurs-check-β-irrel x (u ⇒ v) {b} {c} () | nothing | nothing

occurs-check-β :
  ∀ {Φ i} (x : Ix⋆ (S⋆ Φ) i) (a : Mono-Ty (S⋆ Φ)) {b : Mono-Ty Φ} →
  occurs-check x a ≡ just b →
  apply-Subst⋆ (thicken-except x b) a ≡ b
occurs-check-β x a {b} eq = occurs-check-β-irrel x a {b} {b} eq

flex-rigid-correct : ∀ {Φ Φ′} {i} →
  (x : Ix⋆ Φ i) →
  (a : Mono-Ty Φ) →
  (σ : AList Φ Φ′) →
  flex-rigid x a ≡ just (Φ′ , σ) →
  Unifies (AList-subst σ) (Var x) a

flex-rigid-correct {S⋆ Φ} x a σ eq with occurs-check x a in E
... | just b with inj-just eq
... | refl =
  begin
    AList-subst (asnoc anil b x) x
      ≡⟨ refl ⟩
    apply-Subst⋆ (AList-subst anil) (thicken-except x b x)
      ≡⟨ cong (apply-Subst⋆ (AList-subst anil)) (thicken-except-self x b) ⟩
    apply-Subst⋆ (AList-subst anil) b
      ≡⟨ cong (apply-Subst⋆ (AList-subst anil)) (sym (occurs-check-β x a E)) ⟩
    apply-Subst⋆ (AList-subst anil) (apply-Subst⋆ (thicken-except x b) a)
      ≡⟨ sym (apply-Subst⋆-∘ (AList-subst anil) (thicken-except x b) a) ⟩
    apply-Subst⋆ ((AList-subst anil) ◇ (thicken-except x b)) a
      ≡⟨ refl ⟩
    apply-Subst⋆ (AList-subst (asnoc anil b x)) a
  ∎

-- When 'thick x y' is 'just z', the "for" substitution at y ignores the payload.
thicken-except-just :
  ∀ {Φ i j} (x : Ix⋆ (S⋆ Φ) i) (a : Mono-Ty Φ) (y : Ix⋆ (S⋆ Φ) j) {z} →
  thick x y ≡ just z →
  thicken-except x a y ≡ Var z
thicken-except-just x a y {z} e rewrite e = refl

-- If thick x y = nothing, then Var x ≡ Var y (no index equalities needed).
thick-nothing→Var-eq :
  ∀ {Φ i j}
  (x : Ix⋆ (S⋆ Φ) i) (y : Ix⋆ (S⋆ Φ) j) →
  thick x y ≡ nothing → Var x ≡ Var y

-- Both at the top: thick here⋆ here⋆ = nothing
thick-nothing→Var-eq here⋆ here⋆ _ = refl

-- Mixed cases are impossible because thick = just …
thick-nothing→Var-eq here⋆ (there⋆ y) ()
thick-nothing→Var-eq (there⋆ x) here⋆ ()

-- Tail is empty: the only Ix⋆ ∅⋆ inhabitant is here⋆, so both are there⋆ here⋆.
thick-nothing→Var-eq {∅⋆} (there⋆ here⋆) (there⋆ here⋆) _ = refl

-- General recursive case: both there⋆, peel one level and recurse.
thick-nothing→Var-eq {S⋆ Φ} (there⋆ x) (there⋆ y) E
  with thick x y in E′
... | just z    with E
... | ()        -- contradiction: thick (there⋆ _) (there⋆ _) = just (there⋆ _)
thick-nothing→Var-eq {S⋆ Φ} (there⋆ x) (there⋆ y) E | nothing =
  -- IH gives Var x ≡ Var y at level Φ; lift with weaken⋆
  let ih : Var x ≡ Var y
      ih = thick-nothing→Var-eq x y E′
  in cong weaken⋆ ih

------------------------------------------------------------------------
-- "Soundness" of flex-flex: what it returns does unify the two variables.

flex-flex-correct :
  ∀ {Φ i j}
  (x : Ix⋆ Φ i) (y : Ix⋆ Φ j) →
  let Φ′ , σ = flex-flex x y in
  Unifies (AList-subst σ) (Var x) (Var y)
-- ∅⋆ : flex-flex is (∅⋆ , anil); identity unifies Var x, Var y
flex-flex-correct {∅⋆} here⋆ here⋆ =
  begin
    AList-subst anil here⋆ ≡⟨⟩
    Var here⋆              ≡⟨⟩
    Var here⋆              ≡⟨⟩
    AList-subst anil here⋆
  ∎

-- S⋆ Φ : branch on 'thick x y'
flex-flex-correct {S⋆ Φ} x y with thick x y in E
... | just y′ =
  -- flex-flex x y = (Φ , asnoc anil (Var y′) x)
  begin
    AList-subst (asnoc anil (Var y′) x) x
      ≡⟨⟩
    apply-Subst⋆ (AList-subst anil) (thicken-except x (Var y′) x)
      ≡⟨ cong (apply-Subst⋆ (AList-subst anil)) (thicken-except-self x (Var y′)) ⟩
    apply-Subst⋆ (AList-subst anil) (Var y′)
      ≡⟨⟩
    Var y′
      ≡⟨ sym step-y ⟩
    AList-subst (asnoc anil (Var y′) x) y
  ∎
  where
    step-y :
      AList-subst (asnoc anil (Var y′) x) y ≡ Var y′
    step-y =
      begin
        AList-subst (asnoc anil (Var y′) x) y
          ≡⟨⟩
        apply-Subst⋆ (AList-subst anil) (thicken-except x (Var y′) y)
          ≡⟨ cong (apply-Subst⋆ (AList-subst anil))
                   (thicken-except-just x (Var y′) y E) ⟩
        apply-Subst⋆ (AList-subst anil) (Var y′)
          ≡⟨⟩
        Var y′
      ∎
... | nothing =
  begin
    AList-subst anil x ≡⟨⟩
    Var x              ≡⟨ thick-nothing→Var-eq x y E ⟩
    Var y              ≡⟨⟩
    AList-subst anil y
  ∎


flip-Unifies : ∀ {Φ Ψ} → (σ : Subst⋆ Φ Ψ) → (s t : Mono-Ty Φ) →
  Unifies σ s t →
  Unifies σ t s
flip-Unifies σ s t u = sym u

flex-flex-correct-at :
  ∀ {Φ Φ′ i j}
  (x : Ix⋆ Φ i) (y : Ix⋆ Φ j) →
  (σ : AList Φ Φ′) →
  flex-flex x y ≡ (Φ′ , σ) →
  Unifies (AList-subst σ) (Var x) (Var y)
flex-flex-correct-at x y σ p with flex-flex-correct x y
... | z rewrite p = z

postcompose-preserves :
  ∀ {Φ Ψ Ξ} (τ : Subst⋆ Ψ Ξ) (σ : Subst⋆ Φ Ψ) (s t : Mono-Ty Φ) →
  Unifies σ s t → Unifies (τ ∘S σ) s t
postcompose-preserves τ σ s t u = begin
  apply-Subst⋆ (τ ∘S σ) s
    ≡⟨ apply-Subst⋆-∘ τ σ s ⟩
  apply-Subst⋆ τ (apply-Subst⋆ σ s)
    ≡⟨ cong (apply-Subst⋆ τ) u ⟩
  apply-Subst⋆ τ (apply-Subst⋆ σ t)
    ≡⟨ sym (apply-Subst⋆-∘ τ σ t) ⟩
  apply-Subst⋆ (τ ∘S σ) t
  ∎

-- If two substitutions agree on variables, they agree on all mono types.
subst-ext :
  ∀ {Φ Ψ}
  (σ τ : Subst⋆ Φ Ψ) →
  (∀ {i} (x : Ix⋆ Φ i) → σ x ≡ τ x) →
  ∀ (t : Mono-Ty Φ) →
  apply-Subst⋆ σ t ≡ apply-Subst⋆ τ t
subst-ext σ τ H Bool      = refl
subst-ext σ τ H (u ⇒ v)   = cong₂ _⇒_ (subst-ext σ τ H u) (subst-ext σ τ H v)
subst-ext σ τ H (Var x)   = H x

subst-respects-++ :
  ∀ {Φ Φ′ Φ′′} {i}
  (ρ : AList Φ′ Φ′′) (σ : AList Φ Φ′) (x : Ix⋆ Φ i) →
  AList-subst (ρ ++ σ) x ≡ (AList-subst ρ ◇ AList-subst σ) x
subst-respects-++ ρ anil x = refl
subst-respects-++ ρ (asnoc σ a y) x =
  begin
    AList-subst (ρ ++ asnoc σ a y) x
      ≡⟨⟩
    -- def. of ++ and AList-subst
    apply-Subst⋆ (AList-subst (ρ ++ σ)) (thicken-except y a x)
      ≡⟨ subst-ext (AList-subst (ρ ++ σ))
                   (AList-subst ρ ◇ AList-subst σ)
                   (λ z → subst-respects-++ ρ σ z)
                   (thicken-except y a x) ⟩
    apply-Subst⋆ (AList-subst ρ ◇ AList-subst σ) (thicken-except y a x)
      ≡⟨ apply-Subst⋆-∘ (AList-subst ρ) (AList-subst σ) (thicken-except y a x) ⟩
    apply-Subst⋆ (AList-subst ρ)
                 (apply-Subst⋆ (AList-subst σ) (thicken-except y a x))
      ≡⟨⟩
    -- fold back the definition of AList-subst (asnoc …)
    (AList-subst ρ ◇ AList-subst (asnoc σ a y)) x
  ∎

++-left-id :
  ∀ {Φ Φ′} (σ : AList Φ Φ′) → anil ++ σ ≡ σ
++-left-id anil            = refl
++-left-id (asnoc σ a r)   = cong (λ δ → asnoc δ a r) (++-left-id σ)

++-assoc :
  ∀ {Φ₀ Φ₁ Φ₂ Φ₃}
    (ρ : AList Φ₂ Φ₃) (σ : AList Φ₁ Φ₂) (τ : AList Φ₀ Φ₁) →
  (ρ ++ σ) ++ τ ≡ ρ ++ (σ ++ τ)
++-assoc ρ σ anil            = refl
++-assoc ρ σ (asnoc τ a r)   =
  cong (λ δ → asnoc δ a r) (++-assoc ρ σ τ)

amgu-extends :
  ∀ {Φ Φ′ Φ″} (u v : Mono-Ty Φ) (σ : AList Φ Φ′) {σ′ : AList Φ Φ″} →
  amgu u v (Φ′ , σ) ≡ just (Φ″ , σ′) →
  ∃[ τ ] σ′ ≡ τ ++ σ

-- Bool/Bool returns the accumulator unchanged ⇒ witness τ = anil
amgu-extends Bool Bool σ {σ′} eq
  with inj-just eq
... | refl = anil , sym (++-left-id σ)

-- Shape mismatch branches are impossible (amgu = nothing)
amgu-extends Bool      (_ ⇒ _)  σ ()
amgu-extends (_ ⇒ _)   Bool     σ ()

-- Empty-accumulator variable cases: result itself is the witness (τ = σ′)
amgu-extends (Var _) (Var _) anil {σ′} _ = σ′ , refl
amgu-extends Bool     (Var _) anil {σ′} _ = σ′ , refl
amgu-extends (_ ⇒ _)  (Var _) anil {σ′} _ = σ′ , refl
amgu-extends (Var _)  Bool     anil {σ′} _ = σ′ , refl
amgu-extends (Var _)  (_ ⇒ _)  anil {σ′} _ = σ′ , refl

-- Arrow/Arrow composes the two recursive extensions and uses associativity
amgu-extends (s ⇒ s₁) (t ⇒ t₁) σ {σ′} eq
  with amgu s t (_ , σ) in E₁
... | just (Φ₁ , σ₁)
  with amgu-extends s t σ {σ₁} E₁
... | τ₁ , ext₁
  with amgu s₁ t₁ (Φ₁ , σ₁) in E₂
... | just (Φ″ , σ₂)
  with amgu-extends s₁ t₁ σ₁ {σ₂} E₂ | inj-just eq
... | τ₂ , ext₂ | refl =
  (τ₂ ++ τ₁) ,
    -- σ₂ ≡ τ₂ ++ σ₁ ≡ τ₂ ++ (τ₁ ++ σ) ≡ (τ₂ ++ τ₁) ++ σ
    trans ext₂
      (trans (cong (λ δ → τ₂ ++ δ) ext₁)
             (sym (++-assoc τ₂ τ₁ σ)))

-- Snoc-accumulator cases: reuse the inner extension and re-snoc on both sides
amgu-extends u@Bool v@(Var _) (asnoc σ z r) {σ′} eq
  with amgu (apply-Subst⋆ (thicken-except r z) u)
            (apply-Subst⋆ (thicken-except r z) v)
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with amgu-extends (apply-Subst⋆ (thicken-except r z) u)
                    (apply-Subst⋆ (thicken-except r z) v)
                    σ {σ₁} E
     | inj-just eq
... | τ , ext | refl =
  τ , cong (λ δ → asnoc δ z r) ext

amgu-extends u@(_ ⇒ _) v@(Var _) (asnoc σ z r) {σ′} eq
  with amgu (apply-Subst⋆ (thicken-except r z) u)
            (apply-Subst⋆ (thicken-except r z) v)
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with amgu-extends (apply-Subst⋆ (thicken-except r z) u)
                    (apply-Subst⋆ (thicken-except r z) v)
                    σ {σ₁} E
     | inj-just eq
... | τ , ext | refl =
  τ , cong (λ δ → asnoc δ z r) ext

amgu-extends u@(Var _) v@Bool (asnoc σ z r) {σ′} eq
  with amgu (apply-Subst⋆ (thicken-except r z) u)
            (apply-Subst⋆ (thicken-except r z) v)
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with amgu-extends (apply-Subst⋆ (thicken-except r z) u)
                    (apply-Subst⋆ (thicken-except r z) v)
                    σ {σ₁} E
     | inj-just eq
... | τ , ext | refl =
  τ , cong (λ δ → asnoc δ z r) ext

amgu-extends u@(Var _) v@(_ ⇒ _) (asnoc σ z r) {σ′} eq
  with amgu (apply-Subst⋆ (thicken-except r z) u)
            (apply-Subst⋆ (thicken-except r z) v)
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with amgu-extends (apply-Subst⋆ (thicken-except r z) u)
                    (apply-Subst⋆ (thicken-except r z) v)
                    σ {σ₁} E
     | inj-just eq
... | τ , ext | refl =
  τ , cong (λ δ → asnoc δ z r) ext

amgu-extends u@(Var _) v@(Var _) (asnoc σ z r) {σ′} eq
  with amgu (apply-Subst⋆ (thicken-except r z) u)
            (apply-Subst⋆ (thicken-except r z) v)
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with amgu-extends (apply-Subst⋆ (thicken-except r z) u)
                    (apply-Subst⋆ (thicken-except r z) v)
                    σ {σ₁} E
     | inj-just eq
... | τ , ext | refl =
  τ , cong (λ δ → asnoc δ z r) ext

precompose-on-domain :
  ∀ {Φ Ψ Ξ}
    (τ : Subst⋆ Φ Ψ) (σ : Subst⋆ Ψ Ξ) (s t : Mono-Ty Φ) →
  Unifies σ (apply-Subst⋆ τ s) (apply-Subst⋆ τ t) →
  Unifies (σ ◇ τ) s t
precompose-on-domain τ σ s t u = begin
  apply-Subst⋆ (σ ◇ τ) s
    ≡⟨ apply-Subst⋆-∘ σ τ s ⟩
  apply-Subst⋆ σ (apply-Subst⋆ τ s)
    ≡⟨ u ⟩
  apply-Subst⋆ σ (apply-Subst⋆ τ t)
    ≡⟨ sym (apply-Subst⋆-∘ σ τ t) ⟩
  apply-Subst⋆ (σ ◇ τ) t
  ∎

snoc-preserves-unif :
  ∀ {Φ Φ′ i}
    (σ : AList Φ Φ′) (z : Mono-Ty Φ) (r : Ix⋆ (S⋆ Φ) i)
    (s t : Mono-Ty (S⋆ Φ)) →
  Unifies (AList-subst σ)
          (apply-Subst⋆ (thicken-except r z) s)
          (apply-Subst⋆ (thicken-except r z) t) →
  Unifies (AList-subst (asnoc σ z r)) s t
snoc-preserves-unif σ z r s t u =
  -- AList-subst (asnoc σ z r) ≡ AList-subst σ ◇ thicken-except r z
  precompose-on-domain (thicken-except r z) (AList-subst σ) s t u

amgu-preserves-unification :
  ∀ {Φ Φ′ Φ″} (s t u v : Mono-Ty Φ) (σ : AList Φ Φ′) (σ′ : AList Φ Φ″) →
  Unifies (AList-subst σ) s t →
  amgu u v (Φ′ , σ) ≡ just (Φ″ , σ′) →
  Unifies (AList-subst σ′) s t
amgu-preserves-unification s t u v σ σ′ unif eq
  with amgu-extends u v σ {σ′} eq
... | τ , σ′≡τ++σ =
  begin
    apply-Subst⋆ (AList-subst σ′) s
      ≡⟨ cong (λ ρ → apply-Subst⋆ (AList-subst ρ) s) σ′≡τ++σ ⟩
    apply-Subst⋆ (AList-subst (τ ++ σ)) s
      ≡⟨ subst-ext (AList-subst (τ ++ σ))
                   (AList-subst τ ◇ AList-subst σ)
                   (λ x → subst-respects-++ τ σ x) s ⟩
    apply-Subst⋆ (AList-subst τ ◇ AList-subst σ) s
      ≡⟨ postcompose-preserves (AList-subst τ) (AList-subst σ) s t unif ⟩
    apply-Subst⋆ (AList-subst τ ◇ AList-subst σ) t
      ≡⟨ sym (subst-ext (AList-subst (τ ++ σ))
                         (AList-subst τ ◇ AList-subst σ)
                         (λ x → subst-respects-++ τ σ x) t) ⟩
    apply-Subst⋆ (AList-subst (τ ++ σ)) t
      ≡⟨ cong (λ ρ → apply-Subst⋆ (AList-subst ρ) t) (sym σ′≡τ++σ) ⟩
    apply-Subst⋆ (AList-subst σ′) t
  ∎

-- Generic finisher for the snoc branches
amgu-sound-snoc :
  ∀ {Φ Φ″ i}
    (z : Mono-Ty Φ) (r : Ix⋆ (S⋆ Φ) i)
    (u v : Mono-Ty (S⋆ Φ))
    (σ₁ : AList Φ Φ″) (σ′ : AList (S⋆ Φ) Φ″) →
  -- the outer branch tells us σ′ = asnoc σ₁ z r
  σ′ ≡ asnoc σ₁ z r →
  -- IH on the pushed-down problem
  Unifies (AList-subst σ₁)
          (apply-Subst⋆ (thicken-except r z) u)
          (apply-Subst⋆ (thicken-except r z) v) →
  -- goal: lift back up
  Unifies (AList-subst σ′) u v
amgu-sound-snoc z r u v σ₁ σ′ eqσ′ ih
  rewrite eqσ′ = snoc-preserves-unif σ₁ z r u v ih

amgu-sound :
  ∀ {Φ Φ′ Φ″} (u v : Mono-Ty Φ) (σ : AList Φ Φ′) (σ′ : AList Φ Φ″) →
  amgu u v (Φ′ , σ) ≡ just (Φ″ , σ′) →
  Unifies (AList-subst σ′) u v
amgu-sound Bool Bool σ σ′ eq = refl
amgu-sound Bool (Var x) anil σ′ eq = flip-Unifies (AList-subst σ′) (Var x) Bool (flex-rigid-correct x Bool σ′ eq)
amgu-sound (u ⇒ u₁) (Var x) anil σ′ eq = flip-Unifies (AList-subst σ′) (Var x) (u ⇒ u₁) (flex-rigid-correct x (u ⇒ u₁) σ′ eq)
amgu-sound (Var x) Bool anil σ′ eq = flex-rigid-correct x Bool σ′ eq
amgu-sound (Var x) (v ⇒ v₁) anil σ′ eq = flex-rigid-correct x (v ⇒ v₁) σ′ eq
amgu-sound (Var x) (Var y) anil σ′ refl = flex-flex-correct-at x y σ′ refl

amgu-sound (s ⇒ s₁) (t ⇒ t₁) σ σ′ eq
  -- peel the first recursive call
  with amgu s t (_ , σ) in E₁
... | just (Φ₁ , σ₁)
  -- peel the second recursive call
  with amgu s₁ t₁ (Φ₁ , σ₁) in E₂
... | just (Φ″ , σ₂)
  -- the outer eq identifies σ′ with σ₂ in this branch
  with inj-just eq
... | refl =
  let
    -- IHs for both recursive calls
    ih₁ : Unifies (AList-subst σ₁) s t
    ih₁ = amgu-sound s t σ σ₁ E₁

    ih₂ : Unifies (AList-subst σ₂) s₁ t₁
    ih₂ = amgu-sound s₁ t₁ σ₁ σ₂ E₂

    -- preserve the first unification across the second call
    pres : Unifies (AList-subst σ₂) s t
    pres = amgu-preserves-unification s t s₁ t₁ σ₁ σ₂ ih₁ E₂
  in
  -- put the two equalities together under _⇒_
  cong₂ _⇒_ pres ih₂

amgu-sound Bool (Var x) (asnoc σ z r) σ′ eq
  with amgu (apply-Subst⋆ (thicken-except r z) Bool)
            (apply-Subst⋆ (thicken-except r z) (Var x))
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with inj-just eq
... | refl =
  amgu-sound-snoc z r Bool (Var x) σ₁ (asnoc σ₁ z r) refl
    (amgu-sound (apply-Subst⋆ (thicken-except r z) Bool)
                (apply-Subst⋆ (thicken-except r z) (Var x))
                σ σ₁ E)

amgu-sound (u ⇒ u₁) (Var x) (asnoc σ z r) σ′ eq
  with amgu (apply-Subst⋆ (thicken-except r z) (u ⇒ u₁))
            (apply-Subst⋆ (thicken-except r z) (Var x))
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with inj-just eq
... | refl =
  amgu-sound-snoc z r (u ⇒ u₁) (Var x) σ₁ (asnoc σ₁ z r) refl
    (amgu-sound (apply-Subst⋆ (thicken-except r z) (u ⇒ u₁))
                (apply-Subst⋆ (thicken-except r z) (Var x))
                σ σ₁ E)

amgu-sound (Var x) Bool (asnoc σ z r) σ′ eq
  with amgu (apply-Subst⋆ (thicken-except r z) (Var x))
            (apply-Subst⋆ (thicken-except r z) Bool)
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with inj-just eq
... | refl =
  amgu-sound-snoc z r (Var x) Bool σ₁ (asnoc σ₁ z r) refl
    (amgu-sound (apply-Subst⋆ (thicken-except r z) (Var x))
                (apply-Subst⋆ (thicken-except r z) Bool)
                σ σ₁ E)

amgu-sound (Var x) (v ⇒ v₁) (asnoc σ z r) σ′ eq
  with amgu (apply-Subst⋆ (thicken-except r z) (Var x))
            (apply-Subst⋆ (thicken-except r z) (v ⇒ v₁))
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with inj-just eq
... | refl =
  amgu-sound-snoc z r (Var x) (v ⇒ v₁) σ₁ (asnoc σ₁ z r) refl
    (amgu-sound (apply-Subst⋆ (thicken-except r z) (Var x))
                (apply-Subst⋆ (thicken-except r z) (v ⇒ v₁))
                σ σ₁ E)

amgu-sound (Var x) (Var y) (asnoc σ z r) σ′ eq
  with amgu (apply-Subst⋆ (thicken-except r z) (Var x))
            (apply-Subst⋆ (thicken-except r z) (Var y))
            (_ , σ) in E
... | just (Φ″ , σ₁)
  with inj-just eq
... | refl =
  amgu-sound-snoc z r (Var x) (Var y) σ₁ (asnoc σ₁ z r) refl
    (amgu-sound (apply-Subst⋆ (thicken-except r z) (Var x))
                (apply-Subst⋆ (thicken-except r z) (Var y))
                σ σ₁ E)

mgu-sound :
  ∀ {Φ Φ′} (u v : Mono-Ty Φ) (σ : AList Φ Φ′) →
  mgu u v ≡ just (Φ′ , σ) →
  Unifies (AList-subst σ) u v
mgu-sound u v σ eq = amgu-sound u v anil σ eq