From d8c3ced0f1acb1924c801fadbfd3077dede9b0dd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 2 Feb 2020 17:22:27 +0000 Subject: More errors --- dhall/src/error/builder.rs | 40 ++++++----- dhall/src/semantics/nze/value.rs | 3 + dhall/src/semantics/tck/typecheck.rs | 84 ++++++++++++++++++++-- dhall/tests/type-errors/hurkensParadox.txt | 4 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 4 +- .../unit/FunctionApplicationIsNotFunction.txt | 8 ++- .../type-errors/unit/ListLiteralEmptyNotType.txt | 4 +- .../type-errors/unit/MergeHandlerNotFunction.txt | 10 ++- .../unit/MergeHandlerNotMatchAlternativeType.txt | 10 ++- .../type-errors/unit/NaturalSubtractNotNatural.txt | 4 +- 10 files changed, 138 insertions(+), 33 deletions(-) (limited to 'dhall') 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(), diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index e06c4b2..5241517 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -9,6 +9,6 @@ Type error: Unhandled error: error: Wrong type of function argument 10 | : pow (pow U) → U 11 | = λ(t : pow (pow U)) | ^^^^^ Wrong type of function argument - | --- help: this expects an argument of type: Kind - | - help: but this has type: Sort + | ^^^ this expects an argument of type: Kind + | ^ but this has type: Sort | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 776b14e..d8811c2 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | (λ(_ : Natural) → _) True | ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument - | ------------------ help: this expects an argument of type: Natural - | ---- help: but this has type: Bool + | ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural + | ^^^^ but this has type: Bool | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index a72e120..0732d1c 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1,7 @@ -Type error: Unhandled error: apply to not Pi +Type error: Unhandled error: error: Trying to apply an argument to a value that is not a function + --> :1:0 + | +1 | True True + | ^^^^ this has type: `Bool` + | + = help: only functions can be applied to diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 125cc87..1459ca1 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | [] : List Type | ^^^^^^^^^ Wrong type of function argument - | ---- help: this expects an argument of type: Type - | ---- help: but this has type: Kind + | ^^^^ this expects an argument of type: Type + | ^^^^ but this has type: Kind | diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index f1cdf92..16931a8 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -1 +1,9 @@ -Type error: Unhandled error: NotAFunction +Type error: Unhandled error: error: Handler is not a function + --> :1:0 + | +1 | merge { x = True } (< x : Bool >.x True) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^ the handler `x` had type: `Bool` + | ----------------- help: the corresponding variant has type: `Bool` + | + = help: a handler for this variant must be a function that takes an input of type: `Bool` diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index 8b729a4..1762a7c 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1,9 @@ -Type error: Unhandled error: MergeHandlerTypeMismatch +Type error: Unhandled error: error: Wrong handler input type + --> :1:0 + | +1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression + | ^^^^^^^^^^^^^^^^^^^ the handler `x` expects a value of type: `Bool` + | ^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural` + | + = help: only functions can be applied to diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 5ee2a11..a35b9ab 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -3,6 +3,6 @@ Type error: Unhandled error: error: Wrong type of function argument | 1 | Natural/subtract True True | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument - | ---------------- help: this expects an argument of type: Natural - | ---- help: but this has type: Bool + | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural + | ^^^^ but this has type: Bool | -- cgit v1.2.3