Make most type errors stringy

60 files changed, 159 insertions, 263 deletions

diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 850a792..5330c59 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -3,7 +3,7 @@ use std::io::Error as IOError;
 use crate::semantics::core::value::Value;
 use crate::semantics::phase::resolve::ImportStack;
 use crate::semantics::phase::NormalizedExpr;
-use crate::syntax::{BinOp, Import, Label, ParseError, Span};
+use crate::syntax::{Import, Label, ParseError, Span};
 
 pub type Result<T> = std::result::Result<T, Error>;
 
@@ -48,41 +48,41 @@ pub(crate) enum TypeMessage {
     UnboundVariable(Span),
     InvalidInputType(Value),
     InvalidOutputType(Value),
-    NotAFunction(Value),
-    TypeMismatch(Value, Value, Value),
-    AnnotMismatch(Value, Value),
-    InvalidListElement(usize, Value, Value),
-    InvalidListType(Value),
-    InvalidOptionalType(Value),
-    InvalidPredicate(Value),
-    IfBranchMismatch(Value, Value),
-    IfBranchMustBeTerm(bool, Value),
+    // NotAFunction(Value),
+    // TypeMismatch(Value, Value, Value),
+    // AnnotMismatch(Value, Value),
+    // InvalidListElement(usize, Value, Value),
+    // InvalidListType(Value),
+    // InvalidOptionalType(Value),
+    // InvalidPredicate(Value),
+    // IfBranchMismatch(Value, Value),
+    // IfBranchMustBeTerm(bool, Value),
     InvalidFieldType(Label, Value),
-    NotARecord(Label, Value),
-    MustCombineRecord(Value),
-    MissingRecordField(Label, Value),
-    MissingUnionField(Label, Value),
-    BinOpTypeMismatch(BinOp, Value),
-    InvalidTextInterpolation(Value),
-    Merge1ArgMustBeRecord(Value),
-    Merge2ArgMustBeUnionOrOptional(Value),
-    MergeEmptyNeedsAnnotation,
-    MergeHandlerMissingVariant(Label),
-    MergeVariantMissingHandler(Label),
-    MergeAnnotMismatch,
-    MergeHandlerTypeMismatch,
-    MergeHandlerReturnTypeMustNotBeDependent,
-    ProjectionMustBeRecord,
-    ProjectionMissingEntry,
-    ProjectionDuplicateField,
+    // NotARecord(Label, Value),
+    // MustCombineRecord(Value),
+    // MissingRecordField(Label, Value),
+    // MissingUnionField(Label, Value),
+    // BinOpTypeMismatch(BinOp, Value),
+    // InvalidTextInterpolation(Value),
+    // Merge1ArgMustBeRecord(Value),
+    // Merge2ArgMustBeUnionOrOptional(Value),
+    // MergeEmptyNeedsAnnotation,
+    // MergeHandlerMissingVariant(Label),
+    // MergeVariantMissingHandler(Label),
+    // MergeAnnotMismatch,
+    // MergeHandlerTypeMismatch,
+    // MergeHandlerReturnTypeMustNotBeDependent,
+    // ProjectionMustBeRecord,
+    // ProjectionMissingEntry,
+    // ProjectionDuplicateField,
     Sort,
     RecordTypeDuplicateField,
-    RecordTypeMergeRequiresRecordType(Value),
+    // RecordTypeMergeRequiresRecordType(Value),
     UnionTypeDuplicateField,
-    EquivalenceArgumentMustBeTerm(bool, Value),
-    EquivalenceTypeMismatch(Value, Value),
-    AssertMismatch(Value, Value),
-    AssertMustTakeEquivalence,
+    // EquivalenceArgumentMustBeTerm(bool, Value),
+    // EquivalenceTypeMismatch(Value, Value),
+    // AssertMismatch(Value, Value),
+    // AssertMustTakeEquivalence,
     Custom(String),
 }
 
