[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
polarity-lang · Nov 7, 2024 · 627f6d9 · 627f6d9
1 parent 2b2743c
commit 627f6d9
Show file tree

Hide file tree

Showing 17 changed files with 78 additions and 43 deletions.
diff --git a/lang/driver/src/database.rs b/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),
         }

diff --git a/lang/driver/src/result.rs b/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),
 }

diff --git a/lang/elaborator/src/result.rs b/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("While elaborating")]
+        reason_span: Option<SourceSpan>,
     },
     #[error("Cannot match on codata type {name}")]
     #[diagnostic(code("T-003"))]
@@ -135,6 +137,8 @@ pub enum TypeError {
         lhs_span: Option<SourceSpan>,
         #[label]
         rhs_span: Option<SourceSpan>,
+        #[label("While elaborating")]
+        reason_span: Option<SourceSpan>,
     },
     #[error("The following metavariables were not solved: {message}")]
     #[diagnostic(code("T-017"))]
@@ -157,12 +161,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(),
         }
     }
 
@@ -203,12 +208,13 @@ impl TypeError {
         Self::UnsupportedAnnotation { exp: exp.print_to_string(None), span: exp.span().to_miette() }
     }
 
-    pub fn cannot_decide(lhs: &Exp, rhs: &Exp) -> Self {
+    pub fn cannot_decide(lhs: &Exp, rhs: &Exp, reason: &Option<Span>) -> Self {
         Self::CannotDecide {
             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(),
         }
     }
 }
diff --git a/lang/elaborator/src/typechecker/decls/codefinition.rs b/lang/elaborator/src/typechecker/decls/codefinition.rs
@@ -33,7 +33,7 @@ impl CheckToplevel for Codef {
             };
 
             wd.check_exhaustiveness(ctx)?;
