module Quox.Equal

import Quox.BoolExtra
import public Quox.Typing
import Data.Maybe
import Quox.EffExtra

%default total


public export
EqModeState : Type -> Type
EqModeState = State EqMode

public export
Equal : Type -> Type
Equal = Eff [ErrorEff, DefsReader, NameGen]

public export
Equal_ : Type -> Type
Equal_ = Eff [ErrorEff, NameGen, EqModeState]

export
runEqualWith_ : EqMode -> NameSuf -> Equal_ a -> (Either Error a, NameSuf)
runEqualWith_ mode suf act =
  extract $
  runNameGenWith suf $
  runExcept $
  evalState mode act

export
runEqual_ : EqMode -> Equal_ a -> Either Error a
runEqual_ mode act = fst $ runEqualWith_ mode 0 act


export
runEqualWith : NameSuf -> Definitions -> Equal a -> (Either Error a, NameSuf)
runEqualWith suf defs act =
  extract $
  runStateAt GEN suf $
  runReaderAt DEFS defs $
  runExcept act

export
runEqual : Definitions -> Equal a -> Either Error a
runEqual defs act = fst $ runEqualWith 0 defs act


export %inline
mode : Has EqModeState fs => Eff fs EqMode
mode = get


parameters (loc : Loc) (ctx : EqContext n)
  private %inline
  clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal_ a
  clashT ty s t = throw $ ClashT loc ctx !mode ty s t

  private %inline
  clashTy : Term 0 n -> Term 0 n -> Equal_ a
  clashTy s t = throw $ ClashTy loc ctx !mode s t

  private %inline
  clashE : Elim 0 n -> Elim 0 n -> Equal_ a
  clashE e f = throw $ ClashE loc ctx !mode e f

  private %inline
  wrongType : Term 0 n -> Term 0 n -> Equal_ a
  wrongType ty s = throw $ WrongType loc ctx ty s


public export %inline
sameTyCon : (s, t : Term d n) ->
            (0 ts : So (isTyConE s)) => (0 tt : So (isTyConE t)) =>
            Bool
sameTyCon (TYPE {}) (TYPE {}) = True
sameTyCon (TYPE {}) _         = False
sameTyCon (Pi   {}) (Pi   {}) = True
sameTyCon (Pi   {}) _         = False
sameTyCon (Sig  {}) (Sig  {}) = True
sameTyCon (Sig  {}) _         = False
sameTyCon (W    {}) (W    {}) = True
sameTyCon (W    {}) _         = False
sameTyCon (Enum {}) (Enum {}) = True
sameTyCon (Enum {}) _         = False
sameTyCon (Eq   {}) (Eq   {}) = True
sameTyCon (Eq   {}) _         = False
sameTyCon (Nat  {}) (Nat  {}) = True
sameTyCon (Nat  {}) _         = False
sameTyCon (BOX  {}) (BOX  {}) = True
sameTyCon (BOX  {}) _         = False
sameTyCon (E    {}) (E    {}) = True
sameTyCon (E    {}) _         = False


||| true if a type is known to be a subsingleton purely by its form.
||| a subsingleton is a type with only zero or one possible values.
||| equality/subtyping accepts immediately on values of subsingleton types.
|||
||| * a function type is a subsingleton if its codomain is.
||| * a pair type is a subsingleton if both its elements are.
||| * equality types are subsingletons because of uip.
||| * an enum type is a subsingleton if it has zero or one tags.
||| * a box type is a subsingleton if its content is
public export covering
isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n -> Equal_ Bool
isSubSing defs ctx ty0 = do
  Element ty0 nc <- whnf defs ctx ty0.loc ty0
  case ty0 of
    TYPE {} => pure False
    Pi {arg, res, _} =>
      isSubSing defs (extendTy Zero res.name arg ctx) res.term
    Sig {fst, snd, _} =>
      isSubSing defs ctx fst `andM`
      isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
    W {} => pure False
    Enum {cases, _} =>
      pure $ length (SortedSet.toList cases) <= 1
    Eq {} => pure True
    Nat {} => pure False
    BOX {ty, _} => isSubSing defs ctx ty
    E (Ann {tm, _}) => isSubSing defs ctx tm
    E _ => pure False
    Lam  {} => pure False
    Pair {} => pure False
    Sup  {} => pure False
    Tag  {} => pure False
    DLam {} => pure False
    Zero {} => pure False
    Succ {} => pure False
    Box  {} => pure False


