Test type error messages

89 files changed, 150 insertions, 8 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index c7d339c..337480f 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -394,5 +394,34 @@ fn main() -> std::io::Result<()> {
         },
     )?;
 
+    make_test_module(
+        &mut file,
+        TestFeature {
+            module_name: "type_error",
+            directory: spec_tests_dir.join("type-inference/failure/"),
+            variant: "TypeError",
+            path_filter: |path: &str| {
+                false
+                    // TODO: Enable imports in typecheck tests
+                    || path == "importBoundary"
+                    || path == "customHeadersUsingBoundVariable"
+                    // TODO: projection by expression
+                    || path == "unit/RecordProjectionByTypeFieldTypeMismatch"
+                    || path == "unit/RecordProjectionByTypeNotPresent"
+                    // TODO: toMap
+                    || path == "unit/EmptyToMap"
+                    || path == "unit/HeterogenousToMap"
+                    || path == "unit/MistypedToMap1"
+                    || path == "unit/MistypedToMap2"
+                    || path == "unit/MistypedToMap3"
+                    || path == "unit/MistypedToMap4"
+                    || path == "unit/NonRecordToMap"
+                    || path == "unit/ToMapWrongKind"
+            },
+            input_type: FileType::Text,
+            output_type: None,
+        },
+    )?;
+
     Ok(())
 }
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index b98489f..9790b95 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -21,7 +21,7 @@ right: `{}`"#,
 }
 
 use std::fs::File;
-use std::io::Read;
+use std::io::{Read, Write};
 use std::path::PathBuf;
 
 use crate::error::{Error, Result};