-            let cases = wd.infer_wd(ctx)?;
+            let cases = wd.infer_wd(ctx, span)?;
 
             Ok(Codef {
                 span: *span,

diff --git a/lang/elaborator/src/typechecker/decls/definition.rs b/lang/elaborator/src/typechecker/decls/definition.rs
@@ -32,7 +32,7 @@ impl CheckToplevel for Def {
 
             let ws = WithScrutinee { cases, scrutinee: self_param_nf.expect_typ_app()? };
             ws.check_exhaustiveness(ctx)?;
-            let cases = ws.check_ws(ctx, &ret_typ_nf)?;
+            let cases = ws.check_ws(ctx, &ret_typ_nf, span)?;
             Ok(Def {
                 span: *span,
                 doc: doc.clone(),

diff --git a/lang/elaborator/src/typechecker/exprs/anno.rs b/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(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t, &self.span())?;
         Ok(inferred_term)
     }
 

diff --git a/lang/elaborator/src/typechecker/exprs/call.rs b/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(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t, &self.span())?;
         Ok(inferred_term)
     }
     /// The *inference* rule for calls is:

diff --git a/lang/elaborator/src/typechecker/exprs/dot_call.rs b/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(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t, &self.span())?;
         Ok(inferred_term)
     }
 

diff --git a/lang/elaborator/src/typechecker/exprs/local_comatch.rs b/lang/elaborator/src/typechecker/exprs/local_comatch.rs
@@ -8,6 +8,7 @@ use crate::unifier::constraints::Constraint;
 use crate::unifier::unify::*;
 use ast::ctx::LevelCtx;
 use ast::*;
+use codespan::Span;
 use miette_util::ToMiette;
 
 use super::super::ctx::*;
@@ -34,7 +35,7 @@ impl CheckInfer for LocalComatch {
         let wd = WithExpectedType { cases, label: None, expected_type: expected_type_app.clone() };
 
         wd.check_exhaustiveness(ctx)?;
-        let cases = wd.infer_wd(ctx)?;
+        let cases = wd.infer_wd(ctx, span)?;
 
         Ok(LocalComatch {
             span: *span,
@@ -101,7 +102,7 @@ impl<'a> WithExpectedType<'a> {
         Ok(())
     }
 
-    pub fn infer_wd(&self, ctx: &mut Ctx) -> Result<Vec<Case>, TypeError> {
+    pub fn infer_wd(&self, ctx: &mut Ctx, reason: &Option<Span>) -> Result<Vec<Case>, TypeError> {
         let WithExpectedType { cases, expected_type, label } = &self;
         let TypCtor { args: on_args, .. } = expected_type;
 
@@ -171,7 +172,7 @@ impl<'a> WithExpectedType<'a> {
                         // this case is really absurd. To do this, we verify that the unification
                         // actually fails.
                         None => {
-                            unify(ctx.levels(), &mut ctx.meta_vars, constraint, false)?
+                            unify(ctx.levels(), &mut ctx.meta_vars, constraint, false, reason)?
                                 .map_yes(|_| TypeError::PatternIsNotAbsurd {
                                     name: name.clone(),
                                     span: span.to_miette(),
@@ -286,13 +287,18 @@ impl<'a> WithExpectedType<'a> {
                                 }
                             };
                             let body_out = {
-                                let unif =
-                                    unify(ctx.levels(), &mut ctx.meta_vars, constraint, false)?
-                                        .map_no(|()| TypeError::PatternIsAbsurd {
-                                            name: name.clone(),
-                                            span: span.to_miette(),
-                                        })
-                                        .ok_yes()?;
+                                let unif = unify(
+                                    ctx.levels(),
+                                    &mut ctx.meta_vars,
+                                    constraint,
+                                    false,
+                                    reason,
+                                )?
+                                .map_no(|()| TypeError::PatternIsAbsurd {
+                                    name: name.clone(),
+                                    span: span.to_miette(),
+                                })
+                                .ok_yes()?;
 
                                 ctx.fork::<Result<_, TypeError>, _>(|ctx| {
                                     ctx.subst(&module, &unif)?;

diff --git a/lang/elaborator/src/typechecker/exprs/local_match.rs b/lang/elaborator/src/typechecker/exprs/local_match.rs
@@ -3,6 +3,7 @@
 use ast::ctx::values::Binder;
 use ast::ctx::{BindContext, LevelCtx};
 use ast::*;
+use codespan::Span;
 use miette_util::ToMiette;
 
 use crate::normalizer::env::ToEnv;
@@ -58,7 +59,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(subst_ctx, &mut ctx.meta_vars, motive_t_nf, t, span)?;
 
                 body_t = ctx.bind_single(&self_binder, |ctx| {
                     ret_typ.normalize(&ctx.module, &mut ctx.env())
@@ -83,7 +84,7 @@ impl CheckInfer for LocalMatch {
 
         let ws = WithScrutinee { cases, scrutinee: typ_app_nf.clone() };
         ws.check_exhaustiveness(ctx)?;
-        let cases = ws.check_ws(ctx, &body_t)?;
+        let cases = ws.check_ws(ctx, &body_t, span)?;
 
         Ok(LocalMatch {
             span: *span,
@@ -145,7 +146,12 @@ impl<'a> WithScrutinee<'a> {
         Ok(())
     }
 
-    pub fn check_ws(&self, ctx: &mut Ctx, t: &Exp) -> Result<Vec<Case>, TypeError> {
+    pub fn check_ws(
+        &self,
+        ctx: &mut Ctx,
+        t: &Exp,
+        reason: &Option<Span>,
+    ) -> Result<Vec<Case>, TypeError> {
         let WithScrutinee { cases, .. } = &self;
 
         let cases: Vec<_> = cases.to_vec();
@@ -213,12 +219,13 @@ impl<'a> WithScrutinee<'a> {
 
                     let body_out = match body {
                         Some(body) => {
-                            let unif = unify(ctx.levels(), &mut ctx.meta_vars, constraint, false)?
-                                .map_no(|()| TypeError::PatternIsAbsurd {
-                                    name: name.clone(),
-                                    span: span.to_miette(),
-                                })
-                                .ok_yes()?;
+                            let unif =
+                                unify(ctx.levels(), &mut ctx.meta_vars, constraint, false, reason)?
+                                    .map_no(|()| TypeError::PatternIsAbsurd {
+                                        name: name.clone(),
+                                        span: span.to_miette(),
+                                    })
+                                    .ok_yes()?;
 
                             ctx.fork::<Result<_, TypeError>, _>(|ctx| {
                                 ctx.subst(&module, &unif)?;
@@ -233,7 +240,7 @@ impl<'a> WithScrutinee<'a> {
                             })?
                         }
                         None => {
-                            unify(ctx.levels(), &mut ctx.meta_vars, constraint, false)?
+                            unify(ctx.levels(), &mut ctx.meta_vars, constraint, false, reason)?
                                 .map_yes(|_| TypeError::PatternIsNotAbsurd {
                                     name: name.clone(),
                                     span: span.to_miette(),

diff --git a/lang/elaborator/src/typechecker/exprs/typ_ctor.rs b/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(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t, &self.span())?;
         Ok(inferred_term)
     }
 

diff --git a/lang/elaborator/src/typechecker/exprs/type_univ.rs b/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(
+            ctx.levels(),
+            &mut ctx.meta_vars,
+            Box::new(TypeUniv::new().into()),
+            t,
+            &self.span(),
+        )?;
         Ok(self.clone())
     }
 

diff --git a/lang/elaborator/src/typechecker/exprs/variable.rs b/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(ctx.levels(), &mut ctx.meta_vars, inferred_typ, t, &self.span())?;
         Ok(inferred_term)
     }
 

diff --git a/lang/elaborator/src/typechecker/util.rs b/lang/elaborator/src/typechecker/util.rs
@@ -1,3 +1,4 @@
+use codespan::Span;
 use log::trace;
 
 use ast::ctx::LevelCtx;
@@ -24,15 +25,16 @@ pub fn convert(
     meta_vars: &mut HashMap<MetaVar, MetaVarState>,
     this: Box<Exp>,
     other: &Exp,
+    reason: &Option<Span>,
 ) -> Result<(), TypeError> {
     trace!("{} =? {}", this.print_trace(), other.print_trace());
     // Convertibility is checked using the unification algorithm.
     let constraint: Constraint =
         Constraint::Equality { lhs: this.clone(), rhs: Box::new(other.clone()) };
-    let res = unify(ctx, meta_vars, constraint, true)?;
+    let res = unify(ctx, meta_vars, constraint, true, reason)?;
     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)),
     }
 }
 

diff --git a/lang/elaborator/src/unifier/unify.rs b/lang/elaborator/src/unifier/unify.rs
@@ -2,6 +2,7 @@ use std::collections::HashSet;
 
 use ast::ctx::LevelCtx;
 use ast::{occurs_in, Variable};
+use codespan::Span;
 use ctx::GenericCtx;
 
 use crate::result::TypeError;
@@ -51,9 +52,10 @@ pub fn unify(
     meta_vars: &mut HashMap<MetaVar, MetaVarState>,
     constraint: Constraint,
     vars_are_rigid: bool,
+    reason: &Option<Span>,
 ) -> Result<Dec<Unificator>, TypeError> {
     let mut ctx = Ctx::new(vec![constraint], ctx.clone(), vars_are_rigid);
-    let res = match ctx.unify(meta_vars)? {
+    let res = match ctx.unify(meta_vars, reason)? {
         Yes(_) => Yes(ctx.unif),
         No(()) => No(()),
     };
@@ -107,9 +109,13 @@ impl Ctx {
         }
     }
 
-    fn unify(&mut self, meta_vars: &mut HashMap<MetaVar, MetaVarState>) -> Result<Dec, TypeError> {
+    fn unify(
+        &mut self,
+        meta_vars: &mut HashMap<MetaVar, MetaVarState>,
+        reason: &Option<Span>,
+    ) -> Result<Dec, TypeError> {
         while let Some(constraint) = self.constraints.pop() {
-            match self.unify_eqn(&constraint, meta_vars)? {
+            match self.unify_eqn(&constraint, meta_vars, reason)? {
                 Yes(_) => {
                     self.done.insert(constraint);
                 }
@@ -124,6 +130,7 @@ impl Ctx {
         &mut self,
         eqn: &Constraint,
         meta_vars: &mut HashMap<MetaVar, MetaVarState>,
+        reason: &Option<Span>,
     ) -> Result<Dec, TypeError> {
         match eqn {
             Constraint::Equality { lhs, rhs, .. } => match (&**lhs, &**rhs) {
@@ -149,6 +156,7 @@ impl Ctx {
                                 return Err(TypeError::cannot_decide(
                                     &Box::new(Exp::Hole(h.clone())),
                                     &Box::new(e.clone()),
+                                    reason,
                                 ));
                             }
                         }
@@ -223,7 +231,7 @@ impl Ctx {
                 (Exp::TypeUniv(_), Exp::TypeUniv(_)) => Ok(Yes(())),
                 (Exp::Anno(_), _) => Err(TypeError::unsupported_annotation(lhs)),
                 (_, Exp::Anno(_)) => Err(TypeError::unsupported_annotation(rhs)),
-                (_, _) => Err(TypeError::cannot_decide(lhs, rhs)),
+                (_, _) => Err(TypeError::cannot_decide(lhs, rhs, reason)),
             },
             Constraint::EqualityArgs { lhs, rhs } => {
                 let new_eqns =

diff --git a/lang/lowering/src/lower/decls/data_declaration.rs b/lang/lowering/src/lower/decls/data_declaration.rs
@@ -47,7 +47,7 @@ fn lower_constructor(
             None => {
                 if type_arity == 0 {
                     ast::TypCtor {
-                        span: None,
+                        span: Some(*span),
                         name: typ_name.lower(ctx)?,
                         args: ast::Args { args: vec![] },
                     }

diff --git a/test/test-runner/src/phases.rs b/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,
-                })
+                }))
             })?;
         }