------------------------------------------------------------------------
-- Decidability of bi-derectional typechecking.
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
import Tools.PropositionalEquality as PE
open import Tools.Relation

module Definition.Typechecking.Decidable
  {a} {M : Set a}
  (R : Type-restrictions M)
  (open Type-restrictions R)
  -- Equality is assumed to be decidable for M.
  (_≟_ : Decidable (PE._≡_ {A = M}))
  -- It is decidable whether the Unit type is allowed.
  (Unit-ok? : Dec Unit-allowed)
  -- ΠΣ-allowed is pointwise decidable.
  (ΠΣ-ok? :  b p q  Dec (ΠΣ-allowed b p q))
  where

open import Definition.Typechecking R
open import Definition.Typechecking.Soundness R
open import Definition.Typechecking.Deterministic R
open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Typed.Weakening R as W
open import Definition.Typed.Consequences.Inequality R
open import Definition.Typed.Consequences.Inversion R
open import Definition.Typed.Consequences.Syntactic R
open import Definition.Typed.Consequences.Substitution R
open import Definition.Typed.Decidable.Equality R _≟_
open import Definition.Typed.Decidable.Reduction R _≟_
open import Definition.Untyped M
open import Definition.Untyped.Properties M
import Definition.Untyped M as U

open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat)
open import Tools.Product

private
  variable
    n : Nat
    Γ : Con Term n
    t u A B : Term n
    p q r : M

dec⇉-var : (x : Fin n)   λ A  x  A  Γ
dec⇉-var {Γ = Γ  A} x0 = _ , here
dec⇉-var {Γ = Γ  B} (x +1) =
  let A , x∷A∈Γ = dec⇉-var x
  in  _ , there x∷A∈Γ

dec⇇-var : (x : Fin n)  Γ  A  Dec (Γ  var x  A)
dec⇇-var x ⊢A =
  let B , x∷B∈Γ = dec⇉-var x
  in  case decEq (syntacticVar x∷B∈Γ (wf ⊢A)) ⊢A of λ where
    (yes B≡A)  yes (infᶜ (varᵢ x∷B∈Γ) B≡A)
    (no B≢A)  no λ where
      (infᶜ (varᵢ x) x₁)  case det∈ x x∷B∈Γ of λ where
        PE.refl  B≢A x₁

