summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/semantics/tck/typecheck.rs15
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt2
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt22
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt64
4 files changed, 6 insertions, 97 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 22ba72d..5422e6d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -269,7 +269,7 @@ fn type_one_layer(
let arg_nf = arg.normalize_nf(env.as_nzenv());
closure.apply(arg_nf)
}
- _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
+ _ => return mkerr(format!("apply to not Pi")),
}
}
ExprKind::BoolIf(x, y, z) => {
@@ -447,12 +447,7 @@ fn type_one_layer(
match &*handler_type_borrow {
ValueKind::PiClosure { closure, annot, .. } => {
if variant_type != annot {
- // return mkerr("MergeHandlerTypeMismatch");
- return mkerr(format!(
- "MergeHandlerTypeMismatch: {:#?} != {:#?}",
- variant_type,
- annot
- ));
+ return mkerr("MergeHandlerTypeMismatch");
}
let v = NzVar::fresh();
@@ -470,11 +465,7 @@ fn type_one_layer(
None => inferred_type = Some(handler_return_type),
Some(t) => {
if t != &handler_return_type {
- // return mkerr("MergeHandlerTypeMismatch");
- return mkerr(format!(
- "MergeHandlerTypeMismatch: {:#?} != {:#?}",
- t, handler_return_type,
- ));
+ return mkerr("MergeHandlerTypeMismatch");
}
}
}
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index 13b0819..a72e120 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1 +1 @@
-Type error: Unhandled error: apply to not Pi: AppliedBuiltin(Bool, [], [], NzEnv { items: [] })
+Type error: Unhandled error: apply to not Pi
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
index 77fed39..8b729a4 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -1,21 +1 @@
-Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF {
- value: AppliedBuiltin(
- Natural,
- [],
- [],
- NzEnv {
- items: [],
- },
- ),
- type: Type,
-} != Value@WHNF {
- value: AppliedBuiltin(
- Bool,
- [],
- [],
- NzEnv {
- items: [],
- },
- ),
- type: Type,
-}
+Type error: Unhandled error: MergeHandlerTypeMismatch
diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
index 6b3f8dc..8b729a4 100644
--- a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
@@ -1,63 +1 @@
-Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF {
- value: AppliedBuiltin(
- Bool,
- [],
- [],
- NzEnv {
- items: [
- Replaced(
- Value@Unevaled {
- value: Var(
- Fresh(
- 119,
- ),
- ),
- type: Value@WHNF {
- value: AppliedBuiltin(
- Bool,
- [],
- [],
- NzEnv {
- items: [],
- },
- ),
- type: Type,
- },
- },
- ),
- ],
- },
- ),
- type: Type,
-} != Value@WHNF {
- value: AppliedBuiltin(
- Natural,
- [],
- [],
- NzEnv {
- items: [
- Replaced(
- Value@Unevaled {
- value: Var(
- Fresh(
- 120,
- ),
- ),
- type: Value@WHNF {
- value: AppliedBuiltin(
- Natural,
- [],
- [],
- NzEnv {
- items: [],
- },
- ),
- type: Type,
- },
- },
- ),
- ],
- },
- ),
- type: Type,
-}
+Type error: Unhandled error: MergeHandlerTypeMismatch