diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index bb66b43..adb0de3 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -103,6 +103,7 @@ isSubSing defs ctx ty0 = do Box {} => 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 @@ -127,519 +128,534 @@ 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) -> Eff EqualInner () - 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 +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 -> (ty, s, t : Term 0 n) -> + Eff EqualInner () - 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) => - Eff EqualInner () - compare0' ctx (TYPE {}) s t = compareType ctx s t +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 -> (e, f : Elim 0 n) -> + Eff EqualInner (Term 0 n) - 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 +||| 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 () - -- Γ, 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 ctx e f +||| 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 - (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 +namespace Term + private covering + compare0' : (defs : Definitions) -> EqContext n -> + (ty, s, t : Term 0 n) -> + (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) => + (0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) => + Eff EqualInner () + compare0' defs ctx (TYPE {}) s t = compareType defs ctx s t - eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner () - eta _ e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b - eta loc e (S _ (N _)) = clashT loc ctx ty s t + compare0' defs 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 defs ctx' res.term b1.term b2.term - 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 π ≥ 0 maybe - (Pair sFst sSnd {}, Pair tFst tSnd {}) => do - compare0 ctx fst sFst tFst - compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd + -- Γ, 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 ctx e f + (E e, E f) => ignore $ Elim.compare0 defs ctx e f - (Pair {}, E _) => clashT s.loc ctx ty s t - (E _, Pair {}) => clashT s.loc ctx ty s t + (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 - (Pair {}, t) => wrongType t.loc ctx ty t - (E _, t) => wrongType t.loc ctx ty t - (s, _) => wrongType s.loc ctx ty s + eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner () + eta _ e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b + eta loc e (S _ (N _)) = clashT loc ctx ty s t - 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) => ignore $ 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) => ignore $ 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) => ignore $ 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 - ignore $ 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) -> Eff EqualInner () - 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)) => - Eff EqualInner () - -- 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 a@(Pi {qty = sQty, arg = sArg, res = sRes, _}) - (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do - -- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂ - -- ---------------------------------------- - -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂ - expectEqualQ a.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 (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 (extendDim sTy.name Zero ctx) sTy.zero tTy.zero - compareType (extendDim sTy.name One ctx) sTy.one tTy.one - ty <- bigger 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} + compare0' defs 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 -- - -- no subtyping based on tag subsets, since that would need - -- a runtime coercion - unless (tags1 == tags2) $ clashTy s.loc ctx s t + -- [todo] η for π ≥ 0 maybe + (Pair sFst sSnd {}, Pair tFst tSnd {}) => do + compare0 defs ctx fst sFst tFst + compare0 defs ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd - compareType' ctx (Nat {}) (Nat {}) = - -- ------------ - -- Γ ⊢ ℕ <: ℕ - pure () + (E e, E f) => ignore $ Elim.compare0 defs ctx e f - compareType' ctx (BOX pi a loc) (BOX rh b {}) = do - expectEqualQ loc pi rh - compareType ctx a b + (Pair {}, E _) => clashT s.loc ctx ty s t + (E _, Pair {}) => clashT s.loc ctx ty s t - compareType' ctx (E e) (E f) = do - -- no fanciness needed here cos anything other than a neutral - -- has been inlined by whnf - ignore $ Elim.compare0 ctx e f + (Pair {}, t) => wrongType t.loc ctx ty t + (E _, t) => wrongType t.loc ctx ty t + (s, _) => wrongType s.loc ctx ty s + + compare0' defs 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) => ignore $ Elim.compare0 defs 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' defs 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 defs ctx nat s' t' + + (E e, E f) => ignore $ Elim.compare0 defs 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' defs ctx ty@(BOX q ty' {}) s t = local_ Equal $ + case (s, t) of + -- Γ ⊢ s = t : A + -- ----------------------- + -- Γ ⊢ [s] = [t] : [π.A] + (Box s' {}, Box t' {}) => compare0 defs ctx ty' s' t' + + (E e, E f) => ignore $ Elim.compare0 defs 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' defs 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 + ignore $ Elim.compare0 defs ctx e f - 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 : EqContext n -> (e, f : Elim 0 n) -> Eff EqualInner (Term 0 n) - compare0 ctx e f = do - (err, ty) <- compare0Inner ctx e f - maybe (pure ty) throw err +private covering +compareType' : (defs : Definitions) -> 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)) => + 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 - private covering - compare0Inner : EqContext n -> (e, f : Elim 0 n) -> - Eff EqualInner (Maybe Error, Term 0 n) - compare0Inner 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 - (err, ty) <- compare0' ctx e f ne nf - if !(isSubSing defs ctx ty) - then pure (Nothing, ty) - else pure (err, ty) +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 (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term - private - try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error) - try_ act = lift $ catch (pure . Just) $ act $> Nothing +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 (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term - private - lookupFree : EqContext n -> Name -> Universe -> Loc -> - Eff EqualInner (Term 0 n) - lookupFree ctx x u loc = - let Val n = ctx.termLen in - maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $ - lookup x defs +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 ty.zero sl tl + Term.compare0 defs ctx ty.one sr tr - private covering - compare0' : EqContext n -> - (e, f : Elim 0 n) -> - (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> +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 (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 e f + + +private +try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error) +try_ act = lift $ catch (pure . Just) $ act $> Nothing + +private +lookupFree : Definitions -> EqContext n -> Name -> Universe -> Loc -> + Eff EqualInner (Term 0 n) +lookupFree defs ctx x u loc = + let Val n = ctx.termLen in + maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $ + lookup x defs + + +namespace Elim + ||| 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 EqualInner () + compareArm {b1 = Nothing, b2 = Nothing, _} = pure () + compareArm defs ctx k ret u b1 b2 def = + let def = SN def in + compareArm_ defs ctx k ret u (fromMaybe def b1) (fromMaybe def b2) + where + compareArm_ : Definitions -> EqContext n -> (k : TyConKind) -> + (ret : Term 0 n) -> (u : Universe) -> + (b1, b2 : TypeCaseArmBody k 0 n) -> + Eff EqualInner () + compareArm_ defs ctx KTYPE ret u b1 b2 = + compare0 defs ctx ret b1.term b2.term + + compareArm_ defs 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 defs ctx (weakT 2 ret) b1.term b2.term + + compareArm_ defs 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 defs ctx (weakT 2 ret) b1.term b2.term + + compareArm_ defs ctx KEnum ret u b1 b2 = + compare0 defs ctx ret b1.term b2.term + + compareArm_ defs 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 defs ctx (weakT 5 ret) b1.term b2.term + + compareArm_ defs ctx KNat ret u b1 b2 = + compare0 defs ctx ret b1.term b2.term + + compareArm_ defs ctx KBOX ret u b1 b2 = do + let ctx = extendTy Zero b1.name (TYPE u b1.name.loc) ctx + compare0 defs ctx (weakT 1 ret) b1.term b1.term + + + private covering + compare0Inner : Definitions -> EqContext n -> (e, f : Elim 0 n) -> Eff EqualInner (Maybe Error, Term 0 n) - compare0' ctx e@(F x u loc) f@(F y v _) _ _ = do - pure (guard (x /= y || u /= v) $> ClashE loc ctx !mode e f, - !(lookupFree ctx x u loc)) - compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f + private covering + compare0Inner' : (defs : Definitions) -> EqContext n -> + (e, f : Elim 0 n) -> + (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> + Eff EqualInner (Maybe Error, Term 0 n) - compare0' ctx e@(B i loc) f@(B j _) _ _ = - pure (guard (i /= j) $> ClashE loc ctx !mode e f, - ctx.tctx !! i) - compare0' ctx e@(B {}) f _ _ = clashE e.loc ctx e f + compare0Inner' defs ctx e@(F x u loc) f@(F y v _) _ _ = do + pure (guard (x /= y || u /= v) $> ClashE loc ctx !mode e f, + !(lookupFree defs ctx x u loc)) + compare0Inner' defs ctx e@(F {}) 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 - (err1, ety) <- compare0Inner ctx e f - (_, arg, res) <- expectPi defs ctx eloc ety - err2 <- try_ $ Term.compare0 ctx arg s t - pure (err1 <|> err2, sub1 res $ Ann s arg s.loc) - compare0' ctx e@(App {}) f _ _ = clashE e.loc ctx e f + compare0Inner' defs ctx e@(B i loc) f@(B j _) _ _ = + pure (guard (i /= j) $> ClashE loc ctx !mode e f, + ctx.tctx !! i) + compare0Inner' defs ctx e@(B {}) 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 - (err1, ety) <- compare0Inner ctx e f - compareType (extendTy Zero eret.name ety ctx) eret.term fret.term - (fst, snd) <- expectSig defs ctx eloc ety - let [< x, y] = ebody.names - err2 <- try_ $ - Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) - (substCasePairRet ebody.names ety eret) - ebody.term fbody.term - err3 <- try_ $ expectEqualQ e.loc epi fpi - pure (concat [err1, err2, err3], sub1 eret e) - compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f + -- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B + -- Ψ | Γ ⊢ s = t ⇐ A + -- ------------------------------- + -- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x] + compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf = + local_ Equal $ do + (err1, ety) <- compare0Inner defs ctx e f + (_, arg, res) <- expectPi defs ctx eloc ety + err2 <- try_ $ Term.compare0 defs ctx arg s t + pure (err1 <|> err2, sub1 res $ Ann s arg s.loc) + compare0Inner' defs ctx e@(App {}) 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 - (err1, ety) <- compare0Inner ctx e f - err2 <- try_ $ - compareType (extendTy Zero eret.name ety ctx) eret.term fret.term - cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety - exs <- for cases $ \t => do - l <- lookupArm eloc t earms - r <- lookupArm floc t farms - try_ $ - Term.compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r - err3 <- try_ $ expectEqualQ eloc epi fpi - pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e) - where - lookupArm : Loc -> TagVal -> CaseEnumArms d n -> - Eff EqualInner (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 : 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 (CasePair epi e eret ebody eloc) + (CasePair fpi f fret fbody {}) ne nf = + local_ Equal $ do + (err1, ety) <- compare0Inner defs ctx e f + compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term + (fst, snd) <- expectSig defs ctx eloc ety + let [< x, y] = ebody.names + err2 <- try_ $ + Term.compare0 defs + (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) + (substCasePairRet ebody.names ety eret) + ebody.term fbody.term + err3 <- try_ $ expectEqualQ e.loc epi fpi + pure (concat [err1, err2, err3], sub1 eret e) + compare0Inner' defs ctx e@(CasePair {}) 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 - (err1, ety) <- compare0Inner ctx e f - err2 <- try_ $ - compareType (extendTy Zero eret.name ety ctx) eret.term fret.term - err3 <- try_ $ - Term.compare0 ctx - (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc)) - ezer fzer - let [< p, ih] = esuc.names - err4 <- try_ $ - Term.compare0 - (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) - (substCaseSuccRet esuc.names eret) esuc.term fsuc.term - err5 <- try_ $ expectEqualQ e.loc epi fpi - err6 <- try_ $ expectEqualQ e.loc epi' fpi' - pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e) - compare0' ctx e@(CaseNat {}) 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] + compare0Inner' defs ctx (CaseEnum epi e eret earms eloc) + (CaseEnum fpi f fret farms floc) ne nf = + local_ Equal $ do + (err1, ety) <- compare0Inner defs ctx e f + err2 <- try_ $ + compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term + cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety + exs <- for cases $ \t => do + l <- lookupArm eloc t earms + r <- lookupArm floc t farms + try_ $ + Term.compare0 defs ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r + err3 <- try_ $ expectEqualQ eloc epi fpi + pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e) + where + lookupArm : Loc -> TagVal -> CaseEnumArms d n -> + Eff EqualInner (Term d n) + lookupArm loc t arms = case lookup t arms of + Just arm => pure arm + Nothing => throw $ TagNotIn loc t (fromList $ keys arms) + compare0Inner' defs ctx e@(CaseEnum {}) 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 - (err1, ety) <- compare0Inner ctx e f - err2 <- try_ $ - compareType (extendTy Zero eret.name ety ctx) eret.term fret.term - (q, ty) <- expectBOX defs ctx eloc ety - err3 <- try_ $ - Term.compare0 (extendTy (epi * q) ebody.name ty ctx) - (substCaseBoxRet ebody.name ety eret) - ebody.term fbody.term - err4 <- try_ $ expectEqualQ eloc epi fpi - pure (concat [err1, err2, err3, err4], sub1 eret e) - compare0' ctx e@(CaseBox {}) 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] + compare0Inner' defs ctx (CaseNat epi epi' e eret ezer esuc eloc) + (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf = + local_ Equal $ do + (err1, ety) <- compare0Inner defs ctx e f + err2 <- try_ $ + compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term + err3 <- try_ $ + Term.compare0 defs ctx + (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc)) + ezer fzer + let [< p, ih] = esuc.names + err4 <- try_ $ + Term.compare0 defs + (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) + (substCaseSuccRet esuc.names eret) esuc.term fsuc.term + err5 <- try_ $ expectEqualQ e.loc epi fpi + err6 <- try_ $ expectEqualQ e.loc epi' fpi' + pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e) + compare0Inner' defs ctx e@(CaseNat {}) 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 + -- Ψ | Γ ⊢ 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 (CaseBox epi e eret ebody eloc) + (CaseBox fpi f fret fbody floc) ne nf = + local_ Equal $ do + (err1, ety) <- compare0Inner defs ctx e f + err2 <- try_ $ + compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term + (q, ty) <- expectBOX defs ctx eloc ety + err3 <- try_ $ + Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx) + (substCaseBoxRet ebody.name ety eret) + ebody.term fbody.term + err4 <- try_ $ expectEqualQ eloc epi fpi + pure (concat [err1, err2, err3, err4], sub1 eret e) + compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f - -- Ψ | Γ ⊢ s <: t : B - -- -------------------------------- - -- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B - -- - -- and similar for :> and A - compare0' ctx (Ann s a _) (Ann t b _) _ _ = do - ty <- bigger a b - err <- try_ $ Term.compare0 ctx ty s t - pure (err, ty) + -- all dim apps replaced with ends by whnf + compare0Inner' _ _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne + compare0Inner' _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf - -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› - -- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖› - -- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖› - -- ----------------------------------------------------------- - -- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s - -- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖› - compare0' ctx (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 - err1 <- try_ $ compareType ctx ty1p ty2p - err2 <- try_ $ compareType ctx ty1q ty2q - (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q) - err3 <- try_ $ Term.compare0 ctx ty_p val1 val2 - pure (concat [err1, err2, err3], ty_q) - compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f + -- Ψ | Γ ⊢ s <: t : B + -- -------------------------------- + -- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B + -- + -- and similar for :> and A + compare0Inner' defs ctx (Ann s a _) (Ann t b _) _ _ = do + ty <- bigger a b + err <- try_ $ Term.compare0 defs ctx ty s t + pure (err, ty) - -- (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 + -- Ψ | Γ ⊢ 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 (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 + err1 <- try_ $ compareType defs ctx ty1p ty2p + err2 <- try_ $ compareType defs ctx ty1q ty2q + (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q) + err3 <- try_ $ Term.compare0 defs ctx ty_p val1 val2 + pure (concat [err1, err2, err3], ty_q) + compare0Inner' defs ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f - -- (type case equality purely structural) - compare0' ctx (TypeCase ty1 ret1 arms1 def1 eloc) - (TypeCase ty2 ret2 arms2 def2 floc) ne _ = - local_ Equal $ do - -- try - (err1, ety) <- compare0Inner ctx ty1 ty2 - u <- expectTYPE defs ctx eloc ety - err2 <- try_ $ compareType ctx ret1 ret2 - err3 <- try_ $ compareType ctx def1 def2 - exs <- for allKinds $ \k => - try_ $ - compareArm ctx k ret1 u - (lookupPrecise k arms1) (lookupPrecise k arms2) def1 - pure (concat $ [err1, err2, err3] ++ exs, ret1) - compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f + -- (no neutral compositions in a closed dctx) + compare0Inner' _ _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne + compare0Inner' _ _ (Comp {r = B i _, _}) _ _ _ = absurd i + compare0Inner' _ _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf - -- Ψ | Γ ⊢ s <: f ⇐ A - -- -------------------------- - -- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A - -- - -- and vice versa - compare0' ctx (Ann s a _) f _ _ = do - err <- try_ $ Term.compare0 ctx a s (E f) - pure (err, a) - compare0' ctx e (Ann t b _) _ _ = do - err <- try_ $ Term.compare0 ctx b (E e) t - pure (err, b) - compare0' ctx e@(Ann {}) f _ _ = - clashE e.loc ctx e f + -- (type case equality purely structural) + compare0Inner' defs ctx (TypeCase ty1 ret1 arms1 def1 eloc) + (TypeCase ty2 ret2 arms2 def2 floc) ne _ = + local_ Equal $ do + (err1, ety) <- compare0Inner defs ctx ty1 ty2 + u <- expectTYPE defs ctx eloc ety + err2 <- try_ $ compareType defs ctx ret1 ret2 + err3 <- try_ $ compareType defs ctx def1 def2 + exs <- for allKinds $ \k => + try_ $ + compareArm defs ctx k ret1 u + (lookupPrecise k arms1) (lookupPrecise k arms2) def1 + pure (concat $ [err1, err2, err3] ++ exs, ret1) + compare0Inner' defs ctx e@(TypeCase {}) 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) -> - Eff EqualInner () - 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) + -- Ψ | Γ ⊢ s <: f ⇐ A + -- -------------------------- + -- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A + -- + -- and vice versa + compare0Inner' defs ctx (Ann s a _) f _ _ = do + err <- try_ $ Term.compare0 defs ctx a s (E f) + pure (err, a) + compare0Inner' defs ctx e (Ann t b _) _ _ = do + err <- try_ $ Term.compare0 defs ctx b (E e) t + pure (err, b) + compare0Inner' defs ctx e@(Ann {}) f _ _ = + clashE e.loc ctx e f - private covering - compareArm_ : EqContext n -> (k : TyConKind) -> - (ret : Term 0 n) -> (u : Universe) -> - (b1, b2 : TypeCaseArmBody k 0 n) -> - Eff EqualInner () - compareArm_ ctx KTYPE ret u b1 b2 = - compare0 ctx ret b1.term b2.term + compare0Inner defs 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 + (err, ty) <- compare0Inner' defs ctx e f ne nf + if !(isSubSing defs ctx ty) + then pure (Nothing, ty) + else pure (err, ty) - 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 +namespace Term + compare0 defs 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' defs ctx ty' s' t' - compareArm_ ctx KEnum ret u b1 b2 = - compare0 ctx ret b1.term b2.term +namespace Elim + compare0 defs ctx e f = do + (err, ty) <- compare0Inner defs ctx e f + maybe (pure ty) throw err - 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 +compareType defs 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' defs ctx s' t' - 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)