Merge pull request #114 from Nadrieril/nice-type-errors

Ground work for pretty type errors

98 files changed, 385 insertions, 125 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/core/value.rs b/dhall/src/core/value.rs
index b4b6b08..d4f5131 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -1,7 +1,7 @@
 use std::cell::{Ref, RefCell, RefMut};
 use std::rc::Rc;
 
-use dhall_syntax::{Builtin, Const};
+use dhall_syntax::{Builtin, Const, Span};
 
 use crate::core::context::TypecheckContext;
 use crate::core::valuef::ValueF;
@@ -36,6 +36,7 @@ struct ValueInternal {
     value: ValueF,
     /// This is None if and only if `value` is `Sort` (which doesn't have a type)
     ty: Option<Value>,
+    span: Span,
 }
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
@@ -69,18 +70,21 @@ impl ValueInternal {
                 form: Unevaled,
                 value: ValueF::Const(Const::Type),
                 ty: None,
+                span: Span::Artificial,
             },
             |vint| match (&vint.form, &vint.ty) {
                 (Unevaled, Some(ty)) => ValueInternal {
                     form: WHNF,
                     value: normalize_whnf(vint.value, &ty),
                     ty: vint.ty,
+                    span: vint.span,
                 },
                 // `value` is `Sort`
                 (Unevaled, None) => ValueInternal {
                     form: NF,
                     value: ValueF::Const(Const::Sort),
                     ty: None,
+                    span: vint.span,
                 },
                 // Already in WHNF
                 (WHNF, _) | (NF, _) => vint,
@@ -113,11 +117,12 @@ impl ValueInternal {
 }
 
 impl Value {
-    fn new(value: ValueF, form: Form, ty: Value) -> Value {
+    fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value {
         ValueInternal {
             form,
             value,
             ty: Some(ty),
+            span,
         }
         .into_value()
     }
@@ -126,14 +131,22 @@ impl Value {
             form: NF,
             value: ValueF::Const(Const::Sort),
             ty: None,
+            span: Span::Artificial,
         }
         .into_value()
     }
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
-        Value::new(v, Unevaled, t)
+        Value::new(v, Unevaled, t, Span::Artificial)
+    }
+    pub(crate) fn from_valuef_and_type_and_span(
+        v: ValueF,
+        t: Value,
+        span: Span,
+    ) -> Value {
+        Value::new(v, Unevaled, t, span)
     }
     pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
-        Value::new(v, WHNF, t)
+        Value::new(v, WHNF, t, Span::Artificial)
     }
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
@@ -141,6 +154,10 @@ impl Value {
     pub(crate) fn from_builtin(b: Builtin) -> Self {
         builtin_to_value(b)
     }
+    pub(crate) fn with_span(self, span: Span) -> Self {
+        self.as_internal_mut().span = span;
+        self
+    }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
         match &*self.as_whnf() {
@@ -148,6 +165,9 @@ impl Value {
             _ => None,
         }
     }
+    pub(crate) fn span(&self) -> Span {
+        self.as_internal().span.clone()
+    }
 
     fn as_internal(&self) -> Ref<ValueInternal> {
         self.0.borrow()
@@ -258,6 +278,7 @@ impl Shift for ValueInternal {
             form: self.form,
             value: self.value.shift(delta, var)?,
             ty: self.ty.shift(delta, var)?,
+            span: self.span.clone(),
         })
     }
 }
@@ -285,6 +306,7 @@ impl Subst<Value> for ValueInternal {
             form: Unevaled,
             value: self.value.subst_shift(var, val),
             ty: self.ty.subst_shift(var, val),
+            span: self.span.clone(),
         }
     }
 }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 4e457e6..e5d0807 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -1,12 +1,13 @@
 use std::collections::HashMap;
 
 use dhall_syntax::{
-    rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
+    Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural,
 };
 
 use crate::core::value::{ToExprOptions, Value};
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::phase::typecheck::rc;
 use crate::phase::{Normalized, NormalizedExpr};
 
 /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 6d4e120..4d59cbb 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,6 +1,6 @@
 use std::io::Error as IOError;
 
-use dhall_syntax::{BinOp, Import, Label, ParseError, V};
+use dhall_syntax::{BinOp, Import, Label, ParseError, Span};
 
 use crate::core::context::TypecheckContext;
 use crate::core::value::Value;
