module Quox.Equal

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

%default total


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

public export
Equal : List (Type -> Type)
Equal = [ErrorEff, DefsReader, NameGen]

public export
EqualInner : List (Type -> Type)
EqualInner = [ErrorEff, NameGen, EqModeState]


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 -> Eff EqualInner a
  clashT ty s t = throw $ ClashT loc ctx !mode ty s t

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

  private %inline
  wrongType : Term 0 n -> Term 0 n -> Eff EqualInner 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 (IOState {}) (IOState {}) = True
sameTyCon (IOState {}) _            = False
sameTyCon (Pi      {}) (Pi      {}) = True
sameTyCon (Pi      {}) _            = False
sameTyCon (Sig     {}) (Sig     {}) = True
sameTyCon (Sig     {}) _            = False
sameTyCon (Enum    {}) (Enum    {}) = True
sameTyCon (Enum    {}) _            = False
sameTyCon (Eq      {}) (Eq      {}) = True
sameTyCon (Eq      {}) _            = False
sameTyCon (NAT     {}) (NAT     {}) = True
sameTyCon (NAT     {}) _            = False
sameTyCon (STRING  {}) (STRING  {}) = True
sameTyCon (STRING  {}) _            = False
sameTyCon (BOX     {}) (BOX     {}) = True
sameTyCon (BOX     {}) _            = False
sameTyCon (E       {}) (E       {}) = True
sameTyCon (E       {}) _            = False


||| true if a type is known to be empty.
|||
||| * a pair is empty if either element is.
||| * `{}` is empty.
||| * `[π.A]` is empty if `A` is.
||| * that's it.
public export covering
isEmpty : Definitions -> EqContext n -> SQty -> Term 0 n ->
          Eff EqualInner Bool
isEmpty defs ctx sg ty0 = do
  Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
  let Left  y = choose $ isTyConE ty0
    | Right n => pure False
  case ty0 of
    TYPE {} => pure False
    IOState {} => pure False
    Pi {arg, res, _} => pure False
    Sig {fst, snd, _} =>
      isEmpty defs ctx sg fst `orM`
      isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term
    Enum {cases, _} =>
      pure $ null cases
    Eq {} => pure False
    NAT {} => pure False
    STRING {} => pure False
    BOX {ty, _} => isEmpty defs ctx sg ty
    E _ => pure 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,
|||   or if its domain is empty.
||| * 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 : Definitions -> EqContext n -> SQty -> Term 0 n ->
            Eff EqualInner Bool
isSubSing defs ctx sg ty0 = do
  Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
  let Left  y = choose $ isTyConE ty0
    | Right n => pure False
  case ty0 of
    TYPE {} => pure False
    IOState {} => pure False
    Pi {arg, res, _} =>
      isEmpty defs ctx sg arg `orM`
      isSubSing defs (extendTy0 res.name arg ctx) sg res.term
    Sig {fst, snd, _} =>
      isSubSing defs ctx sg fst `andM`
      isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term
    Enum {cases, _} =>
      pure $ length (SortedSet.toList cases) <= 1
    Eq {} => pure True
    NAT {} => pure False
    STRING {} => pure False
    BOX {ty, _} => isSubSing defs ctx sg ty
    E _ => pure False


||| the left argument if the current mode is `Super`; otherwise the right one.
private %inline
bigger : Has EqModeState fs => (left, right : Lazy a) -> Eff fs a
bigger l r = gets $ \case Super => l; _ => r


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)


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 : Definitions -> EqContext n -> SQty -> (ty, s, t : Term 0 n) ->
             Eff EqualInner ()

namespace Elim
  ||| compare two eliminations according to the given variance `mode`.
  |||
  ||| ⚠ **assumes that they have both been typechecked, and have
  ||| equal types.** ⚠
  export covering %inline
  compare0 : Definitions -> EqContext n -> SQty -> (e, f : Elim 0 n) ->
             Eff EqualInner (Term 0 n)

||| 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 : Definitions -> EqContext n -> (s, t : Term 0 n) ->
              Eff EqualInner ()


