From 60129b7d1c0ea8bdf2ec666fa51957e97465e88f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 6 May 2019 23:17:26 +0200
Subject: Consolidate errors in the error module

---
 dhall/src/error.rs                                 |  60 --------
 dhall/src/error/mod.rs                             | 169 +++++++++++++++++++++
 dhall/src/error/text/AnnotMismatch.txt             | 117 ++++++++++++++
 dhall/src/error/text/CantTextAppend.txt            |  28 ++++
 dhall/src/error/text/DuplicateAlternative.txt      |  18 +++
 dhall/src/error/text/FieldCollision.txt            |  43 ++++++
 dhall/src/error/text/HandlerInputTypeMismatch.txt  |  49 ++++++
 dhall/src/error/text/HandlerNotAFunction.txt       |  32 ++++
 dhall/src/error/text/HandlerOutputTypeMismatch.txt |  51 +++++++
 dhall/src/error/text/IfBranchMismatch.txt          |  63 ++++++++
 dhall/src/error/text/IfBranchMustBeTerm.txt        |  51 +++++++
 dhall/src/error/text/InvalidAlterantive.txt        |  48 ++++++
 dhall/src/error/text/InvalidAlterantiveType.txt    |  49 ++++++
 dhall/src/error/text/InvalidField.txt              |  35 +++++
 dhall/src/error/text/InvalidFieldType.txt          |  34 +++++
 dhall/src/error/text/InvalidInputType.txt          |  61 ++++++++
 dhall/src/error/text/InvalidListElement.txt        |  30 ++++
 dhall/src/error/text/InvalidListType.txt           |  43 ++++++
 dhall/src/error/text/InvalidOptionType.txt         |  44 ++++++
 dhall/src/error/text/InvalidOptionalElement.txt    |  29 ++++
 dhall/src/error/text/InvalidOptionalLiteral.txt    |  53 +++++++
 dhall/src/error/text/InvalidOutputType.txt         |  68 +++++++++
 dhall/src/error/text/InvalidPredicate.txt          |  51 +++++++
 dhall/src/error/text/MissingField.txt              |  30 ++++
 dhall/src/error/text/MissingHandler.txt            |  32 ++++
 dhall/src/error/text/MustCombineARecord.txt        |  46 ++++++
 dhall/src/error/text/MustMergeARecord.txt          |  43 ++++++
 dhall/src/error/text/MustMergeUnion.txt            |  31 ++++
 dhall/src/error/text/NoDependentLet.txt            |  76 +++++++++
 dhall/src/error/text/NoDependentTypes.txt          |  31 ++++
 dhall/src/error/text/NotAFunction.txt              |  68 +++++++++
 dhall/src/error/text/NotARecord.txt                |  48 ++++++
 dhall/src/error/text/TypeMismatch.txt              | 117 ++++++++++++++
 dhall/src/error/text/UnboundVariable.txt           |  97 ++++++++++++
 dhall/src/error/text/Untyped.txt                   | 117 ++++++++++++++
 dhall/src/error/text/UnusedHandler.txt             |  32 ++++
 dhall/src/errors/AnnotMismatch.txt                 | 117 --------------
 dhall/src/errors/CantTextAppend.txt                |  28 ----
 dhall/src/errors/DuplicateAlternative.txt          |  18 ---
 dhall/src/errors/FieldCollision.txt                |  43 ------
 dhall/src/errors/HandlerInputTypeMismatch.txt      |  49 ------
 dhall/src/errors/HandlerNotAFunction.txt           |  32 ----
 dhall/src/errors/HandlerOutputTypeMismatch.txt     |  51 -------
 dhall/src/errors/IfBranchMismatch.txt              |  63 --------
 dhall/src/errors/IfBranchMustBeTerm.txt            |  51 -------
 dhall/src/errors/InvalidAlterantive.txt            |  48 ------
 dhall/src/errors/InvalidAlterantiveType.txt        |  49 ------
 dhall/src/errors/InvalidField.txt                  |  35 -----
 dhall/src/errors/InvalidFieldType.txt              |  34 -----
 dhall/src/errors/InvalidInputType.txt              |  61 --------
 dhall/src/errors/InvalidListElement.txt            |  30 ----
 dhall/src/errors/InvalidListType.txt               |  43 ------
 dhall/src/errors/InvalidOptionType.txt             |  44 ------
 dhall/src/errors/InvalidOptionalElement.txt        |  29 ----
 dhall/src/errors/InvalidOptionalLiteral.txt        |  53 -------
 dhall/src/errors/InvalidOutputType.txt             |  68 ---------
 dhall/src/errors/InvalidPredicate.txt              |  51 -------
 dhall/src/errors/MissingField.txt                  |  30 ----
 dhall/src/errors/MissingHandler.txt                |  32 ----
 dhall/src/errors/MustCombineARecord.txt            |  46 ------
 dhall/src/errors/MustMergeARecord.txt              |  43 ------
 dhall/src/errors/MustMergeUnion.txt                |  31 ----
 dhall/src/errors/NoDependentLet.txt                |  76 ---------
 dhall/src/errors/NoDependentTypes.txt              |  31 ----
 dhall/src/errors/NotAFunction.txt                  |  68 ---------
 dhall/src/errors/NotARecord.txt                    |  48 ------
 dhall/src/errors/TypeMismatch.txt                  | 117 --------------
 dhall/src/errors/UnboundVariable.txt               |  97 ------------
 dhall/src/errors/Untyped.txt                       | 117 --------------
 dhall/src/errors/UnusedHandler.txt                 |  32 ----
 dhall/src/lib.rs                                   |   1 -
 dhall/src/phase/binary.rs                          |  17 ++-
 dhall/src/phase/mod.rs                             |   8 +-
 dhall/src/phase/resolve.rs                         |  11 +-
 dhall/src/phase/typecheck.rs                       | 114 ++------------
 dhall/src/traits/dynamic_type.rs                   |   4 +-
 76 files changed, 1961 insertions(+), 1953 deletions(-)
 delete mode 100644 dhall/src/error.rs
 create mode 100644 dhall/src/error/mod.rs
 create mode 100644 dhall/src/error/text/AnnotMismatch.txt
 create mode 100644 dhall/src/error/text/CantTextAppend.txt
 create mode 100644 dhall/src/error/text/DuplicateAlternative.txt
 create mode 100644 dhall/src/error/text/FieldCollision.txt
 create mode 100644 dhall/src/error/text/HandlerInputTypeMismatch.txt
 create mode 100644 dhall/src/error/text/HandlerNotAFunction.txt
 create mode 100644 dhall/src/error/text/HandlerOutputTypeMismatch.txt
 create mode 100644 dhall/src/error/text/IfBranchMismatch.txt
 create mode 100644 dhall/src/error/text/IfBranchMustBeTerm.txt
 create mode 100644 dhall/src/error/text/InvalidAlterantive.txt
 create mode 100644 dhall/src/error/text/InvalidAlterantiveType.txt
 create mode 100644 dhall/src/error/text/InvalidField.txt
 create mode 100644 dhall/src/error/text/InvalidFieldType.txt
 create mode 100644 dhall/src/error/text/InvalidInputType.txt
 create mode 100644 dhall/src/error/text/InvalidListElement.txt
 create mode 100644 dhall/src/error/text/InvalidListType.txt
 create mode 100644 dhall/src/error/text/InvalidOptionType.txt
 create mode 100644 dhall/src/error/text/InvalidOptionalElement.txt
 create mode 100644 dhall/src/error/text/InvalidOptionalLiteral.txt
 create mode 100644 dhall/src/error/text/InvalidOutputType.txt
 create mode 100644 dhall/src/error/text/InvalidPredicate.txt
 create mode 100644 dhall/src/error/text/MissingField.txt
 create mode 100644 dhall/src/error/text/MissingHandler.txt
 create mode 100644 dhall/src/error/text/MustCombineARecord.txt
 create mode 100644 dhall/src/error/text/MustMergeARecord.txt
 create mode 100644 dhall/src/error/text/MustMergeUnion.txt
 create mode 100644 dhall/src/error/text/NoDependentLet.txt
 create mode 100644 dhall/src/error/text/NoDependentTypes.txt
 create mode 100644 dhall/src/error/text/NotAFunction.txt
 create mode 100644 dhall/src/error/text/NotARecord.txt
 create mode 100644 dhall/src/error/text/TypeMismatch.txt
 create mode 100644 dhall/src/error/text/UnboundVariable.txt
 create mode 100644 dhall/src/error/text/Untyped.txt
 create mode 100644 dhall/src/error/text/UnusedHandler.txt
 delete mode 100644 dhall/src/errors/AnnotMismatch.txt
 delete mode 100644 dhall/src/errors/CantTextAppend.txt
 delete mode 100644 dhall/src/errors/DuplicateAlternative.txt
 delete mode 100644 dhall/src/errors/FieldCollision.txt
 delete mode 100644 dhall/src/errors/HandlerInputTypeMismatch.txt
 delete mode 100644 dhall/src/errors/HandlerNotAFunction.txt
 delete mode 100644 dhall/src/errors/HandlerOutputTypeMismatch.txt
 delete mode 100644 dhall/src/errors/IfBranchMismatch.txt
 delete mode 100644 dhall/src/errors/IfBranchMustBeTerm.txt
 delete mode 100644 dhall/src/errors/InvalidAlterantive.txt
 delete mode 100644 dhall/src/errors/InvalidAlterantiveType.txt
 delete mode 100644 dhall/src/errors/InvalidField.txt
 delete mode 100644 dhall/src/errors/InvalidFieldType.txt
 delete mode 100644 dhall/src/errors/InvalidInputType.txt
 delete mode 100644 dhall/src/errors/InvalidListElement.txt
 delete mode 100644 dhall/src/errors/InvalidListType.txt
 delete mode 100644 dhall/src/errors/InvalidOptionType.txt
 delete mode 100644 dhall/src/errors/InvalidOptionalElement.txt
 delete mode 100644 dhall/src/errors/InvalidOptionalLiteral.txt
 delete mode 100644 dhall/src/errors/InvalidOutputType.txt
 delete mode 100644 dhall/src/errors/InvalidPredicate.txt
 delete mode 100644 dhall/src/errors/MissingField.txt
 delete mode 100644 dhall/src/errors/MissingHandler.txt
 delete mode 100644 dhall/src/errors/MustCombineARecord.txt
 delete mode 100644 dhall/src/errors/MustMergeARecord.txt
 delete mode 100644 dhall/src/errors/MustMergeUnion.txt
 delete mode 100644 dhall/src/errors/NoDependentLet.txt
 delete mode 100644 dhall/src/errors/NoDependentTypes.txt
 delete mode 100644 dhall/src/errors/NotAFunction.txt
 delete mode 100644 dhall/src/errors/NotARecord.txt
 delete mode 100644 dhall/src/errors/TypeMismatch.txt
 delete mode 100644 dhall/src/errors/UnboundVariable.txt
 delete mode 100644 dhall/src/errors/Untyped.txt
 delete mode 100644 dhall/src/errors/UnusedHandler.txt