@@ -41,14 +41,14 @@ pub enum EncodeError {
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError {
-    type_message: TypeMessage,
+    message: TypeMessage,
     context: TypecheckContext,
 }
 
 /// The specific type error
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
-    UnboundVariable(V<Label>),
+    UnboundVariable(Span),
     InvalidInputType(Value),
     InvalidOutputType(Value),
     NotAFunction(Value),
@@ -90,58 +90,37 @@ pub(crate) enum TypeMessage {
 impl TypeError {
     pub(crate) fn new(
         context: &TypecheckContext,
-        type_message: TypeMessage,
+        message: TypeMessage,
     ) -> Self {
         TypeError {
             context: context.clone(),
-            type_message,
+            message,
         }
     }
 }
 
-impl std::error::Error for TypeMessage {
-    fn description(&self) -> &str {
+impl std::fmt::Display for TypeError {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
         use TypeMessage::*;
-        match *self {
-            // UnboundVariable => "Unbound variable",
-            InvalidInputType(_) => "Invalid function input",
-            InvalidOutputType(_) => "Invalid function output",
-            NotAFunction(_) => "Not a function",
-            TypeMismatch(_, _, _) => "Wrong type of function argument",
-            _ => "Unhandled error",
-        }
+        let msg = match &self.message {
+            UnboundVariable(span) => span.error("Type error: Unbound variable"),
+            InvalidInputType(v) => {
+                v.span().error("Type error: Invalid function input")
+            }
+            InvalidOutputType(v) => {
+                v.span().error("Type error: Invalid function output")
+            }
+            NotAFunction(v) => v.span().error("Type error: Not a function"),
+            TypeMismatch(v, _, _) => v
+                .span()
+                .error("Type error: Wrong type of function argument"),
+            _ => "Type error: Unhandled error".to_string(),
+        };
+        write!(f, "{}", msg)
     }
 }
 
-impl std::fmt::Display for TypeMessage {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-        match self {
-            // UnboundVariable(_) => {
-            //     f.write_str(include_str!("errors/UnboundVariable.txt"))
-            // }
-            // TypeMismatch(e0, e1, e2) => {
-            //     let template = include_str!("errors/TypeMismatch.txt");
-            //     let s = template
-            //         .replace("$txt0", &format!("{}", e0.as_expr()))
-            //         .replace("$txt1", &format!("{}", e1.as_expr()))
-            //         .replace("$txt2", &format!("{}", e2.as_expr()))
-            //         .replace(
-            //             "$txt3",
-            //             &format!(
-            //                 "{}",
-            //                 e2.get_type()
-            //                     .unwrap()
-            //                     .as_normalized()
-            //                     .unwrap()
-            //                     .as_expr()
-            //             ),
-            //         );
-            //     f.write_str(&s)
-            // }
-            _ => f.write_str("Unhandled error message"),
-        }
-    }
-}
+impl std::error::Error for TypeError {}
 
 impl std::fmt::Display for Error {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
@@ -151,7 +130,7 @@ impl std::fmt::Display for Error {
             Error::Decode(err) => write!(f, "{:?}", err),
             Error::Encode(err) => write!(f, "{:?}", err),
             Error::Resolve(err) => write!(f, "{:?}", err),
-            Error::Typecheck(err) => write!(f, "{:?}", err),
+            Error::Typecheck(err) => write!(f, "{}", err),
         }
     }
 }
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 8c98f77..b4f18da 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -5,8 +5,9 @@ use std::vec;
 
 use dhall_syntax::map::DupTreeMap;
 use dhall_syntax::{
-    rc, Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation,
-    ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, URL, V,
+    Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation,
+    ImportMode, Integer, InterpolatedText, Label, Natural, RawExpr, Scheme,
+    Span, URL, V,
 };
 
 use crate::error::{DecodeError, EncodeError};
@@ -24,6 +25,11 @@ pub(crate) fn encode<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> {
         .map_err(|e| EncodeError::CBORError(e))
 }
 
+// Should probably rename this
+pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
+    Expr::new(x, Span::Decoded)
+}
+
 fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
     use cbor::Value::*;
     use dhall_syntax::{BinOp, Builtin, Const};
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 9013c1f..33919e4 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -2,7 +2,7 @@ use std::cmp::max;
 use std::collections::HashMap;
 
 use dhall_syntax::{
-    rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label,
+    Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span,
 };
 
 use crate::core::context::TypecheckContext;
@@ -142,6 +142,10 @@ pub(crate) fn const_to_value(c: Const) -> Value {
     }
 }
 
+pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
+    Expr::new(x, Span::Artificial)
+}
+
 // Ad-hoc macro to help construct the types of builtins
 macro_rules! make_type {
     (Type) => { ExprF::Const(Const::Type) };
@@ -300,6 +304,7 @@ fn type_with(
     e: Expr<Normalized>,
 ) -> Result<Value, TypeError> {
     use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
+    let span = e.span();
 
     Ok(match e.as_ref() {
         Lam(var, annot, body) => {
@@ -334,7 +339,7 @@ fn type_with(
             None => {
                 return Err(TypeError::new(
                     ctx,
-                    TypeMessage::UnboundVariable(var.clone()),
+                    TypeMessage::UnboundVariable(span),
                 ))
             }
         },
@@ -344,7 +349,7 @@ fn type_with(
                 |e| type_with(ctx, e.clone()),
                 |_, _| unreachable!(),
             )?;
-            type_last_layer(ctx, expr)?
+            type_last_layer(ctx, expr, span)?
         }
     })
 }
@@ -354,6 +359,7 @@ fn type_with(
 fn type_last_layer(
     ctx: &TypecheckContext,
     e: ExprF<Value, Normalized>,
+    span: Span,
 ) -> Result<Value, TypeError> {
     use crate::error::TypeMessage::*;
     use dhall_syntax::BinOp::*;
@@ -580,6 +586,7 @@ fn type_last_layer(
                 l.get_type()?,
                 r.get_type()?,
             ),
+            Span::Artificial,
         )?),
         BinOp(RecursiveRecordTypeMerge, l, r) => {
             use crate::phase::normalize::merge_maps;
@@ -615,6 +622,7 @@ fn type_last_layer(
                             l.clone(),
                             r.clone(),
                         ),
+                        Span::Artificial,
                     )
                 },
             )?;
@@ -782,10 +790,12 @@ fn type_last_layer(
     };
 
     Ok(match ret {
-        RetTypeOnly(typ) => {
-            Value::from_valuef_and_type(ValueF::PartialExpr(e), typ)
-        }
-        RetWhole(v) => v,
+        RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
+            ValueF::PartialExpr(e),
+            typ,
+            span,
+        ),
+        RetWhole(v) => v.with_span(span),
     })
 }
 
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index b98489f..1037ef9 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -20,8 +20,31 @@ right: `{}`"#,
     }};
 }
 
+/// Wrapper around string slice that makes debug output `{:?}` to print string same way as `{}`.
+/// Used in different `assert*!` macros in combination with `pretty_assertions` crate to make
+/// test failures to show nice diffs.
+#[derive(PartialEq, Eq)]
+#[doc(hidden)]
+pub struct PrettyString(String);
+
+/// Make diff to display string as multi-line string
+impl std::fmt::Debug for PrettyString {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        f.write_str(&self.0)
+    }
+}
+
+macro_rules! assert_eq_pretty_str {
+    ($left:expr, $right:expr) => {
+        assert_eq_pretty!(
+            PrettyString($left.to_string()),
+            PrettyString($right.to_string())
+        );
+    };
+}
+
 use std::fs::File;
-use std::io::Read;
+use std::io::{Read, Write};
 use std::path::PathBuf;
 
 use crate::error::{Error, Result};
