Start implementing error explanations

36 files changed, 1828 insertions, 26 deletions

diff --git a/src/errors/AnnotMismatch.txt b/src/errors/AnnotMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/src/errors/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/src/errors/CantTextAppend.txt b/src/errors/CantTextAppend.txt
new file mode 100644
index 0000000..26b9ceb
--- /dev/null
+++ b/src/errors/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/src/errors/DuplicateAlternative.txt b/src/errors/DuplicateAlternative.txt
new file mode 100644
index 0000000..077f8aa
--- /dev/null
+++ b/src/errors/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/src/errors/FieldCollision.txt b/src/errors/FieldCollision.txt
new file mode 100644
index 0000000..2b2d260
--- /dev/null
+++ b/src/errors/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/src/errors/HandlerInputTypeMismatch.txt b/src/errors/HandlerInputTypeMismatch.txt
new file mode 100644
index 0000000..7d3525b
--- /dev/null
+++ b/src/errors/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/src/errors/HandlerNotAFunction.txt b/src/errors/HandlerNotAFunction.txt
new file mode 100644
index 0000000..ff87443
--- /dev/null
+++ b/src/errors/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/src/errors/HandlerOutputTypeMismatch.txt b/src/errors/HandlerOutputTypeMismatch.txt
new file mode 100644
index 0000000..f359459
--- /dev/null
+++ b/src/errors/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/src/errors/IfBranchMismatch.txt b/src/errors/IfBranchMismatch.txt
new file mode 100644
index 0000000..a95b130
--- /dev/null
+++ b/src/errors/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/src/errors/IfBranchMustBeTerm.txt b/src/errors/IfBranchMustBeTerm.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidAlterantive.txt b/src/errors/InvalidAlterantive.txt
new file mode 100644
index 0000000..391fc3a
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidAlterantiveType.txt b/src/errors/InvalidAlterantiveType.txt
new file mode 100644
index 0000000..f5dadef
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidField.txt b/src/errors/InvalidField.txt
new file mode 100644
index 0000000..bfbf106
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidFieldType.txt b/src/errors/InvalidFieldType.txt
new file mode 100644
index 0000000..4f76a64
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidInputType.txt b/src/errors/InvalidInputType.txt
new file mode 100644
index 0000000..eabafa4
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidListElement.txt b/src/errors/InvalidListElement.txt
new file mode 100644
index 0000000..59db7b7
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidListType.txt b/src/errors/InvalidListType.txt
new file mode 100644
index 0000000..676647e
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidOptionType.txt b/src/errors/InvalidOptionType.txt
new file mode 100644
index 0000000..3bc81de
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidOptionalElement.txt b/src/errors/InvalidOptionalElement.txt
new file mode 100644
index 0000000..0254220
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidOptionalLiteral.txt b/src/errors/InvalidOptionalLiteral.txt
new file mode 100644
index 0000000..41c0fdc
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidOutputType.txt b/src/errors/InvalidOutputType.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/src/errors/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/src/errors/InvalidPredicate.txt b/src/errors/InvalidPredicate.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/src/errors/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/src/errors/MissingField.txt b/src/errors/MissingField.txt
new file mode 100644
index 0000000..de14a33
--- /dev/null
+++ b/src/errors/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/src/errors/MissingHandler.txt b/src/errors/MissingHandler.txt
new file mode 100644
index 0000000..433445e
--- /dev/null
+++ b/src/errors/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/src/errors/MustCombineARecord.txt b/src/errors/MustCombineARecord.txt
new file mode 100644
index 0000000..141b969
--- /dev/null
+++ b/src/errors/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/src/errors/MustMergeARecord.txt b/src/errors/MustMergeARecord.txt
new file mode 100644
index 0000000..79094bd
--- /dev/null
+++ b/src/errors/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/src/errors/MustMergeUnion.txt b/src/errors/MustMergeUnion.txt
new file mode 100644
index 0000000..68df70c
--- /dev/null
+++ b/src/errors/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/src/errors/NoDependentLet.txt b/src/errors/NoDependentLet.txt
new file mode 100644
index 0000000..fdc65b4
--- /dev/null
+++ b/src/errors/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/src/errors/NoDependentTypes.txt b/src/errors/NoDependentTypes.txt
new file mode 100644
index 0000000..435bdcb
--- /dev/null
+++ b/src/errors/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/src/errors/NotAFunction.txt b/src/errors/NotAFunction.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/src/errors/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/src/errors/NotARecord.txt b/src/errors/NotARecord.txt
new file mode 100644
index 0000000..e0eebc8
--- /dev/null
+++ b/src/errors/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/src/errors/TypeMismatch.txt b/src/errors/TypeMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/src/errors/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/src/errors/UnboundVariable.txt b/src/errors/UnboundVariable.txt
new file mode 100644
index 0000000..bd7d483
--- /dev/null
+++ b/src/errors/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/src/errors/Untyped.txt b/src/errors/Untyped.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/src/errors/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/src/errors/UnusedHandler.txt b/src/errors/UnusedHandler.txt
new file mode 100644
index 0000000..2e46a12
--- /dev/null
+++ b/src/errors/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/src/main.rs b/src/main.rs
index 6349ed7..d4b541b 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -16,6 +16,12 @@ pub mod parser;
 pub mod typecheck;
 
 use std::io::{self, Read};
