open import Level hiding (zero ; suc)

open import Chapter4.Desc
open import Chapter4.Desc.Tagged
open import Chapter4.Desc.Fixpoint

module Chapter7.NoConfusion 
         {ℓ : Level}
         (D : tagDesc ℓ) 
       where

open import Level  hiding (zero) renaming (suc to sucL)
open import Function

open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Nat hiding (compare ; pred ; _≟_)
open import Data.Fin hiding (lift)
open import Data.Sum
open import Data.Product

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

Eq : (D : Desc ℓ){X : Set ℓ} → ⟦ D ⟧ X → ⟦ D ⟧ X → Set ℓ
Eq `1 (lift tt) (lift tt) = Lift ⊤
Eq `var xs ys = xs ≡ ys
Eq (D₁ `× D₂) (xs₁ , xs₂) (ys₁ , ys₂) = Eq D₁ xs₁ ys₁ × Eq D₂ xs₂ ys₂
Eq (D₁ `+ D₂) (inj₁ xs₁) (inj₁ ys₁) = Eq D₁ xs₁ ys₁
Eq (D₁ `+ D₂) (inj₁ xs₁) (inj₂ ys₂) = Lift ⊥
Eq (D₁ `+ D₂) (inj₂ xs₁) (inj₁ ys₂) = Lift ⊥
Eq (D₁ `+ D₂) (inj₂ xs₂) (inj₂ ys₂) = Eq D₂ xs₂ ys₂
Eq (`Σ S T) (s₁ , xs) (s₂ , ys) = Σ[ q ∈ s₁ ≡ s₂ ] Eq (T s₁) xs (subst (λ s → ⟦ T s ⟧ _) (sym q) ys)
Eq (`Π S T) xs ys = ∀ s → Eq (T s) (xs s) (ys s)


infix  _≟_

_≟_ : {n : ℕ} → Decidable {A = Fin n} _≡_
zero  ≟ zero   = yes refl
suc m ≟ suc n  with m ≟ n
suc m ≟ suc .m | yes refl = yes refl
suc m ≟ suc n  | no prf = no (λ q → prf (help q)) 
  where help : ∀{k}{m n : Fin k} → _≡_ {A = Fin ((suc k))} (suc m) (suc n) → m ≡ n
        help refl = refl
zero  ≟ suc n  = no λ()
suc m ≟ zero   = no λ()


NoConfusion : (x y : μ (toDesc D)) → Set (sucL ℓ)
NoConfusion ⟨ lift x , args₁ ⟩ ⟨ lift y , args₂ ⟩ with x ≟ y
NoConfusion ⟨ lift .y , args₁ ⟩ ⟨ lift y , args₂ ⟩
    | yes refl = ∀ (P : Set ℓ) → (args₁ ≡ args₂ → P) → P
NoConfusion ⟨ lift x , args₁ ⟩ ⟨ lift y , args₂ ⟩
    | no q = ∀ P → P

noConfusion : (x y : ⟦ toDesc D ⟧ (μ (toDesc D))) → x ≡ y → NoConfusion (⟨ x ⟩) (⟨ y ⟩)
noConfusion (lift x , args₁) (lift y , args₂) q with x ≟ y
noConfusion (lift .y , .args₁) (lift y , args₁) refl | yes refl = λ P rec → rec refl
noConfusion (lift .y , .args₂) (lift y , args₂) refl | no notEq = ⊥-elim (notEq refl)