diff --git a/dhall/src/error.rs b/dhall/src/error.rs
deleted file mode 100644
index 8497a91..0000000
--- a/dhall/src/error.rs
+++ /dev/null
@@ -1,60 +0,0 @@
-use std::io::Error as IOError;
-
-use dhall_syntax::ParseError;
-
-use crate::phase::binary::DecodeError;
-use crate::phase::resolve::ImportError;
-use crate::phase::typecheck::TypeError;
-
-pub type Result<T> = std::result::Result<T, Error>;
-
-#[derive(Debug)]
-#[non_exhaustive]
-pub enum Error {
-    IO(IOError),
-    Parse(ParseError),
-    Decode(DecodeError),
-    Resolve(ImportError),
-    Typecheck(TypeError),
-    Deserialize(String),
-}
-
-impl std::fmt::Display for Error {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-        match self {
-            Error::IO(err) => write!(f, "{}", err),
-            Error::Parse(err) => write!(f, "{}", err),
-            Error::Decode(err) => write!(f, "{:?}", err),
-            Error::Resolve(err) => write!(f, "{:?}", err),
-            Error::Typecheck(err) => write!(f, "{:?}", err),
-            Error::Deserialize(err) => write!(f, "{}", err),
-        }
-    }
-}
-
-impl std::error::Error for Error {}
-impl From<IOError> for Error {
-    fn from(err: IOError) -> Error {
-        Error::IO(err)
-    }
-}
-impl From<ParseError> for Error {
-    fn from(err: ParseError) -> Error {
-        Error::Parse(err)
-    }
-}
-impl From<DecodeError> for Error {
-    fn from(err: DecodeError) -> Error {
-        Error::Decode(err)
-    }
-}
-impl From<ImportError> for Error {
-    fn from(err: ImportError) -> Error {
-        Error::Resolve(err)
-    }
-}
-impl From<TypeError> for Error {
-    fn from(err: TypeError) -> Error {
-        Error::Typecheck(err)
-    }
-}
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
new file mode 100644
index 0000000..e70b9a9
--- /dev/null
+++ b/dhall/src/error/mod.rs
@@ -0,0 +1,169 @@
+use std::io::Error as IOError;
+
+use dhall_syntax::{BinOp, Import, Label, ParseError, V};
+
+use crate::phase::resolve::ImportStack;
+use crate::phase::typecheck::TypecheckContext;
+use crate::phase::{Normalized, Type, Typed};
+
+pub type Result<T> = std::result::Result<T, Error>;
+
+#[derive(Debug)]
+#[non_exhaustive]
+pub enum Error {
+    IO(IOError),
+    Parse(ParseError),
+    Decode(DecodeError),
+    Resolve(ImportError),
+    Typecheck(TypeError),
+    Deserialize(String),
+}
+
+#[derive(Debug)]
+pub enum ImportError {
+    Recursive(Import, Box<Error>),
+    UnexpectedImport(Import),
+    ImportCycle(ImportStack, Import),
+}
+
+#[derive(Debug)]
+pub enum DecodeError {
+    CBORError(serde_cbor::error::Error),
+    WrongFormatError(String),
+}
+
+/// A structured type error that includes context
+#[derive(Debug)]
+pub struct TypeError {
+    type_message: TypeMessage,
+    context: TypecheckContext,
+}
+
+/// The specific type error
+#[derive(Debug)]
+pub(crate) enum TypeMessage {
+    UnboundVariable(V<Label>),
+    InvalidInputType(Normalized),
+    InvalidOutputType(Normalized),
+    NotAFunction(Typed),
+    TypeMismatch(Typed, Normalized, Typed),
+    AnnotMismatch(Typed, Normalized),
+    Untyped,
+    InvalidListElement(usize, Normalized, Typed),
+    InvalidListType(Normalized),
+    InvalidOptionalType(Normalized),
+    InvalidPredicate(Typed),
+    IfBranchMismatch(Typed, Typed),
+    IfBranchMustBeTerm(bool, Typed),
+    InvalidFieldType(Label, Type),
+    NotARecord(Label, Normalized),
+    MissingRecordField(Label, Typed),
+    MissingUnionField(Label, Normalized),
+    BinOpTypeMismatch(BinOp, Typed),
+    NoDependentTypes(Normalized, Normalized),
+    InvalidTextInterpolation(Typed),
+    Sort,
+    Unimplemented,
+}
+
+impl TypeError {
+    pub(crate) fn new(
+        context: &TypecheckContext,
+        type_message: TypeMessage,
+    ) -> Self {
+        TypeError {
+            context: context.clone(),
+            type_message,
+        }
+    }
+}
+
+impl From<TypeError> for std::option::NoneError {
+    fn from(_: TypeError) -> std::option::NoneError {
+        std::option::NoneError
+    }
+}
+
+impl std::error::Error for TypeMessage {
+    fn description(&self) -> &str {
+        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",
+        }
+    }
+}
+
+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::fmt::Display for Error {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        match self {
+            Error::IO(err) => write!(f, "{}", err),
+            Error::Parse(err) => write!(f, "{}", err),
+            Error::Decode(err) => write!(f, "{:?}", err),
+            Error::Resolve(err) => write!(f, "{:?}", err),
+            Error::Typecheck(err) => write!(f, "{:?}", err),
+            Error::Deserialize(err) => write!(f, "{}", err),
+        }
+    }
+}
+
+impl std::error::Error for Error {}
+impl From<IOError> for Error {
+    fn from(err: IOError) -> Error {
+        Error::IO(err)
+    }
+}
+impl From<ParseError> for Error {
+    fn from(err: ParseError) -> Error {
+        Error::Parse(err)
+    }
+}
+impl From<DecodeError> for Error {
+    fn from(err: DecodeError) -> Error {
+        Error::Decode(err)
+    }
+}
+impl From<ImportError> for Error {
+    fn from(err: ImportError) -> Error {
+        Error::Resolve(err)
+    }
+}
+impl From<TypeError> for Error {
+    fn from(err: TypeError) -> Error {
+        Error::Typecheck(err)
+    }
+}
diff --git a/dhall/src/error/text/AnnotMismatch.txt b/dhall/src/error/text/AnnotMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/dhall/src/error/text/AnnotMismatch.txt
@@ -0,0 +1,117 @@
+Explanation: Every function declares what type or kind of argument to accept
+
+For example:
+
+
+    ┌───────────────────────────────┐
+    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts
+    └───────────────────────────────┘  arguments that have type ❰Bool❱
+                        ⇧
+                        The function's input type
+
+
+    ┌───────────────────────────────┐
+    │ Natural/even : Natural → Bool │  This built-in function only accepts
+    └───────────────────────────────┘  arguments that have type ❰Natural❱
+                     ⇧
+                     The function's input type
+
+
+    ┌───────────────────────────────┐
+    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts
+    └───────────────────────────────┘  arguments that have kind ❰Type❱
+                        ⇧
+                        The function's input kind
+
+
+    ┌────────────────────┐
+    │ List : Type → Type │  This built-in function only accepts arguments that
+    └────────────────────┘  have kind ❰Type❱
+             ⇧
+             The function's input kind
+
+
+For example, the following expressions are valid:
+
+
+    ┌────────────────────────┐
+    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type
+    └────────────────────────┘  of argument that the anonymous function accepts
+
+
+    ┌─────────────────┐
+    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
+    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,
+
+
+    ┌────────────────────────┐
+    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
+    └────────────────────────┘  of argument that the anonymous function accepts
+
+
+    ┌───────────┐
+    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
+    └───────────┘  that that the ❰List❱ function accepts
+
+
+However, you can $_NOT apply a function to the wrong type or kind of argument
+
+For example, the following expressions are not valid:
+
+
+    ┌───────────────────────┐
+    │ (λ(x : Bool) → x) "A" │  ❰"A"❱ has type ❰Text❱, but the anonymous function
+    └───────────────────────┘  expects an argument that has type ❰Bool❱
+
+
+    ┌──────────────────┐
+    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
+    └──────────────────┘  expects an argument that has type ❰Natural❱
+
+
+    ┌────────────────────────┐
+    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
+    └────────────────────────┘  function expects an argument of kind ❰Type❱
+
+
+    ┌────────┐
+    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
+    └────────┘  argument that has kind ❰Type❱
+
+
+You tried to invoke the following function:
+
+↳ $txt0
+
+... which expects an argument of type or kind:
+
+↳ $txt1
+
+... on the following argument:
+
+↳ $txt2
+
+... which has a different type or kind:
+
+↳ $txt3
+
+Some common reasons why you might get this error:
+
+● You omit a function argument by mistake:
+
+
+    ┌────────────────────────────────────────┐
+    │ List/head   ([1, 2, 3] : List Integer) │
+    └────────────────────────────────────────┘
+                ⇧
+                ❰List/head❱ is missing the first argument,
+                which should be: ❰Integer❱
+
+
+● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
+
+    ┌────────────────┐
+    │ Natural/even 2 │
+    └────────────────┘
+                   ⇧
+                   This should be ❰+2❱
diff --git a/dhall/src/error/text/CantTextAppend.txt b/dhall/src/error/text/CantTextAppend.txt
new file mode 100644
index 0000000..26b9ceb
--- /dev/null
+++ b/dhall/src/error/text/CantTextAppend.txt
@@ -0,0 +1,28 @@
+Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱
+
+For example, this is a valid use of ❰++❱: 
+
+
+    ┌────────────────┐
+    │ "ABC" ++ "DEF" │
+    └────────────────┘
+
+
+You provided this argument:
+
+↳ $txt0
+
+... which does not have type ❰Text❱ but instead has type:
+
+↳ $txt1
+
+Some common reasons why you might get this error:
+
+● You might have thought that ❰++❱ was the operator to combine two lists:
+
+    ┌───────────────────────────────────────────────────────────┐
+    │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │  Not valid
+    └───────────────────────────────────────────────────────────┘
+
+  The Dhall programming language does not provide a built-in operator for
+  combining two lists
diff --git a/dhall/src/error/text/DuplicateAlternative.txt b/dhall/src/error/text/DuplicateAlternative.txt
new file mode 100644
index 0000000..077f8aa
--- /dev/null
+++ b/dhall/src/error/text/DuplicateAlternative.txt
@@ -0,0 +1,18 @@
+Explanation: Unions may not have two alternatives that share the same name
+
+For example, the following expressions are $_NOT valid:
+
+
+    ┌─────────────────────────────┐
+    │ < foo = True | foo : Text > │  Invalid: ❰foo❱ appears twice
+    └─────────────────────────────┘
+
+
+    ┌───────────────────────────────────────┐
+    │ < foo = 1 | bar : Bool | bar : Text > │  Invalid: ❰bar❱ appears twice
+    └───────────────────────────────────────┘
+
+
+You have more than one alternative named:
+
+↳ $txt0
diff --git a/dhall/src/error/text/FieldCollision.txt b/dhall/src/error/text/FieldCollision.txt
new file mode 100644
index 0000000..2b2d260
--- /dev/null
+++ b/dhall/src/error/text/FieldCollision.txt
@@ -0,0 +1,43 @@
+Explanation: You can combine records if they don't share any fields in common,
+like this:
+
+
+    ┌───────────────────────────────────────────┐
+    │ { foo = 1, bar = "ABC" } ∧ { baz = True } │
+    └───────────────────────────────────────────┘
+
+
+    ┌────────────────────────────────────────┐
+    │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │
+    └────────────────────────────────────────┘
+
+
+... but you cannot merge two records that share the same field
+
+For example, the following expression is $_NOT valid:
+
+
+    ┌───────────────────────────────────────────┐
+    │ { foo = 1, bar = "ABC" } ∧ { foo = True } │  Invalid: Colliding ❰foo❱ fields
+    └───────────────────────────────────────────┘
+
+
+You combined two records that share the following field:
+
+↳ $txt0
+
+... which is not allowed
+
+Some common reasons why you might get this error:
+
+● You tried to use ❰∧❱ to update a field's value, like this:
+
+
+    ┌────────────────────────────────────────┐
+    │ { foo = 1, bar = "ABC" } ∧ { foo = 2 } │
+    └────────────────────────────────────────┘
+                                   ⇧
+                                   Invalid attempt to update ❰foo❱'s value to ❰2❱
+
+  Field updates are intentionally not allowed as the Dhall language discourages
+  patch-oriented programming
diff --git a/dhall/src/error/text/HandlerInputTypeMismatch.txt b/dhall/src/error/text/HandlerInputTypeMismatch.txt
new file mode 100644
index 0000000..7d3525b
--- /dev/null
+++ b/dhall/src/error/text/HandlerInputTypeMismatch.txt
@@ -0,0 +1,49 @@
+Explanation: You can ❰merge❱ the alternatives of a union using a record with one
+handler per alternative, like this:
+
+
+    ┌─────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Bool                                     │
+    └─────────────────────────────────────────────────────────────────────┘
+
+
+... as long as the input type of each handler function matches the type of the
+corresponding alternative:
+
+
+    ┌───────────────────────────────────────────────────────────┐
+    │ union    : < Left : Natural       | Right : Bool        > │
+    └───────────────────────────────────────────────────────────┘
+                          ⇧                       ⇧
+                   These must match        These must match
+                          ⇩                       ⇩
+    ┌───────────────────────────────────────────────────────────┐
+    │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │
+    └───────────────────────────────────────────────────────────┘
+
+
+For example, the following expression is $_NOT valid:
+
+
+      Invalid: Doesn't match the type of the ❰Right❱ alternative
+                                                               ⇩
+    ┌──────────────────────────────────────────────────────────────────────┐
+    │     let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │
+    │ in  let union    = < Left = +2 | Right : Bool >                      │
+    │ in  merge handlers union : Bool                                      │
+    └──────────────────────────────────────────────────────────────────────┘
+
+
+Your handler for the following alternative:
+
+↳ $txt0
+
+... needs to accept an input value of type:
+
+↳ $txt1
+
+... but actually accepts an input value of a different type:
+
+↳ $txt2
diff --git a/dhall/src/error/text/HandlerNotAFunction.txt b/dhall/src/error/text/HandlerNotAFunction.txt
new file mode 100644
index 0000000..ff87443
--- /dev/null
+++ b/dhall/src/error/text/HandlerNotAFunction.txt
@@ -0,0 +1,32 @@
+Explanation: You can ❰merge❱ the alternatives of a union using a record with one
+handler per alternative, like this:
+
+
+    ┌─────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Bool                                     │
+    └─────────────────────────────────────────────────────────────────────┘
+
+
+... as long as each handler is a function
+
+For example, the following expression is $_NOT valid:
+
+
+    ┌─────────────────────────────────────────┐
+    │ merge { Foo = True } < Foo = 1 > : Bool │
+    └─────────────────────────────────────────┘
+                    ⇧
+                    Invalid: Not a function
+
+
+Your handler for this alternative:
+
+↳ $txt0
+
+... has the following type:
+
+↳ $txt1
+
+... which is not the type of a function
diff --git a/dhall/src/error/text/HandlerOutputTypeMismatch.txt b/dhall/src/error/text/HandlerOutputTypeMismatch.txt
new file mode 100644
index 0000000..f359459
--- /dev/null
+++ b/dhall/src/error/text/HandlerOutputTypeMismatch.txt
@@ -0,0 +1,51 @@
+Explanation: You can ❰merge❱ the alternatives of a union using a record with one
+handler per alternative, like this:
+
+
+    ┌─────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Bool                                     │
+    └─────────────────────────────────────────────────────────────────────┘
+
+
+... as long as the output type of each handler function matches the declared type
+of the result:
+
+
+    ┌───────────────────────────────────────────────────────────┐
+    │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │
+    └───────────────────────────────────────────────────────────┘
+                                    ⇧                    ⇧
+                                    These output types ...
+
+                             ... must match the declared type of the ❰merge❱
+                             ⇩
+    ┌─────────────────────────────┐
+    │ merge handlers union : Bool │
+    └─────────────────────────────┘
+
+
+For example, the following expression is $_NOT valid:
+
+
+    ┌──────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Text                                      │
+    └──────────────────────────────────────────────────────────────────────┘
+                                 ⇧
+                                 Invalid: Doesn't match output of either handler
+
+
+Your handler for the following alternative:
+
+↳ $txt0
+
+... needs to return an output value of type:
+
+↳ $txt1
+
+... but actually returns an output value of a different type:
+
+↳ $txt2
diff --git a/dhall/src/error/text/IfBranchMismatch.txt b/dhall/src/error/text/IfBranchMismatch.txt
new file mode 100644
index 0000000..a95b130
--- /dev/null
+++ b/dhall/src/error/text/IfBranchMismatch.txt
@@ -0,0 +1,63 @@
+Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which
+is an expression:
+
+
+                   Expression for ❰then❱ branch
+                   ⇩
+    ┌────────────────────────────────┐
+    │ if True then "Hello, world!"   │
+    │         else "Goodbye, world!" │
+    └────────────────────────────────┘
+                   ⇧
+                   Expression for ❰else❱ branch
+
+
+These two expressions must have the same type.  For example, the following ❰if❱
+expressions are all valid:
+
+
+    ┌──────────────────────────────────┐
+    │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱
+    └──────────────────────────────────┘
+
+
+    ┌────────────────────────────┐
+    │ λ(b : Bool) →              │
+    │     if b then Natural/even │ Both branches have type ❰Natural → Bool❱
+    │          else Natural/odd  │
+    └────────────────────────────┘
+
+
+However, the following expression is $_NOT valid:
+
+
+                   This branch has type ❰Integer❱
+                   ⇩
+    ┌────────────────────────┐
+    │ if True then 0         │
+    │         else "ABC"     │
+    └────────────────────────┘
+                   ⇧
+                   This branch has type ❰Text❱
+
+
+The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is
+always ❰True❱ or ❰False❱
+
+Your ❰if❱ expression has the following ❰then❱ branch:
+
+↳ $txt0
+
+... which has type:
+
+↳ $txt2
+
+... and the following ❰else❱ branch:
+
+↳ $txt1
+
+... which has a different type:
+
+↳ $txt3
+
+Fix your ❰then❱ and ❰else❱ branches to have matching types
diff --git a/dhall/src/error/text/IfBranchMustBeTerm.txt b/dhall/src/error/text/IfBranchMustBeTerm.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/dhall/src/error/text/IfBranchMustBeTerm.txt
@@ -0,0 +1,51 @@
+Explanation: Every ❰if❱ expression begins with a predicate which must have type
+❰Bool❱
+
+For example, these are valid ❰if❱ expressions:
+
+
+    ┌──────────────────────────────┐
+    │ if True then "Yes" else "No" │
+    └──────────────────────────────┘
+         ⇧
+         Predicate
+
+
+    ┌─────────────────────────────────────────┐
+    │ λ(x : Bool) → if x then False else True │
+    └─────────────────────────────────────────┘
+                       ⇧
+                       Predicate
+
+
+... but these are $_NOT valid ❰if❱ expressions:
+
+
+    ┌───────────────────────────┐
+    │ if 0 then "Yes" else "No" │  ❰0❱ does not have type ❰Bool❱
+    └───────────────────────────┘
+
+
+    ┌────────────────────────────┐
+    │ if "" then False else True │  ❰""❱ does not have type ❰Bool❱
+    └────────────────────────────┘
+
+
+Your ❰if❱ expression begins with the following predicate:
+
+↳ $txt0
+
+... that has type:
+
+↳ $txt1
+
+... but the predicate must instead have type ❰Bool❱
+
+Some common reasons why you might get this error:
+
+● You might be used to other programming languages that accept predicates other
+  than ❰Bool❱
+
+  For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
+  them as equivalent to ❰False❱.  However, the Dhall language does not permit
+  this
diff --git a/dhall/src/error/text/InvalidAlterantive.txt b/dhall/src/error/text/InvalidAlterantive.txt
new file mode 100644
index 0000000..391fc3a
--- /dev/null
+++ b/dhall/src/error/text/InvalidAlterantive.txt
@@ -0,0 +1,48 @@
+Explanation: Every union type specifies the type of each alternative, like this:
+
+
+               The type of the first alternative is ❰Bool❱
+               ⇩
+    ┌──────────────────────────────────┐
+    │ < Left : Bool, Right : Natural > │  A union type with two alternatives
+    └──────────────────────────────────┘
+                             ⇧
+                             The type of the second alternative is ❰Natural❱
+
+
+However, these alternatives can only be annotated with types.  For example, the
+following union types are $_NOT valid:
+
+
+    ┌────────────────────────────┐
+    │ < Left : Bool, Right : 1 > │  Invalid union type
+    └────────────────────────────┘
+                             ⇧
+                             This is a term and not a type
+
+
+    ┌───────────────────────────────┐
+    │ < Left : Bool, Right : Type > │  Invalid union type
+    └───────────────────────────────┘
+                             ⇧
+                             This is a kind and not a type
+
+
+You provided a union type with an alternative named:
+
+↳ $txt0
+
+... annotated with the following expression which is not a type:
+
+↳ $txt1
+
+Some common reasons why you might get this error:
+
+● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one
+  alternative:
+
+    ┌─────────────────┐
+    │ < Example : 1 > │
+    └─────────────────┘
+                ⇧
+                This could be ❰=❱ instead
diff --git a/dhall/src/error/text/InvalidAlterantiveType.txt b/dhall/src/error/text/InvalidAlterantiveType.txt
new file mode 100644
index 0000000..f5dadef
--- /dev/null
+++ b/dhall/src/error/text/InvalidAlterantiveType.txt
@@ -0,0 +1,49 @@
+Explanation: Every union literal begins by selecting one alternative and
+specifying the value for that alternative, like this:
+
+
+        Select the ❰Left❱ alternative, whose value is ❰True❱
+        ⇩
+    ┌──────────────────────────────────┐
+    │ < Left = True, Right : Natural > │  A union literal with two alternatives
+    └──────────────────────────────────┘
+
+
+However, this value must be a term and not a type.  For example, the following
+values are $_NOT valid:
+
+
+    ┌──────────────────────────────────┐
+    │ < Left = Text, Right : Natural > │  Invalid union literal
+    └──────────────────────────────────┘
+               ⇧
+               This is a type and not a term
+
+
+    ┌───────────────────────────────┐
+    │ < Left = Type, Right : Type > │  Invalid union type
+    └───────────────────────────────┘
+               ⇧
+               This is a kind and not a term
+
+
+You provided a union literal with an alternative named:
+
+↳ $txt0
+
+... whose value is:
+
+↳ $txt1
+
+... which is not a term
+
+Some common reasons why you might get this error:
+
+● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one
+  alternative:
+
+    ┌────────────────────┐
+    │ < Example = Text > │
+    └────────────────────┘
+                ⇧
+                This could be ❰:❱ instead
diff --git a/dhall/src/error/text/InvalidField.txt b/dhall/src/error/text/InvalidField.txt
new file mode 100644
index 0000000..bfbf106
--- /dev/null
+++ b/dhall/src/error/text/InvalidField.txt
@@ -0,0 +1,35 @@
+Explanation: Every record literal is a set of fields assigned to values, like
+this:
+
+    ┌────────────────────────────────────────┐
+    │ { foo = 100, bar = True, baz = "ABC" } │
+    └────────────────────────────────────────┘
+
+However, fields can only be terms and cannot be types or kinds
+
+For example, these record literals are $_NOT valid:
+
+
+    ┌───────────────────────────┐
+    │ { foo = 100, bar = Text } │
+    └───────────────────────────┘
+                         ⇧
+                         ❰Text❱ is a type and not a term
+
+
+    ┌───────────────────────────┐
+    │ { foo = 100, bar = Type } │
+    └───────────────────────────┘
+                         ⇧
+                         ❰Type❱ is a kind and not a term
+
+
+You provided a record literal with a key named:
+
+↳ $txt0
+
+... whose value is:
+
+↳ $txt1
+
+... which is not a term
diff --git a/dhall/src/error/text/InvalidFieldType.txt b/dhall/src/error/text/InvalidFieldType.txt
new file mode 100644
index 0000000..4f76a64
--- /dev/null
+++ b/dhall/src/error/text/InvalidFieldType.txt
@@ -0,0 +1,34 @@
+Explanation: Every record type documents the type of each field, like this:
+
+    ┌──────────────────────────────────────────────┐
+    │ { foo : Integer, bar : Integer, baz : Text } │
+    └──────────────────────────────────────────────┘
+
+However, fields cannot be annotated with expressions other than types
+
+For example, these record types are $_NOT valid:
+
+
+    ┌────────────────────────────┐
+    │ { foo : Integer, bar : 1 } │
+    └────────────────────────────┘
+                             ⇧
+                             ❰1❱ is an ❰Integer❱ and not a ❰Type❱
+
+
+    ┌───────────────────────────────┐
+    │ { foo : Integer, bar : Type } │
+    └───────────────────────────────┘
+                             ⇧
+                             ❰Type❱ is a ❰Kind❱ and not a ❰Type❱
+
+
+You provided a record type with a key named:
+
+↳ $txt0
+
+... annotated with the following expression:
+
+↳ $txt1
+
+... which is not a type
diff --git a/dhall/src/error/text/InvalidInputType.txt b/dhall/src/error/text/InvalidInputType.txt
new file mode 100644
index 0000000..eabafa4
--- /dev/null
+++ b/dhall/src/error/text/InvalidInputType.txt
@@ -0,0 +1,61 @@
+Explanation: A function can accept an input "term" that has a given "type", like
+this:
+
+
+        This is the input term that the function accepts
+        ⇩
+    ┌───────────────────────┐
+    │ ∀(x : Natural) → Bool │  This is the type of a function that accepts an
+    └───────────────────────┘  input term named ❰x❱ that has type ❰Natural❱
+            ⇧
+            This is the type of the input term
+
+
+    ┌────────────────┐
+    │ Bool → Integer │  This is the type of a function that accepts an anonymous
+    └────────────────┘  input term that has type ❰Bool❱
+      ⇧
+      This is the type of the input term
+
+
+... or a function can accept an input "type" that has a given "kind", like this:
+
+
+        This is the input type that the function accepts
+        ⇩
+    ┌────────────────────┐
+    │ ∀(a : Type) → Type │  This is the type of a function that accepts an input
+    └────────────────────┘  type named ❰a❱ that has kind ❰Type❱
+            ⇧
+            This is the kind of the input type
+
+
+    ┌──────────────────────┐
+    │ (Type → Type) → Type │  This is the type of a function that accepts an
+    └──────────────────────┘  anonymous input type that has kind ❰Type → Type❱
+       ⇧
+       This is the kind of the input type
+
+
+Other function inputs are $_NOT valid, like this:
+
+
+    ┌──────────────┐
+    │ ∀(x : 1) → x │  ❰1❱ is a "term" and not a "type" nor a "kind" so ❰x❱
+    └──────────────┘  cannot have "type" ❰1❱ or "kind" ❰1❱
+            ⇧
+            This is not a type or kind
+
+
+    ┌──────────┐
+    │ True → x │  ❰True❱ is a "term" and not a "type" nor a "kind" so the
+    └──────────┘  anonymous input cannot have "type" ❰True❱ or "kind" ❰True❱
+      ⇧
+      This is not a type or kind
+
+
+You annotated a function input with the following expression:
+
+↳ $txt
+
+... which is neither a type nor a kind
diff --git a/dhall/src/error/text/InvalidListElement.txt b/dhall/src/error/text/InvalidListElement.txt
new file mode 100644
index 0000000..59db7b7
--- /dev/null
+++ b/dhall/src/error/text/InvalidListElement.txt
@@ -0,0 +1,30 @@
+Explanation: Every element in the list must have a type matching the type
+annotation at the end of the list
+
+For example, this is a valid ❰List❱:
+
+
+    ┌──────────────────────────┐
+    │ [1, 2, 3] : List Integer │  Every element in this ❰List❱ is an ❰Integer❱
+    └──────────────────────────┘
+
+
+.. but this is $_NOT a valid ❰List❱:
+
+
+    ┌──────────────────────────────┐
+    │ [1, "ABC", 3] : List Integer │  The second element is not an ❰Integer❱
+    └──────────────────────────────┘
+
+
+Your ❰List❱ elements should have this type:
+
+↳ $txt0
+
+... but the following element at index $txt1:
+
+↳ $txt2
+
+... has this type instead:
+
+↳ $txt3
diff --git a/dhall/src/error/text/InvalidListType.txt b/dhall/src/error/text/InvalidListType.txt
new file mode 100644
index 0000000..676647e
--- /dev/null
+++ b/dhall/src/error/text/InvalidListType.txt
@@ -0,0 +1,43 @@
+Explanation: Every ❰List❱ documents the type of its elements with a type
+annotation, like this:
+
+
+    ┌──────────────────────────┐
+    │ [1, 2, 3] : List Integer │  A ❰List❱ of three ❰Integer❱s
+    └──────────────────────────┘
+                       ⇧
+                       The type of the ❰List❱'s elements, which are ❰Integer❱s
+
+
+    ┌───────────────────┐
+    │ [] : List Integer │  An empty ❰List❱
+    └───────────────────┘
+                ⇧
+                You still specify the type even when the ❰List❱ is empty
+
+
+The element type must be a type and not something else.  For example, the
+following element types are $_NOT valid:
+
+
+    ┌──────────────┐
+    │ ... : List 1 │
+    └──────────────┘
+                 ⇧
+                 This is an ❰Integer❱ and not a ❰Type❱
+
+
+    ┌─────────────────┐
+    │ ... : List Type │
+    └─────────────────┘
+                 ⇧
+                 This is a ❰Kind❱ and not a ❰Type❱
+
+
+Even if the ❰List❱ is empty you still must specify a valid type
+
+You declared that the ❰List❱'s elements should have type:
+
+↳ $txt0
+
+... which is not a ❰Type❱
diff --git a/dhall/src/error/text/InvalidOptionType.txt b/dhall/src/error/text/InvalidOptionType.txt
new file mode 100644
index 0000000..3bc81de
--- /dev/null
+++ b/dhall/src/error/text/InvalidOptionType.txt
@@ -0,0 +1,44 @@
+Explanation: Every optional element ends with a type annotation for the element
+that might be present, like this:
+
+
+    ┌────────────────────────┐
+    │ [1] : Optional Integer │  An optional element that's present
+    └────────────────────────┘
+                     ⇧
+                     The type of the ❰Optional❱ element, which is an ❰Integer❱
+
+
+    ┌────────────────────────┐
+    │ [] : Optional Integer  │  An optional element that's absent
+    └────────────────────────┘
+                    ⇧
+                    You still specify the type even when the element is absent
+
+
+The element type must be a type and not something else.  For example, the
+following element types are $_NOT valid:
+
+
+    ┌──────────────────┐
+    │ ... : Optional 1 │
+    └──────────────────┘
+                     ⇧
+                     This is an ❰Integer❱ and not a ❰Type❱
+
+
+    ┌─────────────────────┐
+    │ ... : Optional Type │
+    └─────────────────────┘
+                     ⇧
+                     This is a ❰Kind❱ and not a ❰Type❱
+
+
+Even if the element is absent you still must specify a valid type
+
+You declared that the ❰Optional❱ element should have type:
+
+↳ $txt0
+
+... which is not a ❰Type❱
+
diff --git a/dhall/src/error/text/InvalidOptionalElement.txt b/dhall/src/error/text/InvalidOptionalElement.txt
new file mode 100644
index 0000000..0254220
--- /dev/null
+++ b/dhall/src/error/text/InvalidOptionalElement.txt
@@ -0,0 +1,29 @@
+Explanation: An ❰Optional❱ element must have a type matching the type annotation
+
+For example, this is a valid ❰Optional❱ value:
+
+
+    ┌────────────────────────┐
+    │ [1] : Optional Integer │  ❰1❱ is an ❰Integer❱, which matches the type
+    └────────────────────────┘
+
+
+... but this is $_NOT a valid ❰Optional❱ value:
+
+
+    ┌────────────────────────────┐
+    │ ["ABC"] : Optional Integer │  ❰"ABC"❱ is not an ❰Integer❱
+    └────────────────────────────┘
+
+
+Your ❰Optional❱ element should have this type:
+
+↳ $txt0
+
+... but the element you provided:
+
+↳ $txt1
+
+... has this type instead:
+
+↳ $txt2
diff --git a/dhall/src/error/text/InvalidOptionalLiteral.txt b/dhall/src/error/text/InvalidOptionalLiteral.txt
new file mode 100644
index 0000000..41c0fdc
--- /dev/null
+++ b/dhall/src/error/text/InvalidOptionalLiteral.txt
@@ -0,0 +1,53 @@
+Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s:
+
+
+    ┌───────────────────────┐
+    │ [] : Optional Integer │  An ❰Optional❱ value which is absent
+    └───────────────────────┘
+
+
+    ┌───────────────────────┐
+    │ [] : List     Integer │  An empty (0-element) ❰List❱
+    └───────────────────────┘
+
+
+    ┌────────────────────────┐
+    │ [1] : Optional Integer │  An ❰Optional❱ value which is present
+    └────────────────────────┘
+
+
+    ┌────────────────────────┐
+    │ [1] : List     Integer │  A singleton (1-element) ❰List❱
+    └────────────────────────┘
+
+
+However, an ❰Optional❱ value can $_NOT have more than one element, whereas a
+❰List❱ can have multiple elements:
+
+
+    ┌───────────────────────────┐
+    │ [1, 2] : Optional Integer │  Invalid: multiple elements $_NOT allowed
+    └───────────────────────────┘
+
+
+    ┌───────────────────────────┐
+    │ [1, 2] : List     Integer │  Valid: multiple elements allowed
+    └───────────────────────────┘
+
+
+Your ❰Optional❱ value had this many elements:
+
+↳ $txt0
+
+... when an ❰Optional❱ value can only have at most one element
+
+Some common reasons why you might get this error:
+
+● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this:
+
+
+    ┌────────────────────────────────────────────────────┐
+    │ List/length Integer ([1, 2, 3] : Optional Integer) │
+    └────────────────────────────────────────────────────┘
+                                       ⇧
+                                       This should be ❰List❱ instead
diff --git a/dhall/src/error/text/InvalidOutputType.txt b/dhall/src/error/text/InvalidOutputType.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/dhall/src/error/text/InvalidOutputType.txt
@@ -0,0 +1,68 @@
+Explanation: A function can return an output "term" that has a given "type",
+like this:
+
+
+    ┌────────────────────┐
+    │ ∀(x : Text) → Bool │  This is the type of a function that returns an
+    └────────────────────┘  output term that has type ❰Bool❱
+                    ⇧
+                    This is the type of the output term
+
+
+    ┌────────────────┐
+    │ Bool → Integer │  This is the type of a function that returns an output
+    └────────────────┘  term that has type ❰Int❱
+             ⇧
+             This is the type of the output term
+
+
+... or a function can return an output "type" that has a given "kind", like
+this:
+
+    ┌────────────────────┐
+    │ ∀(a : Type) → Type │  This is the type of a function that returns an
+    └────────────────────┘  output type that has kind ❰Type❱
+                    ⇧
+                    This is the kind of the output type
+
+
+    ┌──────────────────────┐
+    │ (Type → Type) → Type │  This is the type of a function that returns an
+    └──────────────────────┘  output type that has kind ❰Type❱
+                      ⇧
+                      This is the kind of the output type
+
+
+Other outputs are $_NOT valid, like this:
+
+
+    ┌─────────────────┐
+    │ ∀(x : Bool) → x │  ❰x❱ is a "term" and not a "type" nor a "kind" so the
+    └─────────────────┘  output cannot have "type" ❰x❱ or "kind" ❰x❱
+                    ⇧
+                    This is not a type or kind
+
+
+    ┌─────────────┐
+    │ Text → True │  ❰True❱ is a "term" and not a "type" nor a "kind" so the
+    └─────────────┘  output cannot have "type" ❰True❱ or "kind" ❰True❱
+             ⇧
+             This is not a type or kind
+
+
+You specified that your function outputs a:
+
+↳ $txt
+
+... which is neither a type nor a kind:
+
+Some common reasons why you might get this error:
+
+● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:
+
+
+    ┌────────────────┐
+    │ ∀(x: Bool) → x │
+    └────────────────┘
+      ⇧
+      Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function
diff --git a/dhall/src/error/text/InvalidPredicate.txt b/dhall/src/error/text/InvalidPredicate.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/dhall/src/error/text/InvalidPredicate.txt
@@ -0,0 +1,51 @@
+Explanation: Every ❰if❱ expression begins with a predicate which must have type
+❰Bool❱
+
+For example, these are valid ❰if❱ expressions:
+
+
+    ┌──────────────────────────────┐
+    │ if True then "Yes" else "No" │
+    └──────────────────────────────┘
+         ⇧
+         Predicate
+
+
+    ┌─────────────────────────────────────────┐
+    │ λ(x : Bool) → if x then False else True │
+    └─────────────────────────────────────────┘
+                       ⇧
+                       Predicate
+
+
+... but these are $_NOT valid ❰if❱ expressions:
+
+
+    ┌───────────────────────────┐
+    │ if 0 then "Yes" else "No" │  ❰0❱ does not have type ❰Bool❱
+    └───────────────────────────┘
+
+
+    ┌────────────────────────────┐
+    │ if "" then False else True │  ❰""❱ does not have type ❰Bool❱
+    └────────────────────────────┘
+
+
+Your ❰if❱ expression begins with the following predicate:
+
+↳ $txt0
+
+... that has type:
+
+↳ $txt1
+
+... but the predicate must instead have type ❰Bool❱
+
+Some common reasons why you might get this error:
+
+● You might be used to other programming languages that accept predicates other
+  than ❰Bool❱
+
+  For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
+  them as equivalent to ❰False❱.  However, the Dhall language does not permit
+  this
diff --git a/dhall/src/error/text/MissingField.txt b/dhall/src/error/text/MissingField.txt
new file mode 100644
index 0000000..de14a33
--- /dev/null
+++ b/dhall/src/error/text/MissingField.txt
@@ -0,0 +1,30 @@
+Explanation: You can only access fields on records, like this:
+
+
+    ┌─────────────────────────────────┐
+    │ { foo = True, bar = "ABC" }.foo │  This is valid ...
+    └─────────────────────────────────┘
+
+
+    ┌───────────────────────────────────────────┐
+    │ λ(r : { foo : Bool, bar : Text }) → r.foo │  ... and so is this
+    └───────────────────────────────────────────┘
+
+
+... but you can only access fields if they are present
+
+For example, the following expression is $_NOT valid:
+
+    ┌─────────────────────────────────┐
+    │ { foo = True, bar = "ABC" }.qux │
+    └─────────────────────────────────┘
+                                  ⇧
+                                  Invalid: the record has no ❰qux❱ field
+
+You tried to access a field named:
+
+↳ $txt0
+
+... but the field is missing because the record only defines the following fields:
+
+↳ $txt1
diff --git a/dhall/src/error/text/MissingHandler.txt b/dhall/src/error/text/MissingHandler.txt
new file mode 100644
index 0000000..433445e
--- /dev/null
+++ b/dhall/src/error/text/MissingHandler.txt
@@ -0,0 +1,32 @@
+Explanation: You can ❰merge❱ the alternatives of a union using a record with one
+handler per alternative, like this:
+
+
+    ┌─────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Bool                                     │
+    └─────────────────────────────────────────────────────────────────────┘
+
+
+... but you must provide exactly one handler per alternative in the union.  You
+cannot omit any handlers
+
+For example, the following expression is $_NOT valid:
+
+
+                                              Invalid: Missing ❰Right❱ handler
+                                              ⇩
+    ┌─────────────────────────────────────────────────┐
+    │     let handlers = { Left = Natural/even }      │
+    │ in  let union    = < Left = +2 | Right : Bool > │
+    │ in  merge handlers union : Bool                 │
+    └─────────────────────────────────────────────────┘
+
+
+Note that you need to provide handlers for other alternatives even if those
+alternatives are never used
+
+You need to supply the following handlers:
+
+↳ $txt0
diff --git a/dhall/src/error/text/MustCombineARecord.txt b/dhall/src/error/text/MustCombineARecord.txt
new file mode 100644
index 0000000..141b969
--- /dev/null
+++ b/dhall/src/error/text/MustCombineARecord.txt
@@ -0,0 +1,46 @@
+Explanation: You can combine records using the ❰∧❱ operator, like this:
+
+
+    ┌───────────────────────────────────────────┐
+    │ { foo = 1, bar = "ABC" } ∧ { baz = True } │
+    └───────────────────────────────────────────┘
+
+
+    ┌─────────────────────────────────────────────┐
+    │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │
+    └─────────────────────────────────────────────┘
+
+
+... but you cannot combine values that are not records.
+
+For example, the following expressions are $_NOT valid:
+
+
+    ┌──────────────────────────────┐
+    │ { foo = 1, bar = "ABC" } ∧ 1 │
+    └──────────────────────────────┘
+                                 ⇧
+                                 Invalid: Not a record
+
+
+    ┌───────────────────────────────────────────┐
+    │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │
+    └───────────────────────────────────────────┘
+                                 ⇧
+                                 Invalid: This is a record type and not a record
+
+
+    ┌───────────────────────────────────────────┐
+    │ { foo = 1, bar = "ABC" } ∧ < baz = True > │
+    └───────────────────────────────────────────┘
+                                 ⇧
+                                 Invalid: This is a union and not a record
+
+
+You tried to combine the following value:
+
+↳ $txt0
+
+... which is not a record, but is actually a:
+
+↳ $txt1
diff --git a/dhall/src/error/text/MustMergeARecord.txt b/dhall/src/error/text/MustMergeARecord.txt
new file mode 100644
index 0000000..79094bd
--- /dev/null
+++ b/dhall/src/error/text/MustMergeARecord.txt
@@ -0,0 +1,43 @@
+Explanation: You can ❰merge❱ the alternatives of a union using a record with one
+handler per alternative, like this:
+
+
+    ┌─────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Bool                                     │
+    └─────────────────────────────────────────────────────────────────────┘
+
+
+... but the first argument to ❰merge❱ must be a record and not some other type.
+
+For example, the following expression is $_NOT valid:
+
+
+    ┌─────────────────────────────────────────┐
+    │ let handler = λ(x : Bool) → x           │
+    │ in  merge handler < Foo = True > : True │
+    └─────────────────────────────────────────┘
+                ⇧
+                Invalid: ❰handler❱ isn't a record
+
+
+You provided the following handler:
+
+↳ $txt0
+
+... which is not a record, but is actually a value of type:
+
+↳ $txt1
+
+Some common reasons why you might get this error:
+
+● You accidentally provide an empty record type instead of an empty record when
+  you ❰merge❱ an empty union:
+
+
+    ┌──────────────────────────────────────────┐
+    │ λ(x : <>) → λ(a : Type) → merge {} x : a │
+    └──────────────────────────────────────────┘
+                                      ⇧
+                                      This should be ❰{=}❱ instead
diff --git a/dhall/src/error/text/MustMergeUnion.txt b/dhall/src/error/text/MustMergeUnion.txt
new file mode 100644
index 0000000..68df70c
--- /dev/null
+++ b/dhall/src/error/text/MustMergeUnion.txt
@@ -0,0 +1,31 @@
+Explanation: You can ❰merge❱ the alternatives of a union using a record with one
+handler per alternative, like this:
+
+
+    ┌─────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Bool                                     │
+    └─────────────────────────────────────────────────────────────────────┘
+
+
+... but the second argument to ❰merge❱ must be a union and not some other type.
+
+For example, the following expression is $_NOT valid:
+
+
+    ┌──────────────────────────────────────────┐
+    │ let handlers = { Foo = λ(x : Bool) → x } │
+    │ in  merge handlers True : True           │
+    └──────────────────────────────────────────┘
+                         ⇧
+                         Invalid: ❰True❱ isn't a union
+
+
+You tried to ❰merge❱ this expression:
+
+↳ $txt0
+
+... which is not a union, but is actually a value of type:
+
+↳ $txt1
diff --git a/dhall/src/error/text/NoDependentLet.txt b/dhall/src/error/text/NoDependentLet.txt
new file mode 100644
index 0000000..fdc65b4
--- /dev/null
+++ b/dhall/src/error/text/NoDependentLet.txt
@@ -0,0 +1,76 @@
+Explanation: The Dhall programming language does not allow ❰let❱ expressions
+from terms to types.  These ❰let❱ expressions are also known as "dependent ❰let❱
+expressions" because you have a type whose value depends on the value of a term.
+
+The Dhall language forbids these dependent ❰let❱ expressions in order to
+guarantee that ❰let❱ expressions of the form:
+
+
+    ┌────────────────────┐
+    │ let x : t = r in e │
+    └────────────────────┘
+
+
+... are always equivalent to:
+
+
+    ┌──────────────────┐
+    │ (λ(x : t) → e) r │
+    └──────────────────┘
+
+
+This means that both expressions should normalize to the same result and if one
+of the two fails to type check then the other should fail to type check, too.
+
+For this reason, the following is $_NOT legal code:
+
+
+    ┌───────────────────┐
+    │ let x = 2 in Text │
+    └───────────────────┘
+
+
+... because the above ❰let❱ expression is equivalent to:
+
+
+    ┌─────────────────────────────┐
+    │ let x : Integer = 2 in Text │
+    └─────────────────────────────┘
+
+
+... which in turn must be equivalent to:
+
+
+    ┌───────────────────────────┐
+    │ (λ(x : Integer) → Text) 2 │
+    └───────────────────────────┘
+
+
+... which in turn fails to type check because this sub-expression:
+
+
+    ┌───────────────────────┐
+    │ λ(x : Integer) → Text │
+    └───────────────────────┘
+
+
+... has type:
+
+
+    ┌───────────────────────┐
+    │ ∀(x : Integer) → Text │
+    └───────────────────────┘
+
+
+... which is a forbidden dependent function type (i.e. a function from a term to
+a type).  Therefore the equivalent ❰let❱ expression is also forbidden.
+
+Your ❰let❱ expression is invalid because the input has type:
+
+↳ $txt0
+
+... and the output has kind:
+
+↳ $txt1
+
+... which makes this a forbidden dependent ❰let❱ expression
diff --git a/dhall/src/error/text/NoDependentTypes.txt b/dhall/src/error/text/NoDependentTypes.txt
new file mode 100644
index 0000000..435bdcb
--- /dev/null
+++ b/dhall/src/error/text/NoDependentTypes.txt
@@ -0,0 +1,31 @@
+Explanation: The Dhall programming language does not allow functions from terms
+to types.  These function types are also known as "dependent function types"
+because you have a type whose value "depends" on the value of a term.
+
+For example, this is $_NOT a legal function type:
+
+
+    ┌─────────────┐
+    │ Bool → Type │
+    └─────────────┘
+
+
+Similarly, this is $_NOT legal code:
+
+
+    ┌────────────────────────────────────────────────────┐
+    │ λ(Vector : Natural → Type → Type) → Vector +0 Text │
+    └────────────────────────────────────────────────────┘
+                 ⇧
+                 Invalid dependent type
+
+
+Your function type is invalid because the input has type:
+
+↳ $txt0
+
+... and the output has kind:
+
+↳ $txt1
+
+... which makes this a forbidden dependent function type
diff --git a/dhall/src/error/text/NotAFunction.txt b/dhall/src/error/text/NotAFunction.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/dhall/src/error/text/NotAFunction.txt
@@ -0,0 +1,68 @@
+Explanation: A function can return an output "term" that has a given "type",
+like this:
+
+
+    ┌────────────────────┐
+    │ ∀(x : Text) → Bool │  This is the type of a function that returns an
+    └────────────────────┘  output term that has type ❰Bool❱
+                    ⇧
+                    This is the type of the output term
+
+
+    ┌────────────────┐
+    │ Bool → Integer │  This is the type of a function that returns an output
+    └────────────────┘  term that has type ❰Int❱
+             ⇧
+             This is the type of the output term
+
+
+... or a function can return an output "type" that has a given "kind", like
+this:
+
+    ┌────────────────────┐
+    │ ∀(a : Type) → Type │  This is the type of a function that returns an
+    └────────────────────┘  output type that has kind ❰Type❱
+                    ⇧
+                    This is the kind of the output type
+
+
+    ┌──────────────────────┐
+    │ (Type → Type) → Type │  This is the type of a function that returns an
+    └──────────────────────┘  output type that has kind ❰Type❱
+                      ⇧
+                      This is the kind of the output type
+
+
+Other outputs are $_NOT valid, like this:
+
+
+    ┌─────────────────┐
+    │ ∀(x : Bool) → x │  ❰x❱ is a "term" and not a "type" nor a "kind" so the
+    └─────────────────┘  output cannot have "type" ❰x❱ or "kind" ❰x❱
+                    ⇧
+                    This is not a type or kind
+
+
+    ┌─────────────┐
+    │ Text → True │  ❰True❱ is a "term" and not a "type" nor a "kind" so the
+    └─────────────┘  output cannot have "type" ❰True❱ or "kind" ❰True❱
+             ⇧
+             This is not a type or kind
+
+
+You specified that your function outputs a:
+
+↳ $txt
+
+... which is neither a type nor a kind:
+
+Some common reasons why you might get this error:
+
+● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:
+
+
+    ┌────────────────┐
+    │ ∀(x: Bool) → x │
+    └────────────────┘
+      ⇧
+      Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function
diff --git a/dhall/src/error/text/NotARecord.txt b/dhall/src/error/text/NotARecord.txt
new file mode 100644
index 0000000..e0eebc8
--- /dev/null
+++ b/dhall/src/error/text/NotARecord.txt
@@ -0,0 +1,48 @@
+Explanation: You can only access fields on records, like this:
+
+
+    ┌─────────────────────────────────┐
+    │ { foo = True, bar = "ABC" }.foo │  This is valid ...
+    └─────────────────────────────────┘
+
+
+    ┌───────────────────────────────────────────┐
+    │ λ(r : { foo : Bool, bar : Text }) → r.foo │  ... and so is this
+    └───────────────────────────────────────────┘
+
+
+... but you cannot access fields on non-record expressions
+
+For example, the following expression is $_NOT valid:
+
+
+    ┌───────┐
+    │ 1.foo │
+    └───────┘
+      ⇧
+      Invalid: Not a record
+
+
+You tried to access a field named:
+
+↳ $txt0
+
+... on the following expression which is not a record:
+
+↳ $txt1
+
+... but is actually an expression of type:
+
+↳ $txt2
+
+Some common reasons why you might get this error:
+
+● You accidentally try to access a field of a union instead of a record, like
+  this:
+
+
+    ┌─────────────────┐
+    │ < foo : a >.foo │
+    └─────────────────┘
+      ⇧
+      This is a union, not a record
diff --git a/dhall/src/error/text/TypeMismatch.txt b/dhall/src/error/text/TypeMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/dhall/src/error/text/TypeMismatch.txt
@@ -0,0 +1,117 @@
+Explanation: Every function declares what type or kind of argument to accept
+
+For example:
+
+
+    ┌───────────────────────────────┐
+    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts
+    └───────────────────────────────┘  arguments that have type ❰Bool❱
+                        ⇧
+                        The function's input type
+
+
+    ┌───────────────────────────────┐
+    │ Natural/even : Natural → Bool │  This built-in function only accepts
+    └───────────────────────────────┘  arguments that have type ❰Natural❱
+                     ⇧
+                     The function's input type
+
+
+    ┌───────────────────────────────┐
+    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts
+    └───────────────────────────────┘  arguments that have kind ❰Type❱
+                        ⇧
+                        The function's input kind
+
+
+    ┌────────────────────┐
+    │ List : Type → Type │  This built-in function only accepts arguments that
+    └────────────────────┘  have kind ❰Type❱
+             ⇧
+             The function's input kind
+
+
+For example, the following expressions are valid:
+
+
+    ┌────────────────────────┐
+    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type
+    └────────────────────────┘  of argument that the anonymous function accepts
+
+
+    ┌─────────────────┐
+    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
+    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,
+
+
+    ┌────────────────────────┐
+    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
+    └────────────────────────┘  of argument that the anonymous function accepts
+
+
+    ┌───────────┐
+    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
+    └───────────┘  that that the ❰List❱ function accepts
+
+
+However, you can $_NOT apply a function to the wrong type or kind of argument
+
+For example, the following expressions are not valid:
+
+
+    ┌───────────────────────┐
+    │ (λ(x : Bool) → x) "A" │  ❰"A"❱ has type ❰Text❱, but the anonymous function
+    └───────────────────────┘  expects an argument that has type ❰Bool❱
+
+
+    ┌──────────────────┐
+    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
+    └──────────────────┘  expects an argument that has type ❰Natural❱
+
+
+    ┌────────────────────────┐
+    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
+    └────────────────────────┘  function expects an argument of kind ❰Type❱
+
+
+    ┌────────┐
+    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
+    └────────┘  argument that has kind ❰Type❱
+
+
+You tried to invoke the following function:
+
+↳ $txt0
+
+... which expects an argument of type or kind:
+
+↳ $txt1
+
+... on the following argument:
+
+↳ $txt2
+
+... which has a different type or kind:
+
+↳ $txt3
+
+Some common reasons why you might get this error:
+
+● You omit a function argument by mistake:
+
+
+    ┌────────────────────────────────────────┐
+    │ List/head   ([1, 2, 3] : List Integer) │
+    └────────────────────────────────────────┘
+                ⇧
+                ❰List/head❱ is missing the first argument,
+                which should be: ❰Integer❱
+
+
+● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
+
+    ┌────────────────┐
+    │ Natural/even 2 │
+    └────────────────┘
+                   ⇧
+                   This should be ❰+2❱
diff --git a/dhall/src/error/text/UnboundVariable.txt b/dhall/src/error/text/UnboundVariable.txt
new file mode 100644
index 0000000..bd7d483
--- /dev/null
+++ b/dhall/src/error/text/UnboundVariable.txt
@@ -0,0 +1,97 @@
+Explanation: Expressions can only reference previously introduced (i.e. "bound")
+variables that are still "in scope"
+
+For example, the following valid expressions introduce a "bound" variable named
+❰x❱:
+
+
+    ┌─────────────────┐
+    │ λ(x : Bool) → x │  Anonymous functions introduce "bound" variables
+    └─────────────────┘
+        ⇧
+        This is the bound variable
+
+
+    ┌─────────────────┐
+    │ let x = 1 in x  │  ❰let❱ expressions introduce "bound" variables
+    └─────────────────┘
+          ⇧
+          This is the bound variable
+
+
+However, the following expressions are not valid because they all reference a
+variable that has not been introduced yet (i.e. an "unbound" variable):
+
+
+    ┌─────────────────┐
+    │ λ(x : Bool) → y │  The variable ❰y❱ hasn't been introduced yet
+    └─────────────────┘
+                    ⇧
+                    This is the unbound variable
+
+
+    ┌──────────────────────────┐
+    │ (let x = True in x) && x │  ❰x❱ is undefined outside the parentheses
+    └──────────────────────────┘
+                             ⇧
+                             This is the unbound variable
+
+
+    ┌────────────────┐
+    │ let x = x in x │  The definition for ❰x❱ cannot reference itself
+    └────────────────┘
+              ⇧
+              This is the unbound variable
+
+
+Some common reasons why you might get this error:
+
+● You misspell a variable name, like this:
+
+
+    ┌────────────────────────────────────────────────────┐
+    │ λ(empty : Bool) → if emty then "Empty" else "Full" │
+    └────────────────────────────────────────────────────┘
+                           ⇧
+                           Typo
+
+
+● You misspell a reserved identifier, like this:
+
+
+    ┌──────────────────────────┐
+    │ foral (a : Type) → a → a │
+    └──────────────────────────┘
+      ⇧
+      Typo
+
+
+● You tried to define a recursive value, like this:
+
+
+    ┌─────────────────────┐
+    │ let x = x + +1 in x │
+    └─────────────────────┘
+              ⇧
+              Recursive definitions are not allowed
+
+
+● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱
+
+
+        Unbound variable
+        ⇩
+    ┌─────────────────┐
+    │  (x : Bool) → x │
+    └─────────────────┘
+      ⇧
+      A ❰λ❱ here would transform this into a valid anonymous function 
+
+
+        Unbound variable
+        ⇩
+    ┌────────────────────┐
+    │  (x : Bool) → Bool │
+    └────────────────────┘
+      ⇧
+      A ❰∀❱ or ❰forall❱ here would transform this into a valid function type
diff --git a/dhall/src/error/text/Untyped.txt b/dhall/src/error/text/Untyped.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/dhall/src/error/text/Untyped.txt
@@ -0,0 +1,117 @@
+Explanation: Every function declares what type or kind of argument to accept
+
+For example:
+
+
+    ┌───────────────────────────────┐
+    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts
+    └───────────────────────────────┘  arguments that have type ❰Bool❱
+                        ⇧
+                        The function's input type
+
+
+    ┌───────────────────────────────┐
+    │ Natural/even : Natural → Bool │  This built-in function only accepts
+    └───────────────────────────────┘  arguments that have type ❰Natural❱
+                     ⇧
+                     The function's input type
+
+
+    ┌───────────────────────────────┐
+    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts
+    └───────────────────────────────┘  arguments that have kind ❰Type❱
+                        ⇧
+                        The function's input kind
+
+
+    ┌────────────────────┐
+    │ List : Type → Type │  This built-in function only accepts arguments that
+    └────────────────────┘  have kind ❰Type❱
+             ⇧
+             The function's input kind
+
+
+For example, the following expressions are valid:
+
+
+    ┌────────────────────────┐
+    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type
+    └────────────────────────┘  of argument that the anonymous function accepts
+
+
+    ┌─────────────────┐
+    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
+    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,
+
+
+    ┌────────────────────────┐
+    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
+    └────────────────────────┘  of argument that the anonymous function accepts
+
+
+    ┌───────────┐
+    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
+    └───────────┘  that that the ❰List❱ function accepts
+
+
+However, you can $_NOT apply a function to the wrong type or kind of argument
+
+For example, the following expressions are not valid:
+
+
+    ┌───────────────────────┐
+    │ (λ(x : Bool) → x) "A" │  ❰"A"❱ has type ❰Text❱, but the anonymous function
+    └───────────────────────┘  expects an argument that has type ❰Bool❱
+
+
+    ┌──────────────────┐
+    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
+    └──────────────────┘  expects an argument that has type ❰Natural❱
+
+
+    ┌────────────────────────┐
+    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
+    └────────────────────────┘  function expects an argument of kind ❰Type❱
+
+
+    ┌────────┐
+    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
+    └────────┘  argument that has kind ❰Type❱
+
+
+You tried to invoke the following function:
+
+↳ $txt0
+
+... which expects an argument of type or kind:
+
+↳ $txt1
+
+... on the following argument:
+
+↳ $txt2
+
+... which has a different type or kind:
+
+↳ $txt3
+
+Some common reasons why you might get this error:
+
+● You omit a function argument by mistake:
+
+
+    ┌────────────────────────────────────────┐
+    │ List/head   ([1, 2, 3] : List Integer) │
+    └────────────────────────────────────────┘
+                ⇧
+                ❰List/head❱ is missing the first argument,
+                which should be: ❰Integer❱
+
+
+● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
+
+    ┌────────────────┐
+    │ Natural/even 2 │
+    └────────────────┘
+                   ⇧
+                   This should be ❰+2❱
diff --git a/dhall/src/error/text/UnusedHandler.txt b/dhall/src/error/text/UnusedHandler.txt
new file mode 100644
index 0000000..2e46a12
--- /dev/null
+++ b/dhall/src/error/text/UnusedHandler.txt
@@ -0,0 +1,32 @@
+Explanation: You can ❰merge❱ the alternatives of a union using a record with one
+handler per alternative, like this:
+
+
+    ┌─────────────────────────────────────────────────────────────────────┐
+    │     let union    = < Left = +2 | Right : Bool >                     │
+    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
+    │ in  merge handlers union : Bool                                     │
+    └─────────────────────────────────────────────────────────────────────┘
+
+
+... but you must provide exactly one handler per alternative in the union.  You
+cannot supply extra handlers
+
+For example, the following expression is $_NOT valid:
+
+
+    ┌───────────────────────────────────────┐
+    │     let union    = < Left = +2 >      │  The ❰Right❱ alternative is missing
+    │ in  let handlers =                    │ 
+    │             { Left  = Natural/even    │
+    │             , Right = λ(x : Bool) → x │  Invalid: ❰Right❱ handler isn't used
+    │             }                         │
+    │ in  merge handlers union : Bool       │
+    └───────────────────────────────────────┘
+
+
+You provided the following handlers:
+
+↳ $txt0
+
+... which had no matching alternatives in the union you tried to ❰merge❱
diff --git a/dhall/src/errors/AnnotMismatch.txt b/dhall/src/errors/AnnotMismatch.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/dhall/src/errors/AnnotMismatch.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-Explanation: Every function declares what type or kind of argument to accept
-
-For example:
-
-
-    ┌───────────────────────────────┐
-    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts
-    └───────────────────────────────┘  arguments that have type ❰Bool❱
-                        ⇧
-                        The function's input type
-
-
-    ┌───────────────────────────────┐
-    │ Natural/even : Natural → Bool │  This built-in function only accepts
-    └───────────────────────────────┘  arguments that have type ❰Natural❱
-                     ⇧
-                     The function's input type
-
-
-    ┌───────────────────────────────┐
-    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts
-    └───────────────────────────────┘  arguments that have kind ❰Type❱
-                        ⇧
-                        The function's input kind
-
-
-    ┌────────────────────┐
-    │ List : Type → Type │  This built-in function only accepts arguments that
-    └────────────────────┘  have kind ❰Type❱
-             ⇧
-             The function's input kind
-
-
-For example, the following expressions are valid:
-
-
-    ┌────────────────────────┐
-    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type
-    └────────────────────────┘  of argument that the anonymous function accepts
-
-
-    ┌─────────────────┐
-    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
-    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,
-
-
-    ┌────────────────────────┐
-    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
-    └────────────────────────┘  of argument that the anonymous function accepts
-
-
-    ┌───────────┐
-    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
-    └───────────┘  that that the ❰List❱ function accepts
-
-
-However, you can $_NOT apply a function to the wrong type or kind of argument
-
-For example, the following expressions are not valid:
-
-
-    ┌───────────────────────┐
-    │ (λ(x : Bool) → x) "A" │  ❰"A"❱ has type ❰Text❱, but the anonymous function
-    └───────────────────────┘  expects an argument that has type ❰Bool❱
-
-
-    ┌──────────────────┐
-    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
-    └──────────────────┘  expects an argument that has type ❰Natural❱
-
-
-    ┌────────────────────────┐
-    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
-    └────────────────────────┘  function expects an argument of kind ❰Type❱
-
-
-    ┌────────┐
-    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
-    └────────┘  argument that has kind ❰Type❱
-
-
-You tried to invoke the following function:
-
-↳ $txt0
-
-... which expects an argument of type or kind:
-
-↳ $txt1
-
-... on the following argument:
-
-↳ $txt2
-
-... which has a different type or kind:
-
-↳ $txt3
-
-Some common reasons why you might get this error:
-
-● You omit a function argument by mistake:
-
-
-    ┌────────────────────────────────────────┐
-    │ List/head   ([1, 2, 3] : List Integer) │
-    └────────────────────────────────────────┘
-                ⇧
-                ❰List/head❱ is missing the first argument,
-                which should be: ❰Integer❱
-
-
-● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
-
-    ┌────────────────┐
-    │ Natural/even 2 │
-    └────────────────┘
-                   ⇧
-                   This should be ❰+2❱
diff --git a/dhall/src/errors/CantTextAppend.txt b/dhall/src/errors/CantTextAppend.txt
deleted file mode 100644
index 26b9ceb..0000000
--- a/dhall/src/errors/CantTextAppend.txt
+++ /dev/null
@@ -1,28 +0,0 @@
-Explanation: The ❰++❱ operator expects two arguments that have type ❰Text❱
-
-For example, this is a valid use of ❰++❱: 
-
-
-    ┌────────────────┐
-    │ "ABC" ++ "DEF" │
-    └────────────────┘
-
-
-You provided this argument:
-
-↳ $txt0
-
-... which does not have type ❰Text❱ but instead has type:
-
-↳ $txt1
-
-Some common reasons why you might get this error:
-
-● You might have thought that ❰++❱ was the operator to combine two lists:
-
-    ┌───────────────────────────────────────────────────────────┐
-    │ ([1, 2, 3] : List Integer) ++ ([4, 5, 6] : List Integer ) │  Not valid
-    └───────────────────────────────────────────────────────────┘
-
-  The Dhall programming language does not provide a built-in operator for
-  combining two lists
diff --git a/dhall/src/errors/DuplicateAlternative.txt b/dhall/src/errors/DuplicateAlternative.txt
deleted file mode 100644
index 077f8aa..0000000
--- a/dhall/src/errors/DuplicateAlternative.txt
+++ /dev/null
@@ -1,18 +0,0 @@
-Explanation: Unions may not have two alternatives that share the same name
-
-For example, the following expressions are $_NOT valid:
-
-
-    ┌─────────────────────────────┐
-    │ < foo = True | foo : Text > │  Invalid: ❰foo❱ appears twice
-    └─────────────────────────────┘
-
-
-    ┌───────────────────────────────────────┐
-    │ < foo = 1 | bar : Bool | bar : Text > │  Invalid: ❰bar❱ appears twice
-    └───────────────────────────────────────┘
-
-
-You have more than one alternative named:
-
-↳ $txt0
diff --git a/dhall/src/errors/FieldCollision.txt b/dhall/src/errors/FieldCollision.txt
deleted file mode 100644
index 2b2d260..0000000
--- a/dhall/src/errors/FieldCollision.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-Explanation: You can combine records if they don't share any fields in common,
-like this:
-
-
-    ┌───────────────────────────────────────────┐
-    │ { foo = 1, bar = "ABC" } ∧ { baz = True } │
-    └───────────────────────────────────────────┘
-
-
-    ┌────────────────────────────────────────┐
-    │ λ(r : { baz : Bool}) → { foo = 1 } ∧ r │
-    └────────────────────────────────────────┘
-
-
-... but you cannot merge two records that share the same field
-
-For example, the following expression is $_NOT valid:
-
-
-    ┌───────────────────────────────────────────┐
-    │ { foo = 1, bar = "ABC" } ∧ { foo = True } │  Invalid: Colliding ❰foo❱ fields
-    └───────────────────────────────────────────┘
-
-
-You combined two records that share the following field:
-
-↳ $txt0
-
-... which is not allowed
-
-Some common reasons why you might get this error:
-
-● You tried to use ❰∧❱ to update a field's value, like this:
-
-
-    ┌────────────────────────────────────────┐
-    │ { foo = 1, bar = "ABC" } ∧ { foo = 2 } │
-    └────────────────────────────────────────┘
-                                   ⇧
-                                   Invalid attempt to update ❰foo❱'s value to ❰2❱
-
-  Field updates are intentionally not allowed as the Dhall language discourages
-  patch-oriented programming
diff --git a/dhall/src/errors/HandlerInputTypeMismatch.txt b/dhall/src/errors/HandlerInputTypeMismatch.txt
deleted file mode 100644
index 7d3525b..0000000
--- a/dhall/src/errors/HandlerInputTypeMismatch.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
-    ┌─────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Bool                                     │
-    └─────────────────────────────────────────────────────────────────────┘
-
-
-... as long as the input type of each handler function matches the type of the
-corresponding alternative:
-
-
-    ┌───────────────────────────────────────────────────────────┐
-    │ union    : < Left : Natural       | Right : Bool        > │
-    └───────────────────────────────────────────────────────────┘
-                          ⇧                       ⇧
-                   These must match        These must match
-                          ⇩                       ⇩
-    ┌───────────────────────────────────────────────────────────┐
-    │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │
-    └───────────────────────────────────────────────────────────┘
-
-
-For example, the following expression is $_NOT valid:
-
-
-      Invalid: Doesn't match the type of the ❰Right❱ alternative
-                                                               ⇩
-    ┌──────────────────────────────────────────────────────────────────────┐
-    │     let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │
-    │ in  let union    = < Left = +2 | Right : Bool >                      │
-    │ in  merge handlers union : Bool                                      │
-    └──────────────────────────────────────────────────────────────────────┘
-
-
-Your handler for the following alternative:
-
-↳ $txt0
-
-... needs to accept an input value of type:
-
-↳ $txt1
-
-... but actually accepts an input value of a different type:
-
-↳ $txt2
diff --git a/dhall/src/errors/HandlerNotAFunction.txt b/dhall/src/errors/HandlerNotAFunction.txt
deleted file mode 100644
index ff87443..0000000
--- a/dhall/src/errors/HandlerNotAFunction.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
-    ┌─────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Bool                                     │
-    └─────────────────────────────────────────────────────────────────────┘
-
-
-... as long as each handler is a function
-
-For example, the following expression is $_NOT valid:
-
-
-    ┌─────────────────────────────────────────┐
-    │ merge { Foo = True } < Foo = 1 > : Bool │
-    └─────────────────────────────────────────┘
-                    ⇧
-                    Invalid: Not a function
-
-
-Your handler for this alternative:
-
-↳ $txt0
-
-... has the following type:
-
-↳ $txt1
-
-... which is not the type of a function
diff --git a/dhall/src/errors/HandlerOutputTypeMismatch.txt b/dhall/src/errors/HandlerOutputTypeMismatch.txt
deleted file mode 100644
index f359459..0000000
--- a/dhall/src/errors/HandlerOutputTypeMismatch.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
-    ┌─────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Bool                                     │
-    └─────────────────────────────────────────────────────────────────────┘
-
-
-... as long as the output type of each handler function matches the declared type
-of the result:
-
-
-    ┌───────────────────────────────────────────────────────────┐
-    │ handlers : { Left : Natural → Bool, Right : Bool → Bool } │
-    └───────────────────────────────────────────────────────────┘
-                                    ⇧                    ⇧
-                                    These output types ...
-
-                             ... must match the declared type of the ❰merge❱
-                             ⇩
-    ┌─────────────────────────────┐
-    │ merge handlers union : Bool │
-    └─────────────────────────────┘
-
-
-For example, the following expression is $_NOT valid:
-
-
-    ┌──────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Text                                      │
-    └──────────────────────────────────────────────────────────────────────┘
-                                 ⇧
-                                 Invalid: Doesn't match output of either handler
-
-
-Your handler for the following alternative:
-
-↳ $txt0
-
-... needs to return an output value of type:
-
-↳ $txt1
-
-... but actually returns an output value of a different type:
-
-↳ $txt2
diff --git a/dhall/src/errors/IfBranchMismatch.txt b/dhall/src/errors/IfBranchMismatch.txt
deleted file mode 100644
index a95b130..0000000
--- a/dhall/src/errors/IfBranchMismatch.txt
+++ /dev/null
@@ -1,63 +0,0 @@
-Explanation: Every ❰if❱ expression has a ❰then❱ and ❰else❱ branch, each of which
-is an expression:
-
-
-                   Expression for ❰then❱ branch
-                   ⇩
-    ┌────────────────────────────────┐
-    │ if True then "Hello, world!"   │
-    │         else "Goodbye, world!" │
-    └────────────────────────────────┘
-                   ⇧
-                   Expression for ❰else❱ branch
-
-
-These two expressions must have the same type.  For example, the following ❰if❱
-expressions are all valid:
-
-
-    ┌──────────────────────────────────┐
-    │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱
-    └──────────────────────────────────┘
-
-
-    ┌────────────────────────────┐
-    │ λ(b : Bool) →              │
-    │     if b then Natural/even │ Both branches have type ❰Natural → Bool❱
-    │          else Natural/odd  │
-    └────────────────────────────┘
-
-
-However, the following expression is $_NOT valid:
-
-
-                   This branch has type ❰Integer❱
-                   ⇩
-    ┌────────────────────────┐
-    │ if True then 0         │
-    │         else "ABC"     │
-    └────────────────────────┘
-                   ⇧
-                   This branch has type ❰Text❱
-
-
-The ❰then❱ and ❰else❱ branches must have matching types, even if the predicate is
-always ❰True❱ or ❰False❱
-
-Your ❰if❱ expression has the following ❰then❱ branch:
-
-↳ $txt0
-
-... which has type:
-
-↳ $txt2
-
-... and the following ❰else❱ branch:
-
-↳ $txt1
-
-... which has a different type:
-
-↳ $txt3
-
-Fix your ❰then❱ and ❰else❱ branches to have matching types
diff --git a/dhall/src/errors/IfBranchMustBeTerm.txt b/dhall/src/errors/IfBranchMustBeTerm.txt
deleted file mode 100644
index 4c15881..0000000
--- a/dhall/src/errors/IfBranchMustBeTerm.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-Explanation: Every ❰if❱ expression begins with a predicate which must have type
-❰Bool❱
-
-For example, these are valid ❰if❱ expressions:
-
-
-    ┌──────────────────────────────┐
-    │ if True then "Yes" else "No" │
-    └──────────────────────────────┘
-         ⇧
-         Predicate
-
-
-    ┌─────────────────────────────────────────┐
-    │ λ(x : Bool) → if x then False else True │
-    └─────────────────────────────────────────┘
-                       ⇧
-                       Predicate
-
-
-... but these are $_NOT valid ❰if❱ expressions:
-
-
-    ┌───────────────────────────┐
-    │ if 0 then "Yes" else "No" │  ❰0❱ does not have type ❰Bool❱
-    └───────────────────────────┘
-
-
-    ┌────────────────────────────┐
-    │ if "" then False else True │  ❰""❱ does not have type ❰Bool❱
-    └────────────────────────────┘
-
-
-Your ❰if❱ expression begins with the following predicate:
-
-↳ $txt0
-
-... that has type:
-
-↳ $txt1
-
-... but the predicate must instead have type ❰Bool❱
-
-Some common reasons why you might get this error:
-
-● You might be used to other programming languages that accept predicates other
-  than ❰Bool❱
-
-  For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
-  them as equivalent to ❰False❱.  However, the Dhall language does not permit
-  this
diff --git a/dhall/src/errors/InvalidAlterantive.txt b/dhall/src/errors/InvalidAlterantive.txt
deleted file mode 100644
index 391fc3a..0000000
--- a/dhall/src/errors/InvalidAlterantive.txt
+++ /dev/null
@@ -1,48 +0,0 @@
-Explanation: Every union type specifies the type of each alternative, like this:
-
-
-               The type of the first alternative is ❰Bool❱
-               ⇩
-    ┌──────────────────────────────────┐
-    │ < Left : Bool, Right : Natural > │  A union type with two alternatives
-    └──────────────────────────────────┘
-                             ⇧
-                             The type of the second alternative is ❰Natural❱
-
-
-However, these alternatives can only be annotated with types.  For example, the
-following union types are $_NOT valid:
-
-
-    ┌────────────────────────────┐
-    │ < Left : Bool, Right : 1 > │  Invalid union type
-    └────────────────────────────┘
-                             ⇧
-                             This is a term and not a type
-
-
-    ┌───────────────────────────────┐
-    │ < Left : Bool, Right : Type > │  Invalid union type
-    └───────────────────────────────┘
-                             ⇧
-                             This is a kind and not a type
-
-
-You provided a union type with an alternative named:
-
-↳ $txt0
-
-... annotated with the following expression which is not a type:
-
-↳ $txt1
-
-Some common reasons why you might get this error:
-
-● You accidentally typed ❰:❱ instead of ❰=❱ for a union literal with one
-  alternative:
-
-    ┌─────────────────┐
-    │ < Example : 1 > │
-    └─────────────────┘
-                ⇧
-                This could be ❰=❱ instead
diff --git a/dhall/src/errors/InvalidAlterantiveType.txt b/dhall/src/errors/InvalidAlterantiveType.txt
deleted file mode 100644
index f5dadef..0000000
--- a/dhall/src/errors/InvalidAlterantiveType.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-Explanation: Every union literal begins by selecting one alternative and
-specifying the value for that alternative, like this:
-
-
-        Select the ❰Left❱ alternative, whose value is ❰True❱
-        ⇩
-    ┌──────────────────────────────────┐
-    │ < Left = True, Right : Natural > │  A union literal with two alternatives
-    └──────────────────────────────────┘
-
-
-However, this value must be a term and not a type.  For example, the following
-values are $_NOT valid:
-
-
-    ┌──────────────────────────────────┐
-    │ < Left = Text, Right : Natural > │  Invalid union literal
-    └──────────────────────────────────┘
-               ⇧
-               This is a type and not a term
-
-
-    ┌───────────────────────────────┐
-    │ < Left = Type, Right : Type > │  Invalid union type
-    └───────────────────────────────┘
-               ⇧
-               This is a kind and not a term
-
-
-You provided a union literal with an alternative named:
-
-↳ $txt0
-
-... whose value is:
-
-↳ $txt1
-
-... which is not a term
-
-Some common reasons why you might get this error:
-
-● You accidentally typed ❰=❱ instead of ❰:❱ for a union literal with one
-  alternative:
-
-    ┌────────────────────┐
-    │ < Example = Text > │
-    └────────────────────┘
-                ⇧
-                This could be ❰:❱ instead
diff --git a/dhall/src/errors/InvalidField.txt b/dhall/src/errors/InvalidField.txt
deleted file mode 100644
index bfbf106..0000000
--- a/dhall/src/errors/InvalidField.txt
+++ /dev/null
@@ -1,35 +0,0 @@
-Explanation: Every record literal is a set of fields assigned to values, like
-this:
-
-    ┌────────────────────────────────────────┐
-    │ { foo = 100, bar = True, baz = "ABC" } │
-    └────────────────────────────────────────┘
-
-However, fields can only be terms and cannot be types or kinds
-
-For example, these record literals are $_NOT valid:
-
-
-    ┌───────────────────────────┐
-    │ { foo = 100, bar = Text } │
-    └───────────────────────────┘
-                         ⇧
-                         ❰Text❱ is a type and not a term
-
-
-    ┌───────────────────────────┐
-    │ { foo = 100, bar = Type } │
-    └───────────────────────────┘
-                         ⇧
-                         ❰Type❱ is a kind and not a term
-
-
-You provided a record literal with a key named:
-
-↳ $txt0
-
-... whose value is:
-
-↳ $txt1
-
-... which is not a term
diff --git a/dhall/src/errors/InvalidFieldType.txt b/dhall/src/errors/InvalidFieldType.txt
deleted file mode 100644
index 4f76a64..0000000
--- a/dhall/src/errors/InvalidFieldType.txt
+++ /dev/null
@@ -1,34 +0,0 @@
-Explanation: Every record type documents the type of each field, like this:
-
-    ┌──────────────────────────────────────────────┐
-    │ { foo : Integer, bar : Integer, baz : Text } │
-    └──────────────────────────────────────────────┘
-
-However, fields cannot be annotated with expressions other than types
-
-For example, these record types are $_NOT valid:
-
-
-    ┌────────────────────────────┐
-    │ { foo : Integer, bar : 1 } │
-    └────────────────────────────┘
-                             ⇧
-                             ❰1❱ is an ❰Integer❱ and not a ❰Type❱
-
-
-    ┌───────────────────────────────┐
-    │ { foo : Integer, bar : Type } │
-    └───────────────────────────────┘
-                             ⇧
-                             ❰Type❱ is a ❰Kind❱ and not a ❰Type❱
-
-
-You provided a record type with a key named:
-
-↳ $txt0
-
-... annotated with the following expression:
-
-↳ $txt1
-
-... which is not a type
diff --git a/dhall/src/errors/InvalidInputType.txt b/dhall/src/errors/InvalidInputType.txt
deleted file mode 100644
index eabafa4..0000000
--- a/dhall/src/errors/InvalidInputType.txt
+++ /dev/null
@@ -1,61 +0,0 @@
-Explanation: A function can accept an input "term" that has a given "type", like
-this:
-
-
-        This is the input term that the function accepts
-        ⇩
-    ┌───────────────────────┐
-    │ ∀(x : Natural) → Bool │  This is the type of a function that accepts an
-    └───────────────────────┘  input term named ❰x❱ that has type ❰Natural❱
-            ⇧
-            This is the type of the input term
-
-
-    ┌────────────────┐
-    │ Bool → Integer │  This is the type of a function that accepts an anonymous
-    └────────────────┘  input term that has type ❰Bool❱
-      ⇧
-      This is the type of the input term
-
-
-... or a function can accept an input "type" that has a given "kind", like this:
-
-
-        This is the input type that the function accepts
-        ⇩
-    ┌────────────────────┐
-    │ ∀(a : Type) → Type │  This is the type of a function that accepts an input
-    └────────────────────┘  type named ❰a❱ that has kind ❰Type❱
-            ⇧
-            This is the kind of the input type
-
-
-    ┌──────────────────────┐
-    │ (Type → Type) → Type │  This is the type of a function that accepts an
-    └──────────────────────┘  anonymous input type that has kind ❰Type → Type❱
-       ⇧
-       This is the kind of the input type
-
-
-Other function inputs are $_NOT valid, like this:
-
-
-    ┌──────────────┐
-    │ ∀(x : 1) → x │  ❰1❱ is a "term" and not a "type" nor a "kind" so ❰x❱
-    └──────────────┘  cannot have "type" ❰1❱ or "kind" ❰1❱
-            ⇧
-            This is not a type or kind
-
-
-    ┌──────────┐
-    │ True → x │  ❰True❱ is a "term" and not a "type" nor a "kind" so the
-    └──────────┘  anonymous input cannot have "type" ❰True❱ or "kind" ❰True❱
-      ⇧
-      This is not a type or kind
-
-
-You annotated a function input with the following expression:
-
-↳ $txt
-
-... which is neither a type nor a kind
diff --git a/dhall/src/errors/InvalidListElement.txt b/dhall/src/errors/InvalidListElement.txt
deleted file mode 100644
index 59db7b7..0000000
--- a/dhall/src/errors/InvalidListElement.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-Explanation: Every element in the list must have a type matching the type
-annotation at the end of the list
-
-For example, this is a valid ❰List❱:
-
-
-    ┌──────────────────────────┐
-    │ [1, 2, 3] : List Integer │  Every element in this ❰List❱ is an ❰Integer❱
-    └──────────────────────────┘
-
-
-.. but this is $_NOT a valid ❰List❱:
-
-
-    ┌──────────────────────────────┐
-    │ [1, "ABC", 3] : List Integer │  The second element is not an ❰Integer❱
-    └──────────────────────────────┘
-
-
-Your ❰List❱ elements should have this type:
-
-↳ $txt0
-
-... but the following element at index $txt1:
-
-↳ $txt2
-
-... has this type instead:
-
-↳ $txt3
diff --git a/dhall/src/errors/InvalidListType.txt b/dhall/src/errors/InvalidListType.txt
deleted file mode 100644
index 676647e..0000000
--- a/dhall/src/errors/InvalidListType.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-Explanation: Every ❰List❱ documents the type of its elements with a type
-annotation, like this:
-
-
-    ┌──────────────────────────┐
-    │ [1, 2, 3] : List Integer │  A ❰List❱ of three ❰Integer❱s
-    └──────────────────────────┘
-                       ⇧
-                       The type of the ❰List❱'s elements, which are ❰Integer❱s
-
-
-    ┌───────────────────┐
-    │ [] : List Integer │  An empty ❰List❱
-    └───────────────────┘
-                ⇧
-                You still specify the type even when the ❰List❱ is empty
-
-
-The element type must be a type and not something else.  For example, the
-following element types are $_NOT valid:
-
-
-    ┌──────────────┐
-    │ ... : List 1 │
-    └──────────────┘
-                 ⇧
-                 This is an ❰Integer❱ and not a ❰Type❱
-
-
-    ┌─────────────────┐
-    │ ... : List Type │
-    └─────────────────┘
-                 ⇧
-                 This is a ❰Kind❱ and not a ❰Type❱
-
-
-Even if the ❰List❱ is empty you still must specify a valid type
-
-You declared that the ❰List❱'s elements should have type:
-
-↳ $txt0
-
-... which is not a ❰Type❱
diff --git a/dhall/src/errors/InvalidOptionType.txt b/dhall/src/errors/InvalidOptionType.txt
deleted file mode 100644
index 3bc81de..0000000
--- a/dhall/src/errors/InvalidOptionType.txt
+++ /dev/null
@@ -1,44 +0,0 @@
-Explanation: Every optional element ends with a type annotation for the element
-that might be present, like this:
-
-
-    ┌────────────────────────┐
-    │ [1] : Optional Integer │  An optional element that's present
-    └────────────────────────┘
-                     ⇧
-                     The type of the ❰Optional❱ element, which is an ❰Integer❱
-
-
-    ┌────────────────────────┐
-    │ [] : Optional Integer  │  An optional element that's absent
-    └────────────────────────┘
-                    ⇧
-                    You still specify the type even when the element is absent
-
-
-The element type must be a type and not something else.  For example, the
-following element types are $_NOT valid:
-
-
-    ┌──────────────────┐
-    │ ... : Optional 1 │
-    └──────────────────┘
-                     ⇧
-                     This is an ❰Integer❱ and not a ❰Type❱
-
-
-    ┌─────────────────────┐
-    │ ... : Optional Type │
-    └─────────────────────┘
-                     ⇧
-                     This is a ❰Kind❱ and not a ❰Type❱
-
-
-Even if the element is absent you still must specify a valid type
-
-You declared that the ❰Optional❱ element should have type:
-
-↳ $txt0
-
-... which is not a ❰Type❱
-
diff --git a/dhall/src/errors/InvalidOptionalElement.txt b/dhall/src/errors/InvalidOptionalElement.txt
deleted file mode 100644
index 0254220..0000000
--- a/dhall/src/errors/InvalidOptionalElement.txt
+++ /dev/null
@@ -1,29 +0,0 @@
-Explanation: An ❰Optional❱ element must have a type matching the type annotation
-
-For example, this is a valid ❰Optional❱ value:
-
-
-    ┌────────────────────────┐
-    │ [1] : Optional Integer │  ❰1❱ is an ❰Integer❱, which matches the type
-    └────────────────────────┘
-
-
-... but this is $_NOT a valid ❰Optional❱ value:
-
-
-    ┌────────────────────────────┐
-    │ ["ABC"] : Optional Integer │  ❰"ABC"❱ is not an ❰Integer❱
-    └────────────────────────────┘
-
-
-Your ❰Optional❱ element should have this type:
-
-↳ $txt0
-
-... but the element you provided:
-
-↳ $txt1
-
-... has this type instead:
-
-↳ $txt2
diff --git a/dhall/src/errors/InvalidOptionalLiteral.txt b/dhall/src/errors/InvalidOptionalLiteral.txt
deleted file mode 100644
index 41c0fdc..0000000
--- a/dhall/src/errors/InvalidOptionalLiteral.txt
+++ /dev/null
@@ -1,53 +0,0 @@
-Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s:
-
-
-    ┌───────────────────────┐
-    │ [] : Optional Integer │  An ❰Optional❱ value which is absent
-    └───────────────────────┘
-
-
-    ┌───────────────────────┐
-    │ [] : List     Integer │  An empty (0-element) ❰List❱
-    └───────────────────────┘
-
-
-    ┌────────────────────────┐
-    │ [1] : Optional Integer │  An ❰Optional❱ value which is present
-    └────────────────────────┘
-
-
-    ┌────────────────────────┐
-    │ [1] : List     Integer │  A singleton (1-element) ❰List❱
-    └────────────────────────┘
-
-
-However, an ❰Optional❱ value can $_NOT have more than one element, whereas a
-❰List❱ can have multiple elements:
-
-
-    ┌───────────────────────────┐
-    │ [1, 2] : Optional Integer │  Invalid: multiple elements $_NOT allowed
-    └───────────────────────────┘
-
-
-    ┌───────────────────────────┐
-    │ [1, 2] : List     Integer │  Valid: multiple elements allowed
-    └───────────────────────────┘
-
-
-Your ❰Optional❱ value had this many elements:
-
-↳ $txt0
-
-... when an ❰Optional❱ value can only have at most one element
-
-Some common reasons why you might get this error:
-
-● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this:
-
-
-    ┌────────────────────────────────────────────────────┐
-    │ List/length Integer ([1, 2, 3] : Optional Integer) │
-    └────────────────────────────────────────────────────┘
-                                       ⇧
-                                       This should be ❰List❱ instead
diff --git a/dhall/src/errors/InvalidOutputType.txt b/dhall/src/errors/InvalidOutputType.txt
deleted file mode 100644
index dd2695d..0000000
--- a/dhall/src/errors/InvalidOutputType.txt
+++ /dev/null
@@ -1,68 +0,0 @@
-Explanation: A function can return an output "term" that has a given "type",
-like this:
-
-
-    ┌────────────────────┐
-    │ ∀(x : Text) → Bool │  This is the type of a function that returns an
-    └────────────────────┘  output term that has type ❰Bool❱
-                    ⇧
-                    This is the type of the output term
-
-
-    ┌────────────────┐
-    │ Bool → Integer │  This is the type of a function that returns an output
-    └────────────────┘  term that has type ❰Int❱
-             ⇧
-             This is the type of the output term
-
-
-... or a function can return an output "type" that has a given "kind", like
-this:
-
-    ┌────────────────────┐
-    │ ∀(a : Type) → Type │  This is the type of a function that returns an
-    └────────────────────┘  output type that has kind ❰Type❱
-                    ⇧
-                    This is the kind of the output type
-
-
-    ┌──────────────────────┐
-    │ (Type → Type) → Type │  This is the type of a function that returns an
-    └──────────────────────┘  output type that has kind ❰Type❱
-                      ⇧
-                      This is the kind of the output type
-
-
-Other outputs are $_NOT valid, like this:
-
-
-    ┌─────────────────┐
-    │ ∀(x : Bool) → x │  ❰x❱ is a "term" and not a "type" nor a "kind" so the
-    └─────────────────┘  output cannot have "type" ❰x❱ or "kind" ❰x❱
-                    ⇧
-                    This is not a type or kind
-
-
-    ┌─────────────┐
-    │ Text → True │  ❰True❱ is a "term" and not a "type" nor a "kind" so the
-    └─────────────┘  output cannot have "type" ❰True❱ or "kind" ❰True❱
-             ⇧
-             This is not a type or kind
-
-
-You specified that your function outputs a:
-
-↳ $txt
-
-... which is neither a type nor a kind:
-
-Some common reasons why you might get this error:
-
-● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:
-
-
-    ┌────────────────┐
-    │ ∀(x: Bool) → x │
-    └────────────────┘
-      ⇧
-      Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function
diff --git a/dhall/src/errors/InvalidPredicate.txt b/dhall/src/errors/InvalidPredicate.txt
deleted file mode 100644
index 4c15881..0000000
--- a/dhall/src/errors/InvalidPredicate.txt
+++ /dev/null
@@ -1,51 +0,0 @@
-Explanation: Every ❰if❱ expression begins with a predicate which must have type
-❰Bool❱
-
-For example, these are valid ❰if❱ expressions:
-
-
-    ┌──────────────────────────────┐
-    │ if True then "Yes" else "No" │
-    └──────────────────────────────┘
-         ⇧
-         Predicate
-
-
-    ┌─────────────────────────────────────────┐
-    │ λ(x : Bool) → if x then False else True │
-    └─────────────────────────────────────────┘
-                       ⇧
-                       Predicate
-
-
-... but these are $_NOT valid ❰if❱ expressions:
-
-
-    ┌───────────────────────────┐
-    │ if 0 then "Yes" else "No" │  ❰0❱ does not have type ❰Bool❱
-    └───────────────────────────┘
-
-
-    ┌────────────────────────────┐
-    │ if "" then False else True │  ❰""❱ does not have type ❰Bool❱
-    └────────────────────────────┘
-
-
-Your ❰if❱ expression begins with the following predicate:
-
-↳ $txt0
-
-... that has type:
-
-↳ $txt1
-
-... but the predicate must instead have type ❰Bool❱
-
-Some common reasons why you might get this error:
-
-● You might be used to other programming languages that accept predicates other
-  than ❰Bool❱
-
-  For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
-  them as equivalent to ❰False❱.  However, the Dhall language does not permit
-  this
diff --git a/dhall/src/errors/MissingField.txt b/dhall/src/errors/MissingField.txt
deleted file mode 100644
index de14a33..0000000
--- a/dhall/src/errors/MissingField.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-Explanation: You can only access fields on records, like this:
-
-
-    ┌─────────────────────────────────┐
-    │ { foo = True, bar = "ABC" }.foo │  This is valid ...
-    └─────────────────────────────────┘
-
-
-    ┌───────────────────────────────────────────┐
-    │ λ(r : { foo : Bool, bar : Text }) → r.foo │  ... and so is this
-    └───────────────────────────────────────────┘
-
-
-... but you can only access fields if they are present
-
-For example, the following expression is $_NOT valid:
-
-    ┌─────────────────────────────────┐
-    │ { foo = True, bar = "ABC" }.qux │
-    └─────────────────────────────────┘
-                                  ⇧
-                                  Invalid: the record has no ❰qux❱ field
-
-You tried to access a field named:
-
-↳ $txt0
-
-... but the field is missing because the record only defines the following fields:
-
-↳ $txt1
diff --git a/dhall/src/errors/MissingHandler.txt b/dhall/src/errors/MissingHandler.txt
deleted file mode 100644
index 433445e..0000000
--- a/dhall/src/errors/MissingHandler.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
-    ┌─────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Bool                                     │
-    └─────────────────────────────────────────────────────────────────────┘
-
-
-... but you must provide exactly one handler per alternative in the union.  You
-cannot omit any handlers
-
-For example, the following expression is $_NOT valid:
-
-
-                                              Invalid: Missing ❰Right❱ handler
-                                              ⇩
-    ┌─────────────────────────────────────────────────┐
-    │     let handlers = { Left = Natural/even }      │
-    │ in  let union    = < Left = +2 | Right : Bool > │
-    │ in  merge handlers union : Bool                 │
-    └─────────────────────────────────────────────────┘
-
-
-Note that you need to provide handlers for other alternatives even if those
-alternatives are never used
-
-You need to supply the following handlers:
-
-↳ $txt0
diff --git a/dhall/src/errors/MustCombineARecord.txt b/dhall/src/errors/MustCombineARecord.txt
deleted file mode 100644
index 141b969..0000000
--- a/dhall/src/errors/MustCombineARecord.txt
+++ /dev/null
@@ -1,46 +0,0 @@
-Explanation: You can combine records using the ❰∧❱ operator, like this:
-
-
-    ┌───────────────────────────────────────────┐
-    │ { foo = 1, bar = "ABC" } ∧ { baz = True } │
-    └───────────────────────────────────────────┘
-
-
-    ┌─────────────────────────────────────────────┐
-    │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │
-    └─────────────────────────────────────────────┘
-
-
-... but you cannot combine values that are not records.
-
-For example, the following expressions are $_NOT valid:
-
-
-    ┌──────────────────────────────┐
-    │ { foo = 1, bar = "ABC" } ∧ 1 │
-    └──────────────────────────────┘
-                                 ⇧
-                                 Invalid: Not a record
-
-
-    ┌───────────────────────────────────────────┐
-    │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │
-    └───────────────────────────────────────────┘
-                                 ⇧
-                                 Invalid: This is a record type and not a record
-
-
-    ┌───────────────────────────────────────────┐
-    │ { foo = 1, bar = "ABC" } ∧ < baz = True > │
-    └───────────────────────────────────────────┘
-                                 ⇧
-                                 Invalid: This is a union and not a record
-
-
-You tried to combine the following value:
-
-↳ $txt0
-
-... which is not a record, but is actually a:
-
-↳ $txt1
diff --git a/dhall/src/errors/MustMergeARecord.txt b/dhall/src/errors/MustMergeARecord.txt
deleted file mode 100644
index 79094bd..0000000
--- a/dhall/src/errors/MustMergeARecord.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
-    ┌─────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Bool                                     │
-    └─────────────────────────────────────────────────────────────────────┘
-
-
-... but the first argument to ❰merge❱ must be a record and not some other type.
-
-For example, the following expression is $_NOT valid:
-
-
-    ┌─────────────────────────────────────────┐
-    │ let handler = λ(x : Bool) → x           │
-    │ in  merge handler < Foo = True > : True │
-    └─────────────────────────────────────────┘
-                ⇧
-                Invalid: ❰handler❱ isn't a record
-
-
-You provided the following handler:
-
-↳ $txt0
-
-... which is not a record, but is actually a value of type:
-
-↳ $txt1
-
-Some common reasons why you might get this error:
-
-● You accidentally provide an empty record type instead of an empty record when
-  you ❰merge❱ an empty union:
-
-
-    ┌──────────────────────────────────────────┐
-    │ λ(x : <>) → λ(a : Type) → merge {} x : a │
-    └──────────────────────────────────────────┘
-                                      ⇧
-                                      This should be ❰{=}❱ instead
diff --git a/dhall/src/errors/MustMergeUnion.txt b/dhall/src/errors/MustMergeUnion.txt
deleted file mode 100644
index 68df70c..0000000
--- a/dhall/src/errors/MustMergeUnion.txt
+++ /dev/null
@@ -1,31 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
-    ┌─────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Bool                                     │
-    └─────────────────────────────────────────────────────────────────────┘
-
-
-... but the second argument to ❰merge❱ must be a union and not some other type.
-
-For example, the following expression is $_NOT valid:
-
-
-    ┌──────────────────────────────────────────┐
-    │ let handlers = { Foo = λ(x : Bool) → x } │
-    │ in  merge handlers True : True           │
-    └──────────────────────────────────────────┘
-                         ⇧
-                         Invalid: ❰True❱ isn't a union
-
-
-You tried to ❰merge❱ this expression:
-
-↳ $txt0
-
-... which is not a union, but is actually a value of type:
-
-↳ $txt1
diff --git a/dhall/src/errors/NoDependentLet.txt b/dhall/src/errors/NoDependentLet.txt
deleted file mode 100644
index fdc65b4..0000000
--- a/dhall/src/errors/NoDependentLet.txt
+++ /dev/null
@@ -1,76 +0,0 @@
-Explanation: The Dhall programming language does not allow ❰let❱ expressions
-from terms to types.  These ❰let❱ expressions are also known as "dependent ❰let❱
-expressions" because you have a type whose value depends on the value of a term.
-
-The Dhall language forbids these dependent ❰let❱ expressions in order to
-guarantee that ❰let❱ expressions of the form:
-
-
-    ┌────────────────────┐
-    │ let x : t = r in e │
-    └────────────────────┘
-
-
-... are always equivalent to:
-
-
-    ┌──────────────────┐
-    │ (λ(x : t) → e) r │
-    └──────────────────┘
-
-
-This means that both expressions should normalize to the same result and if one
-of the two fails to type check then the other should fail to type check, too.
-
-For this reason, the following is $_NOT legal code:
-
-
-    ┌───────────────────┐
-    │ let x = 2 in Text │
-    └───────────────────┘
-
-
-... because the above ❰let❱ expression is equivalent to:
-
-
-    ┌─────────────────────────────┐
-    │ let x : Integer = 2 in Text │
-    └─────────────────────────────┘
-
-
-... which in turn must be equivalent to:
-
-
-    ┌───────────────────────────┐
-    │ (λ(x : Integer) → Text) 2 │
-    └───────────────────────────┘
-
-
-... which in turn fails to type check because this sub-expression:
-
-
-    ┌───────────────────────┐
-    │ λ(x : Integer) → Text │
-    └───────────────────────┘
-
-
-... has type:
-
-
-    ┌───────────────────────┐
-    │ ∀(x : Integer) → Text │
-    └───────────────────────┘
-
-
-... which is a forbidden dependent function type (i.e. a function from a term to
-a type).  Therefore the equivalent ❰let❱ expression is also forbidden.
-
-Your ❰let❱ expression is invalid because the input has type:
-
-↳ $txt0
-
-... and the output has kind:
-
-↳ $txt1
-
-... which makes this a forbidden dependent ❰let❱ expression
diff --git a/dhall/src/errors/NoDependentTypes.txt b/dhall/src/errors/NoDependentTypes.txt
deleted file mode 100644
index 435bdcb..0000000
--- a/dhall/src/errors/NoDependentTypes.txt
+++ /dev/null
@@ -1,31 +0,0 @@
-Explanation: The Dhall programming language does not allow functions from terms
-to types.  These function types are also known as "dependent function types"
-because you have a type whose value "depends" on the value of a term.
-
-For example, this is $_NOT a legal function type:
-
-
-    ┌─────────────┐
-    │ Bool → Type │
-    └─────────────┘
-
-
-Similarly, this is $_NOT legal code:
-
-
-    ┌────────────────────────────────────────────────────┐
-    │ λ(Vector : Natural → Type → Type) → Vector +0 Text │
-    └────────────────────────────────────────────────────┘
-                 ⇧
-                 Invalid dependent type
-
-
-Your function type is invalid because the input has type:
-
-↳ $txt0
-
-... and the output has kind:
-
-↳ $txt1
-
-... which makes this a forbidden dependent function type
diff --git a/dhall/src/errors/NotAFunction.txt b/dhall/src/errors/NotAFunction.txt
deleted file mode 100644
index dd2695d..0000000
--- a/dhall/src/errors/NotAFunction.txt
+++ /dev/null
@@ -1,68 +0,0 @@
-Explanation: A function can return an output "term" that has a given "type",
-like this:
-
-
-    ┌────────────────────┐
-    │ ∀(x : Text) → Bool │  This is the type of a function that returns an
-    └────────────────────┘  output term that has type ❰Bool❱
-                    ⇧
-                    This is the type of the output term
-
-
-    ┌────────────────┐
-    │ Bool → Integer │  This is the type of a function that returns an output
-    └────────────────┘  term that has type ❰Int❱
-             ⇧
-             This is the type of the output term
-
-
-... or a function can return an output "type" that has a given "kind", like
-this:
-
-    ┌────────────────────┐
-    │ ∀(a : Type) → Type │  This is the type of a function that returns an
-    └────────────────────┘  output type that has kind ❰Type❱
-                    ⇧
-                    This is the kind of the output type
-
-
-    ┌──────────────────────┐
-    │ (Type → Type) → Type │  This is the type of a function that returns an
-    └──────────────────────┘  output type that has kind ❰Type❱
-                      ⇧
-                      This is the kind of the output type
-
-
-Other outputs are $_NOT valid, like this:
-
-
-    ┌─────────────────┐
-    │ ∀(x : Bool) → x │  ❰x❱ is a "term" and not a "type" nor a "kind" so the
-    └─────────────────┘  output cannot have "type" ❰x❱ or "kind" ❰x❱
-                    ⇧
-                    This is not a type or kind
-
-
-    ┌─────────────┐
-    │ Text → True │  ❰True❱ is a "term" and not a "type" nor a "kind" so the
-    └─────────────┘  output cannot have "type" ❰True❱ or "kind" ❰True❱
-             ⇧
-             This is not a type or kind
-
-
-You specified that your function outputs a:
-
-↳ $txt
-
-... which is neither a type nor a kind:
-
-Some common reasons why you might get this error:
-
-● You use ❰∀❱ instead of ❰λ❱ by mistake, like this:
-
-
-    ┌────────────────┐
-    │ ∀(x: Bool) → x │
-    └────────────────┘
-      ⇧
-      Using ❰λ❱ here instead of ❰∀❱ would transform this into a valid function
diff --git a/dhall/src/errors/NotARecord.txt b/dhall/src/errors/NotARecord.txt
deleted file mode 100644
index e0eebc8..0000000
--- a/dhall/src/errors/NotARecord.txt
+++ /dev/null
@@ -1,48 +0,0 @@
-Explanation: You can only access fields on records, like this:
-
-
-    ┌─────────────────────────────────┐
-    │ { foo = True, bar = "ABC" }.foo │  This is valid ...
-    └─────────────────────────────────┘
-
-
-    ┌───────────────────────────────────────────┐
-    │ λ(r : { foo : Bool, bar : Text }) → r.foo │  ... and so is this
-    └───────────────────────────────────────────┘
-
-
-... but you cannot access fields on non-record expressions
-
-For example, the following expression is $_NOT valid:
-
-
-    ┌───────┐
-    │ 1.foo │
-    └───────┘
-      ⇧
-      Invalid: Not a record
-
-
-You tried to access a field named:
-
-↳ $txt0
-
-... on the following expression which is not a record:
-
-↳ $txt1
-
-... but is actually an expression of type:
-
-↳ $txt2
-
-Some common reasons why you might get this error:
-
-● You accidentally try to access a field of a union instead of a record, like
-  this:
-
-
-    ┌─────────────────┐
-    │ < foo : a >.foo │
-    └─────────────────┘
-      ⇧
-      This is a union, not a record
diff --git a/dhall/src/errors/TypeMismatch.txt b/dhall/src/errors/TypeMismatch.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/dhall/src/errors/TypeMismatch.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-Explanation: Every function declares what type or kind of argument to accept
-
-For example:
-
-
-    ┌───────────────────────────────┐
-    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts
-    └───────────────────────────────┘  arguments that have type ❰Bool❱
-                        ⇧
-                        The function's input type
-
-
-    ┌───────────────────────────────┐
-    │ Natural/even : Natural → Bool │  This built-in function only accepts
-    └───────────────────────────────┘  arguments that have type ❰Natural❱
-                     ⇧
-                     The function's input type
-
-
-    ┌───────────────────────────────┐
-    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts
-    └───────────────────────────────┘  arguments that have kind ❰Type❱
-                        ⇧
-                        The function's input kind
-
-
-    ┌────────────────────┐
-    │ List : Type → Type │  This built-in function only accepts arguments that
-    └────────────────────┘  have kind ❰Type❱
-             ⇧
-             The function's input kind
-
-
-For example, the following expressions are valid:
-
-
-    ┌────────────────────────┐
-    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type
-    └────────────────────────┘  of argument that the anonymous function accepts
-
-
-    ┌─────────────────┐
-    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
-    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,
-
-
-    ┌────────────────────────┐
-    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
-    └────────────────────────┘  of argument that the anonymous function accepts
-
-
-    ┌───────────┐
-    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
-    └───────────┘  that that the ❰List❱ function accepts
-
-
-However, you can $_NOT apply a function to the wrong type or kind of argument
-
-For example, the following expressions are not valid:
-
-
-    ┌───────────────────────┐
-    │ (λ(x : Bool) → x) "A" │  ❰"A"❱ has type ❰Text❱, but the anonymous function
-    └───────────────────────┘  expects an argument that has type ❰Bool❱
-
-
-    ┌──────────────────┐
-    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
-    └──────────────────┘  expects an argument that has type ❰Natural❱
-
-
-    ┌────────────────────────┐
-    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
-    └────────────────────────┘  function expects an argument of kind ❰Type❱
-
-
-    ┌────────┐
-    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
-    └────────┘  argument that has kind ❰Type❱
-
-
-You tried to invoke the following function:
-
-↳ $txt0
-
-... which expects an argument of type or kind:
-
-↳ $txt1
-
-... on the following argument:
-
-↳ $txt2
-
-... which has a different type or kind:
-
-↳ $txt3
-
-Some common reasons why you might get this error:
-
-● You omit a function argument by mistake:
-
-
-    ┌────────────────────────────────────────┐
-    │ List/head   ([1, 2, 3] : List Integer) │
-    └────────────────────────────────────────┘
-                ⇧
-                ❰List/head❱ is missing the first argument,
-                which should be: ❰Integer❱
-
-
-● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
-
-    ┌────────────────┐
-    │ Natural/even 2 │
-    └────────────────┘
-                   ⇧
-                   This should be ❰+2❱
diff --git a/dhall/src/errors/UnboundVariable.txt b/dhall/src/errors/UnboundVariable.txt
deleted file mode 100644
index bd7d483..0000000
--- a/dhall/src/errors/UnboundVariable.txt
+++ /dev/null
@@ -1,97 +0,0 @@
-Explanation: Expressions can only reference previously introduced (i.e. "bound")
-variables that are still "in scope"
-
-For example, the following valid expressions introduce a "bound" variable named
-❰x❱:
-
-
-    ┌─────────────────┐
-    │ λ(x : Bool) → x │  Anonymous functions introduce "bound" variables
-    └─────────────────┘
-        ⇧
-        This is the bound variable
-
-
-    ┌─────────────────┐
-    │ let x = 1 in x  │  ❰let❱ expressions introduce "bound" variables
-    └─────────────────┘
-          ⇧
-          This is the bound variable
-
-
-However, the following expressions are not valid because they all reference a
-variable that has not been introduced yet (i.e. an "unbound" variable):
-
-
-    ┌─────────────────┐
-    │ λ(x : Bool) → y │  The variable ❰y❱ hasn't been introduced yet
-    └─────────────────┘
-                    ⇧
-                    This is the unbound variable
-
-
-    ┌──────────────────────────┐
-    │ (let x = True in x) && x │  ❰x❱ is undefined outside the parentheses
-    └──────────────────────────┘
-                             ⇧
-                             This is the unbound variable
-
-
-    ┌────────────────┐
-    │ let x = x in x │  The definition for ❰x❱ cannot reference itself
-    └────────────────┘
-              ⇧
-              This is the unbound variable
-
-
-Some common reasons why you might get this error:
-
-● You misspell a variable name, like this:
-
-
-    ┌────────────────────────────────────────────────────┐
-    │ λ(empty : Bool) → if emty then "Empty" else "Full" │
-    └────────────────────────────────────────────────────┘
-                           ⇧
-                           Typo
-
-
-● You misspell a reserved identifier, like this:
-
-
-    ┌──────────────────────────┐
-    │ foral (a : Type) → a → a │
-    └──────────────────────────┘
-      ⇧
-      Typo
-
-
-● You tried to define a recursive value, like this:
-
-
-    ┌─────────────────────┐
-    │ let x = x + +1 in x │
-    └─────────────────────┘
-              ⇧
-              Recursive definitions are not allowed
-
-
-● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱
-
-
-        Unbound variable
-        ⇩
-    ┌─────────────────┐
-    │  (x : Bool) → x │
-    └─────────────────┘
-      ⇧
-      A ❰λ❱ here would transform this into a valid anonymous function 
-
-
-        Unbound variable
-        ⇩
-    ┌────────────────────┐
-    │  (x : Bool) → Bool │
-    └────────────────────┘
-      ⇧
-      A ❰∀❱ or ❰forall❱ here would transform this into a valid function type
diff --git a/dhall/src/errors/Untyped.txt b/dhall/src/errors/Untyped.txt
deleted file mode 100644
index 4904bf8..0000000
--- a/dhall/src/errors/Untyped.txt
+++ /dev/null
@@ -1,117 +0,0 @@
-Explanation: Every function declares what type or kind of argument to accept
-
-For example:
-
-
-    ┌───────────────────────────────┐
-    │ λ(x : Bool) → x : Bool → Bool │  This anonymous function only accepts
-    └───────────────────────────────┘  arguments that have type ❰Bool❱
-                        ⇧
-                        The function's input type
-
-
-    ┌───────────────────────────────┐
-    │ Natural/even : Natural → Bool │  This built-in function only accepts
-    └───────────────────────────────┘  arguments that have type ❰Natural❱
-                     ⇧
-                     The function's input type
-
-
-    ┌───────────────────────────────┐
-    │ λ(a : Type) → a : Type → Type │  This anonymous function only accepts
-    └───────────────────────────────┘  arguments that have kind ❰Type❱
-                        ⇧
-                        The function's input kind
-
-
-    ┌────────────────────┐
-    │ List : Type → Type │  This built-in function only accepts arguments that
-    └────────────────────┘  have kind ❰Type❱
-             ⇧
-             The function's input kind
-
-
-For example, the following expressions are valid:
-
-
-    ┌────────────────────────┐
-    │ (λ(x : Bool) → x) True │  ❰True❱ has type ❰Bool❱, which matches the type
-    └────────────────────────┘  of argument that the anonymous function accepts
-
-
-    ┌─────────────────┐
-    │ Natural/even +2 │  ❰+2❱ has type ❰Natural❱, which matches the type of
-    └─────────────────┘  argument that the ❰Natural/even❱ function accepts,
-
-
-    ┌────────────────────────┐
-    │ (λ(a : Type) → a) Bool │  ❰Bool❱ has kind ❰Type❱, which matches the kind
-    └────────────────────────┘  of argument that the anonymous function accepts
-
-
-    ┌───────────┐
-    │ List Text │  ❰Text❱ has kind ❰Type❱, which matches the kind of argument
-    └───────────┘  that that the ❰List❱ function accepts
-
-
-However, you can $_NOT apply a function to the wrong type or kind of argument
-
-For example, the following expressions are not valid:
-
-
-    ┌───────────────────────┐
-    │ (λ(x : Bool) → x) "A" │  ❰"A"❱ has type ❰Text❱, but the anonymous function
-    └───────────────────────┘  expects an argument that has type ❰Bool❱
-
-
-    ┌──────────────────┐
-    │ Natural/even "A" │  ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
-    └──────────────────┘  expects an argument that has type ❰Natural❱
-
-
-    ┌────────────────────────┐
-    │ (λ(a : Type) → a) True │  ❰True❱ has type ❰Bool❱, but the anonymous
-    └────────────────────────┘  function expects an argument of kind ❰Type❱
-
-
-    ┌────────┐
-    │ List 1 │  ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
-    └────────┘  argument that has kind ❰Type❱
-
-
-You tried to invoke the following function:
-
-↳ $txt0
-
-... which expects an argument of type or kind:
-
-↳ $txt1
-
-... on the following argument:
-
-↳ $txt2
-
-... which has a different type or kind:
-
-↳ $txt3
-
-Some common reasons why you might get this error:
-
-● You omit a function argument by mistake:
-
-
-    ┌────────────────────────────────────────┐
-    │ List/head   ([1, 2, 3] : List Integer) │
-    └────────────────────────────────────────┘
-                ⇧
-                ❰List/head❱ is missing the first argument,
-                which should be: ❰Integer❱
-
-
-● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
-
-    ┌────────────────┐
-    │ Natural/even 2 │
-    └────────────────┘
-                   ⇧
-                   This should be ❰+2❱
diff --git a/dhall/src/errors/UnusedHandler.txt b/dhall/src/errors/UnusedHandler.txt
deleted file mode 100644
index 2e46a12..0000000
--- a/dhall/src/errors/UnusedHandler.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-Explanation: You can ❰merge❱ the alternatives of a union using a record with one
-handler per alternative, like this:
-
-
-    ┌─────────────────────────────────────────────────────────────────────┐
-    │     let union    = < Left = +2 | Right : Bool >                     │
-    │ in  let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
-    │ in  merge handlers union : Bool                                     │
-    └─────────────────────────────────────────────────────────────────────┘
-
-
-... but you must provide exactly one handler per alternative in the union.  You
-cannot supply extra handlers
-
-For example, the following expression is $_NOT valid:
-
-
-    ┌───────────────────────────────────────┐
-    │     let union    = < Left = +2 >      │  The ❰Right❱ alternative is missing
-    │ in  let handlers =                    │ 
-    │             { Left  = Natural/even    │
-    │             , Right = λ(x : Bool) → x │  Invalid: ❰Right❱ handler isn't used
-    │             }                         │
-    │ in  merge handlers union : Bool       │
-    └───────────────────────────────────────┘
-
-
-You provided the following handlers:
-
-↳ $txt0
-
-... which had no matching alternatives in the union you tried to ❰merge❱
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index ec110f7..9f9c315 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -123,7 +123,6 @@
 #[macro_use]
 mod tests;
 