namespace Term
  private covering
  compare0' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
              (ty, s, t : Term 0 n) ->
              (0 _ : NotRedex defs SZero ty) => (0 _ : So (isTyConE ty)) =>
              (0 _ : NotRedex defs sg    s)  => (0 _ : NotRedex defs sg t) =>
              Eff EqualInner ()
  compare0' defs ctx sg (TYPE {}) s t = compareType defs ctx s t

  compare0' defs ctx sg ty@(IOState {}) s t =
    --   Γ ⊢ e = f ⇒ IOState
    -- ----------------------
    --   Γ ⊢ e = f ⇐ IOState
    --
    -- (no canonical values, ofc)
    case (s, t) of
      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
      (E _, _)   => wrongType t.loc ctx ty t
      _          => wrongType s.loc ctx ty s

  compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
    --              Γ ⊢ A empty
    -- -------------------------------------------
    --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
    if !(isEmpty defs ctx sg arg) then pure () else
    case (s, t) of
      --           Γ, x : A ⊢ s = t ⇐ B
      -- -------------------------------------------
      --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
      (Lam b1 {}, Lam b2 {}) =>
        compare0 defs ctx' sg 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) => ignore $ Elim.compare0 defs ctx sg 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

    toLamBody : Elim d n -> Term d (S n)
    toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc

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

  compare0' defs ctx sg 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 π ≥ 0 maybe
      (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
        compare0 defs ctx sg fst sFst tFst
        compare0 defs ctx sg (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd

      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f

      (E e,            Pair fst snd _) => eta s.loc e fst snd
      (Pair fst snd _, E f)            => eta s.loc f fst snd

      (Pair {}, t) => wrongType t.loc ctx ty t
      (E _,     t) => wrongType t.loc ctx ty t
      (s,       _) => wrongType s.loc ctx ty s
  where
    eta : Loc -> Elim 0 n -> Term 0 n -> Term 0 n -> Eff EqualInner ()
    eta loc e s t =
      case sg of
        SZero => do
          compare0 defs ctx sg fst                          (E $ Fst e e.loc) s
          compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
        SOne => clashT loc ctx ty s t

  compare0' defs ctx sg 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) => ignore $ Elim.compare0 defs ctx sg 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' defs ctx sg nat@(NAT {}) s t = local_ Equal $
    case (s, t) of
      -- ---------------
      --  Γ ⊢ n = n ⇐ ℕ
      (Nat x {}, Nat y {}) => unless (x == y) $ clashT s.loc ctx nat s t

      --      Γ ⊢ s = t ⇐ ℕ
      -- -------------------------
      --  Γ ⊢ succ s = succ t ⇐ ℕ
      (Succ s'   {}, Succ t'   {}) => compare0 defs ctx sg nat s' t'
      (Nat (S x) {}, Succ t'   {}) => compare0 defs ctx sg nat (Nat x s.loc) t'
      (Succ s'   {}, Nat (S y) {}) => compare0 defs ctx sg nat s' (Nat y t.loc)

      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f

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

      (Nat 0 {}, 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' defs ctx sg str@(STRING {}) s t = local_ Equal $
    case (s, t) of
      (Str x _, Str y _) => unless (x == y) $ clashT s.loc ctx str s t

      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f

      (Str {}, E _) => clashT s.loc ctx str s t
      (E _, Str {}) => clashT s.loc ctx str s t

      (Str {}, _) => wrongType t.loc ctx str t
      (E _,    _) => wrongType t.loc ctx str t
      _           => wrongType s.loc ctx str s

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

      --   Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
      -- -----------------------------------------------
      --            Γ ⊢ [s] = e ⇐ [ρ.A]
      (Box s loc, E f)       => eta s f
      (E e,       Box t loc) => eta t e

      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f

      (Box {}, _) => wrongType t.loc ctx bty t
      (E   _,  _) => wrongType t.loc ctx bty t
      _           => wrongType s.loc ctx bty s
  where
    eta : Term 0 n -> Elim 0 n -> Eff EqualInner ()
    eta s e = do
      nm <- mnb "inner" e.loc
      let e = CaseBox One e (SN ty) (SY [< nm] (BVT 0 nm.loc)) e.loc
      compare0 defs ctx sg ty s (E e)

  compare0' defs ctx sg 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
    ignore $ Elim.compare0 defs ctx sg e f


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

compareType' defs ctx a@(IOState {}) (IOState {}) =
  -- Γ ⊢ IOState <: IOState
  pure ()

compareType' defs 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₂
  expectEqualQ loc sQty tQty
  local flip $ compareType defs ctx sArg tArg -- contra
  compareType defs (extendTy0 sRes.name sArg ctx) sRes.term tRes.term

compareType' defs 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 defs ctx sFst tFst
  compareType defs (extendTy0 sSnd.name sFst ctx) sSnd.term tSnd.term

compareType' defs ctx (Eq {ty = sTy, l = sl, r = sr, _})
                      (Eq {ty = tTy, l = tl, r = tr, _}) = do
  --            Γ ⊢ A₁‹ε/i› <: A₂‹ε/i›
  --  Γ ⊢ l₁ = l₂ : A₁‹𝟎/i›    Γ ⊢ r₁ = r₂ : A₁‹𝟏/i›
  -- ------------------------------------------------
  --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
  compareType defs (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
  compareType defs (extendDim sTy.name One  ctx) sTy.one  tTy.one
  ty <- bigger sTy tTy
  local_ Equal $ do
    Term.compare0 defs ctx SZero ty.zero sl tl
    Term.compare0 defs ctx SZero ty.one  sr tr

compareType' defs 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' defs ctx (NAT {}) (NAT {}) =
  -- ------------
  --  Γ ⊢ ℕ <: ℕ
  pure ()

compareType' defs ctx (STRING {}) (STRING {}) =
  -- ------------
  --  Γ ⊢ String <: String
  pure ()

compareType' defs ctx (BOX pi a loc) (BOX rh b {}) = do
  expectEqualQ loc pi rh
  compareType defs ctx a b

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


private
lookupFree : Has ErrorEff fs =>
             Definitions -> EqContext n -> Name -> Universe -> Loc ->
             Eff fs (Term 0 n)
lookupFree defs ctx x u loc =
  case lookup x defs of
    Nothing => throw $ NotInScope loc x
    Just d  => pure $ d.typeWithAt [|Z|] ctx.termLen u


export
typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
              CtxExtension d n (arity k + n)
typecaseTel k xs u = case k of
  KTYPE => [<]
  KIOState => [<]
  -- A : ★ᵤ, B : 0.A → ★ᵤ
  KPi =>
    let [< a, b] = xs in
    [< (Zero, a, TYPE u a.loc),
       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
  KSig =>
    let [< a, b] = xs in
    [< (Zero, a, TYPE u a.loc),
       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
  KEnum => [<]
  -- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
  KEq =>
    let [< a0, a1, a, l, r] = xs in
    [< (Zero, a0, TYPE u a0.loc),
       (Zero, a1, TYPE u a1.loc),
       (Zero, a,  Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
       (Zero, l,  BVT 2 l.loc),
       (Zero, r,  BVT 2 r.loc)]
  KNat => [<]
  KString => [<]
  -- A : ★ᵤ
  KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]


namespace Elim
  private data InnerErr : Type where

  private
  InnerErrEff : Type -> Type
  InnerErrEff = StateL InnerErr (Maybe Error)

  private
  EqualElim : List (Type -> Type)
  EqualElim = InnerErrEff :: EqualInner

  private covering
  computeElimTypeE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
                     (e : Elim 0 n) -> (0 ne : NotRedex defs sg e) =>
                     Eff EqualElim (Term 0 n)
  computeElimTypeE defs ectx sg e = lift $
    computeElimType defs (toWhnfContext ectx) sg e

  private
  putError : Has InnerErrEff fs => Error -> Eff fs ()
  putError err = modifyAt InnerErr (<|> Just err)

  private
  try : Eff EqualInner () -> Eff EqualElim ()
  try act = lift $ catch putError $ lift act {fs' = EqualElim}

  private covering %inline
  clashE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
           (e, f : Elim 0 n) -> (0 nf : NotRedex defs sg f) =>
           Eff EqualElim (Term 0 n)
  clashE defs ctx sg e f = do
    putError $ ClashE e.loc ctx !mode e f
    computeElimTypeE defs ctx sg 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 : Definitions -> EqContext n -> (k : TyConKind) ->
               (ret : Term 0 n) -> (u : Universe) ->
               (b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
               (def : Term 0 n) ->
               Eff EqualElim ()
  compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
  compareArm defs ctx k ret u b1 b2 def = do
    let def   = SN def
        left  = fromMaybe def b1; right = fromMaybe def b2
        names = (fromMaybe def $ b1 <|> b2).names
    try $ compare0 defs (extendTyN (typecaseTel k names u) ctx)
                   SZero (weakT (arity k) ret) left.term right.term

  private covering
  compare0Inner : Definitions -> EqContext n -> (sg : SQty) ->
                  (e, f : Elim 0 n) -> Eff EqualElim (Term 0 n)

  private covering
  compare0Inner' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
                   (e, f : Elim 0 n) ->
                   (0 ne : NotRedex defs sg e) -> (0 nf : NotRedex defs sg f) ->
                   Eff EqualElim (Term 0 n)

  compare0Inner' defs ctx sg e@(F {}) f _ _ = do
    if e == f then computeElimTypeE defs ctx sg f
              else clashE defs ctx sg e f

  compare0Inner' defs ctx sg e@(B {}) f _ _ = do
    if e == f then computeElimTypeE defs ctx sg f
              else clashE defs ctx sg e f

  --  Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
  --  Ψ | Γ ⊢ s = t ⇐ A
  -- -------------------------------
  --  Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
  compare0Inner' defs ctx sg (App e s eloc) (App f t floc) ne nf = do
    ety <- compare0Inner defs ctx sg e f
    (_, arg, res) <- expectPi defs ctx sg eloc ety
    try $ Term.compare0 defs ctx sg arg s t
    pure $ sub1 res $ Ann s arg s.loc
  compare0Inner' defs ctx sg e'@(App {}) f' ne nf =
    clashE defs ctx sg 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]
  compare0Inner' defs ctx sg (CasePair epi e eret ebody eloc)
                             (CasePair fpi f fret fbody floc) ne nf =
    local_ Equal $ do
      ety <- compare0Inner defs ctx sg e f
      (fst, snd) <- expectSig defs ctx sg eloc ety
      let [< x, y] = ebody.names
      try $ do
        compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
        Term.compare0 defs
          (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) sg
          (substCasePairRet ebody.names ety eret)
          ebody.term fbody.term
        expectEqualQ e.loc epi fpi
      pure $ sub1 eret e
  compare0Inner' defs ctx sg e'@(CasePair {}) f' ne nf =
    clashE defs ctx sg e' f'

  --  Ψ | Γ ⊢ e = f ⇒ (x : A) × B
  -- ------------------------------
  --  Ψ | Γ ⊢ fst e = fst f ⇒ A
  compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf =
    local_ Equal $ do
      ety <- compare0Inner defs ctx sg e f
      fst <$> expectSig defs ctx sg eloc ety
  compare0Inner' defs ctx sg e@(Fst {}) f _ _ =
    clashE defs ctx sg e f

  --  Ψ | Γ ⊢ e = f ⇒ (x : A) × B
  -- ------------------------------------
  --  Ψ | Γ ⊢ snd e = snd f ⇒ B[fst e/x]
  compare0Inner' defs ctx sg (Snd e eloc) (Snd f floc) ne nf =
    local_ Equal $ do
      ety <- compare0Inner defs ctx sg e f
      (_, tsnd) <- expectSig defs ctx sg eloc ety
      pure $ sub1 tsnd (Fst e eloc)
  compare0Inner' defs ctx sg e@(Snd {}) f _ _ =
    clashE defs ctx sg 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]
  compare0Inner' defs ctx sg (CaseEnum epi e eret earms eloc)
                             (CaseEnum fpi f fret farms floc) ne nf =
    local_ Equal $ do
      ety <- compare0Inner defs ctx sg e f
      try $
        compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
      for_ (SortedMap.toList earms) $ \(t, l) => do
        let Just r = lookup t farms
          | Nothing => putError $ TagNotIn floc t (fromList $ keys farms)
        let t' = Ann (Tag t l.loc) ety l.loc
        try $ Term.compare0 defs ctx sg (sub1 eret t') l r
      try $ expectEqualQ eloc epi fpi
      pure $ sub1 eret e
  compare0Inner' defs ctx sg e@(CaseEnum {}) f _ _ = clashE defs ctx sg 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]
  compare0Inner' defs ctx sg (CaseNat epi epi' e eret ezer esuc eloc)
                             (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
    local_ Equal $ do
      ety <- compare0Inner defs ctx sg e f
      let [< p, ih] = esuc.names
      try $ do
        compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
        Term.compare0 defs ctx sg
          (sub1 eret (Ann (Zero ezer.loc) (NAT ezer.loc) ezer.loc))
          ezer fzer
        Term.compare0 defs
          (extendTyN [< (epi, p, NAT p.loc), (epi', ih, eret.term)] ctx) sg
          (substCaseSuccRet esuc.names eret) esuc.term fsuc.term
        expectEqualQ e.loc epi  fpi
        expectEqualQ e.loc epi' fpi'
      pure $ sub1 eret e
  compare0Inner' defs ctx sg e@(CaseNat {}) f _ _ = clashE defs ctx sg 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]
  compare0Inner' defs ctx sg (CaseBox epi e eret ebody eloc)
                             (CaseBox fpi f fret fbody floc) ne nf =
    local_ Equal $ do
      ety <- compare0Inner defs ctx sg e f
      (q, ty) <- expectBOX defs ctx sg eloc ety
      try $ do
        compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
        Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx) sg
          (substCaseBoxRet ebody.name ety eret)
          ebody.term fbody.term
        expectEqualQ eloc epi fpi
      pure $ sub1 eret e
  compare0Inner' defs ctx sg e@(CaseBox {}) f _ _ = clashE defs ctx sg e f

  -- (no neutral dim apps in a closed dctx)
  compare0Inner' _ _ _ (DApp _ (K {}) _) _ ne _ =
    void $ absurd $ noOr2 $ noOr2 ne
  compare0Inner' _ _ _ _ (DApp _ (K {}) _) _ nf =
    void $ absurd $ noOr2 $ noOr2 nf

  --  Ψ | Γ ⊢ s <: t : B
  -- --------------------------------
  --  Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
  --
  -- and similar for :> and A
  compare0Inner' defs ctx sg (Ann s a _) (Ann t b _) _ _ = do
    ty <- bigger a b
    try $ Term.compare0 defs ctx sg ty s t
    pure ty

  --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
  --  Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
  --  Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
  -- -----------------------------------------------------------
  --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
  --       <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
  compare0Inner' defs ctx sg (Coe ty1 p1 q1 val1 _)
                             (Coe ty2 p2 q2 val2 _) ne nf = do
    let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
        ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
    (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q)
    try $ do
      compareType defs ctx ty1p ty2p
      compareType defs ctx ty1q ty2q
      Term.compare0 defs ctx sg ty_p val1 val2
    pure $ ty_q
  compare0Inner' defs ctx sg e@(Coe {}) f _ _ = clashE defs ctx sg e f

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

  -- (type case equality purely structural)
  compare0Inner' defs ctx sg (TypeCase ty1 ret1 arms1 def1 eloc)
                             (TypeCase ty2 ret2 arms2 def2 floc) ne _ =
    case sg `decEq` SZero of
      Yes Refl => local_ Equal $ do
        ety <- compare0Inner defs ctx SZero ty1 ty2
        u   <- expectTYPE defs ctx SZero eloc ety
        try $ do
          compareType defs ctx ret1 ret2
          compareType defs ctx def1 def2
        for_ allKinds $ \k =>
          compareArm defs ctx k ret1 u
            (lookupPrecise k arms1) (lookupPrecise k arms2) def1
        pure ret1
      No _ => do
        putError $ ClashQ eloc sg.qty Zero
        computeElimTypeE defs ctx sg $ TypeCase ty1 ret1 arms1 def1 eloc
  compare0Inner' defs ctx sg e@(TypeCase {}) f _ _ = clashE defs ctx sg e f

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

  compare0Inner defs ctx sg e f = do
    Element e ne <- whnf defs ctx sg e.loc e
    Element f nf <- whnf defs ctx sg f.loc f
    ty <- compare0Inner' defs ctx sg e f ne nf
    if !(lift $ isSubSing defs ctx sg ty) && isJust !(getAt InnerErr)
       then putAt InnerErr Nothing
       else modifyAt InnerErr $ map $ WhileComparingE ctx !mode sg e f
    pure ty


namespace Term
  compare0 defs ctx sg ty s t =
    wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
      Element ty' _ <- whnf defs ctx SZero ty.loc ty
      Element s'  _ <- whnf defs ctx sg s.loc  s
      Element t'  _ <- whnf defs ctx sg t.loc  t
      tty <- ensureTyCon ty.loc ctx ty'
      compare0' defs ctx sg ty' s' t'

namespace Elim
  compare0 defs ctx sg e f = do
    (ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx sg e f
    maybe (pure ty) throw err

compareType defs ctx s t = do
  Element s' _ <- whnf defs ctx SZero s.loc s
  Element t' _ <- whnf defs ctx SZero 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' defs ctx s' t'


parameters (loc : Loc) (ctx : TyContext d n)
  parameters (mode : EqMode)
    private
    fromInner : Eff EqualInner a -> Eff Equal a
    fromInner = lift . map fst . runState mode

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

    private
    CompareAction : Nat -> Nat -> Type
    CompareAction d n =
      Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()

    private
    runCompare : FreeVars d -> CompareAction d n -> Eff Equal ()
    runCompare fvs act = fromInner $ eachFace fvs $ act !(askAt DEFS)

    private
    fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d
    fdvAll = let Val d = ctx.dimLen in foldMap (fdvWith [|d|] ctx.termLen)

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

      export covering
      compareType : (s, t : Term d n) -> Eff Equal ()
      compareType s t = runCompare (fdvAll [s, t]) $ \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 : SQty -> (e, f : Elim d n) -> Eff Equal ()
      compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
        ignore $ compare0 defs ectx sg (e // th) (f // th)

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

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

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