export
ensureTyCon : Has ErrorEff fs =>
              (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
              Eff fs (So (isTyConE t))
ensureTyCon loc ctx t = case nchoose $ isTyConE t of
  Left  y => pure y
  Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen)

||| performs the minimum work required to recompute the type of an elim.
|||
||| ⚠ **assumes the elim is already typechecked.** ⚠
private covering
computeElimTypeE : (defs : Definitions) -> EqContext n ->
                   (e : Elim 0 n) -> (0 ne : NotRedex defs e) =>
                   Equal_ (Term 0 n)
computeElimTypeE defs ectx e =
  let Val n = ectx.termLen in
  lift $ computeElimType defs (toWhnfContext ectx) e

parameters (defs : Definitions)
  mutual
    namespace Term
      ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
      ||| the current variance `mode`.
      |||
      ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
      export covering %inline
      compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Equal_ ()
      compare0 ctx ty s t =
        wrapErr (WhileComparingT ctx !mode ty s t) $ do
          let Val n = ctx.termLen
          Element ty' _ <- whnf defs ctx ty.loc ty
          Element s'  _ <- whnf defs ctx s.loc  s
          Element t'  _ <- whnf defs ctx t.loc  t
          tty <- ensureTyCon ty.loc ctx ty'
          compare0' ctx ty' s' t'

      ||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
      ||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
      private %inline
      toLamBody : Elim d n -> Term d (S n)
      toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc

      private covering
      compare0' : EqContext n ->
                  (ty, s, t : Term 0 n) ->
                  (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
                  (0 _ : NotRedex defs s)  => (0 _ : NotRedex defs t) =>
                  Equal_ ()
      compare0' ctx (TYPE {}) s t = compareType ctx s t

      compare0' ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $
        case (s, t) of
          --           Γ, x : A ⊢ s = t : B
          -- -------------------------------------------
          --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
          (Lam b1 {}, Lam b2 {}) =>
            compare0 ctx' res.term b1.term b2.term

          --       Γ, x : A ⊢ s = e x : B
          -- -----------------------------------
          --  Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
          (E e,      Lam b {}) => eta s.loc e b
          (Lam b {}, E e)      => eta s.loc e b

          (E e, E f) => Elim.compare0 ctx e f

          (Lam {}, t) => wrongType t.loc ctx ty t
          (E _,    t) => wrongType t.loc ctx ty t
          (s,      _) => wrongType s.loc ctx ty s
        where
          ctx' : EqContext (S n)
          ctx' = extendTy qty res.name arg ctx

          eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Equal_ ()
          eta _   e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
          eta loc e (S _ (N _)) = clashT loc ctx ty s t

      compare0' ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
        case (s, t) of
          --  Γ ⊢ s₁ = t₁ : A     Γ ⊢ s₂ = t₂ : B{s₁/x}
          -- --------------------------------------------
          --    Γ ⊢ (s₁, t₁) = (s₂, t₂) : (x : A) × B
          --
          -- [todo] η for π ≰ 1 maybe
          (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
            compare0 ctx fst sFst tFst
            compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd

          (E e, E f) => Elim.compare0 ctx e f

          (Pair {}, E _)     => clashT s.loc ctx ty s t
          (E _,     Pair {}) => clashT s.loc ctx ty s t

          (Pair {}, t) => wrongType t.loc ctx ty t
          (E _,     t) => wrongType t.loc ctx ty t
          (s,       _) => wrongType s.loc ctx ty s

      compare0' ctx ty@(W {shape, body, _}) s t =
        case (s, t) of
          --           Γ ⊢ s₁ = t₁ : A
          --  Γ ⊢ s₂ = t₂ : 1.B[s₁∷A/x] → (x : A) ⊲ B
          -- -----------------------------------------
          --     Γ ⊢ s₁⋄s₂ = t₁⋄t₂ : (x : A) ⊲ B
          (Sup sRoot sSub {}, Sup tRoot tSub {}) => do
            compare0 ctx shape sRoot tRoot
            let arg   = sub1 body (Ann sRoot shape sRoot.loc)
                subTy = Arr One arg ty ty.loc
            compare0 ctx subTy sSub tSub

          (E e, E f) => Elim.compare0 ctx e f

          (Sup {}, E   {}) => clashT s.loc ctx ty s t
          (E   {}, Sup {}) => clashT s.loc ctx ty s t

          (Sup {}, t) => wrongType t.loc ctx ty t
          (E   {}, t) => wrongType t.loc ctx ty t
          (s,      _) => wrongType s.loc ctx ty s

      compare0' ctx ty@(Enum {}) s t = local_ Equal $
        case (s, t) of
          -- --------------------
          --  Γ ⊢ `t = `t : {ts}
          --
          -- t ∈ ts is in the typechecker, not here, ofc
          (Tag t1 {}, Tag t2 {}) =>
            unless (t1 == t2) $ clashT s.loc ctx ty s t
          (E e, E f) => Elim.compare0 ctx e f

          (Tag {}, E _)    => clashT s.loc ctx ty s t
          (E _,    Tag {}) => clashT s.loc ctx ty s t

          (Tag {}, t) => wrongType t.loc ctx ty t
          (E _,    t) => wrongType t.loc ctx ty t
          (s,      _) => wrongType s.loc ctx ty s

      compare0' _ (Eq {}) _ _ =
        -- ✨ uip ✨
        --
        -- ----------------------------
        --  Γ ⊢ e = f : Eq [i ⇒ A] s t
        pure ()

      compare0' ctx nat@(Nat {}) s t = local_ Equal $
        case (s, t) of
          -- ---------------
          --  Γ ⊢ 0 = 0 : ℕ
          (Zero {}, Zero {}) => pure ()

          --      Γ ⊢ s = t : ℕ
          -- -------------------------
          --  Γ ⊢ succ s = succ t : ℕ
          (Succ s' {}, Succ t' {}) => compare0 ctx nat s' t'

          (E e, E f) => Elim.compare0 ctx e f

          (Zero {}, Succ {}) => clashT s.loc ctx nat s t
          (Zero {}, E _)     => clashT s.loc ctx nat s t
          (Succ {}, Zero {}) => clashT s.loc ctx nat s t
          (Succ {}, E _)     => clashT s.loc ctx nat s t
          (E _,     Zero {}) => clashT s.loc ctx nat s t
          (E _,     Succ {}) => clashT s.loc ctx nat s t

          (Zero {}, t) => wrongType t.loc ctx nat t
          (Succ {}, t) => wrongType t.loc ctx nat t
          (E _,     t) => wrongType t.loc ctx nat t
          (s,       _) => wrongType s.loc ctx nat s

      compare0' ctx ty@(BOX q ty' {}) s t = local_ Equal $
        case (s, t) of
          --     Γ ⊢ s = t : A
          -- -----------------------
          --  Γ ⊢ [s] = [t] : [π.A]
          (Box s' {}, Box t' {}) => compare0 ctx ty' s' t'

          (E e, E f) => Elim.compare0 ctx e f

          (Box {}, t) => wrongType t.loc ctx ty t
          (E   _,  t) => wrongType t.loc ctx ty t
          (s,      _) => wrongType s.loc ctx ty s

      compare0' ctx ty@(E _) s t = do
        -- a neutral type can only be inhabited by neutral values
        -- e.g. an abstract value in an abstract type, bound variables, …
        let E e = s | _ => wrongType s.loc ctx ty s
            E f = t | _ => wrongType t.loc ctx ty t
        Elim.compare0 ctx e f

    ||| compares two types, using the current variance `mode` for universes.
    ||| fails if they are not types, even if they would happen to be equal.
    export covering %inline
    compareType : EqContext n -> (s, t : Term 0 n) -> Equal_ ()
    compareType ctx s t = do
      let Val n = ctx.termLen
      Element s' _ <- whnf defs ctx s.loc s
      Element t' _ <- whnf defs ctx t.loc t
      ts <- ensureTyCon s.loc ctx s'
      tt <- ensureTyCon t.loc ctx t'
      st <- either pure (const $ clashTy s.loc ctx s' t') $
            nchoose $ sameTyCon s' t'
      compareType' ctx s' t'

    private covering
    compareType' : EqContext n -> (s, t : Term 0 n) ->
                   (0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
                   (0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
                   (0 _ : So (sameTyCon s t)) =>
                   Equal_ ()
    -- equality is the same as subtyping, except with the
    -- "≤" in the TYPE rule being replaced with "="
    compareType' ctx a@(TYPE k {}) (TYPE l {}) =
      --        𝓀 ≤ ℓ
      -- ----------------------
      --  Γ ⊢ Type 𝓀 <: Type ℓ
      expectModeU a.loc !mode k l

    compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
                     (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
      --   Γ ⊢ A₁ :> A₂    Γ, x : A₁ ⊢ B₁ <: B₂
      -- ----------------------------------------
      --  Γ ⊢ π.(x : A₁) → B₁ <: π.(x : A₂) → B₂
      --
      -- no quantity subtyping since that would need a runtime coercion
      -- e.g. if ⌊0.A → B⌋ ⇝ ⌊B⌋, then the promotion to ω.A → B would need
      -- to re-add the abstraction
      expectEqualQ loc sQty tQty
      local flip $ compareType ctx sArg tArg -- contra
      compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term

    compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
                     (Sig {fst = tFst, snd = tSnd, _}) = do
      --  Γ ⊢ A₁ <: A₂    Γ, x : A₁ ⊢ B₁ <: B₂
      -- --------------------------------------
      --   Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
      compareType ctx sFst tFst
      compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term

    compareType' ctx (W {shape = sShape, body = sBody, loc})
                     (W {shape = tShape, body = tBody, _}) = do
      --  Γ ⊢ A₁ <: A₂    Γ, x : A₁ ⊢ B₁ <: B₂
      -- --------------------------------------
      --   Γ ⊢ (x : A₁) ⊲ B₁ <: (x : A₂) ⊲ B₂
      compareType ctx sShape tShape
      compareType (extendTy Zero sBody.name sShape ctx) sBody.term tBody.term

    compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
                     (Eq {ty = tTy, l = tl, r = tr, _}) = do
      --            Γ ⊢ A₁‹ε/i› <: A₂‹ε/i›
      --  Γ ⊢ l₁ = l₂ : A₁‹0/i›    Γ ⊢ r₁ = r₂ : A₁‹1/i›
      -- ------------------------------------------------
      --    Γ ⊢ Eq (i ⇒ A₁) l₁ r₂ <: Eq (i ⇒ A₂) l₂ r₂
      compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
      compareType (extendDim sTy.name One  ctx) sTy.one  tTy.one
      let ty = case !mode of Super => sTy; _ => tTy
      local_ Equal $ do
        Term.compare0 ctx ty.zero sl tl
        Term.compare0 ctx ty.one  sr tr

    compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
      -- ------------------
      --  Γ ⊢ {ts} <: {ts}
      --
      -- no subtyping based on tag subsets, since that would need
      -- a runtime coercion
      unless (tags1 == tags2) $ clashTy s.loc ctx s t

    compareType' ctx (Nat {}) (Nat {}) =
      -- ------------
      --  Γ ⊢ ℕ <: ℕ
      pure ()

    compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
      --     Γ ⊢ A <: B
      -- --------------------
      --  Γ ⊢ [π.A] <: [π.B]
      expectEqualQ loc pi rh
      compareType ctx a b

    compareType' ctx (E e) (E f) = do
      -- no fanciness needed here cos anything other than a neutral
      -- has been inlined by whnf
      Elim.compare0 ctx e f


    namespace Elim
      -- [fixme] the following code ends up repeating a lot of work in the
      -- computeElimType calls. the results should be shared better

      ||| compare two eliminations according to the given variance `mode`.
      |||
      ||| ⚠ **assumes that they have both been typechecked, and have
      ||| equal types.** ⚠
      export covering %inline
      compare0 : EqContext n -> (e, f : Elim 0 n) -> Equal_ ()
      compare0 ctx e f =
        wrapErr (WhileComparingE ctx !mode e f) $ do
          let Val n = ctx.termLen
          Element e' ne <- whnf defs ctx e.loc e
          Element f' nf <- whnf defs ctx f.loc f
          unless !(isSubSing defs ctx =<< computeElimTypeE defs ctx e') $
            compare0' ctx e' f' ne nf

      private covering
      compare0' : EqContext n ->
                  (e, f : Elim 0 n) ->
                  (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
                  Equal_ ()

      compare0' ctx e@(F x u _) f@(F y v _) _ _ =
        unless (x == y && u == v) $ clashE e.loc ctx e f
      compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f

      compare0' ctx e@(B i _) f@(B j _) _ _ =
        unless (i == j) $ clashE e.loc ctx e f
      compare0' ctx e@(B {}) f _ _ = clashE e.loc ctx e f

      --  Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
      --  Ψ | Γ ⊢ s = t ⇐ A
      -- -------------------------------
      --  Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
      compare0' ctx (App e s eloc) (App f t floc) ne nf =
        local_ Equal $ do
          compare0 ctx e f
          (_, arg, _) <- expectPi defs ctx eloc =<<
                         computeElimTypeE defs ctx e @{noOr1 ne}
          Term.compare0 ctx arg s t
      compare0' ctx e@(App {}) f _ _ = clashE e.loc ctx e f

      --  Ψ | Γ ⊢ e = f ⇒ (x : A) × B
      --  Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R
      --  Ψ | Γ, x : A, y : B ⊢ s = t ⇐ Q[((x, y) ∷ (x : A) × B)/p]
      -- -----------------------------------------------------------
      --    Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s }
      --          = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p]
      compare0' ctx (CasePair epi e eret ebody eloc)
                    (CasePair fpi f fret fbody {}) ne nf =
        local_ Equal $ do
          compare0 ctx e f
          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
          (fst, snd) <- expectSig defs ctx eloc ety
          let [< x, y] = ebody.names
          Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
                        (substCasePairRet ebody.names ety eret)
                        ebody.term fbody.term
          expectEqualQ e.loc epi fpi
      compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f

      --  Ψ | Γ ⊢ e = f ⇒ (x : A) ⊲ B
      --  Ψ | Γ, p : (x : A) ⊲ B ⊢ Q = R ⇐ Type
      --  Ψ | Γ, x : A, y : 1.B → (x : A) ⊲ B, ih : 1.(z : B) → Q[y z/p]
      --    ⊢ s = t ⇐ Q[(x⋄y ∷ (x : A) ⊲ B)/p]
      -- ----------------------------------------------------------------
      --  Ψ | Γ ⊢ caseπ e return Q of { x ⋄ y, ς.ih ⇒ s }
      --        = caseπ f return R of { x ⋄ y, ς.ih ⇒ t } ⇒ Q[e/p]
      compare0' ctx (CaseW epi epi' e eret ebody eloc)
                    (CaseW fpi fpi' f fret fbody floc) ne nf =
        local_ Equal $ do
          compare0 ctx e f
          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
          (shape, tbody) <- expectW defs ctx eloc ety
          let [< x, y, ih] = ebody.names
          z <- mnb "z" ih.loc
          let xbind = (epi, x, shape)
              ybind = (epi, y, Arr One tbody.term (weakT 1 ety) y.loc)
              ihbind = (epi', ih,
                PiY One z
                  (sub1 (weakS 2 tbody) (BV 1 x.loc))
                  (sub1 (weakS 3 eret) (App (BV 1 y.loc) (BVT 0 z.loc) ih.loc))
                  ih.loc)
              ctx' = extendTyN [< xbind, ybind, ihbind] ctx
          Term.compare0 ctx' (substCaseWRet ebody.names ety eret)
            ebody.term fbody.term
          expectEqualQ e.loc epi  fpi
          expectEqualQ e.loc epi' fpi'
      compare0' ctx e@(CaseW {}) f _ _ = clashE e.loc ctx e f

      --  Ψ | Γ ⊢ e = f ⇒ {𝐚s}
      --  Ψ | Γ, x : {𝐚s} ⊢ Q = R
      --  Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
      -- --------------------------------------------------
      --  Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ }
      --        = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
      compare0' ctx (CaseEnum epi e eret earms eloc)
                    (CaseEnum fpi f fret farms floc) ne nf =
        local_ Equal $ do
          compare0 ctx e f
          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
          for_ !(expectEnum defs ctx eloc ety) $ \t => do
            l <- lookupArm eloc t earms
            r <- lookupArm floc t farms
            compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
          expectEqualQ eloc epi fpi
        where
          lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n)
          lookupArm loc t arms = case lookup t arms of
            Just arm => pure arm
            Nothing  => throw $ TagNotIn loc t (fromList $ keys arms)
      compare0' ctx e@(CaseEnum {}) f _ _ = clashE e.loc ctx e f

      --  Ψ | Γ ⊢ e = f ⇒ ℕ
      --  Ψ | Γ, x : ℕ ⊢ Q = R
      --  Ψ | Γ ⊢ s₀ = t₀ ⇐ Q[(0 ∷ ℕ)/x]
      --  Ψ | Γ, x : ℕ, y : Q ⊢ s₁ = t₁ ⇐ Q[(succ x ∷ ℕ)/x]
      -- -----------------------------------------------------
      --  Ψ | Γ ⊢ caseπ e return Q of { 0 ⇒ s₀; x, π.y ⇒ s₁ }
      --        = caseπ f return R of { 0 ⇒ t₀; x, π.y ⇒ t₁ }
      --        ⇒ Q[e/x]
      compare0' ctx (CaseNat epi epi' e eret ezer esuc eloc)
                    (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
        local_ Equal $ do
          compare0 ctx e f
          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
          compare0 ctx
            (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
            ezer fzer
          let [< p, ih] = esuc.names
          compare0
            (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
            (substCaseSuccRet esuc.names eret) esuc.term fsuc.term
          expectEqualQ e.loc epi  fpi
          expectEqualQ e.loc epi' fpi'
      compare0' ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f

      --  Ψ | Γ ⊢ e = f ⇒ [ρ. A]
      --  Ψ | Γ, x : [ρ. A] ⊢ Q = R
      --  Ψ | Γ, x : A ⊢ s = t ⇐ Q[([x] ∷ [ρ. A])/x]
      -- --------------------------------------------------
      --  Ψ | Γ ⊢ caseπ e return Q of { [x] ⇒ s }
      --        = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x]
      compare0' ctx (CaseBox epi e eret ebody eloc)
                    (CaseBox fpi f fret fbody floc) ne nf =
        local_ Equal $ do
          compare0 ctx e f
          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
          (q, ty) <- expectBOX defs ctx eloc ety
          compare0 (extendTy (epi * q) ebody.name ty ctx)
            (substCaseBoxRet ebody.name ety eret)
            ebody.term fbody.term
          expectEqualQ eloc epi fpi
      compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f

      -- all dim apps replaced with ends by whnf
      compare0' _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
      compare0' _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf

      --  Ψ | Γ ⊢ s <: t : B
      -- --------------------------------
      --  Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
      --
      -- and similar for :> and A
      compare0' ctx (Ann s a _) (Ann t b _) _ _ =
        let ty = case !mode of Super => a; _ => b in
        Term.compare0 ctx ty s t

      --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
      --  Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
      --  Ψ | Γ ⊢ e <: f ⇒ _
      --    (non-neutral forms have the coercion already pushed in)
      -- -----------------------------------------------------------
      --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e
      --       <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ B‹q₂/𝑖›
      compare0' ctx (Coe ty1 p1 q1 (E val1) _)
                    (Coe ty2 p2 q2 (E val2) _) ne nf = do
        compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
        compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
        compare0 ctx val1 val2
      compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f

      -- (no neutral compositions in a closed dctx)
      compare0' _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne
      compare0' _ (Comp {r = B i _, _}) _ _ _ = absurd i
      compare0' _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf

      -- (type case equality purely structural)
      compare0' ctx (TypeCase ty1 ret1 arms1 def1 eloc)
                    (TypeCase ty2 ret2 arms2 def2 floc) ne _ =
        local_ Equal $ do
          compare0 ctx ty1 ty2
          u <- expectTYPE defs ctx eloc =<<
               computeElimTypeE defs ctx ty1 @{noOr1 ne}
          compareType ctx ret1 ret2
          compareType ctx def1 def2
          for_ allKinds $ \k =>
            compareArm ctx k ret1 u
              (lookupPrecise k arms1) (lookupPrecise k arms2) def1
      compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f

      --     Ψ | Γ ⊢ s <: f ⇐ A
      -- --------------------------
      --  Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
      --
      -- and vice versa
      compare0' ctx (Ann s a _) f           _ _ = Term.compare0 ctx a s (E f)
      compare0' ctx e           (Ann t b _) _ _ = Term.compare0 ctx b (E e) t
      compare0' ctx e@(Ann {})  f           _ _ = clashE e.loc ctx e f

      ||| compare two type-case branches, which came from the arms of the given
      ||| kind. `ret` is the return type of the case expression, and `u` is the
      ||| universe the head is in.
      private covering
      compareArm : EqContext n -> (k : TyConKind) ->
                   (ret : Term 0 n) -> (u : Universe) ->
                   (b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
                   (def : Term 0 n) ->
                   Equal_ ()
      compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
      compareArm ctx k ret u b1 b2 def =
        let def = SN def in
        compareArm_ ctx k ret u (fromMaybe def b1) (fromMaybe def b2)

      private covering
      compareArm_ : EqContext n -> (k : TyConKind) ->
                    (ret : Term 0 n) -> (u : Universe) ->
                    (b1, b2 : TypeCaseArmBody k 0 n) ->
                    Equal_ ()
      compareArm_ ctx KTYPE ret u b1 b2 =
        compare0 ctx ret b1.term b2.term

      compareArm_ ctx KPi ret u b1 b2 = do
        let [< a, b] = b1.names
            ctx = extendTyN
              [< (Zero, a, TYPE u a.loc),
                 (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
        compare0 ctx (weakT 2 ret) b1.term b2.term

      compareArm_ ctx KSig ret u b1 b2 = do
        let [< a, b] = b1.names
            ctx = extendTyN
              [< (Zero, a, TYPE u a.loc),
                 (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
        compare0 ctx (weakT 2 ret) b1.term b2.term

      compareArm_ ctx KW ret u b1 b2 = do
        let [< a, b] = b1.names
            ctx = extendTyN
              [< (Zero, a, TYPE u a.loc),
                 (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
        compare0 ctx (weakT 2 ret) b1.term b2.term

      compareArm_ ctx KEnum ret u b1 b2 =
        compare0 ctx ret b1.term b2.term

      compareArm_ ctx KEq ret u b1 b2 = do
        let [< a0, a1, a, l, r] = b1.names
            ctx = extendTyN
              [< (Zero, a0, TYPE u a0.loc),
                 (Zero, a1, TYPE u a1.loc),
                 (Zero, a,  Eq0 (TYPE u a.loc)
                                (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc),
                 (Zero, l,  BVT 2 a0.loc),
                 (Zero, r,  BVT 2 a1.loc)] ctx
        compare0 ctx (weakT 5 ret) b1.term b2.term

      compareArm_ ctx KNat ret u b1 b2 =
        compare0 ctx ret b1.term b2.term

      compareArm_ ctx KBOX ret u b1 b2 = do
        let ctx = extendTy Zero b1.name (TYPE u b1.name.loc) ctx
        compare0 ctx (weakT 1 ret) b1.term b1.term


parameters (loc : Loc) (ctx : TyContext d n)
  -- [todo] only split on the dvars that are actually used anywhere in
  -- the calls to `splits`

  parameters (mode : EqMode)
    private
    fromEqual_ : Equal_ a -> Equal a
    fromEqual_ act = lift $ evalState mode act

    private
    eachFace : Applicative f => (EqContext n -> DSubst d 0 -> f ()) -> f ()
    eachFace act =
      for_ (splits loc ctx.dctx) $ \th => act (makeEqContext ctx th) th

    private
    runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) ->
                 Equal ()
    runCompare act = fromEqual_ $ eachFace $ act !(askAt DEFS)

    namespace Term
      export covering
      compare : (ty, s, t : Term d n) -> Equal ()
      compare ty s t = runCompare $ \defs, ectx, th =>
        compare0 defs ectx (ty // th) (s // th) (t // th)

      export covering
      compareType : (s, t : Term d n) -> Equal ()
      compareType s t = runCompare $ \defs, ectx, th =>
        compareType defs ectx (s // th) (t // th)

    namespace Elim
      ||| you don't have to pass the type in but the arguments must still be
      ||| of the same type!!
      export covering
      compare : (e, f : Elim d n) -> Equal ()
      compare e f = runCompare $ \defs, ectx, th =>
        compare0 defs ectx (e // th) (f // th)

  namespace Term
    export covering %inline
    equal, sub, super : (ty, s, t : Term d n) -> Equal ()
    equal = compare Equal
    sub   = compare Sub
    super = compare Super

    export covering %inline
    equalType, subtype, supertype : (s, t : Term d n) -> Equal ()
    equalType = compareType Equal
    subtype   = compareType Sub
    supertype = compareType Super

  namespace Elim
    export covering %inline
    equal, sub, super : (e, f : Elim d n) -> Equal ()
    equal = compare Equal
    sub   = compare Sub
    super = compare Super