From c8a3963af1067cc5d00117674270639eadfce673 Mon Sep 17 00:00:00 2001 From: mangoiv Date: Sun, 27 Oct 2024 12:44:14 +0100 Subject: [PATCH] [fix] allow unification errors to originate from a specific location - add an origin field to NotEq unification error - add an origin field to CannotDecide unification error - reuse the span emitted for a data constructor without type for its type - Box the type error in Error to reduce the size of the enum --- lang/driver/src/database.rs | 6 ++--- lang/driver/src/result.rs | 2 +- lang/elaborator/src/result.rs | 10 +++++-- .../src/typechecker/decls/codefinition.rs | 2 +- .../src/typechecker/decls/definition.rs | 2 +- lang/elaborator/src/typechecker/exprs/anno.rs | 2 +- lang/elaborator/src/typechecker/exprs/call.rs | 2 +- .../src/typechecker/exprs/dot_call.rs | 2 +- .../src/typechecker/exprs/local_comatch.rs | 26 +++++++++++------- .../src/typechecker/exprs/local_match.rs | 27 ++++++++++++------- .../src/typechecker/exprs/typ_ctor.rs | 2 +- .../src/typechecker/exprs/type_univ.rs | 8 +++++- .../src/typechecker/exprs/variable.rs | 2 +- lang/elaborator/src/typechecker/util.rs | 6 +++-- lang/elaborator/src/unifier/unify.rs | 16 ++++++++--- .../src/lower/decls/data_declaration.rs | 2 +- test/test-runner/src/phases.rs | 4 +-- 17 files changed, 78 insertions(+), 43 deletions(-) diff --git a/lang/driver/src/database.rs b/lang/driver/src/database.rs index 460762f94e..b928d14dcd 100644 --- 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 index ac58f9e02c..55ad0a8ffb 100644 --- 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), Xfunc(#[from] transformations::result::XfuncError), Driver(#[from] DriverError), } diff --git a/lang/elaborator/src/result.rs b/lang/elaborator/src/result.rs index f5d33ef4fc..eb92f19797 100644 --- a/lang/elaborator/src/result.rs +++ b/lang/elaborator/src/result.rs @@ -35,6 +35,8 @@ pub enum TypeError { lhs_span: Option, #[label("Source of (2)")] rhs_span: Option, + #[label("While elaborating")] + reason_span: Option, }, #[error("Cannot match on codata type {name}")] #[diagnostic(code("T-003"))] @@ -135,6 +137,8 @@ pub enum TypeError { lhs_span: Option, #[label] rhs_span: Option, + #[label("While elaborating")] + reason_span: Option, }, #[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, 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) -> 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 index c9a7596272..8a0fdb31e4 100644 --- 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 index 36976739dd..604a846e5f 100644 --- 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 index 7e8e720025..eef691af93 100644 --- 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 index a6b68fc098..e72960bcf2 100644 --- 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 index 291a3ee058..b9e9ef8c4e 100644 --- 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 index 08f088c075..34d35ac7a4 100644 --- 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, TypeError> { + pub fn infer_wd(&self, ctx: &mut Ctx, reason: &Option) -> Result, 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::, _>(|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 index a7d8f1e395..2cab2d34fb 100644 --- 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, TypeError> { + pub fn check_ws( + &self, + ctx: &mut Ctx, + t: &Exp, + reason: &Option, + ) -> Result, 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::, _>(|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 index ff1184079d..03a24c489c 100644 --- 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 index 1dfd4824d8..6f187b7307 100644 --- 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 { - 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 index 6b992b1547..6f579a7dd0 100644 --- 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 index 1be4ceeb72..9e099291f8 100644 --- 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, this: Box, other: &Exp, + reason: &Option, ) -> 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 index 0345090d49..b6e617ed01 100644 --- 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, constraint: Constraint, vars_are_rigid: bool, + reason: &Option, ) -> Result, 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) -> Result { + fn unify( + &mut self, + meta_vars: &mut HashMap, + reason: &Option, + ) -> Result { 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, + reason: &Option, ) -> Result { 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 index 39e1239ae5..ee6216f846 100644 --- 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 index 6dad5adf2a..e3d9cafc17 100644 --- 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, - }) + })) })?; }