summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/error/builder.rs9
-rw-r--r--dhall/src/semantics/tck/typecheck.rs87
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt5
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt5
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt5
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt5
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt4
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt3
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt5
9 files changed, 63 insertions, 65 deletions
diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs
index 8c7eef3..39f8dfb 100644
--- a/dhall/src/error/builder.rs
+++ b/dhall/src/error/builder.rs
@@ -63,12 +63,6 @@ impl ErrorBuilder {
consumed: false,
}
}
- pub fn new_span_err(span: Span, message: impl ToString) -> Self {
- let message = message.to_string();
- let mut builder = Self::new(message.clone());
- builder.span_err(span, message);
- builder
- }
pub fn span_annot(
&mut self,
@@ -117,6 +111,9 @@ impl ErrorBuilder {
pub fn help(&mut self, message: impl ToString) -> &mut Self {
self.footer_annot(message, AnnotationType::Help)
}
+ pub fn note(&mut self, message: impl ToString) -> &mut Self {
+ self.footer_annot(message, AnnotationType::Note)
+ }
// TODO: handle multiple files
pub fn format(&mut self) -> String {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7518e90..9a1d0d8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -284,53 +284,53 @@ fn type_one_layer(
}
t
}
- ExprKind::App(f, arg) => match f.get_type()?.kind() {
- ValueKind::PiClosure { annot, closure, .. } => {
- if arg.get_type()? != *annot {
- return mkerr(
- ErrorBuilder::new_span_err(
- &span,
- format!("Wrong type of function argument"),
- )
- .span_err(
- &f.span(),
- format!(
- "this expects an argument of type: {}",
+ ExprKind::App(f, arg) => {
+ match f.get_type()?.kind() {
+ ValueKind::PiClosure { annot, closure, .. } => {
+ if arg.get_type()? != *annot {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "wrong type of function argument"
+ ))
+ .span_err(
+ f.span(),
+ format!(
+ "this expects an argument of type: {}",
+ annot.to_expr_tyenv(env),
+ ),
+ )
+ .span_err(
+ arg.span(),
+ format!(
+ "but this has type: {}",
+ arg.get_type()?.to_expr_tyenv(env),
+ ),
+ )
+ .note(format!(
+ "expected type `{}`\n found type `{}`",
annot.to_expr_tyenv(env),
- ),
- )
- .span_err(
- &arg.span(),
- format!(
- "but this has type: {}",
arg.get_type()?.to_expr_tyenv(env),
- ),
- )
- .format(),
- );
- }
+ ))
+ .format(),
+ );
+ }
- let arg_nf = arg.eval(env.as_nzenv());
- closure.apply(arg_nf)
- }
- _ => {
- return mkerr(
+ let arg_nf = arg.eval(env.as_nzenv());
+ closure.apply(arg_nf)
+ }
+ _ => return mkerr(
ErrorBuilder::new(format!(
- "Trying to apply an argument to a value that is not a \
- function"
+ "expected function, found `{}`",
+ f.get_type()?.to_expr_tyenv(env)
))
.span_err(
- &f.span(),
- format!(
- "this has type: `{}`",
- f.get_type()?.to_expr_tyenv(env)
- ),
+ f.span(),
+ format!("function application requires a function",),
)
- .help("only functions can be applied to")
.format(),
- )
+ ),
}
- },
+ }
ExprKind::BoolIf(x, y, z) => {
if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
return mkerr("InvalidPredicate");
@@ -509,8 +509,8 @@ fn type_one_layer(
.span_err(
record.span(),
format!(
- "the handler `{}` expects a value \
- of type: `{}`",
+ "the handler for `{}` expects a \
+ value of type: `{}`",
x,
annot.to_expr_tyenv(env)
),
@@ -523,7 +523,6 @@ fn type_one_layer(
variant_type.to_expr_tyenv(env)
),
)
- .help("only functions can be applied to")
.format(),
);
}
@@ -535,16 +534,16 @@ fn type_one_layer(
_ => {
return mkerr(
ErrorBuilder::new(format!(
- "Handler is not a function"
+ "merge handler is not a function"
))
.span_err(
span,
- format!("in this merge expression",),
+ format!("in this merge expression"),
)
.span_err(
record.span(),
format!(
- "the handler `{}` had type: `{}`",
+ "the handler for `{}` has type: `{}`",
x,
handler_type.to_expr_tyenv(env)
),
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 5241517..522e1a2 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1,4 +1,4 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
--> <current file>:6:23
|
1 | let bottom : Type = ∀(any : Type) → any
@@ -8,7 +8,8 @@ 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
| ^^^ this expects an argument of type: Kind
| ^ but this has type: Sort
|
+ = note: expected type `Kind`
+ found type `Sort`
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index d8811c2..01facbc 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1,8 +1,9 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
--> <current file>:1:1
|
1 | (λ(_ : Natural) → _) True
- | ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
| ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
| ^^^^ but this has type: Bool
|
+ = note: expected type `Natural`
+ found type `Bool`
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index 0732d1c..f779fd6 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1,7 +1,6 @@
-Type error: Unhandled error: error: Trying to apply an argument to a value that is not a function
+Type error: Unhandled error: error: expected function, found `Bool`
--> <current file>:1:0
|
1 | True True
- | ^^^^ this has type: `Bool`
+ | ^^^^ function application requires a function
|
- = 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 1459ca1..aa7c8c5 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1,8 +1,9 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
--> <current file>:1:5
|
1 | [] : List Type
- | ^^^^^^^^^ Wrong type of function argument
| ^^^^ this expects an argument of type: Type
| ^^^^ but this has type: Kind
|
+ = note: expected type `Type`
+ found type `Kind`
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
index 3a12c06..053a054 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -1,9 +1,9 @@
-Type error: Unhandled error: error: Handler is not a function
+Type error: Unhandled error: error: merge handler is not a function
--> <current file>:1:0
|
1 | merge { x = True } (< x : Bool >.x True)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
- | ^^^^^^^^^^^^ the handler `x` had type: `Bool`
+ | ^^^^^^^^^^^^ the handler for `x` has 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 2afbc78..faca63a 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -3,7 +3,6 @@ Type error: Unhandled error: error: Wrong handler input type
|
1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
- | ^^^^^^^^^^^^^^^^^^^^^^^ the handler `x` expects a value of type: `Bool`
+ | ^^^^^^^^^^^^^^^^^^^^^^^ the handler for `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 a35b9ab..7e410c4 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1,8 +1,9 @@
-Type error: Unhandled error: error: Wrong type of function argument
+Type error: Unhandled error: error: wrong type of function argument
--> <current file>:1:0
|
1 | Natural/subtract True True
- | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument
| ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
| ^^^^ but this has type: Bool
|
+ = note: expected type `Natural`
+ found type `Bool`