+use std::error::Error;
+
+use term_painter::ToStyle;
+
+const ERROR_STYLE: term_painter::Color = term_painter::Color::Red;
+const BOLD: term_painter::Attr = term_painter::Attr::Bold;
 
 fn print_error(message: &str, source: &str, start: usize, end: usize) {
     let line_number = bytecount::count(source[..start].as_bytes(), '\n' as u8);
@@ -28,34 +34,30 @@ fn print_error(message: &str, source: &str, start: usize, end: usize) {
     let line_number_str = line_number.to_string();
     let line_number_width = line_number_str.len();
 
-    use term_painter::ToStyle;
-    let err_style = term_painter::Color::Red;
-    let bold = term_painter::Attr::Bold;
-
-    bold.with(|| {
-        err_style.with(|| {
+    BOLD.with(|| {
+        ERROR_STYLE.with(|| {
             print!("error: ");
         });
         println!("{}", message);
     });
-    bold.with(|| {
+    BOLD.with(|| {
         print!("  -->");
     });
     println!(" {}:{}:0", "(stdin)", line_number);
-    bold.with(|| {
+    BOLD.with(|| {
         println!("{:w$} |", "", w = line_number_width);
         print!("{} |", line_number_str);
     });
     print!(" {}", context_prefix);
-    bold.with(|| {
-        err_style.with(|| {
+    BOLD.with(|| {
+        ERROR_STYLE.with(|| {
             print!("{}", context_highlighted);
         });
     });
     println!("{}", context_suffix);
-    bold.with(|| {
+    BOLD.with(|| {
         print!("{:w$} |", "", w = line_number_width);
-        err_style.with(|| {
+        ERROR_STYLE.with(|| {
             println!(" {:so$}{:^>ew$}", "", "",
                      so = source[line_start..start].chars().count(),
                      ew = ::std::cmp::max(1, source[start..end].chars().count()));
@@ -85,28 +87,31 @@ fn main() {
         }
     };
 
-    println!("{:?}", expr);
-
     /*
     expr' <- load expr
     */
 
     let type_expr = match typecheck::type_of(&expr) {
         Err(e) => {
-            println!("{:?}", e);
+            let explain = ::std::env::args().find(|s| s == "--explain").is_some();
+            if !explain {
+                term_painter::Color::BrightBlack.with(|| {
+                    println!("Use \"dhall --explain\" for detailed errors");
+                });
+            }
+            ERROR_STYLE.with(|| print!("Error: "));
+            println!("{}", e.type_message.description());
+            if explain {
+                println!("{}", e.type_message);
+            }
+            println!("{}", e.current);
+            // FIXME Print source position
             return;
         }
         Ok(type_expr) => type_expr,
     };
+
     println!("{}", type_expr);
     println!("");
     println!("{}", normalize::<_, X, _>(&expr));
-    /*
-    typeExpr <- case Dhall.TypeCheck.typeOf expr' of
-        Left  err      -> Control.Exception.throwIO err
-        Right typeExpr -> return typeExpr
-    Data.Text.Lazy.IO.hPutStrLn stderr (pretty (normalize typeExpr))
-    Data.Text.Lazy.IO.hPutStrLn stderr mempty
-    Data.Text.Lazy.IO.putStrLn (pretty (normalize expr')) )
-    */
 }
diff --git a/src/typecheck.rs b/src/typecheck.rs
index 12555b1..8abc64c 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -1,6 +1,7 @@
 #![allow(non_snake_case)]
 use std::collections::BTreeMap;
 use std::collections::HashSet;
+use std::fmt;
 
 use context::Context;
 use core;
@@ -566,9 +567,9 @@ pub enum TypeMessage<'i, S> {
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError<'i, S> {
-    context: Context<'i, Expr<'i, S, X>>,
-    current: Expr<'i, S, X>,
-    type_message: TypeMessage<'i, S>,
+    pub context: Context<'i, Expr<'i, S, X>>,
+    pub current: Expr<'i, S, X>,
+    pub type_message: TypeMessage<'i, S>,
 }
 
 impl<'i, S: Clone> TypeError<'i, S> {
@@ -583,3 +584,34 @@ impl<'i, S: Clone> TypeError<'i, S> {
         }
     }
 }
+
+impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
+    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<'i, S> fmt::Display for TypeMessage<'i, S> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        match self {
+            &UnboundVariable => f.write_str(include_str!("errors/UnboundVariable.txt")),
+            &TypeMismatch(ref e0, ref e1, ref e2, ref e3) => {
+                let template = include_str!("errors/TypeMismatch.txt");
+                let s = template
+                    .replace("$txt0", &format!("{}", e0))
+                    .replace("$txt1", &format!("{}", e1))
+                    .replace("$txt2", &format!("{}", e2))
+                    .replace("$txt3", &format!("{}", e3));
+                f.write_str(&s)
+            }
+            _ => f.write_str("Unhandled error message"),
+        }
+    }
+}