Split abnf_to_pest and dhall into their own crates

45 files changed, 4440 insertions, 0 deletions

diff --git a/dhall/src/context.rs b/dhall/src/context.rs
new file mode 100644
index 0000000..c2e1913
--- /dev/null
+++ b/dhall/src/context.rs
@@ -0,0 +1,51 @@
+use std::collections::HashMap;
+
+/// A `(Context a)` associates `Text` labels with values of type `a`
+///
+/// The `Context` is used for type-checking when `(a = Expr X)`
+///
+/// * You create a `Context` using `empty` and `insert`
+/// * You transform a `Context` using `fmap`
+/// * You consume a `Context` using `lookup` and `toList`
+///
+/// The difference between a `Context` and a `Map` is that a `Context` lets you
+/// have multiple ordered occurrences of the same key and you can query for the
+/// `n`th occurrence of a given key.
+///
+#[derive(Debug, Clone)]
+pub struct Context<'i, T>(HashMap<&'i str, Vec<T>>);
+
+impl<'i, T> Context<'i, T> {
+    /// An empty context with no key-value pairs
+    pub fn new() -> Self {
+        Context(HashMap::new())
+    }
+
+    /// Look up a key by name and index
+    ///
+    /// ```c
+    /// lookup _ _         empty  = Nothing
+    /// lookup k 0 (insert k v c) = Just v
+    /// lookup k n (insert k v c) = lookup k (n - 1) c  -- 1 <= n
+    /// lookup k n (insert j v c) = lookup k  n      c  -- k /= j
+    /// ```
+    pub fn lookup<'a>(&'a self, k: &str, n: usize) -> Option<&'a T> {
+        self.0.get(k).and_then(|v| v.get(v.len() - 1 - n))
+    }
+
+    pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<'i, U> {
+        Context(self.0.iter().map(|(k, v)| (*k, v.iter().map(&f).collect())).collect())
+    }
+}
+
+impl<'i, T: Clone> Context<'i, T> {
+    /// Add a key-value pair to the `Context`
+    pub fn insert(&self, k: &'i str, v: T) -> Self {
+        let mut ctx = (*self).clone();
+        {
+            let m = ctx.0.entry(k).or_insert_with(Vec::new);
+            m.push(v);
+        }
+        ctx
+    }
+}
diff --git a/dhall/src/core.rs b/dhall/src/core.rs
new file mode 100644
index 0000000..473a6a6
--- /dev/null
+++ b/dhall/src/core.rs
@@ -0,0 +1,1056 @@
+#![allow(non_snake_case)]
+use std::collections::BTreeMap;
+use std::fmt::{self, Display};
+use std::path::PathBuf;
+
+/*
+module Dhall.Core (
+    -- * Syntax
+      Const(..)
+    , Path(..)
+    , Var(..)
+    , Expr(..)
+
+    -- * Normalization
+    , normalize
+    , subst
+    , shift
+
+    -- * Pretty-printing
+    , pretty
+
+    -- * Miscellaneous
+    , internalError
+    ) where
+*/
+
+/// Constants for a pure type system
+///
+/// The only axiom is:
+///
+/// ```c
+/// ⊦ Type : Kind
+/// ```
+///
+/// ... and the valid rule pairs are:
+///
+/// ```c
+/// ⊦ Type ↝ Type : Type  -- Functions from terms to terms (ordinary functions)
+/// ⊦ Kind ↝ Type : Type  -- Functions from types to terms (polymorphic functions)
+/// ⊦ Kind ↝ Kind : Kind  -- Functions from types to types (type constructors)
+/// ```
+///
+/// These are the same rule pairs as System Fω
+///
+/// Note that Dhall does not support functions from terms to types and therefore
+/// Dhall is not a dependently typed language
+///
+#[derive(Debug, Copy, Clone, PartialEq, Eq)] // (Show, Bounded, Enum)
+pub enum Const {
+    Type,
+    Kind,
+}
+
+
+/// Path to an external resource
+#[derive(Debug, Clone, PartialEq, Eq)] // (Eq, Ord, Show)
+pub enum Path {
+    File(PathBuf),
+    URL(String),
+}
+
+/// Label for a bound variable
+///
+/// The `String` field is the variable's name (i.e. \"`x`\").
+///
+/// The `Int` field disambiguates variables with the same name if there are
+/// multiple bound variables of the same name in scope.  Zero refers to the
+/// nearest bound variable and the index increases by one for each bound
+/// variable of the same name going outward.  The following diagram may help:
+///
+/// ```c
+///                                 +---refers to--+
+///                                 |              |
+///                                 v              |
+/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@0
+///
+///   +------------------refers to-----------------+
+///   |                                            |
+///   v                                            |
+/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@1
+/// ```
+///
+/// This `Int` behaves like a De Bruijn index in the special case where all
+/// variables have the same name.
+///
+/// You can optionally omit the index if it is `0`:
+///
+/// ```c
+///                           +refers to+
+///                           |         |
+///                           v         |
+/// \(x : *) -> \(y : *) -> \(x : *) -> x
+/// ```
+///
+/// Zero indices are omitted when pretty-printing `Var`s and non-zero indices
+/// appear as a numeric suffix.
+///
+#[derive(Debug, Copy, Clone, PartialEq, Eq)] // (Eq, Show)
+pub struct V<'i>(pub &'i str, pub usize);
+
+/*
+instance IsString Var where
+    fromString str = V (fromString str) 0
+
+instance Buildable Var where
+    build = buildVar
+*/
+
+/// Syntax tree for expressions
+#[derive(Debug, Clone, PartialEq)] // (Functor, Foldable, Traversable, Show)
+pub enum Expr<'i, S, A> {
+    ///  `Const c                                  ~  c`
+    Const(Const),
+    ///  `Var (V x 0)                              ~  x`<br>
+    ///  `Var (V x n)                              ~  x@n`
+    Var(V<'i>),
+    ///  `Lam x     A b                            ~  λ(x : A) -> b`
+    Lam(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `Pi "_" A B                               ~        A  -> B`
+    ///  `Pi x   A B                               ~  ∀(x : A) -> B`
+    Pi(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `App f A                                  ~  f A`
+    App(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `Let x Nothing  r e  ~  let x     = r in e`
+    ///  `Let x (Just t) r e  ~  let x : t = r in e`
+    Let(&'i str, Option<Box<Expr<'i, S, A>>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `Annot x t                                ~  x : t`
+    Annot(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    /// Built-in types
+    BuiltinType(BuiltinType),
+    /// Built-in function values
+    BuiltinValue(BuiltinValue),
+    ///  `BoolLit b                                ~  b`
+    BoolLit(bool),
+    ///  `BoolAnd x y                              ~  x && y`
+    BoolAnd(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `BoolOr  x y                              ~  x || y`
+    BoolOr(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `BoolEQ  x y                              ~  x == y`
+    BoolEQ(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `BoolNE  x y                              ~  x != y`
+    BoolNE(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `BoolIf x y z                             ~  if x then y else z`
+    BoolIf(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `NaturalLit n                             ~  +n`
+    NaturalLit(Natural),
+    ///  `NaturalPlus x y                          ~  x + y`
+    NaturalPlus(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `NaturalTimes x y                         ~  x * y`
+    NaturalTimes(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `IntegerLit n                             ~  n`
+    IntegerLit(Integer),
+    ///  `DoubleLit n                              ~  n`
+    DoubleLit(Double),
+    ///  `TextLit t                                ~  t`
+    TextLit(Builder),
+    ///  `TextAppend x y                           ~  x ++ y`
+    TextAppend(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `ListLit t [x, y, z]                      ~  [x, y, z] : List t`
+    ListLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
+    ///  `OptionalLit t [e]                        ~  [e] : Optional t`
+    ///  `OptionalLit t []                         ~  []  : Optional t`
+    OptionalLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
+    ///  `Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }`
+    Record(BTreeMap<&'i str, Expr<'i, S, A>>),
+    ///  `RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }`
+    RecordLit(BTreeMap<&'i str, Expr<'i, S, A>>),
+    ///  `Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1, k2 : t2 >`
+    Union(BTreeMap<&'i str, Expr<'i, S, A>>),
+    ///  `UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1, k2 : t2, k3 : t3 >`
+    UnionLit(&'i str, Box<Expr<'i, S, A>>, BTreeMap<&'i str, Expr<'i, S, A>>),
+    ///  `Combine x y                              ~  x ∧ y`
+    Combine(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `Merge x y t                              ~  merge x y : t`
+    Merge(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+    ///  `Field e x                                ~  e.x`
+    Field(Box<Expr<'i, S, A>>, &'i str),
+    ///  `Note S x                                 ~  e`
+    Note(S, Box<Expr<'i, S, A>>),
+    ///  `Embed path                               ~  path`
+    Embed(A),
+}
+
+/// Built-in types
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum BuiltinType {
+    ///  `Bool                                     ~  Bool`
+    Bool,
+    ///  `Natural                                  ~  Natural`
+    Natural,
+    ///  `Integer                                  ~  Integer`
+    Integer,
+    ///  `Double                                   ~  Double`
+    Double,
+    ///  `Text                                     ~  Text`
+    Text,
+    ///  `List                                     ~  List`
+    List,
+    ///  `Optional                                 ~  Optional`
+    Optional,
+}
+
+/// Built-in function values
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum BuiltinValue {
+    ///  `NaturalFold                              ~  Natural/fold`
+    NaturalFold,
+    ///  `NaturalBuild                             ~  Natural/build`
+    NaturalBuild,
+    ///  `NaturalIsZero                            ~  Natural/isZero`
+    NaturalIsZero,
+    ///  `NaturalEven                              ~  Natural/even`
+    NaturalEven,
+    ///  `NaturalOdd                               ~  Natural/odd`
+    NaturalOdd,
+    NaturalShow,
+    ///  `ListBuild                                ~  List/build`
+    ListBuild,
+    ///  `ListFold                                 ~  List/fold`
+    ListFold,
+    ///  `ListLength                               ~  List/length`
+    ListLength,
+    ///  `ListHead                                 ~  List/head`
+    ListHead,
+    ///  `ListLast                                 ~  List/last`
+    ListLast,
+    ///  `ListIndexed                              ~  List/indexed`
+    ListIndexed,
+    ///  `ListReverse                              ~  List/reverse`
+    ListReverse,
+    ///  `OptionalFold                             ~  Optional/fold`
+    OptionalFold,
+}
+
+impl<'i> From<&'i str> for V<'i> {
+    fn from(s: &'i str) -> Self {
+        V(s, 0)
+    }
+}
+
+impl<'i, S, A> From<&'i str> for Expr<'i, S, A> {
+    fn from(s: &'i str) -> Self {
+        Expr::Var(s.into())
+    }
+}
+
+impl<'i, S, A> From<BuiltinType> for Expr<'i, S, A> {
+    fn from(t: BuiltinType) -> Self {
+        Expr::BuiltinType(t)
+    }
+}
+
+impl<'i, S, A> From<BuiltinValue> for Expr<'i, S, A> {
+    fn from(t: BuiltinValue) -> Self {
+        Expr::BuiltinValue(t)
+    }
+}
+
+impl<'i, S, A> Expr<'i, S, A> {
+    fn bool_lit(&self) -> Option<bool> {
+        match *self {
+            Expr::BoolLit(v) => Some(v),
+            _ => None,
+        }
+    }
+
+    fn natural_lit(&self) -> Option<usize> {
+        match *self {
+            Expr::NaturalLit(v) => Some(v),
+            _ => None,
+        }
+    }
+
+    fn text_lit(&self) -> Option<String> {
+        match *self {
+            Expr::TextLit(ref t) => Some(t.clone()), // FIXME?
+            _ => None,
+        }
+    }
+}
+
+//  There is a one-to-one correspondence between the formatters in this section
+//  and the grammar in grammar.lalrpop.  Each formatter is named after the
+//  corresponding grammar rule and the relationship between formatters exactly matches
+//  the relationship between grammar rules.  This leads to the nice emergent property
+//  of automatically getting all the parentheses and precedences right.
+//
+//  This approach has one major disadvantage: you can get an infinite loop if
+//  you add a new constructor to the syntax tree without adding a matching
+//  case the corresponding builder.
+
+impl<'i, S, A: Display> Display for Expr<'i, S, A> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { // buildExprA
+        use crate::Expr::*;
+        match self {
+            &Annot(ref a, ref b) => { a.fmt_b(f)?; write!(f, " : ")?; b.fmt(f) }
+            &Note(_, ref b) => b.fmt(f),
+            a => a.fmt_b(f),
+        }
+    }
+}
+
+impl<'i, S, A: Display> Expr<'i, S, A> {
+    fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use crate::Expr::*;
+        match self {
+            &Lam(a, ref b, ref c) => {
+                write!(f, "λ({} : ", a)?;
+                b.fmt(f)?;
+                write!(f, ") → ")?;
+                c.fmt_b(f)
+            }
+            &BoolIf(ref a, ref b, ref c) => {
+                write!(f, "if ")?;
+                a.fmt(f)?;
+                write!(f, " then ")?;
+                b.fmt_b(f)?;
+                write!(f, " else ")?;
+                c.fmt_c(f)
+            }
+            &Pi("_", ref b, ref c) => {
+                b.fmt_c(f)?;
+                write!(f, " → ")?;
+                c.fmt_b(f)
+            }
+            &Pi(a, ref b, ref c) => {
+                write!(f, "∀({} : ", a)?;
+                b.fmt(f)?;
+                write!(f, ") → ")?;
+                c.fmt_b(f)
+            }
+            &Let(a, None, ref c, ref d) => {
+                write!(f, "let {} = ", a)?;
+                c.fmt(f)?;
+                write!(f, ") → ")?;
+                d.fmt_b(f)
+            }
+            &Let(a, Some(ref b), ref c, ref d) => {
+                write!(f, "let {} : ", a)?;
+                b.fmt(f)?;
+                write!(f, " = ")?;
+                c.fmt(f)?;
+                write!(f, ") → ")?;
+                d.fmt_b(f)
+            }
+            &ListLit(ref t, ref es) => {
+                fmt_list("[", "] : List ", es, f, |e, f| e.fmt(f))?;
+                t.fmt_e(f)
+            }
+            &OptionalLit(ref t, ref es) => {
+                fmt_list("[", "] : Optional ", es, f, |e, f| e.fmt(f))?;
+                t.fmt_e(f)
+            }
+            &Merge(ref a, ref b, ref c) => {
+                write!(f, "merge ")?;
+                a.fmt_e(f)?;
+                write!(f, " ")?;
+                b.fmt_e(f)?;
+                write!(f, " : ")?;
+                c.fmt_d(f)
+            }
+            &Note(_, ref b) => b.fmt_b(f),
+            a => a.fmt_c(f),
+        }
+    }
+
+    fn fmt_c(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use crate::Expr::*;
+        match self {
+            // FIXME precedence
+            &BoolOr(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" || ")?; b.fmt_c(f) }
+            &TextAppend(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ++ ")?; b.fmt_c(f) }
+            &NaturalPlus(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" + ")?; b.fmt_c(f) }
+            &BoolAnd(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" && ")?; b.fmt_c(f) }
+            &Combine(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ^ ")?; b.fmt_c(f) }
+            &NaturalTimes(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" * ")?; b.fmt_c(f) }
+            &BoolEQ(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" == ")?; b.fmt_c(f) }
+            &BoolNE(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" != ")?; b.fmt_c(f) }
+            &Note(_, ref b) => b.fmt_c(f),
+            a => a.fmt_d(f),
+        }
+    }
+
+    fn fmt_d(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use crate::Expr::*;
+        match self {
+            &App(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ")?; b.fmt_e(f) }
+            &Note(_, ref b) => b.fmt_d(f),
+            a => a.fmt_e(f)
+        }
+    }
+
+    fn fmt_e(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use crate::Expr::*;
+        match self {
+            &Field(ref a, b) => { a.fmt_e(f)?; write!(f, ".{}", b) }
+            &Note(_, ref b) => b.fmt_e(f),
+            a => a.fmt_f(f)
+        }
+    }
+
+    fn fmt_f(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use crate::Expr::*;
+        match self {
+            &Var(a) => a.fmt(f),
+            &Const(k) => k.fmt(f),
+            &BuiltinType(t) => t.fmt(f),
+            &BuiltinValue(v) => v.fmt(f),
+            &BoolLit(true) => f.write_str("True"),
+            &BoolLit(false) => f.write_str("False"),
+            &IntegerLit(a) => a.fmt(f),
+            &NaturalLit(a) => {
+                f.write_str("+")?;
+                a.fmt(f)
+            }
+            &DoubleLit(a) => a.fmt(f),
+            &TextLit(ref a) => <String as fmt::Debug>::fmt(a, f), // FIXME Format with Haskell escapes
+            &Record(ref a) if a.is_empty() => f.write_str("{}"),
+            &Record(ref a) => {
+                fmt_list("{ ", " }", a, f, |(k, t), f| write!(f, "{} : {}", k, t))
+            }
+            &RecordLit(ref a) if a.is_empty() => f.write_str("{=}"),
+            &RecordLit(ref a) => {
+                fmt_list("{ ", " }", a, f, |(k, v), f| write!(f, "{} = {}", k, v))
+            }
+            &Union(ref _a) => f.write_str("Union"),
+            &UnionLit(_a, ref _b, ref _c) => f.write_str("UnionLit"),
+            &Embed(ref a) => a.fmt(f),
+            &Note(_, ref b) => b.fmt_f(f),
+            a => write!(f, "({})", a),
+        }
+    }
+}
+
+fn fmt_list<T, I, F>(open: &str,
+                     close: &str,
+                     it: I,
+                     f: &mut fmt::Formatter,
+                     func: F)
+                     -> Result<(), fmt::Error>
+    where I: IntoIterator<Item = T>,
+          F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error>
+{
+    f.write_str(open)?;
+    for (i, x) in it.into_iter().enumerate() {
+        if i > 0 {
+            f.write_str(", ")?;
+        }
+        func(x, f)?;
+    }
+    f.write_str(close)
+}
+
+impl Display for Const {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        <Self as fmt::Debug>::fmt(self, f)
+    }
+}
+
+impl Display for BuiltinType {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        <Self as fmt::Debug>::fmt(self, f)
+    }
+}
+
+impl Display for BuiltinValue {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use crate::BuiltinValue::*;
+        f.write_str(match *self {
+            ListBuild => "List/build",
+            ListFold => "List/fold",
+            ListHead => "List/head",
+            ListIndexed => "List/indexed",
+            ListLast => "List/last",
+            ListLength => "List/length",
+            ListReverse => "List/reverse",
+            NaturalBuild => "Natural/build",
+            NaturalEven => "Natural/even",
+            NaturalFold => "Natural/fold",
+            NaturalIsZero => "Natural/isZero",
+            NaturalOdd => "Natural/odd",
+            NaturalShow => "Natural/show",
+            OptionalFold => "Optional/fold",
+        })
+    }
+}
+
+impl<'i> Display for V<'i> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        let V(x, n) = *self;
+        f.write_str(x)?;
+        if n != 0 {
+            write!(f, "@{}", n)?;
+        }
+        Ok(())
+    }
+}
+
+pub fn pi<'i, S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<'i, S, A>
+    where Name: Into<&'i str>,
+          Et: Into<Expr<'i, S, A>>,
+          Ev: Into<Expr<'i, S, A>>
+{
+    Expr::Pi(var.into(), bx(ty.into()), bx(value.into()))
+}
+
+pub fn app<'i, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<'i, S, A>
+    where Ef: Into<Expr<'i, S, A>>,
+          Ex: Into<Expr<'i, S, A>>
+{
+    Expr::App(bx(f.into()), bx(x.into()))
+}
+
+pub type Builder = String;
+pub type Double = f64;
+pub type Int = isize;
+pub type Integer = isize;
+pub type Natural = usize;
+
+/// A void type
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum X {}
+
+impl Display for X {
+    fn fmt(&self, _: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        match *self {}
+    }
+}
+
+pub fn bx<T>(x: T) -> Box<T> {
+    Box::new(x)
+}
+
+fn add_ui(u: usize, i: isize) -> usize {
+    if i < 0 {
+        u.checked_sub(i.checked_neg().unwrap() as usize).unwrap()
+    } else {
+        u.checked_add(i as usize).unwrap()
+    }
+}
+
+fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
+    where I: IntoIterator<Item = (&'a K, &'a V)>,
+          K: Eq + Ord + Copy + 'a,
+          V: 'a,
+          F: Fn(&V) -> U
+{
+    it.into_iter().map(|(&k, v)| (k, f(v))).collect()
+}
+
+fn map_op2<T, U, V, F, G>(f: F, g: G, a: T, b: T) -> V
+    where F: FnOnce(U, U) -> V,
+          G: Fn(T) -> U,
+{
+    f(g(a), g(b))
+}
+
+/// `shift` is used by both normalization and type-checking to avoid variable
+/// capture by shifting variable indices
+///
+/// For example, suppose that you were to normalize the following expression:
+///
+/// ```c
+/// λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
+/// ```
+///
+/// If you were to substitute `y` with `x` without shifting any variable
+/// indices, then you would get the following incorrect result:
+///
+/// ```c
+/// λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form
+/// ```
+///
+/// In order to substitute `x` in place of `y` we need to `shift` `x` by `1` in
+/// order to avoid being misinterpreted as the `x` bound by the innermost
+/// lambda.  If we perform that `shift` then we get the correct result:
+///
+/// ```c
+/// λ(a : Type) → λ(x : a) → λ(x : a) → x@1
+/// ```
+///
+/// As a more worked example, suppose that you were to normalize the following
+/// expression:
+///
+/// ```c
+///     λ(a : Type)
+/// →   λ(f : a → a → a)
+/// →   λ(x : a)
+/// →   λ(x : a)
+/// →   (λ(x : a) → f x x@1) x@1
+/// ```
+///
+/// The correct normalized result would be:
+///
+/// ```c
+///     λ(a : Type)
+/// →   λ(f : a → a → a)
+/// →   λ(x : a)
+/// →   λ(x : a)
+/// →   f x@1 x
+/// ```
+///
+/// The above example illustrates how we need to both increase and decrease
+/// variable indices as part of substitution:
+///
+/// * We need to increase the index of the outer `x\@1` to `x\@2` before we
+///   substitute it into the body of the innermost lambda expression in order
+///   to avoid variable capture.  This substitution changes the body of the
+///   lambda expression to `(f x\@2 x\@1)`
+///
+/// * We then remove the innermost lambda and therefore decrease the indices of
+///   both `x`s in `(f x\@2 x\@1)` to `(f x\@1 x)` in order to reflect that one
+///   less `x` variable is now bound within that scope
+///
+/// Formally, `(shift d (V x n) e)` modifies the expression `e` by adding `d` to
+/// the indices of all variables named `x` whose indices are greater than
+/// `(n + m)`, where `m` is the number of bound variables of the same name
+/// within that scope
+///
+/// In practice, `d` is always `1` or `-1` because we either:
+///
+/// * increment variables by `1` to avoid variable capture during substitution
+/// * decrement variables by `1` when deleting lambdas after substitution
+///
+/// `n` starts off at `0` when substitution begins and increments every time we
+/// descend into a lambda or let expression that binds a variable of the same
+/// name in order to avoid shifting the bound variables by mistake.
+///
+pub fn shift<'i, S, T, A: Clone>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i, T, A> {
+    use crate::Expr::*;
+    let V(x, n) = v;
+    match *e {
+        Const(a) => Const(a),
+        Var(V(x2, n2)) => {
+            let n3 = if x == x2 && n <= n2 { add_ui(n2, d) } else { n2 };
+            Var(V(x2, n3))
+        }
+        Lam(x2, ref tA, ref b) => {
+            let n2 = if x == x2 { n + 1 } else { n };
+            let tA2 = shift(d, V(x, n ), tA);
+            let b2  = shift(d, V(x, n2), b);
+            Lam(x2, bx(tA2), bx(b2))
+        }
+        Pi(x2, ref tA, ref tB) => {
+            let n2 = if x == x2 { n + 1 } else { n };
+            let tA2 = shift(d, V(x, n ), tA);
+            let tB2 = shift(d, V(x, n2), tB);
+            pi(x2, tA2, tB2)
+        }
+        App(ref f, ref a) => app(shift(d, v, f), shift(d, v, a)),
+        Let(f, ref mt, ref r, ref e) => {
+            let n2 = if x == f { n + 1 } else { n };
+            let e2 = shift(d, V(x, n2), e);
+            let mt2 = mt.as_ref().map(|t| bx(shift(d, V(x, n), t)));
+            let r2  = shift(d, V(x, n), r);
+            Let(f, mt2, bx(r2), bx(e2))
+        }
+        Annot(ref a, ref b) => shift_op2(Annot, d, v, a, b),
+        BuiltinType(t) => BuiltinType(t),
+        BuiltinValue(v) => BuiltinValue(v),
+        BoolLit(a) => BoolLit(a),
+        BoolAnd(ref a, ref b) => shift_op2(BoolAnd, d, v, a, b),
+        BoolOr(ref a, ref b) => shift_op2(BoolOr, d, v, a, b),
+        BoolEQ(ref a, ref b) => shift_op2(BoolEQ, d, v, a, b),
+        BoolNE(ref a, ref b) => shift_op2(BoolNE, d, v, a, b),
+        BoolIf(ref a, ref b, ref c) => {
+            BoolIf(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
+        }
+        NaturalLit(a) => NaturalLit(a),
+        NaturalPlus(ref a, ref b) => NaturalPlus(bx(shift(d, v, a)), bx(shift(d, v, b))),
+        NaturalTimes(ref a, ref b) => shift_op2(NaturalTimes, d, v, a, b),
+        IntegerLit(a) => IntegerLit(a),
+        DoubleLit(a) => DoubleLit(a),
+        TextLit(ref a) => TextLit(a.clone()),
+        TextAppend(ref a, ref b) => shift_op2(TextAppend, d, v, a, b),
+        ListLit(ref t, ref es) => {
+            ListLit(bx(shift(d, v, t)),
+                    es.iter().map(|e| shift(d, v, e)).collect())
+        }
+        OptionalLit(ref t, ref es) => {
+            OptionalLit(bx(shift(d, v, t)),
+                        es.iter().map(|e| shift(d, v, e)).collect())
+        }
+        Record(ref a) => Record(map_record_value(a, |val| shift(d, v, val))),
+        RecordLit(ref a) => RecordLit(map_record_value(a, |val| shift(d, v, val))),
+        Union(ref a) => Union(map_record_value(a, |val| shift(d, v, val))),
+        UnionLit(k, ref uv, ref a) => {
+            UnionLit(k,
+                     bx(shift(d, v, uv)),
+                     map_record_value(a, |val| shift(d, v, val)))
+        }
+        Combine(ref a, ref b) => shift_op2(Combine, d, v, a, b),
+        Merge(ref a, ref b, ref c) => {
+            Merge(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
+        }
+        Field(ref a, b) => Field(bx(shift(d, v, a)), b),
+        Note(_, ref b) => shift(d, v, b),
+        // The Dhall compiler enforces that all embedded values are closed expressions
+        // and `shift` does nothing to a closed expression
+        Embed(ref p) => Embed(p.clone()),
+    }
+}
+
+fn shift_op2<'i, S, T, A, F>(f: F,
+                             d: isize,
+                             v: V,
+                             a: &Expr<'i, S, A>,
+                             b: &Expr<'i, S, A>)
+                             -> Expr<'i, T, A>
+    where F: FnOnce(Box<Expr<'i, T, A>>, Box<Expr<'i, T, A>>) -> Expr<'i, T, A>,
+          A: Clone
+{
+    map_op2(f, |x| bx(shift(d, v, x)), a, b)
+}
+
+/// Substitute all occurrences of a variable with an expression
+///
+/// ```c
+/// subst x C B  ~  B[x := C]
+/// ```
+///
+pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> Expr<'i, S, A>
+    where S: Clone,
+          A: Clone
+{
+    use crate::Expr::*;
+    let V(x, n) = v;
+    match *b {
+        Const(a) => Const(a),
+        Lam(y, ref tA, ref b) => {
+            let n2  = if x == y { n + 1 } else { n };
+            let b2  = subst(V(x, n2), &shift(1, V(y, 0), e), b);
+            let tA2 = subst(V(x, n),                     e, tA);
+            Lam(y, bx(tA2), bx(b2))
+        }
+        Pi(y, ref tA, ref tB) => {
+            let n2  = if x == y { n + 1 } else { n };
+            let tB2 = subst(V(x, n2), &shift(1, V(y, 0), e), tB);
+            let tA2 = subst(V(x, n),                     e,  tA);
+            pi(y, tA2, tB2)
+        }
+        App(ref f, ref a) => {
+            let f2 = subst(v, e, f);
+            let a2 = subst(v, e, a);
+            app(f2, a2)
+        }
+        Var(v2) => if v == v2 { e.clone() } else { Var(v2) },
+        Let(f, ref mt, ref r, ref b) => {
+            let n2 = if x == f { n + 1 } else { n };
+            let b2 = subst(V(x, n2), &shift(1, V(f, 0), e), b);
+            let mt2 = mt.as_ref().map(|t| bx(subst(V(x, n), e, t)));
+            let r2  = subst(V(x, n), e, r);
+            Let(f, mt2, bx(r2), bx(b2))
+        }
+        Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b),
+        BuiltinType(t) => BuiltinType(t),
+        BuiltinValue(v) => BuiltinValue(v),
+        BoolLit(a) => BoolLit(a),
+        BoolAnd(ref a, ref b) => subst_op2(BoolAnd, v, e, a, b),
+        BoolOr(ref a, ref b) => subst_op2(BoolOr, v, e, a, b),
+        BoolEQ(ref a, ref b) => subst_op2(BoolEQ, v, e, a, b),
+        BoolNE(ref a, ref b) => subst_op2(BoolNE, v, e, a, b),
+        BoolIf(ref a, ref b, ref c) => {
+            BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
+        }
+        NaturalLit(a) => NaturalLit(a),
+        NaturalPlus(ref a, ref b) => subst_op2(NaturalPlus, v, e, a, b),
+        NaturalTimes(ref a, ref b) => subst_op2(NaturalTimes, v, e, a, b),
+        IntegerLit(a) => IntegerLit(a),
+        DoubleLit(a) => DoubleLit(a),
+        TextLit(ref a) => TextLit(a.clone()),
+        TextAppend(ref a, ref b) => subst_op2(TextAppend, v, e, a, b),
+        ListLit(ref a, ref b) => {
+            let a2 = subst(v, e, a);
+            let b2 = b.iter().map(|be| subst(v, e, be)).collect();
+            ListLit(bx(a2), b2)
+        }
+        OptionalLit(ref a, ref b) => {
+            let a2 = subst(v, e, a);
+            let b2 = b.iter().map(|be| subst(v, e, be)).collect();
+            OptionalLit(bx(a2), b2)
+        }
+        Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))),
+        RecordLit(ref kvs) => RecordLit(map_record_value(kvs, |val| subst(v, e, val))),
+        Union(ref kts) => Union(map_record_value(kts, |t| subst(v, e, t))),
+        UnionLit(k, ref uv, ref kvs) => {
+            UnionLit(k,
+                     bx(subst(v, e, uv)),
+                     map_record_value(kvs, |val| subst(v, e, val)))
+        }
+        Combine(ref a, ref b) => subst_op2(Combine, v, e, a, b),
+        Merge(ref a, ref b, ref c) => {
+            Merge(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
+        }
+        Field(ref a, b) => Field(bx(subst(v, e, a)), b),
+        Note(_, ref b) => subst(v, e, b),
+        Embed(ref p) => Embed(p.clone()),
+    }
+}
+
+fn subst_op2<'i, S, T, A, F>(f: F,
+                             v: V<'i>,
+                             e: &Expr<'i, S, A>,
+                             a: &Expr<'i, T, A>,
+                             b: &Expr<'i, T, A>)
+                             -> Expr<'i, S, A>
+    where F: FnOnce(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>) -> Expr<'i, S, A>,
+          S: Clone,
+          A: Clone
+{
+    map_op2(f, |x| bx(subst(v, e, x)), a, b)
+}
+
+/// Reduce an expression to its normal form, performing beta reduction
+///
+/// `normalize` does not type-check the expression.  You may want to type-check
+/// expressions before normalizing them since normalization can convert an
+/// ill-typed expression into a well-typed expression.
+///
+/// However, `normalize` will not fail if the expression is ill-typed and will
+/// leave ill-typed sub-expressions unevaluated.
+///
+pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
+    where S: Clone + fmt::Debug,
+          T: Clone + fmt::Debug,
+          A: Clone + fmt::Debug,
+{
+    use crate::BuiltinValue::*;
+    use crate::Expr::*;
+    match *e {
+        Const(k) => Const(k),
+        Var(v) => Var(v),
+        Lam(x, ref tA, ref b) => {
+            let tA2 = normalize(tA);
+            let b2  = normalize(b);
+            Lam(x, bx(tA2), bx(b2))
+        }
+        Pi(x, ref tA, ref tB) => {
+            let tA2 = normalize(tA);
+            let tB2 = normalize(tB);
+            pi(x, tA2, tB2)
+        }
+        App(ref f, ref a) => match normalize::<S, T, A>(f) {
+            Lam(x, _A, b) => { // Beta reduce
+                let vx0 = V(x, 0);
+                let a2 = shift::<S, S, A>( 1, vx0, a);
+                let b2 = subst::<S, T, A>(vx0, &a2, &b);
+                let b3 = shift::<S, T, A>(-1, vx0, &b2);
+                normalize(&b3)
+            }
+            f2 => match (f2, normalize::<S, T, A>(a)) {
+                // fold/build fusion for `List`
+                (App(box BuiltinValue(ListBuild), _), App(box App(box BuiltinValue(ListFold), _), box e2)) |
+                (App(box BuiltinValue(ListFold), _), App(box App(box BuiltinValue(ListBuild), _), box e2)) |
+
+                // fold/build fusion for `Natural`
+                (BuiltinValue(NaturalBuild), App(box BuiltinValue(NaturalFold), box e2)) |
+                (BuiltinValue(NaturalFold), App(box BuiltinValue(NaturalBuild), box e2)) => normalize(&e2),
+
+            /*
+                App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->
+                    normalize (go n0)
+                  where
+                    go !0 = zero
+                    go !n = App succ' (go (n - 1))
+                App NaturalBuild k
+                    | check     -> NaturalLit n
+                    | otherwise -> App f' a'
+                  where
+                    labeled =
+                        normalize (App (App (App k Natural) "Succ") "Zero")
+
+                    n = go 0 labeled
+                      where
+                        go !m (App (Var "Succ") e') = go (m + 1) e'
+                        go !m (Var "Zero")          = m
+                        go !_  _                    = internalError text
+                    check = go labeled
+                      where
+                        go (App (Var "Succ") e') = go e'
+                        go (Var "Zero")          = True
+                        go  _                    = False
+                        */
+                (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
+                (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
+                (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
+                (BuiltinValue(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
+                (App(f@box BuiltinValue(ListBuild), box t), k) => {
+                        let labeled =
+                            normalize::<_, T, _>(&app(app(app(k.clone(), app(
+                                BuiltinType(self::BuiltinType::List), t.clone())), "Cons"), "Nil"));
+
+                        fn list_to_vector<'i, S, A>(v: &mut Vec<Expr<'i, S, A>>, e: Expr<'i, S, A>)
+                            where S: Clone, A: Clone
+                        {
+                            match e {
+                                App(box App(box Var(V("Cons", _)), box x), box e2) => {
+                                    v.push(x);
+                                    list_to_vector(v, e2)
+                                }
+                                Var(V("Nil", _)) => {}
+                                _ => panic!("internalError list_to_vector"),
+                            }
+                        }
+                        fn check<S, A>(e: &Expr<S, A>) -> bool {
+                            match *e {
+                                App(box App(box Var(V("Cons", _)), _), ref e2) => check(e2),
+                                Var(V("Nil", _)) => true,
+                                _ => false,
+                            }
+                        }
+
+                        if check(&labeled) {
+                            let mut v = vec![];
+                            list_to_vector(&mut v, labeled);
+                            ListLit(bx(t), v)
+                        } else {
+                            app(App(f, bx(t)), k)
+                        }
+                    }
+                (App(box App(box App(box App(box BuiltinValue(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
+                    let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr
+                        App(bx(App(cons.clone(), bx(y))), bx(ys))
+                    );
+                    normalize(&e2)
+                }
+                (App(f, x_), ListLit(t, ys)) => match *f {
+                    BuiltinValue(ListLength) =>
+                        NaturalLit(ys.len()),
+                    BuiltinValue(ListHead) =>
+                        normalize(&OptionalLit(t, ys.into_iter().take(1).collect())),
+                    BuiltinValue(ListLast) =>
+                        normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())),
+                    BuiltinValue(ListReverse) => {
+                        let mut xs = ys;
+                        xs.reverse();
+                        normalize(&ListLit(t, xs))
+                    }
+                    _ => app(App(f, x_), ListLit(t, ys)),
+                },
+                /*
+                App (App ListIndexed _) (ListLit t xs) ->
+                    normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))
+                  where
+                    t' = Record (Data.Map.fromList kts)
+                      where
+                        kts = [ ("index", Natural)
+                              , ("value", t)
+                              ]
+                    adapt (n, x) = RecordLit (Data.Map.fromList kvs)
+                      where
+                        kvs = [ ("index", NaturalLit (fromIntegral n))
+                              , ("value", x)
+                              ]
+                App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->
+                    normalize (maybe nothing just' (toMaybe xs))
+                  where
+                    just' y = App just y
+                    toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList
+            */
+                (f2, a2) => app(f2, a2),
+            }
+        },
+        Let(f, _, ref r, ref b) => {
+            let r2 = shift::<_, S, _>( 1, V(f, 0), r);
+            let b2 = subst(V(f, 0), &r2, b);
+            let b3 = shift::<_, T, _>(-1, V(f, 0), &b2);
+            normalize(&b3)
+        }
+        Annot(ref x, _) => normalize(x),
+        BuiltinType(t) => BuiltinType(t),
+        BuiltinValue(v) => BuiltinValue(v),
+        BoolLit(b) => BoolLit(b),
+        BoolAnd(ref x, ref y) => {
+            with_binop(BoolAnd, Expr::bool_lit,
+                       |xn, yn| BoolLit(xn && yn),
+                       normalize(x), normalize(y))
+        }
+        BoolOr(ref x, ref y) => {
+            with_binop(BoolOr, Expr::bool_lit,
+                       |xn, yn| BoolLit(xn || yn),
+                       normalize(x), normalize(y))
+        }
+        BoolEQ(ref x, ref y) => {
+            with_binop(BoolEQ, Expr::bool_lit,
+                       |xn, yn| BoolLit(xn == yn),
+                       normalize(x), normalize(y))
+        }
+        BoolNE(ref x, ref y) => {
+            with_binop(BoolNE, Expr::bool_lit,
+                       |xn, yn| BoolLit(xn != yn),
+                       normalize(x), normalize(y))
+        }
+        BoolIf(ref b, ref t, ref f) => match normalize(b) {
+            BoolLit(true) => normalize(t),
+            BoolLit(false) => normalize(f),
+            b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))),
+        },
+        NaturalLit(n) => NaturalLit(n),
+        NaturalPlus(ref x, ref y) => {
+            with_binop(NaturalPlus, Expr::natural_lit,
+                       |xn, yn| NaturalLit(xn + yn),
+                       normalize(x), normalize(y))
+        }
+        NaturalTimes(ref x, ref y) => {
+            with_binop(NaturalTimes, Expr::natural_lit,
+                       |xn, yn| NaturalLit(xn * yn),
+                       normalize(x), normalize(y))
+        }
+        IntegerLit(n) => IntegerLit(n),
+        DoubleLit(n) => DoubleLit(n),
+        TextLit(ref t) => TextLit(t.clone()),
+        TextAppend(ref x, ref y) => {
+            with_binop(TextAppend, Expr::text_lit,
+                       |xt, yt| TextLit(xt + &yt),
+                       normalize(x), normalize(y))
+        }
+        ListLit(ref t, ref es) => {
+            let t2  = normalize(t);
+            let es2 = es.iter().map(normalize).collect();
+            ListLit(bx(t2), es2)
+        }
+        OptionalLit(ref t, ref es) => {
+            let t2  = normalize(t);
+            let es2 = es.iter().map(normalize).collect();
+            OptionalLit(bx(t2), es2)
+        }
+        Record(ref kts) => Record(map_record_value(kts, normalize)),
+        RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)),
+        Union(ref kts) => Union(map_record_value(kts, normalize)),
+        UnionLit(k, ref v, ref kvs) => UnionLit(k, bx(normalize(v)), map_record_value(kvs, normalize)),
+        Combine(ref _x0, ref _y0) => unimplemented!(),
+        Merge(ref _x, ref _y, ref _t) => unimplemented!(),
+        Field(ref r, x) => match normalize(r) {
+            RecordLit(kvs) => match kvs.get(x) {
+                Some(r2) => normalize(r2),
+                None => Field(bx(RecordLit(map_record_value(&kvs, normalize))), x),
+            },
+            r2 => Field(bx(r2), x),
+        },
+        Note(_, ref e) => normalize(e),
+        Embed(ref a) => Embed(a.clone()),
+    }
+}
+
+fn with_binop<T, U, Get, Set, Op>(op: Op, get: Get, set: Set, x: T, y: T) -> T
+    where Get: Fn(&T) -> Option<U>,
+          Set: FnOnce(U, U) -> T,
+          Op: FnOnce(Box<T>, Box<T>) -> T,
+{
+    if let (Some(xv), Some(yv)) = (get(&x), get(&y)) {
+        set(xv, yv)
+    } else {
+        op(bx(x), bx(y))
+    }
+}
diff --git a/dhall/src/dhall.pest.visibility b/dhall/src/dhall.pest.visibility
new file mode 100644
index 0000000..c09fccf
--- /dev/null
+++ b/dhall/src/dhall.pest.visibility
@@ -0,0 +1,188 @@
+# end_of_line
+# tab
+# block_comment
+# block_comment_chunk
+# block_comment_continue
+# not_end_of_line
+# line_comment
+# whitespace_chunk
+# whitespace
+# nonempty_whitespace
+# ALPHA
+# DIGIT
+# HEXDIG
+# simple_label
+# quoted_label
+# label
+# double_quote_chunk
+# double_quote_literal
+# single_quote_continue
+# single_quote_literal
+# text_literal
+# if_raw
+# then_raw
+# else_raw
+# let_raw
+# in_raw
+# as_raw
+# using_raw
+# merge_raw
+# missing_raw
+# Some_raw
+# constructors_raw
+# Natural_fold_raw
+# Natural_build_raw
+# Natural_isZero_raw
+# Natural_even_raw
+# Natural_odd_raw
+# Natural_toInteger_raw
+# Natural_show_raw
+# Integer_toDouble_raw
+# Integer_show_raw
+# Double_show_raw
+# List_build_raw
+# List_fold_raw
+# List_length_raw
+# List_head_raw
+# List_last_raw
+# List_indexed_raw
+# List_reverse_raw
+# Optional_fold_raw
+# Optional_build_raw
+# Text_show_raw
+# Bool_raw
+# Optional_raw
+# None_raw
+# Natural_raw
+# Integer_raw
+# Double_raw
+# Text_raw
+# List_raw
+# True_raw
+# False_raw
+# NaN_raw
+# Infinity_raw
+# Type_raw
+# Kind_raw
+# Sort_raw
+# reserved_raw
+# reserved_namespaced_raw
+# reserved
+# reserved_namespaced
+# if_
+# then_
+# else_
+# let_
+# in_
+# as_
+# using
+# merge
+# constructors
+# Some
+# Optional
+# Text
+# List
+# equal
+# or
+# plus
+# text_append
+# list_append
+# and
+# times
+# double_equal
+# not_equal
+# dot
+# open_brace
+# close_brace
+# open_bracket
+# close_bracket
+# open_angle
+# close_angle
+# bar
+# comma
+# open_parens
+# close_parens
+# at
+# colon
+# import_alt
+# combine
+# combine_types
+# prefer
+# lambda
+# forall
+# arrow
+# exponent
+# double_literal
+# natural_literal_raw
+integer_literal
+natural_literal
+# identifier
+# identifier_reserved_prefix
+# identifier_reserved_namespaced_prefix
+# missing
+# path_character
+# quoted_path_character
+# path_component
+# directory
+# file
+# local_raw
+# local
+# scheme
+# http_raw
+# authority
+# userinfo
+# host
+# port
+# IP_literal
+# IPvFuture
+# IPv6address
+# h16
+# ls32
+# IPv4address
+# dec_octet
+# reg_name
+# pchar
+# query
+# fragment
+# pct_encoded
+# unreserved
+# sub_delims
+# http
+# env
+# bash_environment_variable
+# posix_environment_variable
+# posix_environment_variable_character
+# import_type
+# hash
+# import_hashed
+# import
+# expression
+# annotated_expression
+# empty_collection
+# non_empty_optional
+# operator_expression
+# import_alt_expression
+# or_expression
+plus_expression
+# text_append_expression
+# list_append_expression
+# and_expression
+# combine_expression
+# prefer_expression
+# combine_types_expression
+times_expression
+# equal_expression
+# not_equal_expression
+# application_expression
+# import_expression
+# selector_expression
+# primitive_expression
+# labels
+# record_type_or_literal
+# non_empty_record_type_or_literal
+# non_empty_record_type
+# non_empty_record_literal
+# union_type_or_literal
+# non_empty_union_type_or_literal
+# non_empty_list_literal
+# complete_expression
diff --git a/dhall/src/errors/AnnotMismatch.txt b/dhall/src/errors/AnnotMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/dhall/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/dhall/src/errors/CantTextAppend.txt b/dhall/src/errors/CantTextAppend.txt
new file mode 100644
index 0000000..26b9ceb
--- /dev/null
+++ b/dhall/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/dhall/src/errors/DuplicateAlternative.txt b/dhall/src/errors/DuplicateAlternative.txt
new file mode 100644
index 0000000..077f8aa
--- /dev/null
+++ b/dhall/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/dhall/src/errors/FieldCollision.txt b/dhall/src/errors/FieldCollision.txt
new file mode 100644
index 0000000..2b2d260
--- /dev/null
+++ b/dhall/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/dhall/src/errors/HandlerInputTypeMismatch.txt b/dhall/src/errors/HandlerInputTypeMismatch.txt
new file mode 100644
index 0000000..7d3525b
--- /dev/null
+++ b/dhall/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/dhall/src/errors/HandlerNotAFunction.txt b/dhall/src/errors/HandlerNotAFunction.txt
new file mode 100644
index 0000000..ff87443
--- /dev/null
+++ b/dhall/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/dhall/src/errors/HandlerOutputTypeMismatch.txt b/dhall/src/errors/HandlerOutputTypeMismatch.txt
new file mode 100644
index 0000000..f359459
--- /dev/null
+++ b/dhall/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/dhall/src/errors/IfBranchMismatch.txt b/dhall/src/errors/IfBranchMismatch.txt
new file mode 100644
index 0000000..a95b130
--- /dev/null
+++ b/dhall/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/dhall/src/errors/IfBranchMustBeTerm.txt b/dhall/src/errors/IfBranchMustBeTerm.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidAlterantive.txt b/dhall/src/errors/InvalidAlterantive.txt
new file mode 100644
index 0000000..391fc3a
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidAlterantiveType.txt b/dhall/src/errors/InvalidAlterantiveType.txt
new file mode 100644
index 0000000..f5dadef
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidField.txt b/dhall/src/errors/InvalidField.txt
new file mode 100644
index 0000000..bfbf106
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidFieldType.txt b/dhall/src/errors/InvalidFieldType.txt
new file mode 100644
index 0000000..4f76a64
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidInputType.txt b/dhall/src/errors/InvalidInputType.txt
new file mode 100644
index 0000000..eabafa4
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidListElement.txt b/dhall/src/errors/InvalidListElement.txt
new file mode 100644
index 0000000..59db7b7
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidListType.txt b/dhall/src/errors/InvalidListType.txt
new file mode 100644
index 0000000..676647e
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidOptionType.txt b/dhall/src/errors/InvalidOptionType.txt
new file mode 100644
index 0000000..3bc81de
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidOptionalElement.txt b/dhall/src/errors/InvalidOptionalElement.txt
new file mode 100644
index 0000000..0254220
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidOptionalLiteral.txt b/dhall/src/errors/InvalidOptionalLiteral.txt
new file mode 100644
index 0000000..41c0fdc
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidOutputType.txt b/dhall/src/errors/InvalidOutputType.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/dhall/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/dhall/src/errors/InvalidPredicate.txt b/dhall/src/errors/InvalidPredicate.txt
new file mode 100644
index 0000000..4c15881
--- /dev/null
+++ b/dhall/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/dhall/src/errors/MissingField.txt b/dhall/src/errors/MissingField.txt
new file mode 100644
index 0000000..de14a33
--- /dev/null
+++ b/dhall/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/dhall/src/errors/MissingHandler.txt b/dhall/src/errors/MissingHandler.txt
new file mode 100644
index 0000000..433445e
--- /dev/null
+++ b/dhall/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/dhall/src/errors/MustCombineARecord.txt b/dhall/src/errors/MustCombineARecord.txt
new file mode 100644
index 0000000..141b969
--- /dev/null
+++ b/dhall/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/dhall/src/errors/MustMergeARecord.txt b/dhall/src/errors/MustMergeARecord.txt
new file mode 100644
index 0000000..79094bd
--- /dev/null
+++ b/dhall/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/dhall/src/errors/MustMergeUnion.txt b/dhall/src/errors/MustMergeUnion.txt
new file mode 100644
index 0000000..68df70c
--- /dev/null
+++ b/dhall/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/dhall/src/errors/NoDependentLet.txt b/dhall/src/errors/NoDependentLet.txt
new file mode 100644
index 0000000..fdc65b4
--- /dev/null
+++ b/dhall/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/dhall/src/errors/NoDependentTypes.txt b/dhall/src/errors/NoDependentTypes.txt
new file mode 100644
index 0000000..435bdcb
--- /dev/null
+++ b/dhall/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/dhall/src/errors/NotAFunction.txt b/dhall/src/errors/NotAFunction.txt
new file mode 100644
index 0000000..dd2695d
--- /dev/null
+++ b/dhall/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/dhall/src/errors/NotARecord.txt b/dhall/src/errors/NotARecord.txt
new file mode 100644
index 0000000..e0eebc8
--- /dev/null
+++ b/dhall/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/dhall/src/errors/TypeMismatch.txt b/dhall/src/errors/TypeMismatch.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/dhall/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/dhall/src/errors/UnboundVariable.txt b/dhall/src/errors/UnboundVariable.txt
new file mode 100644
index 0000000..bd7d483
--- /dev/null
+++ b/dhall/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/dhall/src/errors/Untyped.txt b/dhall/src/errors/Untyped.txt
new file mode 100644
index 0000000..4904bf8
--- /dev/null
+++ b/dhall/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/dhall/src/errors/UnusedHandler.txt b/dhall/src/errors/UnusedHandler.txt
new file mode 100644
index 0000000..2e46a12
--- /dev/null
+++ b/dhall/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/dhall/src/generated_parser.rs b/dhall/src/generated_parser.rs
new file mode 100644
index 0000000..452b4cd
--- /dev/null
+++ b/dhall/src/generated_parser.rs
@@ -0,0 +1,6 @@
+#[allow(unused_imports)]
+use pest_derive::*;
+
+#[derive(Parser)]
+#[grammar = "dhall.pest"]
+pub struct DhallParser;
diff --git a/dhall/src/grammar.lalrpop b/dhall/src/grammar.lalrpop
new file mode 100644
index 0000000..150961f
--- /dev/null
+++ b/dhall/src/grammar.lalrpop
@@ -0,0 +1,162 @@
+use std::collections::BTreeMap;
+use std::iter;
+use std::iter::FromIterator;
+
+use crate::core;
+use crate::core::bx;
+use crate::core::Expr::*;
+use crate::core::BuiltinType::*;
+use crate::grammar_util::*;
+use crate::lexer::*;
+
+grammar<'input>;
+
+extern {
+    type Location = usize;
+    type Error = LexicalError;
+
+    enum Tok<'input> {
+        Pi => Tok::Pi,
+        Lambda => Tok::Lambda,
+        Combine => Tok::Combine,
+        "->" => Tok::Arrow,
+
+        Int => Tok::Integer(<isize>),
+        Nat => Tok::Natural(<usize>),
+        Text => Tok::Text(<String>),
+        Bool => Tok::Bool(<bool>),
+        Label => Tok::Identifier(<&'input str>),
+        Const => Tok::Const(<core::Const>),
+        Let => Tok::Keyword(Keyword::Let),
+        In => Tok::Keyword(Keyword::In),
+        If => Tok::Keyword(Keyword::If),
+        Then => Tok::Keyword(Keyword::Then),
+        Else => Tok::Keyword(Keyword::Else),
+        List => Tok::ListLike(ListLike::List),
+        Optional => Tok::ListLike(ListLike::Optional),
+        Builtin => Tok::Builtin(<Builtin>),
+
+        "{" => Tok::BraceL,
+        "}" => Tok::BraceR,
+        "[" => Tok::BracketL,
+        "]" => Tok::BracketR,
+        "(" => Tok::ParenL,
+        ")" => Tok::ParenR,
+        "&&" => Tok::BoolAnd,
+        "||" => Tok::BoolOr,
+        "==" => Tok::CompareEQ,
+        "!=" => Tok::CompareNE,
+        "++" => Tok::Append,
+        "*" => Tok::Times,
+        "+" => Tok::Plus,
+        "," => Tok::Comma,
+        "." => Tok::Dot,
+        ":" => Tok::Ascription,
+        "=" => Tok::Equals,
+    }
+}
+
+pub Expr: BoxExpr<'input> = { // exprA
+    <ExprB> ":" <Expr> => bx(Annot(<>)),
+    ExprB,
+};
+
+ExprB: BoxExpr<'input> = {
+    Lambda "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Lam(<>)),
+    Pi "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Pi(<>)),
+    If <Expr> Then <ExprB> Else <ExprC> => bx(BoolIf(<>)),
+    <ExprC> "->" <ExprB> => bx(Pi("_", <>)),
+    Let <Label> <(":" <Expr>)?> "=" <Expr> In <ExprB> => bx(Let(<>)),
+    "[" <a:Elems> "]" ":" <b:ListLike> <c:ExprE> => bx(b(c, a)),
+    ExprC,
+};
+
+ListLike: ExprListFn<'input> = {
+    List => ListLit,
+    Optional => OptionalLit,
+};
+
+BoolOr: ExprOpFn<'input> = { "||" => BoolOr };
+NaturalPlus: ExprOpFn<'input> = { "+" => NaturalPlus };
+TextAppend: ExprOpFn<'input> = { "++" => TextAppend };
+BoolAnd: ExprOpFn<'input> = { "&&" => BoolAnd };
+CombineOp: ExprOpFn<'input> = { Combine => Combine };
+NaturalTimes: ExprOpFn<'input> = { "*" => NaturalTimes };
+BoolEQ: ExprOpFn<'input> = { "==" => BoolEQ };
+BoolNE: ExprOpFn<'input> = { "!=" => BoolNE };
+
+Tier<NextTier, Op>: BoxExpr<'input> = {
+    <a:NextTier> <f:Op> <b:Tier<NextTier, Op>> => bx(f(a, b)),
+    // <b:Tier<NextTier, Op>> <f:Op> <a:NextTier> => bx(f(a, b)),
+    NextTier,
+};
+
+ExprC = Tier<ExprC1, BoolOr>;
+ExprC1 = Tier<ExprC2, NaturalPlus>;
+ExprC2 = Tier<ExprC3, TextAppend>;
+ExprC3 = Tier<ExprC4, BoolAnd>;
+ExprC4 = Tier<ExprC5, CombineOp>;
+ExprC5 = Tier<ExprC6, NaturalTimes>;
+ExprC6 = Tier<ExprC7, BoolEQ>;
+ExprC7 = Tier<ExprD, BoolNE>;
+
+ExprD: BoxExpr<'input> = {
+    <v:(ExprE)+> => {
+        let mut it = v.into_iter();
+        let f = it.next().unwrap();
+        it.fold(f, |f, x| bx(App(f, x)))
+    }
+};
+
+ExprE: BoxExpr<'input> = {
+    <a:ExprF> <fields:("." <Label>)*> => {
+        fields.into_iter().fold(a, |x, f| bx(Field(x, f)))
+    },
+};
+
+ExprF: BoxExpr<'input> = {
+    Nat => bx(NaturalLit(<>)),
+    Int => bx(IntegerLit(<>)),
+    Text => bx(TextLit(<>)),
+    Label => bx(Var(core::V(<>, 0))), // FIXME support var@n syntax
+    Const => bx(Const(<>)),
+    List => bx(BuiltinType(List)),
+    Optional => bx(BuiltinType(Optional)),
+    Builtin => bx(builtin_expr(<>)),
+    Bool => bx(BoolLit(<>)),
+    Record,
+    RecordLit,
+    "(" <Expr> ")",
+};
+
+SepBy<S, T>: iter::Chain<::std::vec::IntoIter<T>, ::std::option::IntoIter<T>> = {
+    <v:(<T> S)*> <last:T?> => v.into_iter().chain(last.into_iter()),
+};
+
+SepBy1<S, T>: iter::Chain<::std::vec::IntoIter<T>, iter::Once<T>> = {
+    <v:(<T> S)*> <last:T> => v.into_iter().chain(iter::once(last)),
+};
+
+Elems: Vec<ParsedExpr<'input>> = {
+    <v:SepBy<",", Expr>> => {
+        v.into_iter()
+         .map(|b| *b)
+         .collect::<Vec<_>>()
+    }
+};
+
+RecordLit: BoxExpr<'input> = {
+    "{" "=" "}" => bx(RecordLit(BTreeMap::new())),
+    "{" <FieldValues> "}" => bx(RecordLit(BTreeMap::from_iter(<>))),
+};
+
+Record: BoxExpr<'input> = {
+    "{" <FieldTypes> "}" => bx(Record(BTreeMap::from_iter(<>))),
+};
+
+FieldValues = SepBy1<",", Field<"=">>;
+FieldTypes = SepBy<",", Field<":">>;
+
+Field<Sep>: (&'input str, ParsedExpr<'input>) = {
+    <a:Label> Sep <b:Expr> => (a, *b),
+};
diff --git a/dhall/src/grammar_util.rs b/dhall/src/grammar_util.rs
new file mode 100644
index 0000000..c546a13
--- /dev/null
+++ b/dhall/src/grammar_util.rs
@@ -0,0 +1,14 @@
+use crate::core::{Expr, X};
+use crate::lexer::Builtin;
+
+pub type ParsedExpr<'i> = Expr<'i, X, X>; // FIXME Parse paths and replace the second X with Path
+pub type BoxExpr<'i> = Box<ParsedExpr<'i>>;
+pub type ExprOpFn<'i> = fn(BoxExpr<'i>, BoxExpr<'i>) -> ParsedExpr<'i>;
+pub type ExprListFn<'i> = fn(BoxExpr<'i>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
+
+pub fn builtin_expr<'i, S, A>(b: Builtin) -> Expr<'i, S, A> {
+    match b {
+        Builtin::Type(t)  => Expr::BuiltinType(t),
+        Builtin::Value(v) => Expr::BuiltinValue(v),
+    }
+}
diff --git a/dhall/src/lexer.rs b/dhall/src/lexer.rs
new file mode 100644
index 0000000..5b4dcaa
--- /dev/null
+++ b/dhall/src/lexer.rs
@@ -0,0 +1,378 @@
+use nom::*;
+
+use crate::core::Const;
+use crate::core::BuiltinType;
+use crate::core::BuiltinType::*;
+use crate::core::BuiltinValue;
+use crate::core::BuiltinValue::*;
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Keyword {
+    Let,
+    In,
+    If,
+    Then,
+    Else,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum ListLike {
+    List,
+    Optional,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Builtin {
+    Type(BuiltinType),
+    Value(BuiltinValue),
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Tok<'i> {
+    Identifier(&'i str),
+    Keyword(Keyword),
+    Builtin(Builtin),
+    ListLike(ListLike),
+    Const(Const),
+    Bool(bool),
+    Integer(isize),
+    Natural(usize),
+    Text(String),
+
+    // Symbols
+    BraceL,
+    BraceR,
+    BracketL,
+    BracketR,
+    ParenL,
+    ParenR,
+    Arrow,
+    Lambda,
+    Pi,
+    Combine,
+    BoolAnd,
+    BoolOr,
+    CompareEQ,
+    CompareNE,
+    Append,
+    Times,
+    Plus,
+    Comma,
+    Dot,
+    Ascription,
+    Equals,
+}
+
+#[derive(Debug)]
+pub enum LexicalError {
+    Error(usize, nom::simple_errors::Err<u32>),
+    Incomplete(nom::Needed),
+}
+
+pub type Spanned<Tok, Loc, Error> = Result<(Loc, Tok, Loc), Error>;
+
+#[allow(dead_code)]
+fn is_identifier_first_char(c: char) -> bool {
+    c.is_alphabetic() || c == '_'
+}
+
+fn is_identifier_rest_char(c: char) -> bool {
+    is_identifier_first_char(c) || c.is_digit(10) || c == '/'
+}
+
+macro_rules! digits {
+    ($i:expr, $t:tt, $radix:expr) => {{
+        let r: nom::IResult<&str, $t> =
+            map_res!($i, take_while1_s!(call!(|c: char| c.is_digit($radix))),
+                     |s| $t::from_str_radix(s, $radix));
+        r
+    }}
+}
+
+named!(natural<&str, usize>, digits!(usize, 10));
+named!(integral<&str, isize>, digits!(isize, 10));
+named!(integer<&str, isize>, alt!(
+    preceded!(tag!("-"), map!(integral, |i: isize| -i)) |
+    preceded!(tag!("+"), integral)
+));
+named!(boolean<&str, bool>, alt!(
+    value!(true, tag!("True")) |
+    value!(false, tag!("False"))
+));
+
+named!(identifier<&str, &str>, recognize!(preceded!(
+    take_while1_s!(is_identifier_first_char),
+    take_while_s!(is_identifier_rest_char))
+));
+
+/// Parse an identifier, ensuring a whole identifier is parsed and not just a prefix.
+macro_rules! ident_tag {
+    ($i:expr, $tag:expr) => {
+        match identifier($i) {
+            nom::IResult::Done(i, s) => {
+                if s == $tag {
+                    nom::IResult::Done(i, s)
+                } else {
+                    nom::IResult::Error(error_position!(nom::ErrorKind::Tag, $i))
+                }
+            }
+            r => r,
+        }
+    }
+}
+
+fn string_escape_single(c: char) -> Option<&'static str> {
+    match c {
+        'n'  => Some("\n"),
+        'r'  => Some("\r"),
+        't'  => Some("\t"),
+        '"'  => Some("\""),
+        '\'' => Some("'"),
+        '\\' => Some("\\"),
+        '0'  => Some("\0"),
+        'a'  => Some("\x07"),
+        'b'  => Some("\x08"),
+        'f'  => Some("\x0c"),
+        'v'  => Some("\x0b"),
+        '&'  => Some(""),
+        _    => None,
+    }
+}
+
+named!(string_escape_numeric<&str, char>, map_opt!(alt!(
+    preceded!(tag!("x"), digits!(u32, 16)) |
+    preceded!(tag!("o"), digits!(u32, 8)) |
+    digits!(u32, 10)
+), ::std::char::from_u32));
+
+fn string_lit_inner(input: &str) -> nom::IResult<&str, String> {
+    use nom::IResult::*;;
+    use nom::ErrorKind;
+    let mut s = String::new();
+    let mut cs = input.char_indices().peekable();
+    while let Some((i, c)) = cs.next()  {
+        match c {
+            '"' => return nom::IResult::Done(&input[i..], s),
+            '\\' => match cs.next() {
+                Some((_, s)) if s.is_whitespace() => {
+                    while cs.peek().map(|&(_, s)| s.is_whitespace()) == Some(true) {
+                        let _ = cs.next();
+                    }
+                    if cs.next().map(|p| p.1) != Some('\\') {
+                        return Error(error_position!(ErrorKind::Custom(4 /* FIXME */), input));
+                    }
+                }
+                Some((j, ec)) => {
+                    if let Some(esc) = string_escape_single(ec) {
+                        s.push_str(esc);
+                        // FIXME Named ASCII escapes and control character escapes
+                    } else {
+                        match string_escape_numeric(&input[j..]) {
+                            Done(rest, esc) => {
+                                let &(k, _) = cs.peek().unwrap();
+                                // digits are always single byte ASCII characters
+                                let consumed = input[k..].len() - rest.len();
+                                for _ in 0..consumed { let _ = cs.next(); }
+                                s.push(esc);
+                            }
+                            Incomplete(s) => return Incomplete(s),
+                            Error(e) => return Error(e),
+                        }
+                    }
+                },
+                _ => return Error(error_position!(ErrorKind::Custom(5 /* FIXME */), input)),
+            },
+            _ => s.push(c),
+        }
+    }
+    Error(error_position!(ErrorKind::Custom(3 /* FIXME */), input))
+}
+
+named!(string_lit<&str, String>, delimited!(tag!("\""), string_lit_inner, tag!("\"")));
+
+named!(keyword<&str, Keyword>, alt!(
+    value!(Keyword::Let, ident_tag!("let")) |
+    value!(Keyword::In, ident_tag!("in")) |
+    value!(Keyword::If, ident_tag!("if")) |
+    value!(Keyword::Then, ident_tag!("then")) |
+    value!(Keyword::Else, ident_tag!("else"))
+));
+
+named!(type_const<&str, Const>, alt!(
+    value!(Const::Type, ident_tag!("Type")) |
+    value!(Const::Kind, ident_tag!("Kind"))
+));
+
+named!(list_like<&str, ListLike>, alt!(
+    value!(ListLike::List, ident_tag!("List")) |
+    value!(ListLike::Optional, ident_tag!("Optional"))
+));
+
+named!(builtin<&str, Builtin>, alt!(
+    value!(Builtin::Value(NaturalFold), ident_tag!("Natural/fold")) |
+    value!(Builtin::Value(NaturalBuild), ident_tag!("Natural/build")) |
+    value!(Builtin::Value(NaturalIsZero), ident_tag!("Natural/isZero")) |
+    value!(Builtin::Value(NaturalEven), ident_tag!("Natural/even")) |
+    value!(Builtin::Value(NaturalOdd), ident_tag!("Natural/odd")) |
+    value!(Builtin::Value(NaturalShow), ident_tag!("Natural/show")) |
+    value!(Builtin::Type(Natural), ident_tag!("Natural")) |
+    value!(Builtin::Type(Integer), ident_tag!("Integer")) |
+    value!(Builtin::Type(Double), ident_tag!("Double")) |
+    value!(Builtin::Type(Text), ident_tag!("Text")) |
+    value!(Builtin::Value(ListBuild), ident_tag!("List/build")) |
+    value!(Builtin::Value(ListFold), ident_tag!("List/fold")) |
+    value!(Builtin::Value(ListLength), ident_tag!("List/length")) |
+    value!(Builtin::Value(ListHead), ident_tag!("List/head")) |
+    value!(Builtin::Value(ListLast), ident_tag!("List/last")) |
+    value!(Builtin::Value(ListIndexed), ident_tag!("List/indexed")) |
+    value!(Builtin::Value(ListReverse), ident_tag!("List/reverse")) |
+    value!(Builtin::Value(OptionalFold), ident_tag!("Optional/fold")) |
+    value!(Builtin::Type(Bool), ident_tag!("Bool"))
+));
+
+named!(token<&str, Tok>, alt!(
+    value!(Tok::Pi, ident_tag!("forall")) |
+    value!(Tok::Pi, tag!("∀")) |
+    value!(Tok::Lambda, tag!("\\")) |
+    value!(Tok::Lambda, tag!("λ")) |
+    value!(Tok::Combine, tag!("/\\")) |
+    value!(Tok::Combine, tag!("∧")) |
+    value!(Tok::Arrow, tag!("->")) |
+    value!(Tok::Arrow, tag!("→")) |
+
+    map!(type_const, Tok::Const) |
+    map!(boolean, Tok::Bool) |
+    map!(keyword, Tok::Keyword) |
+    map!(builtin, Tok::Builtin) |
+    map!(list_like, Tok::ListLike) |
+    map!(natural, Tok::Natural) |
+    map!(integer, Tok::Integer) |
+    map!(identifier, Tok::Identifier) |
+    map!(string_lit, Tok::Text) |
+
+    value!(Tok::BraceL, tag!("{")) |
+    value!(Tok::BraceR, tag!("}")) |
+    value!(Tok::BracketL, tag!("[")) |
+    value!(Tok::BracketR, tag!("]")) |
+    value!(Tok::ParenL, tag!("(")) |
+    value!(Tok::ParenR, tag!(")")) |
+    value!(Tok::BoolAnd, tag!("&&")) |
+    value!(Tok::BoolOr, tag!("||")) |
+    value!(Tok::CompareEQ, tag!("==")) |
+    value!(Tok::CompareNE, tag!("!=")) |
+    value!(Tok::Append, tag!("++")) |
+    value!(Tok::Times, tag!("*")) |
+    value!(Tok::Plus, tag!("+")) |
+    value!(Tok::Comma, tag!(",")) |
+    value!(Tok::Dot, tag!(".")) |
+    value!(Tok::Ascription, tag!(":")) |
+    value!(Tok::Equals, tag!("="))
+));
+
+fn find_end(input: &str, ending: &str) -> Option<usize> {
+    input.find(ending).map(|i| i + ending.len())
+}
+
+pub struct Lexer<'input> {
+    input: &'input str,
+    offset: usize,
+}
+
+impl<'input> Lexer<'input> {
+    pub fn new(input: &'input str) -> Self {
+        Lexer {
+            input: input,
+            offset: 0,
+        }
+    }
+
+    fn current_input(&mut self) -> &'input str {
+        &self.input[self.offset..]
+    }
+
+    fn skip_whitespace(&mut self) -> bool {
+        let input = self.current_input();
+        let trimmed = input.trim_start();
+        let whitespace_len = input.len() - trimmed.len();
+        let skipped = whitespace_len > 0;
+        if skipped {
+            // println!("skipped {} whitespace bytes in {}..{}", whitespace_len, self.offset, self.offset + whitespace_len);
+            self.offset += whitespace_len;
+        }
+        skipped
+    }
+
+    fn skip_comments(&mut self) -> bool {
+        let input = self.current_input();
+        if !input.is_char_boundary(0) || !input.is_char_boundary(2) {
+            return false;
+        }
+        let skip = match &input[0..2] {
+            "{-" => find_end(input, "-}"),
+            "--" => find_end(input, "\n"), // Also skips past \r\n (CRLF)
+            _ => None,
+        }.unwrap_or(0);
+        // println!("skipped {} bytes of comment", skip);
+        self.offset += skip;
+        skip != 0
+    }
+
+    fn skip_comments_and_whitespace(&mut self) {
+        while self.skip_whitespace() || self.skip_comments() {}
+    }
+}
+
+impl<'input> Iterator for Lexer<'input> {
+    type Item = Spanned<Tok<'input>, usize, LexicalError>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        use nom::IResult::*;
+        self.skip_comments_and_whitespace();
+        let input = self.current_input();
+        if input.is_empty() {
+            return None;
+        }
+        match token(input) {
+            Done(rest, t) => {
+                let parsed_len = input.len() - rest.len();
+                //println!("parsed {} bytes => {:?}", parsed_len, t);
+                let start = self.offset;
+                self.offset += parsed_len;
+                Some(Ok((start, t, self.offset)))
+            }
+            Error(e) => {
+                let offset = self.offset;
+                self.offset = self.input.len();
+                Some(Err(LexicalError::Error(offset, e)))
+            }
+            Incomplete(needed) => {
+                Some(Err(LexicalError::Incomplete(needed)))
+            }
+        }
+    }
+}
+
+#[test]
+fn test_lex() {
+    use self::Tok::*;
+    let s = "λ(b : Bool) → b == False";
+    let expected = [Lambda,
+                    ParenL,
+                    Identifier("b"),
+                    Ascription,
+                    Builtin(self::Builtin::Type(crate::core::BuiltinType::Bool)),
+                    ParenR,
+                    Arrow,
+                    Identifier("b"),
+                    CompareEQ,
+                    Bool(false)];
+    let lexer = Lexer::new(s);
+    let tokens = lexer.map(|r| r.unwrap().1).collect::<Vec<_>>();
+    assert_eq!(&tokens, &expected);
+
+    assert_eq!(string_lit(r#""a\&b""#).to_result(), Ok("ab".to_owned()));
+    assert_eq!(string_lit(r#""a\     \b""#).to_result(), Ok("ab".to_owned()));
+    assert!(string_lit(r#""a\     b""#).is_err());
+    assert_eq!(string_lit(r#""a\nb""#).to_result(), Ok("a\nb".to_owned()));
+    assert_eq!(string_lit(r#""\o141\x62\99""#).to_result(), Ok("abc".to_owned()));
+}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
new file mode 100644
index 0000000..e07071d
--- /dev/null
+++ b/dhall/src/lib.rs
@@ -0,0 +1,12 @@
+#![feature(box_patterns)]
+
+pub mod context;
+mod core;
+pub use crate::core::*;
+use lalrpop_util::lalrpop_mod;
+lalrpop_mod!(pub grammar); // synthesized by LALRPOP
+mod grammar_util;
+mod generated_parser;
+pub mod lexer;
+pub mod parser;
+pub mod typecheck;
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
new file mode 100644
index 0000000..cdab3c0
--- /dev/null
+++ b/dhall/src/main.rs
@@ -0,0 +1,101 @@
+use std::io::{self, Read};
+use std::error::Error;
+use term_painter::ToStyle;
+
+use dhall::*;
+
+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(), b'\n');
+    let line_start = source[..start].rfind('\n').map(|i| i + 1).unwrap_or(0);
+    let line_end = source[end..].find('\n').unwrap_or(0) + end;
+    let context_prefix = &source[line_start..start];
+    let context_highlighted = &source[start..end];
+    let context_suffix = &source[end..line_end];
+
+    let line_number_str = line_number.to_string();
+    let line_number_width = line_number_str.len();
+
+    BOLD.with(|| {
+        ERROR_STYLE.with(|| {
+            print!("error: ");
+        });
+        println!("{}", message);
+    });
+    BOLD.with(|| {
+        print!("  -->");
+    });
+    println!(" {}:{}:0", "(stdin)", line_number);
+    BOLD.with(|| {
+        println!("{:w$} |", "", w = line_number_width);
+        print!("{} |", line_number_str);
+    });
+    print!(" {}", context_prefix);
+    BOLD.with(|| {
+        ERROR_STYLE.with(|| {
+            print!("{}", context_highlighted);
+        });
+    });
+    println!("{}", context_suffix);
+    BOLD.with(|| {
+        print!("{:w$} |", "", w = line_number_width);
+        ERROR_STYLE.with(|| {
+            println!(" {:so$}{:^>ew$}", "", "",
+                     so = source[line_start..start].chars().count(),
+                     ew = ::std::cmp::max(1, source[start..end].chars().count()));
+        });
+    });
+}
+
+fn main() {
+    let mut buffer = String::new();
+    io::stdin().read_to_string(&mut buffer).unwrap();
+    let expr = match parser::parse_expr(&buffer) {
+        Ok(e) => e,
+        Err(lalrpop_util::ParseError::User { error: lexer::LexicalError::Error(pos, e) }) => {
+            print_error(&format!("Unexpected token {:?}", e), &buffer, pos, pos);
+            return;
+        }
+        Err(lalrpop_util::ParseError::UnrecognizedToken { token: Some((start, t, end)), expected: e }) => {
+            print_error(&format!("Unrecognized token {:?}", t), &buffer, start, end);
+            if !e.is_empty() {
+                println!("Expected {:?}", e);
+            }
+            return;
+        }
+        Err(e) => {
+            print_error(&format!("Parser error {:?}", e), &buffer, 0, 0);
+            return;
+        }
+    };
+
+    /*
+    expr' <- load expr
+    */
+
+    let type_expr = match typecheck::type_of(&expr) {
+        Err(e) => {
+            let explain = ::std::env::args().any(|s| s == "--explain");
+            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));
+}
diff --git a/dhall/src/parser.rs b/dhall/src/parser.rs
new file mode 100644
index 0000000..057fce2
--- /dev/null
+++ b/dhall/src/parser.rs
@@ -0,0 +1,91 @@
+use lalrpop_util;
+
+use crate::grammar;
+use crate::grammar_util::BoxExpr;
+use crate::lexer::{Lexer, LexicalError, Tok};
+use crate::core::{bx, Expr};
+
+pub type ParseError<'i> = lalrpop_util::ParseError<usize, Tok<'i>, LexicalError>;
+
+pub fn parse_expr(s: &str) -> Result<BoxExpr, ParseError>  {
+    grammar::ExprParser::new().parse(Lexer::new(s))
+}
+
+use pest::Parser;
+use pest::error::Error;
+use pest::iterators::Pair;
+use crate::generated_parser::{DhallParser, Rule};
+
+fn debug_pair(pair: Pair<Rule>) {
+    fn aux(indent: usize, pair: Pair<Rule>) {
+        let indent_str = "| ".repeat(indent);
+        println!(r#"{}{:?}: "{}""#, indent_str, pair.as_rule(), pair.as_str());
+        for p in pair.into_inner() {
+            aux(indent+1, p);
+        }
+    }
+    aux(0, pair)
+}
+
+pub fn parse_expr_pest(s: &str) -> Result<BoxExpr, Error<Rule>>  {
+    let parsed_expr = DhallParser::parse(Rule::complete_expression, s)?.next().unwrap();
+    debug_pair(parsed_expr.clone());
+    // println!("{}", parsed_expr.clone());
+
+    fn parse_pair(pair: Pair<Rule>) -> BoxExpr {
+        match pair.as_rule() {
+            Rule::natural_literal => bx(Expr::NaturalLit(str::parse(pair.as_str().trim()).unwrap())),
+            Rule::plus_expression => {
+                let mut inner = pair.into_inner().map(parse_pair);
+                let first_expr = inner.next().unwrap();
+                inner.fold(first_expr, |acc, e| bx(Expr::NaturalPlus(acc, e)))
+            }
+            Rule::times_expression => {
+                let mut inner = pair.into_inner().map(parse_pair);
+                let first_expr = inner.next().unwrap();
+                inner.fold(first_expr, |acc, e| bx(Expr::NaturalTimes(acc, e)))
+            }
+            r => panic!("{:?}", r),
+        }
+    }
+
+    Ok(parse_pair(parsed_expr))
+}
+
+
+#[test]
+fn test_parse() {
+    use crate::core::Expr::*;
+    let expr = "((22 + 3) * 10)";
+    println!("{:?}", parse_expr(expr));
+    match parse_expr_pest(expr) {
+        Err(e) => println!("{}", e),
+        ok => println!("{:?}", ok),
+    }
+    assert_eq!(parse_expr_pest(expr).unwrap(), parse_expr(expr).unwrap());
+    assert!(false);
+
+    println!("test {:?}", parse_expr("3 + 5 * 10"));
+    assert!(parse_expr("22").is_ok());
+    assert!(parse_expr("(22)").is_ok());
+    assert_eq!(parse_expr("3 + 5 * 10").ok(),
+               Some(Box::new(NaturalPlus(Box::new(NaturalLit(3)),
+                                Box::new(NaturalTimes(Box::new(NaturalLit(5)),
+                                                      Box::new(NaturalLit(10))))))));
+    // The original parser is apparently right-associative
+    assert_eq!(parse_expr("2 * 3 * 4").ok(),
+               Some(Box::new(NaturalTimes(Box::new(NaturalLit(2)),
+                                 Box::new(NaturalTimes(Box::new(NaturalLit(3)),
+                                                       Box::new(NaturalLit(4))))))));
+    assert!(parse_expr("((((22))))").is_ok());
+    assert!(parse_expr("((22)").is_err());
+    println!("{:?}", parse_expr("\\(b : Bool) -> b == False"));
+    assert!(parse_expr("\\(b : Bool) -> b == False").is_ok());
+    println!("{:?}", parse_expr("foo.bar"));
+    assert!(parse_expr("foo.bar").is_ok());
+    assert!(parse_expr("[] : List Bool").is_ok());
+
+    // println!("{:?}", parse_expr("< Left = True | Right : Natural >"));
+    // println!("{:?}", parse_expr(r#""bl${42}ah""#));
+    // assert!(parse_expr("< Left = True | Right : Natural >").is_ok());
+}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
new file mode 100644
index 0000000..62ff7d2
--- /dev/null
+++ b/dhall/src/typecheck.rs
@@ -0,0 +1,616 @@
+#![allow(non_snake_case)]
+use std::collections::BTreeMap;
+use std::collections::HashSet;
+use std::fmt;
+
+use crate::context::Context;
+use crate::core;
+use crate::core::{Expr, V, X, bx, normalize, shift, subst};
+use crate::core::{pi, app};
+use crate::core::BuiltinType::*;
+use crate::core::BuiltinValue::*;
+use crate::core::Const::*;
+use crate::core::Expr::*;
+
+use self::TypeMessage::*;
+
+fn axiom<'i, S: Clone>(c: core::Const) -> Result<core::Const, TypeError<'i, S>> {
+    match c {
+        Type => Ok(Kind),
+        Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)),
+    }
+}
+
+fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
+    match (a, b) {
+        (Type, Kind) => Err(()),
+        (Kind, Kind) => Ok(Kind),
+        (Type, Type) |
+        (Kind, Type) => Ok(Type),
+    }
+}
+
+fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool {
+    let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1));
+    match (vl, vr, xxs) {
+        (&V(xL, nL), &V(xR, nR), None) => xL == xR && nL == nR,
+        (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _))) if xL == xL2 && xR == xR2 => true,
+        (&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => {
+            let nL2 = if xL == xL2 { nL - 1 } else { nL };
+            let nR2 = if xR == xR2 { nR - 1 } else { nR };
+            match_vars(&V(xL, nL2), &V(xR, nR2), xs)
+        }
+    }
+}
+
+fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
+    where S: Clone + ::std::fmt::Debug,
+          T: Clone + ::std::fmt::Debug
+{
+    fn go<'i, S, T>(ctx: &mut Vec<(&'i str, &'i str)>, el: &'i Expr<'i, S, X>, er: &'i Expr<'i, T, X>) -> bool
+        where S: Clone + ::std::fmt::Debug,
+              T: Clone + ::std::fmt::Debug
+    {
+        match (el, er) {
+            (&Const(Type), &Const(Type)) |
+            (&Const(Kind), &Const(Kind)) => true,
+            (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx),
+            (&Pi(xL, ref tL, ref bL), &Pi(xR, ref tR, ref bR)) => {
+                //ctx <- State.get
+                let eq1 = go(ctx, tL, tR);
+                if eq1 {
+                    //State.put ((xL, xR):ctx)
+                    ctx.push((xL, xR));
+                    let eq2 = go(ctx, bL, bR);
+                    //State.put ctx
+                    let _ = ctx.pop();
+                    eq2
+                } else {
+                    false
+                }
+            }
+            (&App(ref fL, ref aL), &App(ref fR, ref aR)) =>
+                if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false },
+            (&BuiltinType(a), &BuiltinType(b)) => a == b,
+            (&Record(ref ktsL0), &Record(ref ktsR0)) => {
+                if ktsL0.len() != ktsR0.len() {
+                    return false;
+                }
+                /*
+                let go ((kL, tL):ktsL) ((kR, tR):ktsR)
+                        | kL == kR = do
+                            b <- go tL tR
+                            if b
+                                then go ktsL ktsR
+                                else return False
+                    go [] [] = return True
+                    go _  _  = return False
+                */
+                /*
+                for ((kL, tL), (kR, tR)) in ktsL0.iter().zip(ktsR0.iter()) {
+                    if kL == kR {
+                        if !go(ctx, tL, tR) {
+                            return false;
+                        }
+                    } else {
+                        return false;
+                    }
+                }
+                true
+                */
+                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
+                    kL != kR || !go(ctx, tL, tR)
+                })
+            }
+            (&Union(ref ktsL0), &Union(ref ktsR0)) => {
+                if ktsL0.len() != ktsR0.len() {
+                    return false;
+                }
+            /*
+                let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
+                        | kL == kR = do
+                            b <- go tL tR
+                            if b
+                                then loop ktsL ktsR
+                                else return False
+                    loop [] [] = return True
+                    loop _  _  = return False
+                loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)
+            */
+                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
+                    kL != kR || !go(ctx, tL, tR)
+                })
+            }
+            (_, _) => false,
+        }
+    }
+    let mut ctx = vec![];
+    go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
+}
+
+fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
+                       e: &Expr<'i, S, X>,
+                       t: core::BuiltinType,
+                       ef: EF,
+                       l: &Expr<'i, S, X>,
+                       r: &Expr<'i, S, X>)
+                       -> Result<Expr<'i, S, X>, TypeError<'i, S>>
+    where S: Clone + ::std::fmt::Debug + 'i,
+          EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>,
+{
+    let tl = normalize(&type_with(ctx, l)?);
+    match tl {
+        BuiltinType(lt) if lt == t => {}
+        _ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))),
+    }
+
+    let tr = normalize(&type_with(ctx, r)?);
+    match tr {
+        BuiltinType(rt) if rt == t => {}
+        _ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))),
+    }
+
+    Ok(BuiltinType(t))
+}
+
+/// Type-check an expression and return the expression'i type if type-checking
+/// suceeds or an error if type-checking fails
+///
+/// `type_with` does not necessarily normalize the type since full normalization
+/// is not necessary for just type-checking.  If you actually care about the
+/// returned type then you may want to `normalize` it afterwards.
+pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
+                        e: &Expr<'i, S, X>)
+                        -> Result<Expr<'i, S, X>, TypeError<'i, S>>
+    where S: Clone + ::std::fmt::Debug + 'i
+{
+    match *e {
+        Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
+        Var(V(x, n)) => {
+            ctx.lookup(x, n)
+                .cloned()
+                //.map(Cow::Borrowed)
+                .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable))
+        }
+        Lam(x, ref tA, ref b) => {
+            let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
+            let tB = type_with(&ctx2, b)?;
+            let p = Pi(x, tA.clone(), bx(tB));
+            let _ = type_with(ctx, &p)?;
+            //Ok(Cow::Owned(p))
+            Ok(p)
+        }
+        Pi(x, ref tA, ref tB) => {
+            let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
+            let kA = match tA2 {
+                Const(k) => k,
+                _        => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))),
+            };
+
+            let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e));
+            let tB = normalize(&type_with(&ctx2, tB)?);
+            let kB = match tB {
+                Const(k) => k,
+                _        => return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB))),
+            };
+
+            match rule(kA, kB) {
+                Err(()) => Err(TypeError::new(ctx, e, NoDependentTypes((**tA).clone(), tB))),
+                Ok(k) => Ok(Const(k)),
+            }
+        }
+        App(ref f, ref a) => {
+            let tf = normalize(&type_with(ctx, f)?);
+            let (x, tA, tB) = match tf {
+                Pi(x, tA, tB) => (x, tA, tB),
+                _             => return Err(TypeError::new(ctx, e, NotAFunction((**f).clone(), tf))),
+            };
+            let tA2 = type_with(ctx, a)?;
+            if prop_equal(&tA, &tA2) {
+                let vx0 = V(x, 0);
+                let a2  = shift::<S, S, X>( 1, vx0, a);
+                let tB2 = subst(vx0, &a2, &tB);
+                let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
+                Ok(tB3)
+            } else {
+                let nf_A  = normalize(&tA);
+                let nf_A2 = normalize(&tA2);
+                Err(TypeError::new(ctx, e, TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2)))
+            }
+        }
+        Let(f, ref mt, ref r, ref b) => {
+            let tR  = type_with(ctx, r)?;
+            let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
+            let kR  = match ttR {
+                Const(k) => k,
+                // Don't bother to provide a `let`-specific version of this error
+                // message because this should never happen anyway
+                _        => return Err(TypeError::new(ctx, e, InvalidInputType(tR))),
+            };
+
+            let ctx2 = ctx.insert(f, tR.clone());
+            let tB  = type_with(&ctx2, b)?;
+            let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
+            let kB  = match ttB {
+                Const(k) => k,
+                // Don't bother to provide a `let`-specific version of this error
+                // message because this should never happen anyway
+                _        => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))),
+            };
+
+            if let Err(()) = rule(kR, kB) {
+                return Err(TypeError::new(ctx, e, NoDependentLet(tR, tB)));
+            }
+
+            if let Some(ref t) = *mt {
+                let nf_t  = normalize(t);
+                let nf_tR = normalize(&tR);
+                if !prop_equal(&nf_tR, &nf_t) {
+                    return Err(TypeError::new(ctx, e, AnnotMismatch((**r).clone(), nf_t, nf_tR)));
+                }
+            }
+
+            Ok(tB)
+        }
+        Annot(ref x, ref t) => {
+            // This is mainly just to check that `t` is not `Kind`
+            let _ = type_with(ctx, t)?;
+
+            let t2 = type_with(ctx, x)?;
+            if prop_equal(t, &t2) {
+                Ok((**t).clone())
+            } else {
+                let nf_t  = normalize(t);
+                let nf_t2 = normalize(&t2);
+                Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2)))
+            }
+        }
+        BuiltinType(t) => Ok(match t {
+            List | Optional => pi("_", Const(Type), Const(Type)),
+            Bool | Natural | Integer | Double | Text => Const(Type),
+        }),
+        BoolLit(_) => Ok(BuiltinType(Bool)),
+        BoolAnd(ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r),
+        BoolOr(ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r),
+        BoolEQ(ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r),
+        BoolNE(ref l, ref r) => op2_type(ctx, e, Bool, CantNE, l, r),
+        BoolIf(ref x, ref y, ref z) => {
+            let tx = normalize(&type_with(ctx, x)?);
+            match tx {
+                BuiltinType(Bool) => {}
+                _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))),
+            }
+            let ty = normalize(&type_with(ctx, y)?);
+            let tty = normalize(&type_with(ctx, &ty)?);
+            match tty {
+                Const(Type) => {}
+                _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(true, (**y).clone(), ty, tty))),
+            }
+
+            let tz = normalize(&type_with(ctx, z)?);
+            let ttz = normalize(&type_with(ctx, &tz)?);
+            match ttz {
+                Const(Type) => {}
+                _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(false, (**z).clone(), tz, ttz))),
+            }
+
+            if !prop_equal(&ty, &tz) {
+                return Err(TypeError::new(ctx, e, IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz)));
+            }
+            Ok(ty)
+        }
+        NaturalLit(_) => Ok(BuiltinType(Natural)),
+        BuiltinValue(NaturalFold) =>
+            Ok(pi("_", Natural,
+                pi("natural", Const(Type),
+                    pi("succ", pi("_", "natural", "natural"),
+                        pi("zero", "natural", "natural"))))),
+        BuiltinValue(NaturalBuild) =>
+            Ok(pi("_",
+                pi("natural", Const(Type),
+                    pi("succ", pi("_", "natural", "natural"),
+                        pi("zero", "natural", "natural"))),
+                Natural)),
+        BuiltinValue(NaturalIsZero) |
+        BuiltinValue(NaturalEven) |
+        BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)),
+        NaturalPlus(ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r),
+        NaturalTimes(ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r),
+        IntegerLit(_) => Ok(BuiltinType(Integer)),
+        DoubleLit(_) => Ok(BuiltinType(Double)),
+        TextLit(_) => Ok(BuiltinType(Text)),
+        TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
+        ListLit(ref t, ref xs) => {
+            let s = normalize::<_, S, _>(&type_with(ctx, t)?);
+            match s {
+                Const(Type) => {}
+                _ => return Err(TypeError::new(ctx, e, InvalidListType((**t).clone()))),
+            }
+            for (i, x) in xs.iter().enumerate() {
+                let t2 = type_with(ctx, x)?;
+                if !prop_equal(t, &t2) {
+                    let nf_t  = normalize(t);
+                    let nf_t2 = normalize(&t2);
+                    return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
+                }
+            }
+            Ok(App(bx(BuiltinType(List)), t.clone()))
+        }
+        BuiltinValue(ListBuild) =>
+            Ok(pi("a", Const(Type),
+                pi("_",
+                    pi("list", Const(Type),
+                        pi("cons", pi("_", "a", pi("_", "list", "list")),
+                            pi("nil", "list", "list"))),
+                    app(List, "a")))),
+        BuiltinValue(ListFold) =>
+            Ok(pi("a", Const(Type),
+                pi("_", app(List, "a"),
+                    pi("list", Const(Type),
+                        pi("cons", pi("_", "a", pi("_", "list", "list")),
+                            pi("nil", "list", "list")))))),
+        BuiltinValue(ListLength) =>
+            Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
+        BuiltinValue(ListHead) |
+        BuiltinValue(ListLast) =>
+            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
+        BuiltinValue(ListIndexed) => {
+            let mut m = BTreeMap::new();
+            m.insert("index", BuiltinType(Natural));
+            m.insert("value", Expr::from("a"));
+            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m)))))
+        }
+        BuiltinValue(ListReverse) =>
+            Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
+        OptionalLit(ref t, ref xs) => {
+            let s = normalize::<_, S, _>(&type_with(ctx, t)?);
+            match s {
+                Const(Type) => {}
+                _ => return Err(TypeError::new(ctx, e, InvalidOptionalType((**t).clone()))),
+            }
+            let n = xs.len();
+            if 2 <= n {
+                return Err(TypeError::new(ctx, e, InvalidOptionalLiteral(n)));
+            }
+            for x in xs {
+                let t2 = type_with(ctx, x)?;
+                if !prop_equal(t, &t2) {
+                    let nf_t  = normalize(t);
+                    let nf_t2 = normalize(&t2);
+                    return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
+                }
+            }
+            Ok(App(bx(BuiltinType(Optional)), t.clone()))
+        }
+        BuiltinValue(OptionalFold) =>
+            Ok(pi("a", Const(Type),
+                pi("_", app(Optional, "a"),
+                    pi("optional", Const(Type),
+                        pi("just", pi("_", "a", "optional"),
+                            pi("nothing", "optional", "optional")))))),
+        Record(ref kts) => {
+            for (k, t) in kts {
+                let s = normalize::<S, S, X>(&type_with(ctx, t)?);
+                match s {
+                    Const(Type) => {}
+                    _ => return Err(TypeError::new(ctx, e, InvalidFieldType((*k).to_owned(), (*t).clone()))),
+                }
+            }
+            Ok(Const(Type))
+        }
+        RecordLit(ref kvs) => {
+            let kts = kvs.iter().map(|(&k, v)| {
+                let t = type_with(ctx, v)?;
+                let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
+                match s {
+                    Const(Type) => {}
+                    _ => return Err(TypeError::new(ctx, e, InvalidField((*k).to_owned(), (*v).clone()))),
+                }
+                Ok((k, t))
+            }).collect::<Result<_, _>>()?;
+            Ok(Record(kts))
+        }
+/*
+type_with ctx e@(Union     kts   ) = do
+    let process (k, t) = do
+            s <- fmap Dhall.Core.normalize (type_with ctx t)
+            case s of
+                Const Type -> return ()
+                _          -> Left (TypeError ctx e (InvalidAlternativeType k t))
+    mapM_ process (Data.Map.toList kts)
+    return (Const Type)
+type_with ctx e@(UnionLit k v kts) = do
+    case Data.Map.lookup k kts of
+        Just _  -> Left (TypeError ctx e (DuplicateAlternative k))
+        Nothing -> return ()
+    t <- type_with ctx v
+    let union = Union (Data.Map.insert k t kts)
+    _ <- type_with ctx union
+    return union
+type_with ctx e@(Combine kvsX kvsY) = do
+    tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
+    ktsX  <- case tKvsX of
+        Record kts -> return kts
+        _          -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))
+
+    tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
+    ktsY  <- case tKvsY of
+        Record kts -> return kts
+        _          -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))
+
+    let combineTypes ktsL ktsR = do
+            let ks =
+                    Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR)
+            kts <- forM (toList ks) (\k -> do
+                case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of
+                    (Just (Record ktsL'), Just (Record ktsR')) -> do
+                        t <- combineTypes ktsL' ktsR'
+                        return (k, t)
+                    (Nothing, Just t) -> do
+                        return (k, t)
+                    (Just t, Nothing) -> do
+                        return (k, t)
+                    _ -> do
+                        Left (TypeError ctx e (FieldCollision k)) )
+            return (Record (Data.Map.fromList kts))
+
+    combineTypes ktsX ktsY
+type_with ctx e@(Merge kvsX kvsY t) = do
+    tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX)
+    ktsX  <- case tKvsX of
+        Record kts -> return kts
+        _          -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX))
+    let ksX = Data.Map.keysSet ktsX
+
+    tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY)
+    ktsY  <- case tKvsY of
+        Union kts -> return kts
+        _         -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY))
+    let ksY = Data.Map.keysSet ktsY
+
+    let diffX = Data.Set.difference ksX ksY
+    let diffY = Data.Set.difference ksY ksX
+
+    if Data.Set.null diffX
+        then return ()
+        else Left (TypeError ctx e (UnusedHandler diffX))
+
+    let process (kY, tY) = do
+            case Data.Map.lookup kY ktsX of
+                Nothing  -> Left (TypeError ctx e (MissingHandler diffY))
+                Just tX  ->
+                    case tX of
+                        Pi _ tY' t' -> do
+                            if prop_equal tY tY'
+                                then return ()
+                                else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))
+                            if prop_equal t t'
+                                then return ()
+                                else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t'))
+                        _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))
+    mapM_ process (Data.Map.toList ktsY)
+    return t
+    */
+        Field(ref r, x) => {
+            let t = normalize(&type_with(ctx, r)?);
+            match t {
+                Record(ref kts) =>
+                    kts.get(x).cloned().ok_or_else(|| TypeError::new(ctx, e, MissingField(x.to_owned(), t.clone()))),
+                _ => Err(TypeError::new(ctx, e, NotARecord(x.to_owned(), (**r).clone(), t.clone()))),
+            }
+        }
+        /*
+type_with ctx   (Note s e'       ) = case type_with ctx e' of
+    Left (TypeError ctx2 (Note s' e'') m) -> Left (TypeError ctx2 (Note s' e'') m)
+    Left (TypeError ctx2          e''  m) -> Left (TypeError ctx2 (Note s  e'') m)
+    Right r                               -> Right r
+*/
+        Embed(p) => match p {},
+        _ => panic!("Unimplemented typecheck case: {:?}", e),
+    }
+}
+
+/// `typeOf` is the same as `type_with` with an empty context, meaning that the
+/// expression must be closed (i.e. no free variables), otherwise type-checking
+/// will fail.
+pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(e: &Expr<'i, S, X>) -> Result<Expr<'i, S, X>, TypeError<'i, S>> {
+    let ctx = Context::new();
+    type_with(&ctx, e) //.map(|e| e.into_owned())
+}
+
+/// The specific type error
+#[derive(Debug)]
+pub enum TypeMessage<'i, S> {
+    UnboundVariable,
+    InvalidInputType(Expr<'i, S, X>),
+    InvalidOutputType(Expr<'i, S, X>),
+    NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>),
+    TypeMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    Untyped,
+    InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidListType(Expr<'i, S, X>),
+    InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidOptionalLiteral(usize),
+    InvalidOptionalType(Expr<'i, S, X>),
+    InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>),
+    IfBranchMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidField(String, Expr<'i, S, X>),
+    InvalidFieldType(String, Expr<'i, S, X>),
+    InvalidAlternative(String, Expr<'i, S, X>),
+    InvalidAlternativeType(String, Expr<'i, S, X>),
+    DuplicateAlternative(String),
+    MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>),
+    FieldCollision(String),
+    MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>),
+    MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>),
+    UnusedHandler(HashSet<String>),
+    MissingHandler(HashSet<String>),
+    HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
+    HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
+    HandlerNotAFunction(String, Expr<'i, S, X>),
+    NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>),
+    MissingField(String, Expr<'i, S, X>),
+    CantAnd(Expr<'i, S, X>, Expr<'i, S, X>),
+    CantOr(Expr<'i, S, X>, Expr<'i, S, X>),
+    CantEQ(Expr<'i, S, X>, Expr<'i, S, X>),
+    CantNE(Expr<'i, S, X>, Expr<'i, S, X>),
+    CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>),
+    CantAdd(Expr<'i, S, X>, Expr<'i, S, X>),
+    CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>),
+    NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>),
+    NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>),
+}
+
+/// A structured type error that includes context
+#[derive(Debug)]
+pub struct TypeError<'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> {
+    pub fn new(context: &Context<'i, Expr<'i, S, X>>,
+               current: &Expr<'i, S, X>,
+               type_message: TypeMessage<'i, S>)
+               -> Self {
+        TypeError {
+            context: context.clone(),
+            current: current.clone(),
+            type_message: type_message,
+        }
+    }
+}
+
+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"),
+        }
+    }
+}