@@ -103,21 +103,22 @@ impl std::fmt::Display for TypeError {
             InvalidOutputType(v) => {
                 v.span().error("Type error: Invalid function output")
             }
-            NotAFunction(v) => v.span().error("Type error: Not a function"),
-            TypeMismatch(x, y, z) => {
-                x.span()
-                    .error("Type error: Wrong type of function argument")
-                    + "\n"
-                    + &z.span().error(format!(
-                        "This argument has type {:?}",
-                        z.get_type().unwrap()
-                    ))
-                    + "\n"
-                    + &y.span().error(format!(
-                        "But the function expected an argument of type {:?}",
-                        y
-                    ))
-            }
+            // NotAFunction(v) => v.span().error("Type error: Not a function"),
+            // TypeMismatch(x, y, z) => {
+            //     x.span()
+            //         .error("Type error: Wrong type of function argument")
+            //         + "\n"
+            //         + &z.span().error(format!(
+            //             "This argument has type {:?}",
+            //             z.get_type().unwrap()
+            //         ))
+            //         + "\n"
+            //         + &y.span().error(format!(
+            //             "But the function expected an argument of type {:?}",
+            //             y
+            //         ))
+            // }
+            Custom(s) => format!("Type error: Unhandled error: {}", s),
             _ => format!("Type error: Unhandled error: {:?}", self.message),
         };
         write!(f, "{}", msg)
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 0f3754e..44678cd 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -357,8 +357,8 @@ fn type_last_layer(
     use syntax::Builtin::*;
     use syntax::Const::Type;
     use syntax::ExprKind::*;
-    use TypeMessage::*;
-    let mkerr = |msg: TypeMessage| Err(TypeError::new(msg));
+    let mkerr =
+        |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string())));
 
     /// Intermediary return type
     enum Ret {
@@ -381,10 +381,10 @@ fn type_last_layer(
             let tf_borrow = tf.as_whnf();
             let (tx, tb) = match &*tf_borrow {
                 ValueKind::Pi(_, tx, tb) => (tx, tb),
-                _ => return mkerr(NotAFunction(f.clone())),
+                _ => return mkerr("NotAFunction"),
             };
             if &a.get_type()? != tx {
-                return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
+                return mkerr("TypeMismatch");
             }
 
             let ret = tb.subst_shift(&AlphaVar::default(), a);
@@ -393,35 +393,33 @@ fn type_last_layer(
         }
         Annot(x, t) => {
             if &x.get_type()? != t {
-                return mkerr(AnnotMismatch(x.clone(), t.clone()));
+                return mkerr("AnnotMismatch");
             }
             RetWhole(x.clone())
         }
         Assert(t) => {
             match &*t.as_whnf() {
                 ValueKind::Equivalence(x, y) if x == y => {}
-                ValueKind::Equivalence(x, y) => {
-                    return mkerr(AssertMismatch(x.clone(), y.clone()))
-                }
-                _ => return mkerr(AssertMustTakeEquivalence),
+                ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
+                _ => return mkerr("AssertMustTakeEquivalence"),
             }
             RetTypeOnly(t.clone())
         }
         BoolIf(x, y, z) => {
             if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
-                return mkerr(InvalidPredicate(x.clone()));
+                return mkerr("InvalidPredicate");
             }
 
             if y.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(IfBranchMustBeTerm(true, y.clone()));
+                return mkerr("IfBranchMustBeTerm");
             }
 
             if z.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(IfBranchMustBeTerm(false, z.clone()));
+                return mkerr("IfBranchMustBeTerm");
             }
 
             if y.get_type()? != z.get_type()? {
-                return mkerr(IfBranchMismatch(y.clone(), z.clone()));
+                return mkerr("IfBranchMismatch");
             }
 
             RetTypeOnly(y.get_type()?)