@@ -40,6 +63,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 +168,41 @@ 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();
+        }
+        // Checks the output of the type error against a text file. If the text file doesn't exist,
+        // we instead write to it the output we got. This makes it easy to update those files: just
+        // `rm -r dhall/tests/type-errors` and run the tests again.
+        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_str!(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..69428b8
--- /dev/null
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -0,0 +1 @@
+[unknown location] Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/mixedUnions.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/recordOfKind.txt b/dhall/tests/type-errors/recordOfKind.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/recordOfKind.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
new file mode 100644
index 0000000..2969c18
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -0,0 +1,6 @@
+ --> 1:47
+  |
+1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)␊
+  |                                               ^
+  |
+  = Type error: Unbound variable
diff --git a/dhall/tests/type-errors/unit/AssertNotEquivalence.txt b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
new file mode 100644
index 0000000..69428b8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -0,0 +1 @@
+[unknown location] Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
new file mode 100644
index 0000000..062f9de
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+  |
+1 | True True␊
+  | ^--^
+  |
+  = Type error: Not a function
diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
new file mode 100644
index 0000000..9e43c33
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -0,0 +1,6 @@
+ --> 1:7
+  |
+1 | λ(_ : 1) → _␊
+  |       ^
+  |
+  = Type error: Invalid function input
diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
new file mode 100644
index 0000000..dd2e758
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+  |
+1 | 2 → _␊
+  | ^
+  |
+  = Type error: Invalid function input
diff --git a/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotType.txt b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
new file mode 100644
index 0000000..bc5cc40
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -0,0 +1,6 @@
+ --> 1:6
+  |
+1 | [] : List Type␊
+  |      ^--^
+  |
+  = Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/unit/ListLiteralNotType.txt b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
new file mode 100644
index 0000000..c5ed223
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -0,0 +1 @@
+[unknown location] Type error: Not a function
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
new file mode 100644
index 0000000..69428b8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -0,0 +1 @@
+[unknown location] Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
new file mode 100644
index 0000000..fd906bf
--- /dev/null
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+  |
+1 | Natural/subtract True True␊
+  | ^--------------^
+  |
+  = Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordMixedKinds3.txt b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/SomeNotType.txt b/dhall/tests/type-errors/unit/SomeNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/SomeNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/Sort.txt b/dhall/tests/type-errors/unit/Sort.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/Sort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
new file mode 100644
index 0000000..9cc0c19
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+  |
+1 | constructors < Left : Natural | Right : Bool >␊
+  | ^----------^
+  |
+  = Type error: Unbound variable
diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
new file mode 100644
index 0000000..a46aac0
--- /dev/null
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+  |
+1 | x␊
+  | ^
+  |
+  = Type error: Unbound variable
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index 2ad3ba8..750b58b 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -1,5 +1,3 @@
-use std::rc::Rc;
-
 use crate::map::{DupTreeMap, DupTreeSet};
 use crate::visitor::{self, ExprFMutVisitor, ExprFVisitor};
 use crate::*;
@@ -15,40 +13,6 @@ pub fn trivial_result<T>(x: Result<T, !>) -> T {
     }
 }
 
-/// A location in the source text
-#[derive(Debug, Clone)]
-pub struct Span {
-    input: Rc<str>,
-    /// # Safety
-    ///
-    /// Must be a valid character boundary index into `input`.
-    start: usize,
-    /// # Safety
-    ///
-    /// Must be a valid character boundary index into `input`.
-    end: usize,
-}
-
-impl Span {
-    pub(crate) fn make(input: Rc<str>, sp: pest::Span) -> Self {
-        Span {
-            input,
-            start: sp.start(),
-            end: sp.end(),
-        }
-    }
-    /// Takes the union of the two spans. Assumes that the spans come from the same input.
-    /// This will also capture any input between the spans.
-    pub fn union(&self, other: &Span) -> Self {
-        use std::cmp::{max, min};
-        Span {
-            input: self.input.clone(),
-            start: min(self.start, other.start),
-            end: max(self.start, other.start),
-        }
-    }
-}
-
 /// Double with bitwise equality
 #[derive(Debug, Copy, Clone)]
 pub struct NaiveDouble(f64);