@@ -40,6 +40,7 @@ pub enum Test<'a> {
     ImportFailure(&'a str),
     TypeInferenceSuccess(&'a str, &'a str),
     TypeInferenceFailure(&'a str),
+    TypeError(&'a str),
     Normalization(&'a str, &'a str),
     AlphaNormalization(&'a str, &'a str),
 }
@@ -144,13 +145,38 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             assert_eq_display!(ty, expected);
         }
         TypeInferenceFailure(file_path) => {
-            let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck();
-            match res {
-                Err(_) => {}
-                // If e did typecheck, check that it doesn't have a type
-                Ok(e) => {
-                    e.get_type().unwrap_err();
-                }
+            let mut res =
+                parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+            if let Ok(e) = &res {
+                // If e did typecheck, check that get_type fails
+                res = e.get_type();
+            }
+            res.unwrap_err();
+        }
+        TypeError(file_path) => {
+            let mut res =
+                parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+            let file_path = PathBuf::from(file_path);
+            let error_file_path = file_path
+                .strip_prefix("../dhall-lang/tests/type-inference/failure/")
+                .unwrap();
+            let error_file_path =
+                PathBuf::from("tests/type-errors/").join(error_file_path);
+            let error_file_path = error_file_path.with_extension("txt");
+            if let Ok(e) = &res {
+                // If e did typecheck, check that get_type fails
+                res = e.get_type();
+            }
+            let err: Error = res.unwrap_err().into();
+
+            if error_file_path.is_file() {
+                let expected_msg = std::fs::read_to_string(error_file_path)?;
+                let msg = format!("{}\n", err);
+                assert_eq_pretty!(msg, expected_msg);
+            } else {
+                std::fs::create_dir_all(error_file_path.parent().unwrap())?;
+                let mut file = File::create(error_file_path)?;
+                writeln!(file, "{}", err)?;
             }
         }
         Normalization(expr_file_path, expected_file_path) => {
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
new file mode 100644
index 0000000..398ca09
--- /dev/null
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -0,0 +1 @@
+TypeError { type_message: TypeMismatch(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Kind, Value@Unevaled { value: Pi(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind })), type: Kind })), type: Kind }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind }), type: Kind }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind })), type: Kind })), type: Kind }), type: Kind }), type: Sort }), context: TypecheckContext([(Label("bottom"), Replaced(Value@Unevaled { value: Pi(AlphaLabel(any), Type, Value@Unevaled { value: Var(AlphaVar(any, 0)), type: Type }), type: Type })), (Label("not"), Replaced(Value@Unevaled { value: Lam(AlphaLabel(p), Type, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(p, 0)), type: Type }, Value@Unevaled { value: Pi(AlphaLabel(any), Type, Value@Unevaled { value: Var(AlphaVar(any, 0)), type: Type }), type: Type }), type: Type }), type: Value@WHNF { value: Pi(AlphaLabel(p), Type, Type), type: Kind } })), (Label("pow"), Replaced(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } })), (Label("U"), Replaced(Value@Unevaled { value: Pi(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind })), type: Kind })), type: Kind }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind }), type: Kind }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: PartialExpr(App(Value@Unevaled { value: Lam(AlphaLabel(X), Kind, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: Var(AlphaVar(X, 0)), type: Kind }, Type), type: Kind }), type: Value@WHNF { value: Pi(AlphaLabel(X), Kind, Kind), type: Sort } }, Value@Unevaled { value: Var(AlphaVar(X, 1)), type: Kind })), type: Kind })), type: Kind }), type: Kind }), type: Sort }))]) }
diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt
new file mode 100644
index 0000000..e163733
--- /dev/null
+++ b/dhall/tests/type-errors/mixedUnions.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidFieldType(Label("Right"), Type), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/recordOfKind.txt b/dhall/tests/type-errors/recordOfKind.txt
new file mode 100644
index 0000000..37111df
--- /dev/null
+++ b/dhall/tests/type-errors/recordOfKind.txt
@@ -0,0 +1 @@
+TypeError { type_message: Sort, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
new file mode 100644
index 0000000..57ebd63
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
@@ -0,0 +1 @@
+TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): One(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type } })}, size: 1 })), type: Value@WHNF { value: RecordType({Label("x"): Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }}), type: Type } }, Value@WHNF { value: RecordType({Label("y"): Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }}), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
new file mode 100644
index 0000000..e829fbd
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
@@ -0,0 +1 @@
+TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): One(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } })}, size: 1 })), type: Value@WHNF { value: RecordType({Label("x"): Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }}), type: Type } }, Value@WHNF { value: RecordType({Label("x"): Value@WHNF { value: AppliedBuiltin(Text, []), type: Type }}), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
new file mode 100644
index 0000000..78d25d8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -0,0 +1 @@
+TypeError { type_message: UnboundVariable(V(Label("_"), 0)), context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }))]) }
diff --git a/dhall/tests/type-errors/unit/AssertNotEquivalence.txt b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt
new file mode 100644
index 0000000..d2aa197
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt
@@ -0,0 +1 @@
+TypeError { type_message: AssertMustTakeEquivalence, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
new file mode 100644
index 0000000..caf115d
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
@@ -0,0 +1 @@
+TypeError { type_message: AssertMismatch(Value@WHNF { value: NaturalLit(1), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }, Value@WHNF { value: NaturalLit(2), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
new file mode 100644
index 0000000..ca31211
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
@@ -0,0 +1 @@
+TypeError { type_message: EquivalenceTypeMismatch(Value@Unevaled { value: PartialExpr(BoolLit(false)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
new file mode 100644
index 0000000..2ee2629
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
@@ -0,0 +1 @@
+TypeError { type_message: EquivalenceArgumentMustBeTerm(true, Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
new file mode 100644
index 0000000..61cd80c
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -0,0 +1 @@
+TypeError { type_message: TypeMismatch(Value@Unevaled { value: Lam(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: Var(AlphaVar(`_`, 0)), type: Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type } }), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
new file mode 100644
index 0000000..0ea727a
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -0,0 +1 @@
+TypeError { type_message: NotAFunction(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
new file mode 100644
index 0000000..77e88e8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidInputType(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
new file mode 100644
index 0000000..65825de
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidInputType(Value@Unevaled { value: PartialExpr(NaturalLit(2)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt
new file mode 100644
index 0000000..37111df
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt
@@ -0,0 +1 @@
+TypeError { type_message: Sort, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt
new file mode 100644
index 0000000..37111df
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt
@@ -0,0 +1 @@
+TypeError { type_message: Sort, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
new file mode 100644
index 0000000..f9e5a8a
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
@@ -0,0 +1 @@
+TypeError { type_message: IfBranchMismatch(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }, Value@Unevaled { value: PartialExpr(TextLit(InterpolatedText { head: "", tail: [] })), type: Value@WHNF { value: AppliedBuiltin(Text, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotType.txt b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
new file mode 100644
index 0000000..a906556
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
@@ -0,0 +1 @@
+TypeError { type_message: IfBranchMustBeTerm(true, Type), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt
new file mode 100644
index 0000000..49c0522
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfNotBool.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidPredicate(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
new file mode 100644
index 0000000..f44f646
--- /dev/null
+++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
@@ -0,0 +1 @@
+TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
new file mode 100644
index 0000000..2808281
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -0,0 +1 @@
+TypeError { type_message: TypeMismatch(Value@Unevaled { value: AppliedBuiltin(List, []), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Type, Type), type: Kind } }, Type, Type), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/ListLiteralNotType.txt b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
new file mode 100644
index 0000000..7c2565d
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidListType(Type), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
new file mode 100644
index 0000000..d7bb559
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidListElement(1, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
new file mode 100644
index 0000000..b2ecee8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeVariantMissingHandler(Label("x")), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt
new file mode 100644
index 0000000..194cb5e
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeAnnotMismatch, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
new file mode 100644
index 0000000..0ecd67a
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
@@ -0,0 +1 @@
+TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt
new file mode 100644
index 0000000..611abfb
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeEmptyNeedsAnnotation, context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@WHNF { value: UnionType({}), type: Type }))]) }
diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt
new file mode 100644
index 0000000..611abfb
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeEmptyNeedsAnnotation, context: TypecheckContext([(Label("x"), Kept(AlphaVar(x, 0), Value@WHNF { value: UnionType({}), type: Type }))]) }
diff --git a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
new file mode 100644
index 0000000..0ecd67a
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
@@ -0,0 +1 @@
+TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
new file mode 100644
index 0000000..ebc53e2
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeHandlerReturnTypeMustNotBeDependent, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
new file mode 100644
index 0000000..3555147
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -0,0 +1 @@
+TypeError { type_message: NotAFunction(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
new file mode 100644
index 0000000..0ecd67a
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
@@ -0,0 +1 @@
+TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: UnionType({}), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
new file mode 100644
index 0000000..6003f32
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -0,0 +1 @@
+TypeError { type_message: TypeMismatch(Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), type: Type }, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
new file mode 100644
index 0000000..2e03930
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeHandlerTypeMismatch, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
new file mode 100644
index 0000000..d0feb80
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
@@ -0,0 +1 @@
+TypeError { type_message: Merge1ArgMustBeRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
new file mode 100644
index 0000000..b2ecee8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeVariantMissingHandler(Label("x")), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
new file mode 100644
index 0000000..daa1668
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
@@ -0,0 +1 @@
+TypeError { type_message: MergeVariantMissingHandler(Label("y")), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
new file mode 100644
index 0000000..3c0edc2
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
@@ -0,0 +1 @@
+TypeError { type_message: Merge2ArgMustBeUnion(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
new file mode 100644
index 0000000..f2c1d54
--- /dev/null
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -0,0 +1 @@
+TypeError { type_message: TypeMismatch(Value@Unevaled { value: AppliedBuiltin(NaturalSubtract, []), type: Value@WHNF { value: Pi(AlphaLabel(`_`), Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: Pi(AlphaLabel(`_`), Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }), type: Type }), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
new file mode 100644
index 0000000..4c1b625
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(BoolAnd, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
new file mode 100644
index 0000000..fa484e1
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(BoolEQ, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
new file mode 100644
index 0000000..6a5e164
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
new file mode 100644
index 0000000..dd0e6fc
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NEListLit([Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }])), type: Value@WHNF { value: AppliedBuiltin(List, [Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type }]), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
new file mode 100644
index 0000000..6a5e164
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
new file mode 100644
index 0000000..6a5e164
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
new file mode 100644
index 0000000..7aed0a1
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(BoolNE, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
new file mode 100644
index 0000000..031600c
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(BoolOr, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
new file mode 100644
index 0000000..cb055e8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(NaturalPlus, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
new file mode 100644
index 0000000..aa1d741
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
new file mode 100644
index 0000000..aa1d741
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
new file mode 100644
index 0000000..95f6dda
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
@@ -0,0 +1 @@
+TypeError { type_message: BinOpTypeMismatch(NaturalTimes, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
new file mode 100644
index 0000000..6e3a002
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidListType(Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }]), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
new file mode 100644
index 0000000..f8a4bd0
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -0,0 +1 @@
+TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(NEListLit([Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type } }])), type: Value@WHNF { value: AppliedBuiltin(List, [Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }]), type: Type } }, Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Natural, []), type: Type }]), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt
new file mode 100644
index 0000000..bda01cc
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeDuplicateField, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordMixedKinds3.txt b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt
new file mode 100644
index 0000000..37111df
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt
@@ -0,0 +1 @@
+TypeError { type_message: Sort, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt
new file mode 100644
index 0000000..e0df8ad
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt
@@ -0,0 +1 @@
+TypeError { type_message: ProjectionMissingEntry, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt
new file mode 100644
index 0000000..e0df8ad
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt
@@ -0,0 +1 @@
+TypeError { type_message: ProjectionMissingEntry, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt
new file mode 100644
index 0000000..1e0607a
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt
@@ -0,0 +1 @@
+TypeError { type_message: ProjectionMustBeRecord, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
new file mode 100644
index 0000000..73b8483
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
@@ -0,0 +1 @@
+TypeError { type_message: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {}, size: 0 })), type: Value@WHNF { value: RecordType({}), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
new file mode 100644
index 0000000..036b1c9
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
@@ -0,0 +1 @@
+TypeError { type_message: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("y"): One(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {}, size: 0 })), type: Value@Unevaled { value: RecordType({}), type: Type } })}, size: 1 })), type: Value@WHNF { value: RecordType({Label("y"): Value@Unevaled { value: RecordType({}), type: Type }}), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
new file mode 100644
index 0000000..ed34e38
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
@@ -0,0 +1 @@
+TypeError { type_message: NotARecord(Label("x"), Value@WHNF { value: BoolLit(true), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
new file mode 100644
index 0000000..8c7b9ae
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
@@ -0,0 +1 @@
+TypeError { type_message: NotARecord(Label("x"), Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt
new file mode 100644
index 0000000..bda01cc
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeDuplicateField, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
new file mode 100644
index 0000000..2829d96
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..2cde255
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
new file mode 100644
index 0000000..2cde255
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..2cde255
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
new file mode 100644
index 0000000..2cde255
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
new file mode 100644
index 0000000..2cde255
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
new file mode 100644
index 0000000..2cde255
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
@@ -0,0 +1 @@
+TypeError { type_message: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..9c34fe3
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
@@ -0,0 +1 @@
+TypeError { type_message: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt
new file mode 100644
index 0000000..37111df
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -0,0 +1 @@
+TypeError { type_message: Sort, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt
new file mode 100644
index 0000000..37111df
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -0,0 +1 @@
+TypeError { type_message: Sort, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..9c34fe3
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
@@ -0,0 +1 @@
+TypeError { type_message: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/SomeNotType.txt b/dhall/tests/type-errors/unit/SomeNotType.txt
new file mode 100644
index 0000000..7502c06
--- /dev/null
+++ b/dhall/tests/type-errors/unit/SomeNotType.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidOptionalType(Type), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/Sort.txt b/dhall/tests/type-errors/unit/Sort.txt
new file mode 100644
index 0000000..37111df
--- /dev/null
+++ b/dhall/tests/type-errors/unit/Sort.txt
@@ -0,0 +1 @@
+TypeError { type_message: Sort, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
new file mode 100644
index 0000000..fefa10f
--- /dev/null
+++ b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidTextInterpolation(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
new file mode 100644
index 0000000..142d81f
--- /dev/null
+++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
@@ -0,0 +1 @@
+TypeError { type_message: AnnotMismatch(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
new file mode 100644
index 0000000..22ddeec
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
@@ -0,0 +1 @@
+TypeError { type_message: MissingUnionField(Label("y"), Value@WHNF { value: UnionType({Label("x"): Some(Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type })}), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
new file mode 100644
index 0000000..db9a35a
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -0,0 +1 @@
+TypeError { type_message: UnboundVariable(V(Label("constructors"), 0)), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt
new file mode 100644
index 0000000..fcf31b5
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt
@@ -0,0 +1 @@
+TypeError { type_message: UnionTypeDuplicateField, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt
new file mode 100644
index 0000000..fcf31b5
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt
@@ -0,0 +1 @@
+TypeError { type_message: UnionTypeDuplicateField, context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
new file mode 100644
index 0000000..85e187e
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidFieldType(Label("y"), Type), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
new file mode 100644
index 0000000..85e187e
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidFieldType(Label("y"), Type), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
new file mode 100644
index 0000000..72210d5
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidFieldType(Label("y"), Value@Unevaled { value: AppliedBuiltin(Bool, []), type: Type }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
new file mode 100644
index 0000000..2829d96
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
@@ -0,0 +1 @@
+TypeError { type_message: InvalidFieldType(Label("x"), Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, []), type: Type } }), context: TypecheckContext([]) }
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
new file mode 100644
index 0000000..8787a2f
--- /dev/null
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -0,0 +1 @@
+TypeError { type_message: UnboundVariable(V(Label("x"), 0)), context: TypecheckContext([]) }