@@ -433,7 +431,7 @@ fn type_last_layer(
                 {
                     args[0].clone()
                 }
-                _ => return mkerr(InvalidListType(t.clone())),
+                _ => return mkerr("InvalidListType"),
             };
             RetWhole(Value::from_kind_and_type(
                 ValueKind::EmptyListLit(arg),
@@ -443,18 +441,14 @@ fn type_last_layer(
         NEListLit(xs) => {
             let mut iter = xs.iter().enumerate();
             let (_, x) = iter.next().unwrap();
-            for (i, y) in iter {
+            for (_, y) in iter {
                 if x.get_type()? != y.get_type()? {
-                    return mkerr(InvalidListElement(
-                        i,
-                        x.get_type()?,
-                        y.clone(),
-                    ));
+                    return mkerr("InvalidListElement");
                 }
             }
             let t = x.get_type()?;
             if t.get_type()?.as_const() != Some(Type) {
-                return mkerr(InvalidListType(t));
+                return mkerr("InvalidListType");
             }
 
             RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t))
@@ -462,7 +456,7 @@ fn type_last_layer(
         SomeLit(x) => {
             let t = x.get_type()?;
             if t.get_type()?.as_const() != Some(Type) {
-                return mkerr(InvalidOptionalType(t));
+                return mkerr("InvalidOptionalType");
             }
 
             RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t))
@@ -479,48 +473,25 @@ fn type_last_layer(
         Field(r, x) => {
             match &*r.get_type()?.as_whnf() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
-                    Some(tth) => {
-                        RetTypeOnly(tth.clone())
-                    },
-                    None => return mkerr(MissingRecordField(x.clone(),
-                                        r.clone())),
+                    Some(tth) => RetTypeOnly(tth.clone()),
+                    None => return mkerr("MissingRecordField"),
                 },
                 // TODO: branch here only when r.get_type() is a Const
                 _ => {
                     match &*r.as_whnf() {
                         ValueKind::UnionType(kts) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
-                            Some(Some(t)) => {
-                                RetTypeOnly(
-                                    tck_pi_type(
-                                        ctx.new_binder(x),
-                                        t.clone(),
-                                        r.under_binder(),
-                                    )?
-                                )
-                            },
-                            Some(None) => {
-                                RetTypeOnly(r.clone())
-                            },
-                            None => {
-                                return mkerr(MissingUnionField(
-                                    x.clone(),
-                                    r.clone(),
-                                ))
-                            },
-                        },
-                        _ => {
-                            return mkerr(NotARecord(
-                                x.clone(),
-                                r.clone()
-                            ))
+                            Some(Some(t)) => RetTypeOnly(tck_pi_type(
+                                ctx.new_binder(x),
+                                t.clone(),
+                                r.under_binder(),
+                            )?),
+                            Some(None) => RetTypeOnly(r.clone()),
+                            None => return mkerr("MissingUnionField"),
                         },
+                        _ => return mkerr("NotARecord"),
                     }
-                }
-                // _ => mkerr(NotARecord(
-                //     x,
-                //     r?,
-                // )),
+                } // _ => mkerr("NotARecord"),
             }
         }
         Const(c) => RetWhole(const_to_value(*c)),
@@ -535,7 +506,7 @@ fn type_last_layer(
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
                     if x.get_type()? != text_type {
-                        return mkerr(InvalidTextInterpolation(x.clone()));
+                        return mkerr("InvalidTextInterpolation");
                     }
                 }
             }
@@ -549,14 +520,14 @@ fn type_last_layer(
             let l_type_borrow = l_type.as_whnf();
             let kts_x = match &*l_type_borrow {
                 ValueKind::RecordType(kts) => kts,
-                _ => return mkerr(MustCombineRecord(l.clone())),
+                _ => return mkerr("MustCombineRecord"),
             };
 
             // Extract the RHS record type
             let r_type_borrow = r_type.as_whnf();
             let kts_y = match &*r_type_borrow {
                 ValueKind::RecordType(kts) => kts,
-                _ => return mkerr(MustCombineRecord(r.clone())),
+                _ => return mkerr("MustCombineRecord"),
             };
 
             // Union the two records, prefering
@@ -584,18 +555,14 @@ fn type_last_layer(
             let borrow_l = l.as_whnf();
             let kts_x = match &*borrow_l {
                 ValueKind::RecordType(kts) => kts,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
-                }
+                _ => return mkerr("RecordTypeMergeRequiresRecordType"),
             };
 
             // Extract the RHS record type
             let borrow_r = r.as_whnf();
             let kts_y = match &*borrow_r {
                 ValueKind::RecordType(kts) => kts,
-                _ => {
-                    return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
-                }
+                _ => return mkerr("RecordTypeMergeRequiresRecordType"),
             };
 
             // Ensure that the records combine without a type error
@@ -618,28 +585,28 @@ fn type_last_layer(
 
             RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
         }
-        BinOp(o @ ListAppend, l, r) => {
+        BinOp(ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
                 ValueKind::AppliedBuiltin(List, _, _) => {}
-                _ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
+                _ => return mkerr("BinOpTypeMismatch"),
             }
 
             if l.get_type()? != r.get_type()? {
-                return mkerr(BinOpTypeMismatch(*o, r.clone()));
+                return mkerr("BinOpTypeMismatch");
             }
 
             RetTypeOnly(l.get_type()?)
         }
         BinOp(Equivalence, l, r) => {
             if l.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone()));
