Consolidate errors in the error module

35 files changed, 1934 insertions, 0 deletions

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❱