wrap type errors in extra context

lib/Quox/Equal.idr

@@ -116,12 +116,13 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
       export covering %inline
       compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
-      compare0 ctx ty s t = do
-        let Element ty nty = whnfD defs ty
-            Element s  ns  = whnfD defs s
-            Element t  nt  = whnfD defs t
-        tty <- ensureTyCon ty
-        compare0' ctx ty s t
+      compare0 ctx ty s t =
+        wrapErr (WhileComparingT (MkTyContext new ctx) !mode ty s t) $ do
+          let Element ty nty = whnfD defs ty
+              Element s  ns  = whnfD defs s
+              Element t  nt  = whnfD defs t
+          tty <- ensureTyCon 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".
@@ -289,12 +290,12 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       export covering %inline
       compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
       compare0 ctx e f =
-        let Element e ne = whnfD defs e
-            Element f nf = whnfD defs f
-        in
-        -- [fixme] there is a better way to do this "isSubSing" stuff for sure
-        unless (isSubSing defs !(computeElimType ctx e ne)) $
-          compare0' ctx e f ne nf
+        wrapErr (WhileComparingE (MkTyContext new ctx) !mode e f) $ do
+          let Element e ne = whnfD defs e
+              Element f nf = whnfD defs f
+          -- [fixme] there is a better way to do this "isSubSing" stuff for sure
+          unless (isSubSing defs !(computeElimType ctx e ne)) $
+            compare0' ctx e f ne nf
 
       private covering
       compare0' : TContext q 0 n ->

lib/Quox/Typechecker.idr

@@ -80,8 +80,9 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   checkC : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
            m (CheckResult' q n)
   checkC ctx sg subj ty =
-    let Element subj nc = pushSubsts subj in
-    check' ctx sg subj nc ty
+    wrapErr (WhileChecking ctx sg.fst subj ty) $
+      let Element subj nc = pushSubsts subj in
+      check' ctx sg subj nc ty
 
 
   ||| "Ψ | Γ ⊢ σ · e ⇒ A ⊳ Σ"
@@ -104,8 +105,9 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   inferC : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
            m (InferResult' q d n)
   inferC ctx sg subj =
-    let Element subj nc = pushSubsts subj in
-    infer' ctx sg subj nc
+    wrapErr (WhileInferring ctx sg.fst subj) $
+      let Element subj nc = pushSubsts subj in
+      infer' ctx sg subj nc
 
 
   private covering

lib/Quox/Typing.idr

@@ -124,10 +124,34 @@ data Error q
 | NotType (Term q d n)
 | WrongType (Term q d n) (Term q d n) (Term q d n)
 
+-- extra context
+| WhileChecking
+    (TyContext q d n) q
+    (Term q d n) -- term
+    (Term q d n) -- type
+    (Error q)
+| WhileInferring
+    (TyContext q d n) q
+    (Elim q d n)
+    (Error q)
+| WhileComparingT
+    (TyContext q d n) EqMode
+    (Term q d n) -- type
+    (Term q d n) (Term q d n) -- lhs/rhs
+    (Error q)
+| WhileComparingE
+    (TyContext q d n) EqMode
+    (Elim q d n) (Elim q d n)
+    (Error q)
+
 public export
 0 HasErr : Type -> (Type -> Type) -> Type
 HasErr q = MonadError (Error q)
 
+export %inline
+wrapErr : HasErr q m => (Error q -> Error q) -> m a -> m a
+wrapErr f act = catchError act $ throwError . f
+
 export %inline
 ucmp : EqMode -> Universe -> Universe -> Bool
 ucmp Equal = (==)