diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/error/builder.rs | 40 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 3 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 84 |
3 files changed, 105 insertions, 22 deletions
diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs index 22b0d77..29d0d35 100644 --- a/dhall/src/error/builder.rs +++ b/dhall/src/error/builder.rs @@ -70,10 +70,11 @@ impl ErrorBuilder { builder } - pub fn span_err( + pub fn span_annot( &mut self, span: &Span, message: impl ToString, + annotation_type: AnnotationType, ) -> &mut Self { // Ignore spans not coming from a source file let span = match span { @@ -83,33 +84,38 @@ impl ErrorBuilder { self.annotations.push(SpannedAnnotation { span: span.clone(), message: message.to_string(), - annotation_type: AnnotationType::Error, + annotation_type, }); self } - pub fn span_help( + pub fn footer_annot( &mut self, - span: &Span, message: impl ToString, + annotation_type: AnnotationType, ) -> &mut Self { - // Ignore spans not coming from a source file - let span = match span { - Span::Parsed(span) => span, - _ => return self, - }; - self.annotations.push(SpannedAnnotation { - span: span.clone(), + self.footer.push(FreeAnnotation { message: message.to_string(), - annotation_type: AnnotationType::Help, + annotation_type, }); self } + + pub fn span_err( + &mut self, + span: &Span, + message: impl ToString, + ) -> &mut Self { + self.span_annot(span, message, AnnotationType::Error) + } + pub fn span_help( + &mut self, + span: &Span, + message: impl ToString, + ) -> &mut Self { + self.span_annot(span, message, AnnotationType::Help) + } pub fn help(&mut self, message: impl ToString) -> &mut Self { - self.footer.push(FreeAnnotation { - message: message.to_string(), - annotation_type: AnnotationType::Help, - }); - self + self.footer_annot(message, AnnotationType::Help) } // TODO: handle multiple files diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index bb3e3c0..d97b8c4 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -174,6 +174,9 @@ impl Value { _ => None, } } + pub(crate) fn span(&self) -> Span { + self.0.span.clone() + } /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index e642b8f..d99f549 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -293,14 +293,14 @@ fn type_one_layer( &span, format!("Wrong type of function argument"), ) - .span_help( + .span_err( &f.span(), format!( "this expects an argument of type: {}", annot.to_expr_tyenv(env), ), ) - .span_help( + .span_err( &arg.span(), format!( "but this has type: {}", @@ -314,7 +314,23 @@ fn type_one_layer( let arg_nf = arg.eval(env.as_nzenv()); closure.apply(arg_nf) } - _ => return mkerr(format!("apply to not Pi")), + _ => { + return mkerr( + ErrorBuilder::new(format!( + "Trying to apply an argument \ + to a value that is not a function" + )) + .span_err( + &f.span(), + format!( + "this has type: `{}`", + f.get_type()?.to_expr_tyenv(env) + ), + ) + .help("only functions can be applied to") + .format(), + ) + } }, ExprKind::BoolIf(x, y, z) => { if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { @@ -483,14 +499,72 @@ fn type_one_layer( Some(Some(variant_type)) => match handler_type.kind() { ValueKind::PiClosure { closure, annot, .. } => { if variant_type != annot { - return mkerr("MergeHandlerTypeMismatch"); + return mkerr( + ErrorBuilder::new(format!( + "Wrong handler input type" + )) + .span_err( + &span, + format!( + "in this merge expression", + ), + ) + .span_err( + &record.span(), + format!( + "the handler `{}` expects a value of type: `{}`", + x, + annot.to_expr_tyenv(env) + ), + ) + .span_err( + &union.span(), + format!( + "but the corresponding variant has type: `{}`", + variant_type.to_expr_tyenv(env) + ), + ) + .help("only functions can be applied to") + .format(), + ); } closure.remove_binder().or_else(|()| { mkerr("MergeReturnTypeIsDependent") })? } - _ => return mkerr("NotAFunction"), + _ => + return mkerr( + ErrorBuilder::new(format!( + "Handler is not a function" + )) + .span_err( + &span, + format!( + "in this merge expression", + ), + ) + .span_err( + &record.span(), + format!( + "the handler `{}` had type: `{}`", + x, + handler_type.to_expr_tyenv(env) + ), + ) + .span_help( + &union.span(), + format!( + "the corresponding variant has type: `{}`", + variant_type.to_expr_tyenv(env) + ), + ) + .help(format!( + "a handler for this variant must be a function that takes an input of type: `{}`", + variant_type.to_expr_tyenv(env) + )) + .format(), + ) }, // Union alternative without type Some(None) => handler_type.clone(), |