summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/error/builder.rs40
-rw-r--r--dhall/src/semantics/nze/value.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs84
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt4
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt4
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt8
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt4
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt10
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt10
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt4
-rw-r--r--serde_dhall/src/lib.rs2
-rw-r--r--serde_dhall/src/serde.rs2
12 files changed, 140 insertions, 35 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(),
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
+ --> <current file>: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
+ --> <current file>: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
+ --> <current file>: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
|
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index 0381fec..7bf6d30 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -181,8 +181,8 @@ pub use value::Value;
// A Dhall value.
#[doc(hidden)]
pub mod value {
- use dhall::{Normalized, NormalizedExpr, Parsed};
use dhall::syntax::Builtin;
+ use dhall::{Normalized, NormalizedExpr, Parsed};
use super::de::{Error, Result};
diff --git a/serde_dhall/src/serde.rs b/serde_dhall/src/serde.rs
index 336330a..3e78987 100644
--- a/serde_dhall/src/serde.rs
+++ b/serde_dhall/src/serde.rs
@@ -4,8 +4,8 @@ use serde::de::value::{
MapAccessDeserializer, MapDeserializer, SeqDeserializer,
};
-use dhall::NormalizedExpr;
use dhall::syntax::ExprKind;
+use dhall::NormalizedExpr;
use crate::de::{Deserialize, Error, Result};
use crate::Value;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 08:42:22 +0000