+                return mkerr("EquivalenceArgumentMustBeTerm");
             }
             if r.get_type()?.get_type()?.as_const() != Some(Type) {
-                return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone()));
+                return mkerr("EquivalenceArgumentMustBeTerm");
             }
 
             if l.get_type()? != r.get_type()? {
-                return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
+                return mkerr("EquivalenceTypeMismatch");
             }
 
             RetWhole(Value::from_kind_and_type(
@@ -665,11 +632,11 @@ fn type_last_layer(
             });
 
             if l.get_type()? != t {
-                return mkerr(BinOpTypeMismatch(*o, l.clone()));
+                return mkerr("BinOpTypeMismatch");
             }
 
             if r.get_type()? != t {
-                return mkerr(BinOpTypeMismatch(*o, r.clone()));
+                return mkerr("BinOpTypeMismatch");
             }
 
             RetTypeOnly(t)
@@ -679,7 +646,7 @@ fn type_last_layer(
             let record_borrow = record_type.as_whnf();
             let handlers = match &*record_borrow {
                 ValueKind::RecordType(kts) => kts,
-                _ => return mkerr(Merge1ArgMustBeRecord(record.clone())),
+                _ => return mkerr("Merge1ArgMustBeRecord"),
             };
 
             let union_type = union.get_type()?;
@@ -697,9 +664,7 @@ fn type_last_layer(
                     kts.insert("Some".into(), Some(ty.clone()));
                     Cow::Owned(kts)
                 }
-                _ => {
-                    return mkerr(Merge2ArgMustBeUnionOrOptional(union.clone()))
-                }
+                _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
             };
 
             let mut inferred_type = None;
@@ -711,19 +676,11 @@ fn type_last_layer(
                             let handler_type_borrow = handler_type.as_whnf();
                             let (tx, tb) = match &*handler_type_borrow {
                                 ValueKind::Pi(_, tx, tb) => (tx, tb),
-                                _ => {
-                                    return mkerr(NotAFunction(
-                                        handler_type.clone(),
-                                    ))
-                                }
+                                _ => return mkerr("NotAFunction"),
                             };
 
                             if variant_type != tx {
-                                return mkerr(TypeMismatch(
-                                    handler_type.clone(),
-                                    tx.clone(),
-                                    variant_type.clone(),
-                                ));
+                                return mkerr("TypeMismatch");
                             }
 
                             // Extract `tb` from under the binder. Fails if the variable was used
@@ -731,41 +688,39 @@ fn type_last_layer(
                             match tb.over_binder() {
                                 Some(x) => x,
                                 None => return mkerr(
-                                    MergeHandlerReturnTypeMustNotBeDependent,
+                                    "MergeHandlerReturnTypeMustNotBeDependent",
                                 ),
                             }
                         }
                         // Union alternative without type
                         Some(None) => handler_type.clone(),
-                        None => {
-                            return mkerr(MergeHandlerMissingVariant(x.clone()))
-                        }
+                        None => return mkerr("MergeHandlerMissingVariant"),
                     };
                 match &inferred_type {
                     None => inferred_type = Some(handler_return_type),
                     Some(t) => {
                         if t != &handler_return_type {
-                            return mkerr(MergeHandlerTypeMismatch);
+                            return mkerr("MergeHandlerTypeMismatch");
                         }
                     }
                 }
             }
             for x in variants.keys() {
                 if !handlers.contains_key(x) {
-                    return mkerr(MergeVariantMissingHandler(x.clone()));
+                    return mkerr("MergeVariantMissingHandler");
                 }
             }
 
             match (inferred_type, type_annot.as_ref()) {
                 (Some(t1), Some(t2)) => {
                     if &t1 != t2 {
-                        return mkerr(MergeAnnotMismatch);
+                        return mkerr("MergeAnnotMismatch");
                     }
                     RetTypeOnly(t1)
                 }
                 (Some(t), None) => RetTypeOnly(t),
                 (None, Some(t)) => RetTypeOnly(t.clone()),
-                (None, None) => return mkerr(MergeEmptyNeedsAnnotation),
+                (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
             }
         }
         ToMap(_, _) => unimplemented!("toMap"),