mutual

  -- Decidability of terms being inferable

  dec-Inferable : (t : Term n)  Dec (Inferable t)
  dec-Inferable (var x) = yes varᵢ
  dec-Inferable U = yes Uᵢ
  dec-Inferable (ΠΣ⟨ b  p , q  F  G) =
    case dec-Checkable F of λ where
      (yes F′)  case dec-Checkable G of λ where
        (yes G′)  yes (ΠΣᵢ F′ G′)
        (no ¬G′)  no λ where
          (ΠΣᵢ x x₁)  ¬G′ x₁
      (no ¬F′)  no λ where
        (ΠΣᵢ x x₁)  ¬F′ x
  dec-Inferable (lam p t) = no λ ()
  dec-Inferable (t ∘⟨ p  u) = case dec-Inferable t of λ where
    (yes t′)  case dec-Checkable u of λ where
      (yes u′)  yes (∘ᵢ t′ u′)
      (no ¬u′)  no λ where
        (∘ᵢ x x₁)  ¬u′ x₁
    (no ¬t′)  no λ where
      (∘ᵢ x x₁)  ¬t′ x
  dec-Inferable (prod! t u) = no λ ()
  dec-Inferable (fst p t) = case dec-Inferable t of λ where
    (yes t′)  yes (fstᵢ t′)
    (no ¬t′)  no λ where
      (fstᵢ x)  ¬t′ x
  dec-Inferable (snd p t) = case dec-Inferable t of λ where
    (yes t′)  yes (sndᵢ t′)
    (no ¬t′)  no λ where
      (sndᵢ x)  ¬t′ x
  dec-Inferable (prodrec r p q A t u) = case dec-Checkable A of λ where
    (yes A′)  case dec-Inferable t of λ where
      (yes t′)  case dec-Checkable u of λ where
        (yes u′)  yes (prodrecᵢ A′ t′ u′)
        (no ¬u′)  no λ where
          (prodrecᵢ x x₁ x₂)  ¬u′ x₂
      (no ¬t′)  no λ where
        (prodrecᵢ x x₁ x₂)  ¬t′ x₁
    (no ¬A′)  no λ where
      (prodrecᵢ x x₁ x₂)  ¬A′ x
  dec-Inferable  = yes ℕᵢ
  dec-Inferable zero = yes zeroᵢ
  dec-Inferable (suc t) = case dec-Checkable t of λ where
    (yes t′)  yes (sucᵢ t′)
    (no ¬t′)  no λ where
      (sucᵢ x)  ¬t′ x
  dec-Inferable (natrec p q r A z s n) = case dec-Checkable A of λ where
    (yes A′)  case dec-Checkable z of λ where
      (yes z′)  case dec-Checkable s of λ where
        (yes s′)  case dec-Checkable n of λ where
          (yes n′)  yes (natrecᵢ A′ z′ s′ n′)
          (no ¬n′)   no λ where
            (natrecᵢ x x₁ x₂ x₃)  ¬n′ x₃
        (no ¬s′)   no λ where
          (natrecᵢ x x₁ x₂ x₃)  ¬s′ x₂
      (no ¬z′)   no λ where
        (natrecᵢ x x₁ x₂ x₃)  ¬z′ x₁
    (no ¬A′)  no λ where
      (natrecᵢ x x₁ x₂ x₃)  ¬A′ x
  dec-Inferable Unit = yes Unitᵢ
  dec-Inferable star = yes starᵢ
  dec-Inferable Empty = yes Emptyᵢ
  dec-Inferable (emptyrec p A t) = case dec-Checkable A of λ where
    (yes A′)  case dec-Checkable t of λ where
      (yes t′)  yes (emptyrecᵢ A′ t′)
      (no ¬t′)   no λ where
        (emptyrecᵢ x x₁)  ¬t′ x₁
    (no ¬A′)  no λ where
      (emptyrecᵢ x x₁)  ¬A′ x

  -- Decidability of terms being checkable

  dec-Checkable : (t : Term n)  Dec (Checkable t)
  dec-Checkable (var x) = yes (infᶜ varᵢ)
  dec-Checkable U = yes (infᶜ Uᵢ)
  dec-Checkable (ΠΣ⟨ b  p , q  F  G) = case dec-Checkable F of λ where
    (yes F′)  case dec-Checkable G of λ where
      (yes G′)  yes (infᶜ (ΠΣᵢ F′ G′))
      (no ¬G′)  no λ where
        (infᶜ (ΠΣᵢ x x₁))  ¬G′ x₁
    (no ¬F′)  no λ where
      (infᶜ (ΠΣᵢ x x₁))  ¬F′ x
  dec-Checkable (lam p t) = case dec-Checkable t of λ where
    (yes t′)  yes (lamᶜ t′)
    (no ¬t′)  no λ where
      (lamᶜ x)  ¬t′ x
  dec-Checkable (t ∘⟨ p  u) = case dec-Inferable t of λ where
    (yes t′)  case dec-Checkable u of λ where
      (yes u′)  yes (infᶜ (∘ᵢ t′ u′))
      (no ¬u′)  no λ where
        (infᶜ (∘ᵢ x x₁))  ¬u′ x₁
    (no ¬t′)  no λ where
      (infᶜ (∘ᵢ x x₁))  ¬t′ x
  dec-Checkable (prod! t u) = case dec-Checkable t of λ where
    (yes t′)  case dec-Checkable u of λ where
      (yes u′)  yes (prodᶜ t′ u′)
      (no ¬u′)  no λ where
        (prodᶜ x x₁)  ¬u′ x₁
    (no ¬t′)  no λ where
      (prodᶜ x x₁)  ¬t′ x
  dec-Checkable (fst p t) = case dec-Inferable t of λ where
    (yes t′)  yes (infᶜ (fstᵢ t′))
    (no ¬t′)  no λ where
      (infᶜ (fstᵢ t′))  ¬t′ t′
  dec-Checkable (snd p t) = case dec-Inferable t of λ where
    (yes t′)  yes (infᶜ (sndᵢ t′))
    (no ¬t′)  no λ where
      (infᶜ (sndᵢ t′))  ¬t′ t′
  dec-Checkable (prodrec r p q A t u) = case dec-Checkable A of λ where
    (yes A′)  case dec-Inferable t of λ where
      (yes t′)  case dec-Checkable u of λ where
        (yes u′)  yes (infᶜ (prodrecᵢ A′ t′ u′))
        (no ¬u′)  no λ where
          (infᶜ (prodrecᵢ x x₁ x₂))  ¬u′ x₂
      (no ¬t′)  no λ where
        (infᶜ (prodrecᵢ x x₁ x₂))  ¬t′ x₁
    (no ¬A′)  no λ where
      (infᶜ (prodrecᵢ x x₁ x₂))  ¬A′ x
  dec-Checkable  = yes (infᶜ ℕᵢ)
  dec-Checkable zero = yes (infᶜ zeroᵢ)
  dec-Checkable (suc t) = case dec-Checkable t of λ where
    (yes t′)  yes (infᶜ (sucᵢ t′))
    (no ¬t′)  no λ where
      (infᶜ (sucᵢ x))  ¬t′ x
  dec-Checkable (natrec p q r A z s n) = case dec-Checkable A of λ where
    (yes A′)  case dec-Checkable z of λ where
      (yes z′)  case dec-Checkable s of λ where
        (yes s′)  case dec-Checkable n of λ where
          (yes n′)  yes (infᶜ (natrecᵢ A′ z′ s′ n′))
          (no ¬n′)  no λ where
            (infᶜ (natrecᵢ x x₁ x₂ x₃))  ¬n′ x₃
        (no ¬s′)  no λ where
          (infᶜ (natrecᵢ x x₁ x₂ x₃))  ¬s′ x₂
      (no ¬z′)  no λ where
        (infᶜ (natrecᵢ x x₁ x₂ x₃))  ¬z′ x₁
    (no ¬A′)  no λ where
      (infᶜ (natrecᵢ x x₁ x₂ x₃))  ¬A′ x
  dec-Checkable Unit = yes (infᶜ Unitᵢ)
  dec-Checkable star = yes (infᶜ starᵢ)
  dec-Checkable Empty = yes (infᶜ Emptyᵢ)
  dec-Checkable (emptyrec p A t) = case dec-Checkable A of λ where
    (yes A′)  case dec-Checkable t of λ where
      (yes t′)  yes (infᶜ (emptyrecᵢ A′ t′))
      (no ¬t′)  no λ where
        (infᶜ (emptyrecᵢ x x₁))  ¬t′ x₁
    (no ¬A′)  no λ where
      (infᶜ (emptyrecᵢ x x₁))  ¬A′ x

