[fix] allow unification errors to originate from a specific location

- add an origin field to NotEq unification error
- Box the type error in Error to reduce the size of the enum

lang/driver/src/database.rs

@@ -228,7 +228,7 @@ impl Database {
         let ust = self.ust(uri).map(|x| (*x).clone())?;
         let ast = elaborator::typechecker::check_with_lookup_table(Rc::new(ust), &info_table)
             .map(Arc::new)
-            .map_err(Error::Type);
+            .map_err(|arg| Error::Type(Box::new(arg)));
         self.ast.insert(uri.clone(), ast.clone());
         ast
     }
@@ -370,8 +370,8 @@ impl Database {
 
         match main {
             Some(exp) => {
-                let nf = exp.normalize_in_empty_env(&ast)?;
-                Ok(Some(nf))
+                let nf = exp.normalize_in_empty_env(&ast);
+                nf.map(Some).map_err(|err| Error::Type(Box::new(err)))
             }
             None => Ok(None),
         }

lang/driver/src/result.rs

@@ -10,7 +10,7 @@ use url::Url;
 pub enum Error {
     Parser(#[from] parser::ParseError),
     Lowering(#[from] lowering::LoweringError),
-    Type(#[from] elaborator::result::TypeError),
+    Type(#[from] Box<elaborator::result::TypeError>),
     Xfunc(#[from] transformations::result::XfuncError),
     Driver(#[from] DriverError),
 }

lang/elaborator/src/result.rs

@@ -35,6 +35,8 @@ pub enum TypeError {
         lhs_span: Option<SourceSpan>,
         #[label("Source of (2)")]
         rhs_span: Option<SourceSpan>,
+        #[label("Originating from")]
+        reason_span: Option<SourceSpan>,
     },
     #[error("Cannot match on codata type {name}")]
     #[diagnostic(code("T-003"))]
@@ -157,12 +159,13 @@ pub enum TypeError {
 }
 
 impl TypeError {
-    pub fn not_eq(lhs: &Exp, rhs: &Exp) -> Self {
+    pub fn not_eq(reason: &Option<Span>, lhs: &Exp, rhs: &Exp) -> Self {
         Self::NotEq {
             lhs: lhs.print_to_string(None),
             rhs: rhs.print_to_string(None),
             lhs_span: lhs.span().to_miette(),
             rhs_span: rhs.span().to_miette(),
+            reason_span: reason.to_miette(),
         }
     }
 

lang/elaborator/src/typechecker/exprs/anno.rs

@@ -16,7 +16,7 @@ impl CheckInfer for Anno {
             message: "Expected inferred type".to_owned(),
             span: None,
         })?;
-        convert(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
+        convert(&self.span(), ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
         Ok(inferred_term)
     }
 

lang/elaborator/src/typechecker/exprs/call.rs

@@ -25,7 +25,7 @@ impl CheckInfer for Call {
             message: "Expected inferred type".to_owned(),
             span: None,
         })?;
-        convert(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
+        convert(&self.span(), ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
         Ok(inferred_term)
     }
     /// The *inference* rule for calls is:

lang/elaborator/src/typechecker/exprs/dot_call.rs

@@ -24,7 +24,7 @@ impl CheckInfer for DotCall {
             message: "Expected inferred type".to_owned(),
             span: None,
         })?;
-        convert(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
+        convert(&self.span(), ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
         Ok(inferred_term)
     }
 

lang/elaborator/src/typechecker/exprs/local_match.rs

@@ -58,7 +58,7 @@ impl CheckInfer for LocalMatch {
                 let mut motive_t = ret_typ.subst(&mut subst_ctx, &subst);
                 motive_t.shift((-1, 0));
                 let motive_t_nf = motive_t.normalize(&ctx.module, &mut ctx.env())?;
-                convert(subst_ctx, &mut ctx.meta_vars, motive_t_nf, t)?;
+                convert(span, subst_ctx, &mut ctx.meta_vars, motive_t_nf, t)?;
 
                 body_t = ctx.bind_single(&self_binder, |ctx| {
                     ret_typ.normalize(&ctx.module, &mut ctx.env())

lang/elaborator/src/typechecker/exprs/typ_ctor.rs

@@ -22,7 +22,7 @@ impl CheckInfer for TypCtor {
             message: "Expected inferred type".to_owned(),
             span: None,
         })?;
-        convert(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
+        convert(&self.span(), ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
         Ok(inferred_term)
     }
 

lang/elaborator/src/typechecker/exprs/type_univ.rs

@@ -19,7 +19,13 @@ impl CheckInfer for TypeUniv {
     ///            P, Γ ⊢ Type ⇐ τ
     /// ```
     fn check(&self, ctx: &mut Ctx, t: &Exp) -> Result<Self, TypeError> {
-        convert(ctx.levels(), &mut ctx.meta_vars, Box::new(TypeUniv::new().into()), t)?;
+        convert(
+            &self.span(),
+            ctx.levels(),
+            &mut ctx.meta_vars,
+            Box::new(TypeUniv::new().into()),
+            t,
+        )?;
         Ok(self.clone())
     }
 

lang/elaborator/src/typechecker/exprs/variable.rs

@@ -21,7 +21,7 @@ impl CheckInfer for Variable {
             message: "Expected inferred type".to_owned(),
             span: None,
         })?;
-        convert(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
+        convert(&self.span(), ctx.levels(), &mut ctx.meta_vars, inferred_typ, t)?;
         Ok(inferred_term)
     }
 

lang/elaborator/src/typechecker/util.rs

@@ -1,3 +1,4 @@
+use codespan::Span;
 use log::trace;
 
 use ast::ctx::LevelCtx;
@@ -20,6 +21,7 @@ pub fn uses_self(codata: &Codata) -> Result<bool, TypeError> {
 }
 
 pub fn convert(
+    reason: &Option<Span>,
     ctx: LevelCtx,
     meta_vars: &mut HashMap<MetaVar, MetaVarState>,
     this: Box<Exp>,
@@ -32,7 +34,7 @@ pub fn convert(
     let res = unify(ctx, meta_vars, constraint, true)?;
     match res {
         crate::unifier::dec::Dec::Yes(_) => Ok(()),
-        crate::unifier::dec::Dec::No(_) => Err(TypeError::not_eq(&this, other)),
+        crate::unifier::dec::Dec::No(_) => Err(TypeError::not_eq(reason, &this, other)),
     }
 }
 

test/test-runner/src/phases.rs

@@ -363,10 +363,10 @@ impl Phase for Xfunc {
             let new_source = db.edited(uri, xfunc_out.edits);
             db.write_source(&new_uri, &new_source.to_string())?;
             db.ast(&new_uri).map_err(|err| {
-                driver::Error::Type(elaborator::result::TypeError::Impossible {
+                driver::Error::Type(Box::new(elaborator::result::TypeError::Impossible {
                     message: format!("Failed to xfunc {type_name}: {err}"),
                     span: None,
-                })
+                }))
             })?;
         }