@@ -774,18 +729,18 @@ fn type_last_layer(
             let record_type_borrow = record_type.as_whnf();
             let kts = match &*record_type_borrow {
                 ValueKind::RecordType(kts) => kts,
-                _ => return mkerr(ProjectionMustBeRecord),
+                _ => return mkerr("ProjectionMustBeRecord"),
             };
 
             let mut new_kts = HashMap::new();
             for l in labels {
                 match kts.get(l) {
-                    None => return mkerr(ProjectionMissingEntry),
+                    None => return mkerr("ProjectionMissingEntry"),
                     Some(t) => {
                         use std::collections::hash_map::Entry;
                         match new_kts.entry(l.clone()) {
                             Entry::Occupied(_) => {
-                                return mkerr(ProjectionDuplicateField)
+                                return mkerr("ProjectionDuplicateField")
                             }
                             Entry::Vacant(e) => e.insert(t.clone()),
                         }
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 870388d..9342fd8 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1,8 +1 @@
-[unknown location] Type error: Wrong type of function argument
-[unknown location] This argument has type Sort
- --> 5:21
-  |
-5 | in  let pow = λ(X : Kind) → X → Type␊
-  |                     ^--^
-  |
-  = But the function expected an argument of type Kind
+Type error: Unhandled error: TypeMismatch
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
index 3f737c2..045eb98 100644
--- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): [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 })
+Type error: Unhandled error: AnnotMismatch
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
index d211716..045eb98 100644
--- a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("x"): [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 })
+Type error: Unhandled error: AnnotMismatch
diff --git a/dhall/tests/type-errors/unit/AssertDoubleZeros.txt b/dhall/tests/type-errors/unit/AssertDoubleZeros.txt
index 6886495..d8627ba 100644
--- a/dhall/tests/type-errors/unit/AssertDoubleZeros.txt
+++ b/dhall/tests/type-errors/unit/AssertDoubleZeros.txt
@@ -1 +1 @@
-Type error: Unhandled error: AssertMismatch(Value@WHNF { value: DoubleLit(NaiveDouble(-0.0)), type: Value@WHNF { value: AppliedBuiltin(Double, [], []), type: Type } }, Value@WHNF { value: DoubleLit(NaiveDouble(0.0)), type: Value@WHNF { value: AppliedBuiltin(Double, [], []), type: Type } })
+Type error: Unhandled error: AssertMismatch
diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
index 6f8e4a7..d8627ba 100644
--- a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
+++ b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
@@ -1 +1 @@
-Type error: Unhandled error: 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 } })
+Type error: Unhandled error: AssertMismatch
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
index bdbe0e4..89749e9 100644
--- a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
+++ b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
@@ -1 +1 @@
-Type error: Unhandled error: 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 } })
+Type error: Unhandled error: EquivalenceTypeMismatch
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
index 23b37d3..7c48d6f 100644
--- a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
+++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
@@ -1 +1 @@
-Type error: Unhandled error: EquivalenceArgumentMustBeTerm(true, Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: EquivalenceArgumentMustBeTerm
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index 8507ccf..9342fd8 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1,13 +1 @@
-[unknown location] Type error: Wrong type of function argument
- --> 1:22
-  |
-1 | (λ(_ : Natural) → _) True␊
-  |                      ^--^
-  |
-  = This argument has type Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }
- --> 1:8
-  |
-1 | (λ(_ : Natural) → _) True␊
-  |        ^-----^
-  |
-  = But the function expected an argument of type Value@NF { value: AppliedBuiltin(Natural, [], []), type: Type }
+Type error: Unhandled error: TypeMismatch
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index 062f9de..f1cdf92 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1,6 +1 @@
- --> 1:1
-  |
-1 | True True␊
-  | ^--^
-  |
-  = Type error: Not a function
+Type error: Unhandled error: NotAFunction
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
index 4d28695..6b1dcdd 100644
--- a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
+++ b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
@@ -1 +1 @@
-Type error: Unhandled error: 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 } })
+Type error: Unhandled error: IfBranchMismatch
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotType.txt b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
index 8ef3a40..06039a7 100644
--- a/dhall/tests/type-errors/unit/IfBranchesNotType.txt
+++ b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: IfBranchMustBeTerm(true, Type)
+Type error: Unhandled error: IfBranchMustBeTerm
diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt
index 665093f..b2d200c 100644
--- a/dhall/tests/type-errors/unit/IfNotBool.txt
+++ b/dhall/tests/type-errors/unit/IfNotBool.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidPredicate(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: InvalidPredicate
diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
index 61096d0..045eb98 100644
--- a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
+++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type })
+Type error: Unhandled error: AnnotMismatch
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index e075521..9342fd8 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1,13 +1 @@
- --> 1:6
-  |
-1 | [] : List Type␊
-  |      ^--^
-  |
-  = Type error: Wrong type of function argument
- --> 1:11
-  |
-1 | [] : List Type␊
-  |           ^--^
-  |
-  = This argument has type Kind
-[unknown location] But the function expected an argument of type Type
+Type error: Unhandled error: TypeMismatch
diff --git a/dhall/tests/type-errors/unit/ListLiteralNotType.txt b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
index 99b95a3..3937453 100644
--- a/dhall/tests/type-errors/unit/ListLiteralNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidListType(Type)
+Type error: Unhandled error: InvalidListType
diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
index 2355b7c..a64cf67 100644
--- a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidListElement(1, Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: InvalidListElement
diff --git a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
index d4e9024..711d77d 100644
--- a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
+++ b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
@@ -1 +1 @@
-Type error: Unhandled error: MergeVariantMissingHandler(Label("x"))
+Type error: Unhandled error: MergeVariantMissingHandler
diff --git a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
index 7da5cb9..4c72653 100644
--- a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
+++ b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: UnionType({}), type: Type })
+Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional
diff --git a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
index 7da5cb9..4c72653 100644
--- a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
+++ b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
@@ -1 +1 @@
-Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: UnionType({}), type: Type })
+Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
index c5ed223..f1cdf92 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -1 +1 @@
-[unknown location] Type error: Not a function
+Type error: Unhandled error: NotAFunction
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
index 7da5cb9..4c72653 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
@@ -1 +1 @@
-Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: UnionType({}), type: Type })
+Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
index 19f375a..9342fd8 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -1,13 +1 @@
-[unknown location] Type error: Wrong type of function argument
- --> 1:38
-  |
-1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)␊
-  |                                      ^-----^
-  |
-  = This argument has type Type
- --> 1:19
-  |
-1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)␊
-  |                   ^--^
-  |
-  = But the function expected an argument of type Value@NF { value: AppliedBuiltin(Bool, [], []), type: Type }
+Type error: Unhandled error: TypeMismatch
diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
index 785fc63..d151710 100644
--- a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
+++ b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
@@ -1 +1 @@
-Type error: Unhandled error: Merge1ArgMustBeRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: Merge1ArgMustBeRecord
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
index d4e9024..711d77d 100644
--- a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
@@ -1 +1 @@
-Type error: Unhandled error: MergeVariantMissingHandler(Label("x"))
+Type error: Unhandled error: MergeVariantMissingHandler
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
index d583de7..711d77d 100644
--- a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
@@ -1 +1 @@
-Type error: Unhandled error: MergeVariantMissingHandler(Label("y"))
+Type error: Unhandled error: MergeVariantMissingHandler
diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
index 8954538..4c72653 100644
--- a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
+++ b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
@@ -1 +1 @@
-Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: Merge2ArgMustBeUnionOrOptional
diff --git a/dhall/tests/type-errors/unit/MergeUnusedHandler.txt b/dhall/tests/type-errors/unit/MergeUnusedHandler.txt
index b7eefdd..a429b89 100644
--- a/dhall/tests/type-errors/unit/MergeUnusedHandler.txt
+++ b/dhall/tests/type-errors/unit/MergeUnusedHandler.txt
@@ -1 +1 @@
-Type error: Unhandled error: MergeHandlerMissingVariant(Label("y"))
+Type error: Unhandled error: MergeHandlerMissingVariant
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 784fd8a..9342fd8 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1,13 +1 @@
- --> 1:1
-  |
-1 | Natural/subtract True True␊
-  | ^--------------^
-  |
-  = Type error: Wrong type of function argument
- --> 1:18
-  |
-1 | Natural/subtract True True␊
-  |                  ^--^
-  |
-  = This argument has type Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type }
-[unknown location] But the function expected an argument of type Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type }
+Type error: Unhandled error: TypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
index b9314fb..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
+++ b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(BoolAnd, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
index 253e2f2..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
+++ b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(BoolEQ, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
index 735d101..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
index b931c01..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
@@ -1 +1 @@
-Type error: Unhandled error: 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 }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
index 735d101..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
index 735d101..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(ListAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
index c3c83b1..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
+++ b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(BoolNE, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
index 32caf35..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
+++ b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(BoolOr, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
index 4e578c4..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
+++ b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(NaturalPlus, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
index 58d4b23..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
index 58d4b23..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(TextAppend, Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
index 8caf338..9f10587 100644
--- a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
+++ b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
@@ -1 +1 @@
-Type error: Unhandled error: BinOpTypeMismatch(NaturalTimes, Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: BinOpTypeMismatch
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
index e524a07..3937453 100644
--- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidListType(Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type })
+Type error: Unhandled error: InvalidListType
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
index 5ff6a69..045eb98 100644
--- a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -1 +1 @@
-Type error: Unhandled error: 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 }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type } }, Value@WHNF { value: AppliedBuiltin(Optional, [Value@Unevaled { value: AppliedBuiltin(Natural, [], []), type: Type }], [Value@WHNF { value: Pi(Binder(`_`), Type, Type), type: Kind }]), type: Type })
+Type error: Unhandled error: AnnotMismatch
diff --git a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
index 1770faa..ea48374 100644
--- a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
+++ b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
@@ -1 +1 @@
-Type error: Unhandled error: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {}, size: 0 })), type: Value@WHNF { value: RecordType({}), type: Type } })
+Type error: Unhandled error: MissingRecordField
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
index 9211e05..ea48374 100644
--- a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
@@ -1 +1 @@
-Type error: Unhandled error: MissingRecordField(Label("x"), Value@Unevaled { value: PartialExpr(RecordLit(DupTreeMap { map: {Label("y"): [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 } })
+Type error: Unhandled error: MissingRecordField
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
index 292ab0e..35d604f 100644
--- a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
@@ -1 +1 @@
-Type error: Unhandled error: NotARecord(Label("x"), Value@WHNF { value: BoolLit(true), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: NotARecord
diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
index dff292e..35d604f 100644
--- a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
+++ b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
@@ -1 +1 @@
-Type error: Unhandled error: NotARecord(Label("x"), Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: NotARecord
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
index 27ed928..7fd03d3 100644
--- a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -1 +1 @@
-Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
index 27ed928..7fd03d3 100644
--- a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
@@ -1 +1 @@
-Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
index 27ed928..7fd03d3 100644
--- a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -1 +1 @@
-Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
index 27ed928..7fd03d3 100644
--- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
@@ -1 +1 @@
-Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
index 27ed928..7fd03d3 100644
--- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -1 +1 @@
-Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
index 27ed928..7fd03d3 100644
--- a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
@@ -1 +1 @@
-Type error: Unhandled error: RecordTypeMergeRequiresRecordType(Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: RecordTypeMergeRequiresRecordType
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
index fbb410f..42600a4 100644
--- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
@@ -1 +1 @@
-Type error: Unhandled error: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: MustCombineRecord
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
index fbb410f..42600a4 100644
--- a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
@@ -1 +1 @@
-Type error: Unhandled error: MustCombineRecord(Value@Unevaled { value: PartialExpr(BoolLit(true)), type: Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type } })
+Type error: Unhandled error: MustCombineRecord
diff --git a/dhall/tests/type-errors/unit/SomeNotType.txt b/dhall/tests/type-errors/unit/SomeNotType.txt
index 43581a0..63fec72 100644
--- a/dhall/tests/type-errors/unit/SomeNotType.txt
+++ b/dhall/tests/type-errors/unit/SomeNotType.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidOptionalType(Type)
+Type error: Unhandled error: InvalidOptionalType
diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
index feb6b2e..f1a77d9 100644
--- a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
+++ b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
@@ -1 +1 @@
-Type error: Unhandled error: InvalidTextInterpolation(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } })
+Type error: Unhandled error: InvalidTextInterpolation
diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
index 869e9c3..045eb98 100644
--- a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
+++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
@@ -1 +1 @@
-Type error: Unhandled error: AnnotMismatch(Value@Unevaled { value: PartialExpr(NaturalLit(1)), type: Value@WHNF { value: AppliedBuiltin(Natural, [], []), type: Type } }, Value@WHNF { value: AppliedBuiltin(Bool, [], []), type: Type })
+Type error: Unhandled error: AnnotMismatch
diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
index eb3e09a..f88cb57 100644
--- a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
+++ b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
@@ -1 +1 @@
-Type error: Unhandled error: MissingUnionField(Label("y"), Value@WHNF { value: UnionType({Label("x"): Some(Value@Unevaled { value: AppliedBuiltin(Bool, [], []), type: Type })}), type: Type })
+Type error: Unhandled error: MissingUnionField