@@ -178,7 +142,7 @@ pub enum Builtin {
 
 // Each node carries an annotation.
 #[derive(Debug, Clone)]
-pub struct Expr<Embed>(Box<(RawExpr<Embed>, Option<Span>)>);
+pub struct Expr<Embed>(Box<(RawExpr<Embed>, Span)>);
 
 pub type RawExpr<Embed> = ExprF<Expr<Embed>, Embed>;
 
@@ -334,16 +298,12 @@ impl<E> Expr<E> {
     pub fn as_mut(&mut self) -> &mut RawExpr<E> {
         &mut self.0.as_mut().0
     }
-    pub fn span(&self) -> Option<Span> {
+    pub fn span(&self) -> Span {
         self.0.as_ref().1.clone()
     }
 
-    pub(crate) fn new(x: RawExpr<E>, n: Span) -> Self {
-        Expr(Box::new((x, Some(n))))
-    }
-
-    pub fn from_expr_no_span(x: RawExpr<E>) -> Self {
-        Expr(Box::new((x, None)))
+    pub fn new(x: RawExpr<E>, n: Span) -> Self {
+        Expr(Box::new((x, n)))
     }
 
     pub fn rewrap<E2>(&self, x: RawExpr<E2>) -> Expr<E2> {
@@ -388,11 +348,6 @@ impl<E> Expr<E> {
     }
 }
 
-// Should probably rename this
-pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
-    Expr::from_expr_no_span(x)
-}
-
 /// Add an isize to an usize
 /// Panics on over/underflow
 fn add_ui(u: usize, i: isize) -> Option<usize> {
diff --git a/dhall_syntax/src/core/mod.rs b/dhall_syntax/src/core/mod.rs
index fe2c0be..66bf229 100644
--- a/dhall_syntax/src/core/mod.rs
+++ b/dhall_syntax/src/core/mod.rs
@@ -4,6 +4,8 @@ mod import;
 pub use import::*;
 mod label;
 pub use label::*;
+mod span;
+pub use span::*;
 mod text;
 pub use text::*;
 pub mod context;
diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs
new file mode 100644
index 0000000..f9c7008
--- /dev/null
+++ b/dhall_syntax/src/core/span.rs
@@ -0,0 +1,81 @@
+use std::rc::Rc;
+
+/// A location in the source text
+#[derive(Debug, Clone)]
+pub struct ParsedSpan {
+    input: Rc<str>,
+    /// # Safety
+    ///
+    /// Must be a valid character boundary index into `input`.
+    start: usize,
+    /// # Safety
+    ///
+    /// Must be a valid character boundary index into `input`.
+    end: usize,
+}
+
+#[derive(Debug, Clone)]
+pub enum Span {
+    /// A location in the source text
+    Parsed(ParsedSpan),
+    /// For expressions obtained from decoding binary
+    Decoded,
+    /// For expressions constructed during normalization/typecheck
+    Artificial,
+}
+
+impl Span {
+    pub(crate) fn make(input: Rc<str>, sp: pest::Span) -> Self {
+        Span::Parsed(ParsedSpan {
+            input,
+            start: sp.start(),
+            end: sp.end(),
+        })
+    }
+
+    /// Takes the union of the two spans, i.e. the range of input covered by the two spans plus any
+    /// input between them. Assumes that the spans come from the same input. Fails if one of the
+    /// spans does not point to an input location.
+    pub fn union(&self, other: &Span) -> Self {
+        use std::cmp::{max, min};
+        use Span::*;
+        match (self, other) {
+            (Parsed(x), Parsed(y)) if Rc::ptr_eq(&x.input, &y.input) => {
+                Parsed(ParsedSpan {
+                    input: x.input.clone(),
+                    start: min(x.start, y.start),
+                    end: max(x.end, y.end),
+                })
+            }
+            _ => panic!(
+                "Tried to union incompatible spans: {:?} and {:?}",
+                self, other
+            ),
+        }
+    }
+
+    /// Merges two spans assumed to point to a similar thing. If only one of them points to an
+    /// input location, use that one.
+    pub fn merge(&self, other: &Span) -> Self {
+        use Span::*;
+        match (self, other) {
+            (Parsed(x), _) | (_, Parsed(x)) => Parsed(x.clone()),
+            (Artificial, _) | (_, Artificial) => Artificial,
+            (Decoded, Decoded) => Decoded,
+        }
+    }
+
+    pub fn error(&self, message: impl Into<String>) -> String {
+        use pest::error::{Error, ErrorVariant};
+        use pest::Span;
+        let message: String = message.into();
+        let span = match self {
+            self::Span::Parsed(span) => span,
+            _ => return format!("[unknown location] {}", message),
+        };
+        let span = Span::new(&*span.input, span.start, span.end).unwrap();
+        let err: ErrorVariant<!> = ErrorVariant::CustomError { message };
+        let err = Error::new_from_span(err, span);
+        format!("{}", err)
+    }
+}
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 83f62ee..eaded50 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -650,7 +650,7 @@ impl DhallParser {
                     final_expr,
                     |acc, x| {
                         spanned_union(
-                            acc.span().unwrap(),
+                            acc.span(),
                             x.3,
                             Let(x.0, x.1, x.2, acc)
                         )
@@ -717,11 +717,7 @@ impl DhallParser {
             r => Err(op.error(format!("Rule {:?} isn't an operator", r)))?,
         };
 
-        Ok(spanned_union(
-            l.span().unwrap(),
-            r.span().unwrap(),
-            BinOp(op, l, r),
-        ))
+        Ok(spanned_union(l.span(), r.span(), BinOp(op, l, r)))
     }
 
     fn Some_(_input: ParseInput) -> ParseResult<()> {
@@ -739,8 +735,8 @@ impl DhallParser {
                     first,
                     |acc, e| {
                         spanned_union(
-                            acc.span().unwrap(),
-                            e.span().unwrap(),
+                            acc.span(),
+                            e.span(),
                             App(acc, e)
                         )
                     }
@@ -778,7 +774,7 @@ impl DhallParser {
                     first,
                     |acc, e| {
                         spanned_union(
-                            acc.span().unwrap(),
+                            acc.span(),
                             e.1,
                             match e.0 {
                                 Either::Left(l) => Field(acc, l),