mutual

  dec⇉-app :  Γ  Inferable t  Checkable u  Dec ( λ A  Γ  t ∘⟨ p  u  A)
  dec⇉-app {p = p′} ⊢Γ t u = case dec⇉ ⊢Γ t of λ where
    (yes (A , t⇉A))  case isΠ (proj₁ (soundness⇉ ⊢Γ t⇉A)) of λ where
      (yes (F , G , p , q , ⊢F , ⊢G , A⇒Π))  case dec⇇ ⊢Γ u ⊢F of λ where
        (yes u⇇F)  case p  p′ of λ where
          (yes PE.refl)  yes (_ , appᵢ t⇉A (A⇒Π , ΠΣₙ) u⇇F)
          (no p≢p′)  no λ where
            (_ , appᵢ x x₁ x₂)  case deterministic⇉ x t⇉A of λ where
              PE.refl  case whrDet* (A⇒Π , ΠΣₙ) x₁ of λ where
                PE.refl  p≢p′ PE.refl
        (no ¬u⇇F)  no λ where
          (_ , appᵢ x x₁ x₂)  case deterministic⇉ x t⇉A of λ where
             PE.refl  case whrDet* (A⇒Π , ΠΣₙ) x₁ of λ where
               PE.refl  ¬u⇇F x₂
      (no ¬isΠ)  no λ where
        (_ , appᵢ x x₁ x₂)  case deterministic⇉ x t⇉A of λ where
             PE.refl 
               let _ , ⊢Π = syntacticRed (proj₁ x₁)
                   ⊢F , ⊢G = syntacticΠ ⊢Π
               in  ¬isΠ (_ , _ , _ , _ , ⊢F , ⊢G , proj₁ x₁)
    (no ¬t⇉A)  no λ where
      (_ , appᵢ x x₁ x₂)  ¬t⇉A (_ , x)

  dec⇉-fst :  Γ  Inferable t  Dec ( λ A  Γ  fst p t  A)
  dec⇉-fst {p = p′} ⊢Γ t = case dec⇉ ⊢Γ t of λ where
    (yes (A , t⇉A))  case isΣₚ (proj₁ (soundness⇉ ⊢Γ t⇉A)) of λ where
      (yes (F , G , p , q , ⊢F , ⊢G , A⇒Σ))  case p  p′ of λ where
        (yes PE.refl)  yes (_ , fstᵢ t⇉A (A⇒Σ , U.ΠΣₙ))
        (no p≢p′)  no λ where
          (_ , fstᵢ x x₁)  case deterministic⇉ x t⇉A of λ where
             PE.refl  case whrDet* (A⇒Σ , ΠΣₙ) x₁ of λ where
               PE.refl  p≢p′ PE.refl
      (no ¬isΣ)  no λ where
        (_ , fstᵢ x x₁)  case deterministic⇉ x t⇉A of λ where
          PE.refl 
            let _ , ⊢Σ = syntacticRed (proj₁ x₁)
                ⊢F , ⊢G = syntacticΣ ⊢Σ
            in  ¬isΣ (_ , _ , _ , _ , ⊢F , ⊢G , proj₁ x₁)
    (no ¬t⇉A)  no λ where
      (_ , fstᵢ x x₁)  ¬t⇉A (_ , x)

  dec⇉-snd :  Γ  Inferable t  Dec ( λ A  Γ  snd p t  A)
  dec⇉-snd {p = p′} ⊢Γ t = case dec⇉ ⊢Γ t of λ where
    (yes (A , t⇉A))  case isΣₚ (proj₁ (soundness⇉ ⊢Γ t⇉A)) of λ where
      (yes (F , G , p , q , ⊢F , ⊢G , A⇒Σ))  case p  p′ of λ where
        (yes PE.refl)  yes (_ , sndᵢ t⇉A (A⇒Σ , U.ΠΣₙ))
        (no p≢p′)  no λ where
          (_ , sndᵢ x x₁)  case deterministic⇉ x t⇉A of λ where
             PE.refl  case whrDet* (A⇒Σ , ΠΣₙ) x₁ of λ where
               PE.refl  p≢p′ PE.refl
      (no ¬isΣ)  no λ where
        (_ , sndᵢ x x₁)  case deterministic⇉ x t⇉A of λ where
          PE.refl 
            let _ , ⊢Σ = syntacticRed (proj₁ x₁)
                ⊢F , ⊢G = syntacticΣ ⊢Σ
            in  ¬isΣ (_ , _ , _ , _ , ⊢F , ⊢G , proj₁ x₁)
    (no ¬t⇉A)  no λ where
      (_ , sndᵢ x x₁)  ¬t⇉A (_ , x)

  dec⇉-natrec :  {A z s n}   Γ  Checkable A  Checkable z  Checkable s  Checkable n
               Dec ( λ B  Γ  natrec p q r A z s n  B)
  dec⇉-natrec ⊢Γ A z s n = case dec⇇ ⊢Γ n (ℕⱼ ⊢Γ) of λ where
    (yes n⇇ℕ)  case dec⇇Type (⊢Γ  ℕⱼ ⊢Γ) A of λ where
      (yes A⇇Type) 
        let ⊢A = soundness⇇Type (⊢Γ  ℕⱼ ⊢Γ) A⇇Type
            ⊢A₀ = substType ⊢A (zeroⱼ ⊢Γ)
        in  case dec⇇ ⊢Γ z ⊢A₀ of λ where
          (yes z⇇A₀) 
            let ⊢Γ₊ = ⊢Γ  ℕⱼ ⊢Γ  ⊢A
                ⊢A₊ =  subst↑²Type (ℕⱼ ⊢Γ) ⊢A ⊢A (sucⱼ (var ⊢Γ₊ (there here)))
            in  case dec⇇ ⊢Γ₊ s ⊢A₊ of λ where
              (yes s⇇A₊)  yes (_ , natrecᵢ A⇇Type z⇇A₀ s⇇A₊ n⇇ℕ)
              (no ¬s⇇A₊)  no λ where
                (_ , natrecᵢ x x₁ x₂ x₃)  ¬s⇇A₊ x₂ --¬s⇇A₊ x₂
          (no ¬z⇇A₀)  no λ where
            (_ , natrecᵢ x x₁ x₂ x₃)  ¬z⇇A₀ x₁
      (no ¬A⇇Type)  no λ where
        (_ , natrecᵢ x x₁ x₂ x₃)  ¬A⇇Type x
    (no ¬n⇇ℕ)  no λ where
      (_ , natrecᵢ x x₁ x₂ x₃)  ¬n⇇ℕ x₃

  dec⇉-prodrec :  Γ  Checkable A  Inferable t  Checkable u
                Dec ( λ B  Γ  prodrec r p q A t u  B)
  dec⇉-prodrec {r = r} {p = p′} {q = q} ⊢Γ A t u =
    case dec⇉ ⊢Γ t of λ where
      (yes (B , t⇉B))  case isΣᵣ (proj₁ (soundness⇉ ⊢Γ t⇉B)) of λ where
        (yes (F , G , p , _ , ⊢F , ⊢G , B⇒Σ)) 
          case inversion-ΠΣ (syntacticRed B⇒Σ .proj₂) of λ {
            (_ , _ , ok) 
          case dec⇇Type (⊢Γ  ΠΣⱼ ⊢F ⊢G ok) A of λ where
            (yes A⇇Type) 
              let ⊢ΓΣ = ⊢Γ  ΠΣⱼ {p = p} ⊢F ⊢G ok
                  ⊢A = soundness⇇Type ⊢ΓΣ A⇇Type
                  ⊢A₊ = subst↑²Type-prod ⊢A ok
              in  case dec⇇ (⊢Γ  ⊢F  ⊢G) u ⊢A₊ of λ where
                (yes u⇇A₊)  case p  p′ of λ where
                  (yes PE.refl) 
                    yes (_ , prodrecᵢ A⇇Type t⇉B (B⇒Σ , ΠΣₙ) u⇇A₊)
                  (no p≢p′)  no λ where
                    (_ , prodrecᵢ _ x₁ x₂ _) 
                      case deterministic⇉ t⇉B x₁ of λ where
                        PE.refl  case whrDet* (B⇒Σ , ΠΣₙ) x₂ of λ where
                          PE.refl  p≢p′ PE.refl
                (no ¬u⇇A₊)  no λ where
                  (_ , prodrecᵢ _ x₁ x₂ x₃) 
                    case deterministic⇉ t⇉B x₁ of λ where
                       PE.refl  case whrDet* (B⇒Σ , ΠΣₙ) x₂ of λ where
                         PE.refl  ¬u⇇A₊ x₃
            (no ¬A⇇Type)  no λ where
              (_ , prodrecᵢ x x₁ x₂ _) 
                case deterministic⇉ t⇉B x₁ of λ where
                  PE.refl  case whrDet* (B⇒Σ , ΠΣₙ) x₂ of λ where
                    PE.refl  ¬A⇇Type x }
        (no ¬isΣ)  no λ where
          (_ , prodrecᵢ _ x₁ x₂ _) 
            case deterministic⇉ t⇉B x₁ of λ where
              PE.refl 
                let _ , ⊢Σ = syntacticRed (proj₁ x₂)
                    ⊢F , ⊢G = syntacticΣ ⊢Σ
                in  ¬isΣ (_ , _ , _ , _ , ⊢F , ⊢G , proj₁ x₂)
      (no ¬t⇉B)  no λ where
        (_ , prodrecᵢ x x₁ x₂ x₃)  ¬t⇉B (_ , x₁)

  dec⇉-emptyrec :  Γ  Checkable A  Checkable t  Dec ( λ B  Γ  emptyrec p A t  B)
  dec⇉-emptyrec ⊢Γ A t = case dec⇇Type ⊢Γ A of λ where
    (yes A⇇Type)  case dec⇇ ⊢Γ t (Emptyⱼ ⊢Γ) of λ where
      (yes t⇇Empty)  yes (_ , emptyrecᵢ A⇇Type t⇇Empty)
      (no ¬t⇇Empty)  no λ where
        (_ , emptyrecᵢ x x₁)  ¬t⇇Empty x₁
    (no ¬A⇇Type)  no λ where
      (_ , emptyrecᵢ x x₁)  ¬A⇇Type x

  -- Decidability of checking that an inferable term is a type

  dec⇉Type :  Γ  Inferable A  Dec (Γ  A ⇇Type)
  dec⇉Type ⊢Γ Uᵢ = yes Uᶜ
  dec⇉Type ⊢Γ (ΠΣᵢ {b = b} {p = p} {q = q} F G) =
    case dec⇇Type ⊢Γ F of λ where
      (yes F⇇Type) 
        case dec⇇Type (⊢Γ  soundness⇇Type ⊢Γ F⇇Type) G of λ where
          (yes G⇇Type)  case ΠΣ-ok? b p q of λ where
            (yes ok)     yes (ΠΣᶜ F⇇Type G⇇Type ok)
            (no not-ok)  no λ where
              (ΠΣᶜ _ _ ok)                   not-ok ok
              (univᶜ (infᶜ (ΠΣᵢ _ _ ok) _))  not-ok ok
          (no ¬G⇇Type)  no λ where
            (ΠΣᶜ _ x _)                   ¬G⇇Type x
            (univᶜ (infᶜ (ΠΣᵢ _ x _) _))  ¬G⇇Type (univᶜ x)
      (no ¬F⇇Type)  no λ where
        (ΠΣᶜ x _ _)                   ¬F⇇Type x
        (univᶜ (infᶜ (ΠΣᵢ x _ _) _))  ¬F⇇Type (univᶜ x)
  dec⇉Type ⊢Γ (varᵢ {x = x}) = case dec⇇-var x (Uⱼ ⊢Γ) of λ where
    (yes x⇇U)  yes (univᶜ x⇇U)
    (no ¬x⇇U)  no λ where
      (univᶜ x)  ¬x⇇U x
  dec⇉Type ⊢Γ (∘ᵢ t u) = case dec⇉-app ⊢Γ t u of λ where
    (yes (A , tu⇉A))  case decEq (proj₁ (soundness⇉ ⊢Γ tu⇉A)) (Uⱼ ⊢Γ) of λ where
      (yes A≡U)  yes (univᶜ (infᶜ tu⇉A A≡U))
      (no A≢U)  no λ where
        (univᶜ (infᶜ x x₁))  case deterministic⇉ tu⇉A x of λ where
          PE.refl  A≢U x₁
    (no ¬t′)  no λ where
      (univᶜ (infᶜ x x₁))  ¬t′ (_ , x)
  dec⇉Type ⊢Γ (fstᵢ t) = case dec⇉-fst ⊢Γ t of λ where
    (yes (A , t₁⇉A))  case decEq (proj₁ (soundness⇉ ⊢Γ t₁⇉A)) (Uⱼ ⊢Γ) of λ where
      (yes A≡U)  yes (univᶜ (infᶜ t₁⇉A A≡U))
      (no A≢U)  no λ where
        (univᶜ (infᶜ x x₁))  case deterministic⇉ t₁⇉A x of λ where
          PE.refl  A≢U x₁
    (no ¬t₁⇉A)  no λ where
      (univᶜ (infᶜ x x₁))  ¬t₁⇉A (_ , x)
  dec⇉Type ⊢Γ (sndᵢ t) = case dec⇉-snd ⊢Γ t of λ where
    (yes (A , t₂⇉A))  case decEq (proj₁ (soundness⇉ ⊢Γ t₂⇉A)) (Uⱼ ⊢Γ) of λ where
      (yes A≡U)  yes (univᶜ (infᶜ t₂⇉A A≡U))
      (no A≢U)  no λ where
        (univᶜ (infᶜ x x₁))  case deterministic⇉ t₂⇉A x of λ where
          PE.refl  A≢U x₁
    (no ¬t₂⇉A)  no λ where
      (univᶜ (infᶜ x x₁))  ¬t₂⇉A (_ , x)
  dec⇉Type ⊢Γ (prodrecᵢ B t u) = case dec⇉-prodrec ⊢Γ B t u of λ where
    (yes (A , pr⇉A))  case decEq (proj₁ (soundness⇉ ⊢Γ pr⇉A)) (Uⱼ ⊢Γ) of λ where
      (yes A≡U)  yes (univᶜ (infᶜ pr⇉A A≡U))
      (no A≢U)  no λ where
        (univᶜ (infᶜ x x₁))  case deterministic⇉ pr⇉A x of λ where
          PE.refl  A≢U x₁
    (no ¬pr⇉A)  no λ where
      (univᶜ (infᶜ x x₁))  ¬pr⇉A (_ , x)
  dec⇉Type ⊢Γ ℕᵢ = yes ℕᶜ
  dec⇉Type ⊢Γ zeroᵢ = no λ where
    (univᶜ (infᶜ zeroᵢ x₁))  U≢ℕ (sym x₁)
  dec⇉Type ⊢Γ (sucᵢ x) = no λ where
    (univᶜ (infᶜ (sucᵢ x) x₁))  U≢ℕ (sym x₁)
  dec⇉Type ⊢Γ (natrecᵢ B z s n) = case dec⇉-natrec ⊢Γ B z s n of λ where
    (yes (A , pr⇉A))  case decEq (proj₁ (soundness⇉ ⊢Γ pr⇉A)) (Uⱼ ⊢Γ) of λ where
      (yes A≡U)  yes (univᶜ (infᶜ pr⇉A A≡U))
      (no A≢U)  no λ where
        (univᶜ (infᶜ x x₁))  case deterministic⇉ pr⇉A x of λ where
          PE.refl  A≢U x₁
    (no ¬pr⇉A)  no λ where
      (univᶜ (infᶜ x x₁))  ¬pr⇉A (_ , x)
  dec⇉Type ⊢Γ Unitᵢ = case Unit-ok? of λ where
    (yes ok)     yes (Unitᶜ ok)
    (no not-ok)  no λ where
      (Unitᶜ ok)                   not-ok ok
      (univᶜ (infᶜ (Unitᵢ ok) _))  not-ok ok
  dec⇉Type ⊢Γ starᵢ = no λ where
    (univᶜ (infᶜ (starᵢ _) x))  U≢Unitⱼ (sym x)
  dec⇉Type ⊢Γ Emptyᵢ = yes Emptyᶜ
  dec⇉Type ⊢Γ (emptyrecᵢ B t) = case dec⇉-emptyrec ⊢Γ B t of λ where
    (yes (A , pr⇉A))  case decEq (proj₁ (soundness⇉ ⊢Γ pr⇉A)) (Uⱼ ⊢Γ) of λ where
      (yes A≡U)  yes (univᶜ (infᶜ pr⇉A A≡U))
      (no A≢U)  no λ where
        (univᶜ (infᶜ x x₁))  case deterministic⇉ pr⇉A x of λ where
          PE.refl  A≢U x₁
    (no ¬pr⇉A)  no λ where
      (univᶜ (infᶜ x x₁))  ¬pr⇉A (_ , x)

  -- Decidability of checking that a checkable term is a type

  dec⇇Type :  Γ  Checkable A  Dec (Γ  A ⇇Type)
  dec⇇Type ⊢Γ (lamᶜ t) = no λ where
    (univᶜ (lamᶜ x x₁))  U.U≢B BΠ! (whnfRed* (proj₁ x) Uₙ)
  dec⇇Type ⊢Γ (prodᶜ t u) = no λ where
    (univᶜ (prodᶜ x x₁ x₂))  U.U≢B BΣ! (whnfRed* (proj₁ x) Uₙ)
  dec⇇Type ⊢Γ (infᶜ x) = dec⇉Type ⊢Γ x

  -- Decidability of bi-directional type inference

  dec⇉ :  Γ  Inferable t  Dec ( λ A  Γ  t  A)
  dec⇉ ⊢Γ Uᵢ = no λ where (A , ())
  dec⇉ ⊢Γ (ΠΣᵢ {b = b} {p = p} {q = q} F G) =
    case dec⇇ ⊢Γ F (Uⱼ ⊢Γ) of λ where
      (yes F⇇U) 
        let ⊢F = soundness⇇ ⊢Γ F⇇U
        in  case dec⇇ (⊢Γ  univ ⊢F) G (Uⱼ (⊢Γ  univ ⊢F)) of λ where
          (yes G⇇U)  case ΠΣ-ok? b p q of λ where
            (yes ok)     yes (_ , ΠΣᵢ F⇇U G⇇U ok)
            (no not-ok)  no λ where
              (_ , ΠΣᵢ _ _ ok)  not-ok ok
          (no ¬G⇇U)  no λ where
            (_ , ΠΣᵢ _ x _)  ¬G⇇U x
      (no ¬F⇇U)  no λ where
        (_ , ΠΣᵢ x _ _)  ¬F⇇U x
  dec⇉ ⊢Γ varᵢ = yes (_ , varᵢ (proj₂ (dec⇉-var _)))
  dec⇉ ⊢Γ (∘ᵢ t u) = dec⇉-app ⊢Γ t u
  dec⇉ ⊢Γ (fstᵢ t) = dec⇉-fst ⊢Γ t
  dec⇉ ⊢Γ (sndᵢ t) = dec⇉-snd ⊢Γ t
  dec⇉ ⊢Γ (prodrecᵢ A t u) = dec⇉-prodrec ⊢Γ A t u
  dec⇉ ⊢Γ ℕᵢ = yes (U , ℕᵢ)
  dec⇉ ⊢Γ zeroᵢ = yes ( , zeroᵢ)
  dec⇉ ⊢Γ (sucᵢ t) = case dec⇇ ⊢Γ t (ℕⱼ ⊢Γ) of λ where
    (yes t⇇ℕ)  yes (_ , sucᵢ t⇇ℕ)
    (no ¬t⇇ℕ)  no λ where
      (_ , sucᵢ x)  ¬t⇇ℕ x
  dec⇉ ⊢Γ (natrecᵢ A z s n) = dec⇉-natrec ⊢Γ A z s n
  dec⇉ ⊢Γ Unitᵢ = case Unit-ok? of λ where
    (yes ok)     yes (U , Unitᵢ ok)
    (no not-ok)  no λ where
      (_ , Unitᵢ ok)  not-ok ok
  dec⇉ ⊢Γ starᵢ = case Unit-ok? of λ where
    (yes ok)     yes (Unit , starᵢ ok)
    (no not-ok)  no λ where
      (_ , starᵢ ok)  not-ok ok
  dec⇉ ⊢Γ Emptyᵢ = yes (U , Emptyᵢ)
  dec⇉ ⊢Γ (emptyrecᵢ A t) = dec⇉-emptyrec ⊢Γ A t

  -- Decidability of bi-directional type checking

  dec⇇ :  Γ  Checkable t  Γ  A  Dec (Γ  t  A)
  dec⇇ ⊢Γ (lamᶜ {p = p′} t) ⊢A = case isΠ ⊢A of λ where
    (yes (F , G , p , q , ⊢F , ⊢G , A⇒Π))  case dec⇇ (⊢Γ  ⊢F) t ⊢G of λ where
      (yes t⇇G)  case p  p′ of λ where
        (yes PE.refl)  yes (lamᶜ (A⇒Π , ΠΣₙ) t⇇G)
        (no p≢p′)  no λ where
          (lamᶜ x x₁)  case whrDet* (A⇒Π , ΠΣₙ) x of λ where
            PE.refl  p≢p′ PE.refl
      (no ¬t⇇G)  no λ where
        (lamᶜ x x₁)  case whrDet* (A⇒Π , ΠΣₙ) x of λ where
          PE.refl  ¬t⇇G x₁
    (no ¬isΠ)  no λ where
      (lamᶜ x x₁) 
        let _ , ⊢Π = syntacticRed (proj₁ x)
            ⊢F , ⊢G = syntacticΠ ⊢Π
        in  ¬isΠ (_ , _ , _ , _ , ⊢F , ⊢G , proj₁ x)
  dec⇇ ⊢Γ (prodᶜ {p = p′} {m = m′} t u) ⊢A = case isΣ ⊢A of λ where
    (yes (F , G , m , p , q , ⊢F , ⊢G , A⇒Σ))  case dec⇇ ⊢Γ t ⊢F of λ where
      (yes t⇇F)  case dec⇇ ⊢Γ u (substType ⊢G (soundness⇇ ⊢Γ t⇇F)) of λ where
        (yes u⇇Gₜ)  case p  p′ of λ where
          (yes PE.refl)  case decSigmaMode m m′ of λ where
            (yes PE.refl)  yes (prodᶜ (A⇒Σ , ΠΣₙ) t⇇F u⇇Gₜ)
            (no m≢m′)  no λ where
              (prodᶜ x x₁ x₂) 
                let Σ≡Σ′ = whrDet* (A⇒Σ , ΠΣₙ) x
                    _ , _ , W≡W′ = B-PE-injectivity BΣ! BΣ! Σ≡Σ′
                    _ , _ , m≡m′ = BΣ-PE-injectivity W≡W′
                in  m≢m′ m≡m′
          (no p≢p′)  no λ where
            (prodᶜ x x₁ x₂)  case whrDet* (A⇒Σ , ΠΣₙ) x of λ where
              PE.refl  p≢p′ PE.refl
        (no ¬u⇇Gₜ)  no λ where
          (prodᶜ x x₁ x₂)  case whrDet* (A⇒Σ , ΠΣₙ) x of λ where
            PE.refl  ¬u⇇Gₜ x₂
      (no ¬t⇇F)  no λ where
        (prodᶜ x x₁ x₂)  case whrDet* (A⇒Σ , ΠΣₙ) x of λ where
          PE.refl  ¬t⇇F x₁
    (no ¬isΣ)  no λ where
      (prodᶜ x x₁ x₂) 
        let _ , ⊢Σ = syntacticRed (proj₁ x)
            ⊢F , ⊢G = syntacticΣ ⊢Σ
        in  ¬isΣ (_ , _ , _ , _ , _ , ⊢F , ⊢G , proj₁ x)
  dec⇇ ⊢Γ (infᶜ t) ⊢A = case dec⇉ ⊢Γ t of λ where
    (yes (B , t⇉B))  case decEq (proj₁ (soundness⇉ ⊢Γ t⇉B)) ⊢A of λ where
      (yes B≡A)  yes (infᶜ t⇉B B≡A)
      (no B≢A)  no λ where
        (infᶜ x x₁)  case deterministic⇉ t⇉B x of λ where
          PE.refl  B≢A x₁
    (no ¬t⇉B)  no λ where
      (infᶜ x x₁)  ¬t⇉B (_ , x)