-/// When manipulating Dhall expressions goes wrong.
 pub mod error;
 mod phase;
 mod serde;
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 9c31d4c..30aa7a0 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -1,14 +1,15 @@
-use dhall_syntax::*;
-use itertools::*;
+use itertools::Itertools;
 use serde_cbor::value::value as cbor;
 
-type ParsedExpr = SubExpr<X, Import>;
+use dhall_syntax::{
+    rc, ExprF, FilePrefix, Hash, Import, ImportHashed, ImportLocation,
+    ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, SubExpr,
+    URL, V, X,
+};
 
-#[derive(Debug)]
-pub enum DecodeError {
-    CBORError(serde_cbor::error::Error),
-    WrongFormatError(String),
-}
+use crate::error::DecodeError;
+
+type ParsedExpr = SubExpr<X, Import>;
 
 pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
     match serde_cbor::de::from_slice(data) {
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 0b6eca6..4262dc1 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,13 +4,11 @@ use std::path::Path;
 
 use dhall_syntax::{Const, Import, Span, SubExpr, X};
 
-use crate::error::Error;
+use crate::error::{Error, ImportError, TypeError, TypeMessage};
 
 use normalize::{AlphaVar, Thunk, Value};
-use resolve::{ImportError, ImportRoot};
-use typecheck::{
-    const_to_typed, type_of_const, TypeError, TypeMessage, TypecheckContext,
-};
+use resolve::ImportRoot;
+use typecheck::{const_to_typed, type_of_const, TypecheckContext};
 
 pub(crate) mod binary;
 pub(crate) mod normalize;
diff --git a/dhall/src/phase/resolve.rs b/dhall/src/phase/resolve.rs
index afb49cb..5ab03ac 100644
--- a/dhall/src/phase/resolve.rs
+++ b/dhall/src/phase/resolve.rs
@@ -3,16 +3,9 @@ use std::path::{Path, PathBuf};
 
 use dhall_syntax::Import;
 
-use crate::error::Error;
+use crate::error::{Error, ImportError};
 use crate::phase::{Normalized, Parsed, Resolved};
 
-#[derive(Debug)]
-pub enum ImportError {
-    Recursive(Import, Box<Error>),
-    UnexpectedImport(Import),
-    ImportCycle(ImportStack, Import),
-}
-
 /// A root from which to resolve relative imports.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum ImportRoot {
@@ -21,7 +14,7 @@ pub enum ImportRoot {
 
 type ImportCache = HashMap<Import, Normalized>;
 
-type ImportStack = Vec<Import>;
+pub(crate) type ImportStack = Vec<Import>;
 
 fn resolve_import(
     import: &Import,
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 6b12077..aee9892 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -2,19 +2,20 @@
 use std::borrow::Borrow;
 use std::borrow::Cow;
 use std::collections::BTreeMap;
-use std::fmt;
 
+use dhall_proc_macros as dhall;
+use dhall_syntax::context::Context;
+use dhall_syntax::{
+    rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, Span,
+    SubExpr, V, X,
+};
+
+use crate::error::{TypeError, TypeMessage};
 use crate::phase::normalize::{
     AlphaVar, NormalizationContext, Thunk, TypeThunk, Value,
 };
-use crate::phase::*;
+use crate::phase::{Normalized, Resolved, Type, TypeInternal, Typed};
 use crate::traits::DynamicType;
-use dhall_proc_macros as dhall;
-use dhall_syntax;
-use dhall_syntax::context::Context;
-use dhall_syntax::*;
-
-use self::TypeMessage::*;
 
 impl TypeThunk {
     fn to_type(&self, ctx: &TypecheckContext) -> Result<Type, TypeError> {
@@ -244,6 +245,7 @@ pub(crate) enum TypeIntermediate {
 
 impl TypeIntermediate {
     fn typecheck(self) -> Result<Typed, TypeError> {
+        use crate::error::TypeMessage::*;
         let mkerr = |ctx, msg| TypeError::new(ctx, msg);
         Ok(match &self {
             TypeIntermediate::Pi(ctx, x, ta, tb) => {
@@ -503,6 +505,7 @@ fn type_last_layer(
     ctx: &TypecheckContext,
     e: ExprF<Typed, Label, Normalized>,
 ) -> Result<Ret, TypeError> {
+    use crate::error::TypeMessage::*;
     use dhall_syntax::BinOp::*;
     use dhall_syntax::Builtin::*;
     use dhall_syntax::ExprF::*;
@@ -801,101 +804,6 @@ pub(crate) fn skip_typecheck(e: Resolved) -> Typed {
     Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0))
 }
 
-/// The specific type error
-#[derive(Debug)]
-pub(crate) enum TypeMessage {
-    UnboundVariable(V<Label>),
-    InvalidInputType(Normalized),
-    InvalidOutputType(Normalized),
-    NotAFunction(Typed),
-    TypeMismatch(Typed, Normalized, Typed),
-    AnnotMismatch(Typed, Normalized),
-    Untyped,
-    InvalidListElement(usize, Normalized, Typed),
-    InvalidListType(Normalized),
-    InvalidOptionalType(Normalized),
-    InvalidPredicate(Typed),
-    IfBranchMismatch(Typed, Typed),
-    IfBranchMustBeTerm(bool, Typed),
-    InvalidFieldType(Label, Type),
-    NotARecord(Label, Normalized),
-    MissingRecordField(Label, Typed),
-    MissingUnionField(Label, Normalized),
-    BinOpTypeMismatch(BinOp, Typed),
-    NoDependentTypes(Normalized, Normalized),
-    InvalidTextInterpolation(Typed),
-    Sort,
-    Unimplemented,
-}
-
-/// A structured type error that includes context
-#[derive(Debug)]
-pub struct TypeError {
-    type_message: TypeMessage,
-    context: TypecheckContext,
-}
-
-impl TypeError {
-    pub(crate) fn new(
-        context: &TypecheckContext,
-        type_message: TypeMessage,
-    ) -> Self {
-        TypeError {
-            context: context.clone(),
-            type_message,
-        }
-    }
-}
-
-impl From<TypeError> for std::option::NoneError {
-    fn from(_: TypeError) -> std::option::NoneError {
-        std::option::NoneError
-    }
-}
-
-impl ::std::error::Error for TypeMessage {
-    fn description(&self) -> &str {
-        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",
-        }
-    }
-}
-
-impl fmt::Display for TypeMessage {
-    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        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"),
-        }
-    }
-}
-
 #[cfg(test)]
 mod spec_tests {
     #![rustfmt::skip]
diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs
index 3f8d117..7763a28 100644
--- a/dhall/src/traits/dynamic_type.rs
+++ b/dhall/src/traits/dynamic_type.rs
@@ -1,5 +1,5 @@
-use crate::phase::typecheck::TypeError;
-use crate::phase::*;
+use crate::error::TypeError;
+use crate::phase::{Normalized, Type, Typed};
 use crate::traits::StaticType;
 use std::borrow::Cow;
 
-- 
cgit v1.2.3