Merge pull request #159 from Nadrieril/operations

Factor out operations

36 files changed, 1527 insertions, 1706 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index 784ce93..893a4f9 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -308,9 +308,6 @@ fn generate_tests() -> std::io::Result<()> {
                     || path == "simple/integerToDouble"
                     // TODO: fix Double/show
                     || path == "prelude/JSON/number/1"
-                    // TODO: Further record simplifications
-                    || path == "simplifications/issue661"
-                    || path == "unit/RightBiasedRecordMergeWithinRecordProjection"
             }),
             output_type: Some(FileType::Text),
             ..default_feature.clone()
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/builtins.rs
index 6007a92..67929a0 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/builtins.rs
@@ -1,15 +1,91 @@
+use std::collections::{BTreeMap, HashMap};
+use std::convert::TryInto;
+
+use crate::operations::{BinOp, OpKind};
 use crate::semantics::{
     skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv,
 };
-use crate::syntax::map::DupTreeMap;
 use crate::syntax::Const::Type;
 use crate::syntax::{
-    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
-    InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr,
-    V,
+    Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label,
+    NaiveDouble, NumKind, Span, UnspannedExpr, V,
 };
-use std::collections::HashMap;
-use std::convert::TryInto;
+
+/// Built-ins
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
+pub enum Builtin {
+    Bool,
+    Natural,
+    Integer,
+    Double,
+    Text,
+    List,
+    Optional,
+    OptionalNone,
+    NaturalBuild,
+    NaturalFold,
+    NaturalIsZero,
+    NaturalEven,
+    NaturalOdd,
+    NaturalToInteger,
+    NaturalShow,
+    NaturalSubtract,
+    IntegerToDouble,
+    IntegerShow,
+    IntegerNegate,
+    IntegerClamp,
+    DoubleShow,
+    ListBuild,
+    ListFold,
+    ListLength,
+    ListHead,
+    ListLast,
+    ListIndexed,
+    ListReverse,
+    OptionalFold,
+    OptionalBuild,
+    TextShow,
+}
+
+impl Builtin {
+    pub fn parse(s: &str) -> Option<Self> {
+        use Builtin::*;
+        match s {
+            "Bool" => Some(Bool),
+            "Natural" => Some(Natural),
+            "Integer" => Some(Integer),
+            "Double" => Some(Double),
+            "Text" => Some(Text),
+            "List" => Some(List),
+            "Optional" => Some(Optional),
+            "None" => Some(OptionalNone),
+            "Natural/build" => Some(NaturalBuild),
+            "Natural/fold" => Some(NaturalFold),
+            "Natural/isZero" => Some(NaturalIsZero),
+            "Natural/even" => Some(NaturalEven),
+            "Natural/odd" => Some(NaturalOdd),
+            "Natural/toInteger" => Some(NaturalToInteger),
+            "Natural/show" => Some(NaturalShow),
+            "Natural/subtract" => Some(NaturalSubtract),
+            "Integer/toDouble" => Some(IntegerToDouble),
+            "Integer/show" => Some(IntegerShow),
+            "Integer/negate" => Some(IntegerNegate),
+            "Integer/clamp" => Some(IntegerClamp),
+            "Double/show" => Some(DoubleShow),
+            "List/build" => Some(ListBuild),
+            "List/fold" => Some(ListFold),
+            "List/length" => Some(ListLength),
+            "List/head" => Some(ListHead),
+            "List/last" => Some(ListLast),
+            "List/indexed" => Some(ListIndexed),
+            "List/reverse" => Some(ListReverse),
+            "Optional/fold" => Some(OptionalFold),
+            "Optional/build" => Some(OptionalBuild),
+            "Text/show" => Some(TextShow),
+            _ => None,
+        }
+    }
+}
 
 /// A partially applied builtin.
 /// Invariant: the evaluation of the given args must not be able to progress further
@@ -34,10 +110,10 @@ impl BuiltinClosure {
         HirKind::Expr(self.args.iter().fold(
             ExprKind::Builtin(self.b),
             |acc, v| {
-                ExprKind::App(
+                ExprKind::Op(OpKind::App(
                     Hir::new(HirKind::Expr(acc), Span::Artificial),
                     v.to_hir(venv),
-                )
+                ))
             },
         ))
     }
@@ -59,19 +135,19 @@ macro_rules! make_type {
         rc(ExprKind::Var(V(stringify!($var).into(), 0)))
     };
     (Optional $ty:ident) => {
-        rc(ExprKind::App(
+        rc(ExprKind::Op(OpKind::App(
             rc(ExprKind::Builtin(Builtin::Optional)),
             make_type!($ty)
-        ))
+        )))
     };
     (List $($rest:tt)*) => {
-        rc(ExprKind::App(
+        rc(ExprKind::Op(OpKind::App(
             rc(ExprKind::Builtin(Builtin::List)),
             make_type!($($rest)*)
-        ))
+        )))
     };
     ({ $($label:ident : $ty:ident),* }) => {{
-        let mut kts = DupTreeMap::new();
+        let mut kts = BTreeMap::new();
         $(
             kts.insert(
                 Label::from(stringify!($label)),
@@ -214,10 +290,10 @@ macro_rules! make_closure {
     };
     (List $($ty:tt)*) => {{
         let ty = make_closure!($($ty)*);
-        rc(ExprKind::App(
+        rc(ExprKind::Op(OpKind::App(
             rc(ExprKind::Builtin(Builtin::List)),
             ty
-        ))
+        )))
     }};
     (Some($($v:tt)*)) => {
         rc(ExprKind::SomeLit(
@@ -225,20 +301,20 @@ macro_rules! make_closure {
         ))
     };
     (1 + $($v:tt)*) => {
-        rc(ExprKind::BinOp(
+        rc(ExprKind::Op(OpKind::BinOp(
             BinOp::NaturalPlus,
             make_closure!($($v)*),
             rc(ExprKind::Num(NumKind::Natural(1)))
-        ))
+        )))
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {{
         let head = make_closure!($($head)*);
         let tail = make_closure!($($tail)*);
-        rc(ExprKind::BinOp(
+        rc(ExprKind::Op(OpKind::BinOp(
             BinOp::ListAppend,
             rc(ExprKind::NEListLit(vec![head])),
             tail,
-        ))
+        )))
     }};
 }
 
@@ -491,3 +567,42 @@ impl std::cmp::PartialEq for BuiltinClosure {
     }
 }
 impl std::cmp::Eq for BuiltinClosure {}
+
+impl std::fmt::Display for Builtin {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        use Builtin::*;
+        f.write_str(match *self {
+            Bool => "Bool",
+            Natural => "Natural",
+            Integer => "Integer",
+            Double => "Double",
+            Text => "Text",
+            List => "List",
+            Optional => "Optional",
+            OptionalNone => "None",
+            NaturalBuild => "Natural/build",
+            NaturalFold => "Natural/fold",
+            NaturalIsZero => "Natural/isZero",
+            NaturalEven => "Natural/even",
+            NaturalOdd => "Natural/odd",
+            NaturalToInteger => "Natural/toInteger",
+            NaturalShow => "Natural/show",
+            NaturalSubtract => "Natural/subtract",
+            IntegerToDouble => "Integer/toDouble",
+            IntegerNegate => "Integer/negate",
+            IntegerClamp => "Integer/clamp",
+            IntegerShow => "Integer/show",
+            DoubleShow => "Double/show",
+            ListBuild => "List/build",
+            ListFold => "List/fold",
+            ListLength => "List/length",
+            ListHead => "List/head",
+            ListLast => "List/last",
+            ListIndexed => "List/indexed",
+            ListReverse => "List/reverse",
+            OptionalFold => "Optional/fold",
+            OptionalBuild => "Optional/build",
+            TextShow => "Text/show",
+        })
+    }
+}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 98ad4f0..61327cb 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -10,7 +10,9 @@
 
 mod tests;
 
+pub mod builtins;
 pub mod error;
+pub mod operations;
 pub mod semantics;
 pub mod syntax;
 
diff --git a/dhall/src/operations/kind.rs b/dhall/src/operations/kind.rs
new file mode 100644
index 0000000..5415637
--- /dev/null
+++ b/dhall/src/operations/kind.rs
@@ -0,0 +1,97 @@
+use std::collections::BTreeSet;
+
+use crate::syntax::{trivial_result, Label};
+
+// Definition order must match precedence order for
+// pretty-printing to work correctly
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum BinOp {
+    /// `x ? y`
+    ImportAlt,
+    /// `x || y`
+    BoolOr,
+    /// `x + y`
+    NaturalPlus,
+    /// `x ++ y`
+    TextAppend,
+    /// `x # y`
+    ListAppend,
+    /// `x && y`
+    BoolAnd,
+    /// `x ∧ y`
+    RecursiveRecordMerge,
+    /// `x ⫽ y`
+    RightBiasedRecordMerge,
+    /// `x ⩓ y`
+    RecursiveRecordTypeMerge,
+    /// `x * y`
+    NaturalTimes,
+    /// `x == y`
+    BoolEQ,
+    /// `x != y`
+    BoolNE,
+    /// x === y
+    Equivalence,
+}
+
+/// Operations
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum OpKind<SubExpr> {
+    ///  `f a`
+    App(SubExpr, SubExpr),
+    /// Binary operations
+    BinOp(BinOp, SubExpr, SubExpr),
+    ///  `if x then y else z`
+    BoolIf(SubExpr, SubExpr, SubExpr),
+    ///  `merge x y : t`
+    Merge(SubExpr, SubExpr, Option<SubExpr>),
+    ///  `toMap x : t`
+    ToMap(SubExpr, Option<SubExpr>),
+    ///  `e.x`
+    Field(SubExpr, Label),
+    ///  `e.{ x, y, z }`
+    Projection(SubExpr, BTreeSet<Label>),
+    ///  `e.(t)`
+    ProjectionByExpr(SubExpr, SubExpr),
+    ///  `x::y`
+    Completion(SubExpr, SubExpr),
+}
+
+impl<SE> OpKind<SE> {
+    pub fn traverse_ref<'a, SE2, Err>(
+        &'a self,
+        mut f: impl FnMut(&'a SE) -> Result<SE2, Err>,
+    ) -> Result<OpKind<SE2>, Err> {
+        // Can't use closures because of borrowing rules
+        macro_rules! expr {
+            ($e:expr) => {
+                f($e)?
+            };
+        }
+        macro_rules! opt {
+            ($e:expr) => {
+                $e.as_ref().map(|e| Ok(expr!(e))).transpose()?
+            };
+        }
+
+        use OpKind::*;
+        Ok(match self {
+            App(f, a) => App(expr!(f), expr!(a)),
+            BinOp(o, x, y) => BinOp(*o, expr!(x), expr!(y)),
+            BoolIf(b, t, f) => BoolIf(expr!(b), expr!(t), expr!(f)),
+            Merge(x, y, t) => Merge(expr!(x), expr!(y), opt!(t)),
+            ToMap(x, t) => ToMap(expr!(x), opt!(t)),
+            Field(e, l) => Field(expr!(e), l.clone()),
+            Projection(e, ls) => Projection(expr!(e), ls.clone()),
+            ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e), expr!(x)),
+            Completion(e, x) => Completion(expr!(e), expr!(x)),
+        })
+    }
+
+    pub fn map_ref<'a, SE2>(
+        &'a self,
+        mut f: impl FnMut(&'a SE) -> SE2,
+    ) -> OpKind<SE2> {
+        trivial_result(self.traverse_ref(|x| Ok(f(x))))
+    }
+}
diff --git a/dhall/src/operations/mod.rs b/dhall/src/operations/mod.rs
new file mode 100644
index 0000000..1a3b65b
--- /dev/null
+++ b/dhall/src/operations/mod.rs
@@ -0,0 +1,6 @@
+mod kind;
+mod normalization;
+mod typecheck;
+pub use kind::*;
+pub use normalization::*;
+pub use typecheck::*;
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
new file mode 100644
index 0000000..e3a9415
--- /dev/null
+++ b/dhall/src/operations/normalization.rs
@@ -0,0 +1,306 @@
+use itertools::Itertools;
+use std::collections::HashMap;
+use std::iter::once;
+
+use crate::operations::{BinOp, OpKind};
+use crate::semantics::{
+    merge_maps, ret_kind, ret_op, ret_ref, Nir, NirKind, Ret, TextLit,
+};
+use crate::syntax::{ExprKind, Label, NumKind};
+
+fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret {
+    use BinOp::*;
+    use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
+    use NumKind::{Bool, Natural};
+
+    match (o, x.kind(), y.kind()) {
+        (BoolAnd, Num(Bool(true)), _) => ret_ref(y),
+        (BoolAnd, _, Num(Bool(true))) => ret_ref(x),
+        (BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))),
+        (BoolAnd, _, Num(Bool(false))) => ret_kind(Num(Bool(false))),
+        (BoolAnd, _, _) if x == y => ret_ref(x),
+        (BoolOr, Num(Bool(true)), _) => ret_kind(Num(Bool(true))),
+        (BoolOr, _, Num(Bool(true))) => ret_kind(Num(Bool(true))),
+        (BoolOr, Num(Bool(false)), _) => ret_ref(y),
+        (BoolOr, _, Num(Bool(false))) => ret_ref(x),
+        (BoolOr, _, _) if x == y => ret_ref(x),
+        (BoolEQ, Num(Bool(true)), _) => ret_ref(y),
+        (BoolEQ, _, Num(Bool(true))) => ret_ref(x),
+        (BoolEQ, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x == y))),
+        (BoolEQ, _, _) if x == y => ret_kind(Num(Bool(true))),
+        (BoolNE, Num(Bool(false)), _) => ret_ref(y),
+        (BoolNE, _, Num(Bool(false))) => ret_ref(x),
+        (BoolNE, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x != y))),
+        (BoolNE, _, _) if x == y => ret_kind(Num(Bool(false))),
+
+        (NaturalPlus, Num(Natural(0)), _) => ret_ref(y),
+        (NaturalPlus, _, Num(Natural(0))) => ret_ref(x),
+        (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => {
+            ret_kind(Num(Natural(x + y)))
+        }
+        (NaturalTimes, Num(Natural(0)), _) => ret_kind(Num(Natural(0))),
+        (NaturalTimes, _, Num(Natural(0))) => ret_kind(Num(Natural(0))),
+        (NaturalTimes, Num(Natural(1)), _) => ret_ref(y),
+        (NaturalTimes, _, Num(Natural(1))) => ret_ref(x),
+        (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => {
+            ret_kind(Num(Natural(x * y)))
+        }
+
+        (ListAppend, EmptyListLit(_), _) => ret_ref(y),
+        (ListAppend, _, EmptyListLit(_)) => ret_ref(x),
+        (ListAppend, NEListLit(xs), NEListLit(ys)) => {
+            ret_kind(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
+        }
+
+        (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => ret_ref(y),
+        (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_ref(x),
+        (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
+            ret_kind(NirKind::TextLit(x.concat(y)))
+        }
+        (TextAppend, NirKind::TextLit(x), _) => ret_kind(NirKind::TextLit(
+            x.concat(&TextLit::interpolate(y.clone())),
+        )),
+        (TextAppend, _, NirKind::TextLit(y)) => ret_kind(NirKind::TextLit(
+            TextLit::interpolate(x.clone()).concat(y),
+        )),
+
+        (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+            ret_ref(x)
+        }
+        (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+            ret_ref(y)
+        }
+        (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+            let mut kvs = kvs2.clone();
+            for (x, v) in kvs1 {
+                // Insert only if key not already present
+                kvs.entry(x.clone()).or_insert_with(|| v.clone());
+            }
+            ret_kind(RecordLit(kvs))
+        }
+        (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y),
+
+        (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+            ret_ref(x)
+        }
+        (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+            ret_ref(y)
+        }
+        (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+            let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| {
+                Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp(
+                    RecursiveRecordMerge,
+                    v1.clone(),
+                    v2.clone(),
+                )))
+            });
+            ret_kind(RecordLit(kvs))
+        }
+
+        (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
+            let kts = merge_maps(
+                kts_x,
+                kts_y,
+                // If the Label exists for both records, then we hit the recursive case.
+                |_, l: &Nir, r: &Nir| {
+                    Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp(
+                        RecursiveRecordTypeMerge,
+                        l.clone(),
+                        r.clone(),
+                    )))
+                },
+            );
+            ret_kind(RecordType(kts))
+        }
+
+        (Equivalence, _, _) => {
+            ret_kind(NirKind::Equivalence(x.clone(), y.clone()))
+        }
+
+        _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())),
+    }
+}
+
+fn normalize_field(v: &Nir, field: &Label) -> Ret {
+    use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge};
+    use NirKind::{Op, RecordLit, UnionConstructor, UnionType};
+    use OpKind::{BinOp, Field, Projection};
+    let nothing_to_do = || ret_op(Field(v.clone(), field.clone()));
+
+    match v.kind() {
+        RecordLit(kvs) => match kvs.get(field) {
+            Some(r) => ret_ref(r),
+            None => nothing_to_do(),
+        },
+        UnionType(kts) => {
+            ret_kind(UnionConstructor(field.clone(), kts.clone()))
+        }
+        Op(Projection(x, _)) => normalize_field(x, field),
+        Op(BinOp(RightBiasedRecordMerge, x, y)) => match (x.kind(), y.kind()) {
+            (_, RecordLit(kvs)) => match kvs.get(field) {
+                Some(r) => ret_ref(r),
+                None => normalize_field(x, field),
+            },
+            (RecordLit(kvs), _) => match kvs.get(field) {
+                Some(r) => ret_op(Field(
+                    Nir::from_kind(Op(BinOp(
+                        RightBiasedRecordMerge,
+                        Nir::from_kind(RecordLit(
+                            once((field.clone(), r.clone())).collect(),
+                        )),
+                        y.clone(),
+                    ))),
+                    field.clone(),
+                )),
+                None => normalize_field(y, field),
+            },
+            _ => nothing_to_do(),
+        },
+        Op(BinOp(RecursiveRecordMerge, x, y)) => match (x.kind(), y.kind()) {
+            (RecordLit(kvs), _) => match kvs.get(field) {
+                Some(r) => ret_op(Field(
+                    Nir::from_kind(Op(BinOp(
+                        RecursiveRecordMerge,
+                        Nir::from_kind(RecordLit(
+                            once((field.clone(), r.clone())).collect(),
+                        )),
+                        y.clone(),
+                    ))),
+                    field.clone(),
+                )),
+                None => normalize_field(y, field),
+            },
+            (_, RecordLit(kvs)) => match kvs.get(field) {
+                Some(r) => ret_op(Field(
+                    Nir::from_kind(Op(BinOp(
+                        RecursiveRecordMerge,
+                        x.clone(),
+                        Nir::from_kind(RecordLit(
+                            once((field.clone(), r.clone())).collect(),
+                        )),
+                    ))),
+                    field.clone(),
+                )),
+                None => normalize_field(x, field),
+            },
+            _ => nothing_to_do(),
+        },
+        _ => nothing_to_do(),
+    }
+}
+
+pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
+    use self::BinOp::RightBiasedRecordMerge;
+    use NirKind::{
+        EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op,
+        RecordLit, RecordType, UnionConstructor, UnionLit,
+    };
+    use NumKind::Bool;
+    use OpKind::*;
+    let nothing_to_do = || ret_op(opkind.clone());
+
+    match opkind {
+        App(v, a) => ret_kind(v.app_to_kind(a.clone())),
+        BinOp(o, x, y) => normalize_binop(*o, x, y),
+        BoolIf(b, e1, e2) => {
+            match b.kind() {
+                Num(Bool(true)) => ret_ref(e1),
+                Num(Bool(false)) => ret_ref(e2),
+                _ => {
+                    match (e1.kind(), e2.kind()) {
+                        // Simplify `if b then True else False`
+                        (Num(Bool(true)), Num(Bool(false))) => ret_ref(b),
+                        _ if e1 == e2 => ret_ref(e1),
+                        _ => nothing_to_do(),
+                    }
+                }
+            }
+        }
+        Merge(handlers, variant, _) => match handlers.kind() {
+            RecordLit(kvs) => match variant.kind() {
+                UnionConstructor(l, _) => match kvs.get(l) {
+                    Some(h) => ret_ref(h),
+                    None => nothing_to_do(),
+                },
+                UnionLit(l, v, _) => match kvs.get(l) {
+                    Some(h) => ret_kind(h.app_to_kind(v.clone())),
+                    None => nothing_to_do(),
+                },
+                EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
+                    Some(h) => ret_ref(h),
+                    None => nothing_to_do(),
+                },
+                NEOptionalLit(v) => match kvs.get(&"Some".into()) {
+                    Some(h) => ret_kind(h.app_to_kind(v.clone())),
+                    None => nothing_to_do(),
+                },
+                _ => nothing_to_do(),
+            },
+            _ => nothing_to_do(),
+        },
+        ToMap(v, annot) => match v.kind() {
+            RecordLit(kvs) if kvs.is_empty() => {
+                match annot.as_ref().map(|v| v.kind()) {
+                    Some(NirKind::ListType(t)) => {
+                        ret_kind(EmptyListLit(t.clone()))
+                    }
+                    _ => nothing_to_do(),
+                }
+            }
+            RecordLit(kvs) => ret_kind(NEListLit(
+                kvs.iter()
+                    .sorted_by_key(|(k, _)| *k)
+                    .map(|(k, v)| {
+                        let mut rec = HashMap::new();
+                        rec.insert("mapKey".into(), Nir::from_text(k));
+                        rec.insert("mapValue".into(), v.clone());
+                        Nir::from_kind(NirKind::RecordLit(rec))
+                    })
+                    .collect(),
+            )),
+            _ => nothing_to_do(),
+        },
+        Field(v, field) => normalize_field(v, field),
+        Projection(_, ls) if ls.is_empty() => {
+            ret_kind(RecordLit(HashMap::new()))
+        }
+        Projection(v, ls) => match v.kind() {
+            RecordLit(kvs) => ret_kind(RecordLit(
+                ls.iter()
+                    .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+                    .collect(),
+            )),
+            Op(Projection(v2, _)) => {
+                normalize_operation(&Projection(v2.clone(), ls.clone()))
+            }
+            Op(BinOp(RightBiasedRecordMerge, l, r)) => match r.kind() {
+                RecordLit(kvs) => {
+                    let r_keys = kvs.keys().cloned().collect();
+                    normalize_operation(&BinOp(
+                        RightBiasedRecordMerge,
+                        Nir::from_partial_expr(ExprKind::Op(Projection(
+                            l.clone(),
+                            ls.difference(&r_keys).cloned().collect(),
+                        ))),
+                        Nir::from_partial_expr(ExprKind::Op(Projection(
+                            r.clone(),
+                            ls.intersection(&r_keys).cloned().collect(),
+                        ))),
+                    ))
+                }
+                _ => nothing_to_do(),
+            },
+            _ => nothing_to_do(),
+        },
+        ProjectionByExpr(v, t) => match t.kind() {
+            RecordType(kts) => normalize_operation(&Projection(
+                v.clone(),
+                kts.keys().cloned().collect(),
+            )),
+            _ => nothing_to_do(),
+        },
+        Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
+        }
+    }
+}
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
new file mode 100644
index 0000000..91d5059
--- /dev/null
+++ b/dhall/src/operations/typecheck.rs
@@ -0,0 +1,510 @@
+use std::borrow::Cow;
+use std::cmp::max;
+use std::collections::HashMap;
+
+use crate::builtins::Builtin;
+use crate::error::{ErrorBuilder, TypeError};
+use crate::operations::{BinOp, OpKind};
+use crate::semantics::{
+    merge_maps, mk_span_err, mkerr, Binder, Closure, Hir, HirKind, Nir,
+    NirKind, Tir, TyEnv, Type,
+};
+use crate::syntax::{Const, ExprKind, Span};
+
+fn check_rectymerge(
+    span: &Span,
+    env: &TyEnv,
+    x: Nir,
+    y: Nir,
+) -> Result<(), TypeError> {
+    let kts_x = match x.kind() {
+        NirKind::RecordType(kts) => kts,
+        _ => {
+            return mk_span_err(
+                span.clone(),
+                "RecordTypeMergeRequiresRecordType",
+            )
+        }
+    };
+    let kts_y = match y.kind() {
+        NirKind::RecordType(kts) => kts,
+        _ => {
+            return mk_span_err(
+                span.clone(),
+                "RecordTypeMergeRequiresRecordType",
+            )
+        }
+    };
+    for (k, tx) in kts_x {
+        if let Some(ty) = kts_y.get(k) {
+            // TODO: store Type in RecordType ?
+            check_rectymerge(span, env, tx.clone(), ty.clone())?;
+        }
+    }
+    Ok(())
+}
+
+fn typecheck_binop(
+    env: &TyEnv,
+    span: Span,
+    op: BinOp,
+    l: &Tir<'_>,
+    r: &Tir<'_>,
+) -> Result<Type, TypeError> {
+    let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+    use BinOp::*;
+    use NirKind::{ListType, RecordType};
+
+    Ok(match op {
+        RightBiasedRecordMerge => {
+            let x_type = l.ty();
+            let y_type = r.ty();
+
+            // Extract the LHS record type
+            let kts_x = match x_type.kind() {
+                RecordType(kts) => kts,
+                _ => return span_err("MustCombineRecord"),
+            };
+            // Extract the RHS record type
+            let kts_y = match y_type.kind() {
+                RecordType(kts) => kts,
+                _ => return span_err("MustCombineRecord"),
+            };
+
+            // Union the two records, prefering
+            // the values found in the RHS.
+            let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone());
+
+            let u = max(l.ty().ty(), r.ty().ty());
+            Nir::from_kind(RecordType(kts)).to_type(u)
+        }
+        RecursiveRecordMerge => {
+            check_rectymerge(&span, env, l.ty().to_nir(), r.ty().to_nir())?;
+
+            let hir = Hir::new(
+                HirKind::Expr(ExprKind::Op(OpKind::BinOp(
+                    RecursiveRecordTypeMerge,
+                    l.ty().to_hir(env.as_varenv()),
+                    r.ty().to_hir(env.as_varenv()),
+                ))),
+                span.clone(),
+            );
+            let x_u = l.ty().ty();
+            let y_u = r.ty().ty();
+            Type::new(hir.eval(env), max(x_u, y_u))
+        }
+        RecursiveRecordTypeMerge => {
+            check_rectymerge(&span, env, l.eval(env), r.eval(env))?;
+
+            // A RecordType's type is always a const
+            let xk = l.ty().as_const().unwrap();
+            let yk = r.ty().as_const().unwrap();
+            Type::from_const(max(xk, yk))
+        }
+        ListAppend => {
+            match l.ty().kind() {
+                ListType(..) => {}
+                _ => return span_err("BinOpTypeMismatch"),
+            }
+
+            if l.ty() != r.ty() {
+                return span_err("BinOpTypeMismatch");
+            }
+
+            l.ty().clone()
+        }
+        Equivalence => {
+            if l.ty() != r.ty() {
+                return span_err("EquivalenceTypeMismatch");
+            }
+            if l.ty().ty().as_const() != Some(Const::Type) {
+                return span_err("EquivalenceArgumentsMustBeTerms");
+            }
+
+            Type::from_const(Const::Type)
+        }
+        op => {
+            let t = Type::from_builtin(match op {
+                BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool,
+                NaturalPlus | NaturalTimes => Builtin::Natural,
+                TextAppend => Builtin::Text,
+                ListAppend
+                | RightBiasedRecordMerge
+                | RecursiveRecordMerge
+                | RecursiveRecordTypeMerge
+                | Equivalence => unreachable!(),
+                ImportAlt => unreachable!("ImportAlt leftover in tck"),
+            });
+
+            if *l.ty() != t {
+                return span_err("BinOpTypeMismatch");
+            }
+
+            if *r.ty() != t {
+                return span_err("BinOpTypeMismatch");
+            }
+
+            t
+        }
+    })
+}
+
+fn typecheck_merge(
+    env: &TyEnv,
+    span: Span,
+    record: &Tir<'_>,
+    scrut: &Tir<'_>,
+    type_annot: Option<&Tir<'_>>,
+) -> Result<Type, TypeError> {
+    let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+    use NirKind::{OptionalType, PiClosure, RecordType, UnionType};
+
+    let record_type = record.ty();
+    let handlers = match record_type.kind() {
+        RecordType(kts) => kts,
+        _ => return span_err("Merge1ArgMustBeRecord"),
+    };
+
+    let scrut_type = scrut.ty();
+    let variants = match scrut_type.kind() {
+        UnionType(kts) => Cow::Borrowed(kts),
+        OptionalType(ty) => {
+            let mut kts = HashMap::new();
+            kts.insert("None".into(), None);
+            kts.insert("Some".into(), Some(ty.clone()));
+            Cow::Owned(kts)
+        }
+        _ => return span_err("Merge2ArgMustBeUnionOrOptional"),
+    };
+
+    let mut inferred_type = None;
+    for (x, handler_type) in handlers {
+        let handler_return_type: Type = match variants.get(x) {
+            // Union alternative with type
+            Some(Some(variant_type)) => match handler_type.kind() {
+                PiClosure { closure, annot, .. } => {
+                    if variant_type != annot {
+                        return mkerr(
+                            ErrorBuilder::new(format!(
+                                "Wrong handler input type"
+                            ))
+                            .span_err(
+                                span,
+                                format!("in this merge expression",),
+                            )
+                            .span_err(
+                                record.span(),
+                                format!(
+                                    "the handler for `{}` expects a value of \
+                                     type: `{}`",
+                                    x,
+                                    annot.to_expr_tyenv(env)
+                                ),
+                            )
+                            .span_err(
+                                scrut.span(),
+                                format!(
+                                    "but the corresponding variant has type: \
+                                     `{}`",
+                                    variant_type.to_expr_tyenv(env)
+                                ),
+                            )
+                            .format(),
+                        );
+                    }
+
+                    // TODO: this actually doesn't check anything yet
+                    match closure.remove_binder() {
+                        Ok(v) => Type::new_infer_universe(env, v.clone())?,
+                        Err(()) => {
+                            return span_err("MergeReturnTypeIsDependent")
+                        }
+                    }
+                }
+                _ => {
+                    return mkerr(
+                        ErrorBuilder::new(format!(
+                            "merge handler is not a function"
+                        ))
+                        .span_err(span, format!("in this merge expression"))
+                        .span_err(
+                            record.span(),
+                            format!(
+                                "the handler for `{}` has type: `{}`",
+                                x,
+                                handler_type.to_expr_tyenv(env)
+                            ),
+                        )
+                        .span_help(
+                            scrut.span(),
+                            format!(
+                                "the corresponding variant has type: `{}`",
+                                variant_type.to_expr_tyenv(env)
+                            ),
+                        )
+                        .help(format!(
+                            "a handler for this variant must be a function \
+                             that takes an input of type: `{}`",
+                            variant_type.to_expr_tyenv(env)
+                        ))
+                        .format(),
+                    )
+                }
+            },
+            // Union alternative without type
+            Some(None) => Type::new_infer_universe(env, handler_type.clone())?,
+            None => return span_err("MergeHandlerMissingVariant"),
+        };
+        match &inferred_type {
+            None => inferred_type = Some(handler_return_type),
+            Some(t) => {
+                if t != &handler_return_type {
+                    return span_err("MergeHandlerTypeMismatch");
+                }
+            }
+        }
+    }
+    for x in variants.keys() {
+        if !handlers.contains_key(x) {
+            return span_err("MergeVariantMissingHandler");
+        }
+    }
+
+    let type_annot = type_annot
+        .as_ref()
+        .map(|t| t.eval_to_type(env))
+        .transpose()?;
+    Ok(match (inferred_type, type_annot) {
+        (Some(t1), Some(t2)) => {
+            if t1 != t2 {
+                return span_err("MergeAnnotMismatch");
+            }
+            t1
+        }
+        (Some(t), None) => t,
+        (None, Some(t)) => t,
+        (None, None) => return span_err("MergeEmptyNeedsAnnotation"),
+    })
+}
+
+pub fn typecheck_operation(
+    env: &TyEnv,
+    span: Span,
+    opkind: &OpKind<Tir<'_>>,
+) -> Result<Type, TypeError> {
+    let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+    use NirKind::{ListType, PiClosure, RecordType, UnionType};
+    use OpKind::*;
+
+    Ok(match opkind {
+        App(f, arg) => {
+            match f.ty().kind() {
+                // TODO: store Type in closure
+                PiClosure { annot, closure, .. } => {
+                    if arg.ty().as_nir() != annot {
+                        return mkerr(
+                            ErrorBuilder::new(format!(
+                                "wrong type of function argument"
+                            ))
+                            .span_err(
+                                f.span(),
+                                format!(
+                                    "this expects an argument of type: {}",
+                                    annot.to_expr_tyenv(env),
+                                ),
+                            )
+                            .span_err(
+                                arg.span(),
+                                format!(
+                                    "but this has type: {}",
+                                    arg.ty().to_expr_tyenv(env),
+                                ),
+                            )
+                            .note(format!(
+                                "expected type `{}`\n   found type `{}`",
+                                annot.to_expr_tyenv(env),
+                                arg.ty().to_expr_tyenv(env),
+                            ))
+                            .format(),
+                        );
+                    }
+
+                    let arg_nf = arg.eval(env);
+                    Type::new_infer_universe(env, closure.apply(arg_nf))?
+                }
+                _ => return mkerr(
+                    ErrorBuilder::new(format!(
+                        "expected function, found `{}`",
+                        f.ty().to_expr_tyenv(env)
+                    ))
+                    .span_err(
+                        f.span(),
+                        format!("function application requires a function",),
+                    )
+                    .format(),
+                ),
+            }
+        }
+        BinOp(o, l, r) => typecheck_binop(env, span, *o, l, r)?,
+        BoolIf(x, y, z) => {
+            if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
+                return span_err("InvalidPredicate");
+            }
+            if y.ty().ty().as_const() != Some(Const::Type) {
+                return span_err("IfBranchMustBeTerm");
+            }
+            if y.ty() != z.ty() {
+                return span_err("IfBranchMismatch");
+            }
+
+            y.ty().clone()
+        }
+        Merge(record, scrut, type_annot) => {
+            typecheck_merge(env, span, record, scrut, type_annot.as_ref())?
+        }
+        ToMap(record, annot) => {
+            if record.ty().ty().as_const() != Some(Const::Type) {
+                return span_err("`toMap` only accepts records of type `Type`");
+            }
+            let record_t = record.ty();
+            let kts = match record_t.kind() {
+                RecordType(kts) => kts,
+                _ => {
+                    return span_err("The argument to `toMap` must be a record")
+                }
+            };
+
+            if kts.is_empty() {
+                let annot = if let Some(annot) = annot {
+                    annot
+                } else {
+                    return span_err(
+                        "`toMap` applied to an empty record requires a type \
+                         annotation",
+                    );
+                };
+                let annot_val = annot.eval_to_type(env)?;
+
+                let err_msg = "The type of `toMap x` must be of the form \
+                               `List { mapKey : Text, mapValue : T }`";
+                let arg = match annot_val.kind() {
+                    ListType(t) => t,
+                    _ => return span_err(err_msg),
+                };
+                let kts = match arg.kind() {
+                    RecordType(kts) => kts,
+                    _ => return span_err(err_msg),
+                };
+                if kts.len() != 2 {
+                    return span_err(err_msg);
+                }
+                match kts.get(&"mapKey".into()) {
+                    Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
+                    _ => return span_err(err_msg),
+                }
+                match kts.get(&"mapValue".into()) {
+                    Some(_) => {}
+                    None => return span_err(err_msg),
+                }
+                annot_val
+            } else {
+                let entry_type = kts.iter().next().unwrap().1.clone();
+                for (_, t) in kts.iter() {
+                    if *t != entry_type {
+                        return span_err(
+                            "Every field of the record must have the same type",
+                        );
+                    }
+                }
+
+                let mut kts = HashMap::new();
+                kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
+                kts.insert("mapValue".into(), entry_type);
+                let output_type: Type = Nir::from_builtin(Builtin::List)
+                    .app(Nir::from_kind(RecordType(kts)))
+                    .to_type(Const::Type);
+                if let Some(annot) = annot {
+                    let annot_val = annot.eval_to_type(env)?;
+                    if output_type != annot_val {
+                        return span_err("Annotation mismatch");
+                    }
+                }
+                output_type
+            }
+        }
+        Field(scrut, x) => {
+            match scrut.ty().kind() {
+                RecordType(kts) => match kts.get(&x) {
+                    Some(val) => Type::new_infer_universe(env, val.clone())?,
+                    None => return span_err("MissingRecordField"),
+                },
+                NirKind::Const(_) => {
+                    let scrut = scrut.eval_to_type(env)?;
+                    match scrut.kind() {
+                        UnionType(kts) => match kts.get(x) {
+                            // Constructor has type T -> < x: T, ... >
+                            Some(Some(ty)) => Nir::from_kind(PiClosure {
+                                binder: Binder::new(x.clone()),
+                                annot: ty.clone(),
+                                closure: Closure::new_constant(scrut.to_nir()),
+                            })
+                            .to_type(scrut.ty()),
+                            Some(None) => scrut,
+                            None => return span_err("MissingUnionField"),
+                        },
+                        _ => return span_err("NotARecord"),
+                    }
+                }
+                _ => return span_err("NotARecord"),
+            }
+        }
+        Projection(record, labels) => {
+            let record_type = record.ty();
+            let kts = match record_type.kind() {
+                RecordType(kts) => kts,
+                _ => return span_err("ProjectionMustBeRecord"),
+            };
+
+            let mut new_kts = HashMap::new();
+            for l in labels {
+                match kts.get(l) {
+                    None => return span_err("ProjectionMissingEntry"),
+                    Some(t) => {
+                        new_kts.insert(l.clone(), t.clone());
+                    }
+                };
+            }
+
+            Type::new_infer_universe(env, Nir::from_kind(RecordType(new_kts)))?
+        }
+        ProjectionByExpr(record, selection) => {
+            let record_type = record.ty();
+            let rec_kts = match record_type.kind() {
+                RecordType(kts) => kts,
+                _ => return span_err("ProjectionMustBeRecord"),
+            };
+
+            let selection_val = selection.eval_to_type(env)?;
+            let sel_kts = match selection_val.kind() {
+                RecordType(kts) => kts,
+                _ => return span_err("ProjectionByExprTakesRecordType"),
+            };
+
+            for (l, sel_ty) in sel_kts {
+                match rec_kts.get(l) {
+                    Some(rec_ty) => {
+                        if rec_ty != sel_ty {
+                            return span_err("ProjectionWrongType");
+                        }
+                    }
+                    None => return span_err("ProjectionMissingEntry"),
+                }
+            }
+
+            selection_val
+        }
+        Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
+        }
+    })
+}
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 468d8b1..a488c31 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,9 +1,7 @@
-pub mod builtins;
 pub mod nze;
 pub mod parse;
 pub mod resolve;
 pub mod tck;
-pub use self::builtins::*;
 pub use self::nze::*;
 pub use self::resolve::*;
 pub use self::tck::*;
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index e0d227e..12f1b14 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -1,14 +1,15 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
+use crate::builtins::{Builtin, BuiltinClosure};
+use crate::operations::{BinOp, OpKind};
 use crate::semantics::nze::lazy;
 use crate::semantics::{
-    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
-    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+    apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, Hir,
+    HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
-    NumKind, Span,
+    Const, Expr, ExprKind, InterpolatedTextContents, Label, NumKind, Span,
 };
 use crate::ToExprOptions;
 
@@ -74,25 +75,27 @@ pub enum NirKind {
 
     Var(NzVar),
     Const(Const),
+    Num(NumKind),
     // Must be a number type, Bool or Text
     BuiltinType(Builtin),
-    Num(NumKind),
-    OptionalType(Nir),
+    TextLit(TextLit),
     EmptyOptionalLit(Nir),
     NEOptionalLit(Nir),
-    ListType(Nir),
+    OptionalType(Nir),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
     EmptyListLit(Nir),
     NEListLit(Vec<Nir>),
-    RecordType(HashMap<Label, Nir>),
+    ListType(Nir),
     RecordLit(HashMap<Label, Nir>),
-    UnionType(HashMap<Label, Option<Nir>>),
+    RecordType(HashMap<Label, Nir>),
     UnionConstructor(Label, HashMap<Label, Option<Nir>>),
     UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
-    TextLit(TextLit),
+    UnionType(HashMap<Label, Option<Nir>>),
     Equivalence(Nir, Nir),
-    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
-    PartialExpr(ExprKind<Nir>),
+    Assert(Nir),
+    /// Invariant: evaluation must not be able to progress with `normalize_operation`.
+    /// This is used when an operation couldn't proceed further, for example because of variables.
+    Op(OpKind<Nir>),
 }
 
 impl Nir {
@@ -111,8 +114,7 @@ impl Nir {
         NirInternal::from_whnf(v).into_nir()
     }
     pub fn from_const(c: Const) -> Self {
-        let v = NirKind::Const(c);
-        NirInternal::from_whnf(v).into_nir()
+        Self::from_kind(NirKind::Const(c))
     }
     pub fn from_builtin(b: Builtin) -> Self {
         Self::from_builtin_env(b, &NzEnv::new())
@@ -148,7 +150,10 @@ impl Nir {
     }
 
     pub fn app(&self, v: Nir) -> Nir {
-        Nir::from_kind(apply_any(self.clone(), v))
+        Nir::from_kind(self.app_to_kind(v))
+    }
+    pub fn app_to_kind(&self, v: Nir) -> NirKind {
+        apply_any(self, v)
     }
 
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
@@ -190,24 +195,24 @@ impl Nir {
                 NirKind::Const(c) => ExprKind::Const(*c),
                 NirKind::BuiltinType(b) => ExprKind::Builtin(*b),
                 NirKind::Num(l) => ExprKind::Num(l.clone()),
-                NirKind::OptionalType(t) => ExprKind::App(
+                NirKind::OptionalType(t) => ExprKind::Op(OpKind::App(
                     Nir::from_builtin(Builtin::Optional).to_hir(venv),
                     t.to_hir(venv),
-                ),
-                NirKind::EmptyOptionalLit(n) => ExprKind::App(
+                )),
+                NirKind::EmptyOptionalLit(n) => ExprKind::Op(OpKind::App(
                     Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
                     n.to_hir(venv),
-                ),
+                )),
                 NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
-                NirKind::ListType(t) => ExprKind::App(
+                NirKind::ListType(t) => ExprKind::Op(OpKind::App(
                     Nir::from_builtin(Builtin::List).to_hir(venv),
                     t.to_hir(venv),
-                ),
+                )),
                 NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
-                    HirKind::Expr(ExprKind::App(
+                    HirKind::Expr(ExprKind::Op(OpKind::App(
                         Nir::from_builtin(Builtin::List).to_hir(venv),
                         n.to_hir(venv),
-                    )),
+                    ))),
                     Span::Artificial,
                 )),
                 NirKind::NEListLit(elts) => ExprKind::NEListLit(
@@ -229,32 +234,35 @@ impl Nir {
                         .collect(),
                 ),
                 NirKind::UnionType(kts) => map_uniontype(kts),
-                NirKind::UnionConstructor(l, kts) => ExprKind::Field(
-                    Hir::new(
-                        HirKind::Expr(map_uniontype(kts)),
-                        Span::Artificial,
-                    ),
-                    l.clone(),
-                ),
-                NirKind::UnionLit(l, v, kts) => ExprKind::App(
+                NirKind::UnionConstructor(l, kts) => {
+                    ExprKind::Op(OpKind::Field(
+                        Hir::new(
+                            HirKind::Expr(map_uniontype(kts)),
+                            Span::Artificial,
+                        ),
+                        l.clone(),
+                    ))
+                }
+                NirKind::UnionLit(l, v, kts) => ExprKind::Op(OpKind::App(
                     Hir::new(
-                        HirKind::Expr(ExprKind::Field(
+                        HirKind::Expr(ExprKind::Op(OpKind::Field(
                             Hir::new(
                                 HirKind::Expr(map_uniontype(kts)),
                                 Span::Artificial,
                             ),
                             l.clone(),
-                        )),
+                        ))),
                         Span::Artificial,
                     ),
                     v.to_hir(venv),
-                ),
-                NirKind::Equivalence(x, y) => ExprKind::BinOp(
+                )),
+                NirKind::Equivalence(x, y) => ExprKind::Op(OpKind::BinOp(
                     BinOp::Equivalence,
                     x.to_hir(venv),
                     y.to_hir(venv),
-                ),
-                NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+                )),
+                NirKind::Assert(x) => ExprKind::Assert(x.to_hir(venv)),
+                NirKind::Op(e) => ExprKind::Op(e.map_ref(|v| v.to_hir(venv))),
             }),
         };
 
@@ -307,7 +315,7 @@ impl Thunk {
     }
     fn eval(self) -> NirKind {
         match self {
-            Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
+            Thunk::Thunk { env, body } => normalize_hir(&env, &body),
             Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
         }
     }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 570e106..d042f3f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -1,18 +1,18 @@
-use itertools::Itertools;
 use std::collections::HashMap;
 
+use crate::operations::{normalize_operation, OpKind};
 use crate::semantics::NzEnv;
 use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
-use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind};
+use crate::syntax::{ExprKind, InterpolatedTextContents};
 
-pub fn apply_any(f: Nir, a: Nir) -> NirKind {
+pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
     match f.kind() {
         NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
         NirKind::AppliedBuiltin(closure) => closure.apply(a),
         NirKind::UnionConstructor(l, kts) => {
             NirKind::UnionLit(l.clone(), a, kts.clone())
         }
-        _ => NirKind::PartialExpr(ExprKind::App(f, a)),
+        _ => NirKind::Op(OpKind::App(f.clone(), a)),
     }
 }
 
@@ -81,393 +81,83 @@ where
     kvs
 }
 
-// Small helper enum to avoid repetition
-enum Ret<'a> {
-    NirKind(NirKind),
-    Nir(Nir),
-    NirRef(&'a Nir),
-    Expr(ExprKind<Nir>),
-}
-
-fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
-    use BinOp::{
-        BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
-        NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
-        RightBiasedRecordMerge, TextAppend,
-    };
-    use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
-    use NumKind::{Bool, Natural};
-
-    Some(match (o, x.kind(), y.kind()) {
-        (BoolAnd, Num(Bool(true)), _) => Ret::NirRef(y),
-        (BoolAnd, _, Num(Bool(true))) => Ret::NirRef(x),
-        (BoolAnd, Num(Bool(false)), _) => Ret::NirKind(Num(Bool(false))),
-        (BoolAnd, _, Num(Bool(false))) => Ret::NirKind(Num(Bool(false))),
-        (BoolAnd, _, _) if x == y => Ret::NirRef(x),
-        (BoolOr, Num(Bool(true)), _) => Ret::NirKind(Num(Bool(true))),
-        (BoolOr, _, Num(Bool(true))) => Ret::NirKind(Num(Bool(true))),
-        (BoolOr, Num(Bool(false)), _) => Ret::NirRef(y),
-        (BoolOr, _, Num(Bool(false))) => Ret::NirRef(x),
-        (BoolOr, _, _) if x == y => Ret::NirRef(x),
-        (BoolEQ, Num(Bool(true)), _) => Ret::NirRef(y),
-        (BoolEQ, _, Num(Bool(true))) => Ret::NirRef(x),
-        (BoolEQ, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x == y))),
-        (BoolEQ, _, _) if x == y => Ret::NirKind(Num(Bool(true))),
-        (BoolNE, Num(Bool(false)), _) => Ret::NirRef(y),
-        (BoolNE, _, Num(Bool(false))) => Ret::NirRef(x),
-        (BoolNE, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x != y))),
-        (BoolNE, _, _) if x == y => Ret::NirKind(Num(Bool(false))),
-
-        (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y),
-        (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x),
-        (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => {
-            Ret::NirKind(Num(Natural(x + y)))
-        }
-        (NaturalTimes, Num(Natural(0)), _) => Ret::NirKind(Num(Natural(0))),
-        (NaturalTimes, _, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))),
-        (NaturalTimes, Num(Natural(1)), _) => Ret::NirRef(y),
-        (NaturalTimes, _, Num(Natural(1))) => Ret::NirRef(x),
-        (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => {
-            Ret::NirKind(Num(Natural(x * y)))
-        }
-
-        (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
-        (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x),
-        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit(
-            xs.iter().chain(ys.iter()).cloned().collect(),
-        )),
-
-        (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y),
-        (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x),
-        (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
-            Ret::NirKind(NirKind::TextLit(x.concat(y)))
-        }
-        (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit(
-            x.concat(&TextLit::interpolate(y.clone())),
-        )),
-        (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit(
-            TextLit::interpolate(x.clone()).concat(y),
-        )),
+pub type Ret = NirKind;
 
-        (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::NirRef(x)
-        }
-        (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::NirRef(y)
-        }
-        (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let mut kvs = kvs2.clone();
-            for (x, v) in kvs1 {
-                // Insert only if key not already present
-                kvs.entry(x.clone()).or_insert_with(|| v.clone());
-            }
-            Ret::NirKind(RecordLit(kvs))
-        }
-        (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y),
-
-        (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::NirRef(x)
-        }
-        (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::NirRef(y)
-        }
-        (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| {
-                Nir::from_partial_expr(ExprKind::BinOp(
-                    RecursiveRecordMerge,
-                    v1.clone(),
-                    v2.clone(),
-                ))
-            });
-            Ret::NirKind(RecordLit(kvs))
-        }
-
-        (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
-            let kts = merge_maps(
-                kts_x,
-                kts_y,
-                // If the Label exists for both records, then we hit the recursive case.
-                |_, l: &Nir, r: &Nir| {
-                    Nir::from_partial_expr(ExprKind::BinOp(
-                        RecursiveRecordTypeMerge,
-                        l.clone(),
-                        r.clone(),
-                    ))
-                },
-            );
-            Ret::NirKind(RecordType(kts))
-        }
-
-        (Equivalence, _, _) => {
-            Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone()))
-        }
-
-        _ => return None,
-    })
+pub fn ret_nir(x: Nir) -> Ret {
+    ret_ref(&x)
+}
+pub fn ret_kind(x: NirKind) -> Ret {
+    x
+}
+pub fn ret_ref(x: &Nir) -> Ret {
+    x.kind().clone()
+}
+pub fn ret_op(x: OpKind<Nir>) -> Ret {
+    NirKind::Op(x)
 }
 
-#[allow(clippy::cognitive_complexity)]
 pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
     use NirKind::{
-        EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num,
-        PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+        Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType,
         UnionType,
     };
-    use NumKind::Bool;
 
-    let ret = match expr {
-        ExprKind::Import(..) | ExprKind::Completion(..) => {
-            unreachable!("This case should have been handled in resolution")
-        }
+    match expr {
         ExprKind::Var(..)
         | ExprKind::Lam(..)
         | ExprKind::Pi(..)
-        | ExprKind::Let(..) => unreachable!(
-            "This case should have been handled in normalize_hir_whnf"
-        ),
+        | ExprKind::Let(..) => {
+            unreachable!("This case should have been handled in normalize_hir")
+        }
 
-        ExprKind::Annot(x, _) => Ret::Nir(x),
-        ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)),
-        ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
-        ExprKind::Assert(_) => Ret::Expr(expr),
-        ExprKind::App(v, a) => Ret::Nir(v.app(a)),
-        ExprKind::Num(l) => Ret::NirKind(Num(l)),
-        ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
+        ExprKind::Const(c) => ret_kind(Const(c)),
+        ExprKind::Num(l) => ret_kind(Num(l)),
+        ExprKind::Builtin(b) => {
+            ret_kind(NirKind::from_builtin_env(b, env.clone()))
+        }
+        ExprKind::TextLit(elts) => {
+            let tlit = TextLit::new(elts.into_iter());
+            // Simplify bare interpolation
+            if let Some(v) = tlit.as_single_expr() {
+                ret_ref(v)
+            } else {
+                ret_kind(NirKind::TextLit(tlit))
+            }
+        }
+        ExprKind::SomeLit(e) => ret_kind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match t.kind() {
                 NirKind::ListType(t) => t.clone(),
                 _ => panic!("internal type error"),
             };
-            Ret::NirKind(NirKind::EmptyListLit(arg))
+            ret_kind(NirKind::EmptyListLit(arg))
         }
         ExprKind::NEListLit(elts) => {
-            Ret::NirKind(NEListLit(elts.into_iter().collect()))
+            ret_kind(NEListLit(elts.into_iter().collect()))
         }
         ExprKind::RecordLit(kvs) => {
-            Ret::NirKind(RecordLit(kvs.into_iter().collect()))
+            ret_kind(RecordLit(kvs.into_iter().collect()))
         }
         ExprKind::RecordType(kvs) => {
-            Ret::NirKind(RecordType(kvs.into_iter().collect()))
+            ret_kind(RecordType(kvs.into_iter().collect()))
         }
         ExprKind::UnionType(kvs) => {
-            Ret::NirKind(UnionType(kvs.into_iter().collect()))
-        }
-        ExprKind::TextLit(elts) => {
-            let tlit = TextLit::new(elts.into_iter());
-            // Simplify bare interpolation
-            if let Some(v) = tlit.as_single_expr() {
-                Ret::Nir(v.clone())
-            } else {
-                Ret::NirKind(NirKind::TextLit(tlit))
-            }
-        }
-        ExprKind::BoolIf(ref b, ref e1, ref e2) => {
-            match b.kind() {
-                Num(Bool(true)) => Ret::NirRef(e1),
-                Num(Bool(false)) => Ret::NirRef(e2),
-                _ => {
-                    match (e1.kind(), e2.kind()) {
-                        // Simplify `if b then True else False`
-                        (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b),
-                        _ if e1 == e2 => Ret::NirRef(e1),
-                        _ => Ret::Expr(expr),
-                    }
-                }
-            }
-        }
-        ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
-            Some(ret) => ret,
-            None => Ret::Expr(expr),
-        },
-
-        ExprKind::Field(ref v, ref field) => match v.kind() {
-            RecordLit(kvs) => match kvs.get(field) {
-                Some(r) => Ret::Nir(r.clone()),
-                None => Ret::Expr(expr),
-            },
-            UnionType(kts) => {
-                Ret::NirKind(UnionConstructor(field.clone(), kts.clone()))
-            }
-            PartialExpr(ExprKind::Projection(x, _)) => {
-                return normalize_one_layer(
-                    ExprKind::Field(x.clone(), field.clone()),
-                    env,
-                )
-            }
-            PartialExpr(ExprKind::BinOp(
-                BinOp::RightBiasedRecordMerge,
-                x,
-                y,
-            )) => match (x.kind(), y.kind()) {
-                (_, RecordLit(kvs)) => match kvs.get(field) {
-                    Some(r) => Ret::Nir(r.clone()),
-                    None => {
-                        return normalize_one_layer(
-                            ExprKind::Field(x.clone(), field.clone()),
-                            env,
-                        )
-                    }
-                },
-                (RecordLit(kvs), _) => match kvs.get(field) {
-                    Some(r) => Ret::Expr(ExprKind::Field(
-                        Nir::from_kind(PartialExpr(ExprKind::BinOp(
-                            BinOp::RightBiasedRecordMerge,
-                            Nir::from_kind(RecordLit(
-                                Some((field.clone(), r.clone()))
-                                    .into_iter()
-                                    .collect(),
-                            )),
-                            y.clone(),
-                        ))),
-                        field.clone(),
-                    )),
-                    None => {
-                        return normalize_one_layer(
-                            ExprKind::Field(y.clone(), field.clone()),
-                            env,
-                        )
-                    }
-                },
-                _ => Ret::Expr(expr),
-            },
-            PartialExpr(ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => {
-                match (x.kind(), y.kind()) {
-                    (RecordLit(kvs), _) => match kvs.get(field) {
-                        Some(r) => Ret::Expr(ExprKind::Field(
-                            Nir::from_kind(PartialExpr(ExprKind::BinOp(
-                                BinOp::RecursiveRecordMerge,
-                                Nir::from_kind(RecordLit(
-                                    Some((field.clone(), r.clone()))
-                                        .into_iter()
-                                        .collect(),
-                                )),
-                                y.clone(),
-                            ))),
-                            field.clone(),
-                        )),
-                        None => {
-                            return normalize_one_layer(
-                                ExprKind::Field(y.clone(), field.clone()),
-                                env,
-                            )
-                        }
-                    },
-                    (_, RecordLit(kvs)) => match kvs.get(field) {
-                        Some(r) => Ret::Expr(ExprKind::Field(
-                            Nir::from_kind(PartialExpr(ExprKind::BinOp(
-                                BinOp::RecursiveRecordMerge,
-                                x.clone(),
-                                Nir::from_kind(RecordLit(
-                                    Some((field.clone(), r.clone()))
-                                        .into_iter()
-                                        .collect(),
-                                )),
-                            ))),
-                            field.clone(),
-                        )),
-                        None => {
-                            return normalize_one_layer(
-                                ExprKind::Field(x.clone(), field.clone()),
-                                env,
-                            )
-                        }
-                    },
-                    _ => Ret::Expr(expr),
-                }
-            }
-            _ => Ret::Expr(expr),
-        },
-        ExprKind::Projection(_, ref ls) if ls.is_empty() => {
-            Ret::NirKind(RecordLit(HashMap::new()))
+            ret_kind(UnionType(kvs.into_iter().collect()))
         }
-        ExprKind::Projection(ref v, ref ls) => match v.kind() {
-            RecordLit(kvs) => Ret::NirKind(RecordLit(
-                ls.iter()
-                    .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
-                    .collect(),
-            )),
-            PartialExpr(ExprKind::Projection(v2, _)) => {
-                return normalize_one_layer(
-                    ExprKind::Projection(v2.clone(), ls.clone()),
-                    env,
-                )
-            }
-            _ => Ret::Expr(expr),
-        },
-        ExprKind::ProjectionByExpr(ref v, ref t) => match t.kind() {
-            RecordType(kts) => {
-                return normalize_one_layer(
-                    ExprKind::Projection(
-                        v.clone(),
-                        kts.keys().cloned().collect(),
-                    ),
-                    env,
-                )
-            }
-            _ => Ret::Expr(expr),
-        },
-
-        ExprKind::Merge(ref handlers, ref variant, _) => {
-            match handlers.kind() {
-                RecordLit(kvs) => match variant.kind() {
-                    UnionConstructor(l, _) => match kvs.get(l) {
-                        Some(h) => Ret::Nir(h.clone()),
-                        None => Ret::Expr(expr),
-                    },
-                    UnionLit(l, v, _) => match kvs.get(l) {
-                        Some(h) => Ret::Nir(h.app(v.clone())),
-                        None => Ret::Expr(expr),
-                    },
-                    EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
-                        Some(h) => Ret::Nir(h.clone()),
-                        None => Ret::Expr(expr),
-                    },
-                    NEOptionalLit(v) => match kvs.get(&"Some".into()) {
-                        Some(h) => Ret::Nir(h.app(v.clone())),
-                        None => Ret::Expr(expr),
-                    },
-                    _ => Ret::Expr(expr),
-                },
-                _ => Ret::Expr(expr),
-            }
+        ExprKind::Op(ref op) => normalize_operation(op),
+        ExprKind::Annot(x, _) => ret_nir(x),
+        ExprKind::Assert(x) => ret_kind(Assert(x)),
+        ExprKind::Import(..) => {
+            unreachable!("This case should have been handled in resolution")
         }
-        ExprKind::ToMap(ref v, ref annot) => match v.kind() {
-            RecordLit(kvs) if kvs.is_empty() => {
-                match annot.as_ref().map(|v| v.kind()) {
-                    Some(NirKind::ListType(t)) => {
-                        Ret::NirKind(EmptyListLit(t.clone()))
-                    }
-                    _ => Ret::Expr(expr),
-                }
-            }
-            RecordLit(kvs) => Ret::NirKind(NEListLit(
-                kvs.iter()
-                    .sorted_by_key(|(k, _)| *k)
-                    .map(|(k, v)| {
-                        let mut rec = HashMap::new();
-                        rec.insert("mapKey".into(), Nir::from_text(k));
-                        rec.insert("mapValue".into(), v.clone());
-                        Nir::from_kind(NirKind::RecordLit(rec))
-                    })
-                    .collect(),
-            )),
-            _ => Ret::Expr(expr),
-        },
-    };
-
-    match ret {
-        Ret::NirKind(v) => v,
-        Ret::Nir(v) => v.kind().clone(),
-        Ret::NirRef(v) => v.kind().clone(),
-        Ret::Expr(expr) => NirKind::PartialExpr(expr),
     }
 }
 
 /// Normalize Hir into WHNF
-pub fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
+pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind {
     match hir.kind() {
         HirKind::Var(var) => env.lookup_val(*var),
-        HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
+        HirKind::Import(hir, _) => normalize_hir(env, hir),
         HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
             NirKind::LamClosure {
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 6e50fa6..e96f16b 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -1,17 +1,19 @@
 use itertools::Itertools;
 use std::borrow::Cow;
+use std::collections::BTreeMap;
 use std::env;
 use std::path::PathBuf;
 use url::Url;
 
+use crate::builtins::Builtin;
 use crate::error::ErrorBuilder;
 use crate::error::{Error, ImportError};
+use crate::operations::{BinOp, OpKind};
 use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
 use crate::syntax;
-use crate::syntax::map::DupTreeMap;
 use crate::syntax::{
-    BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode,
-    ImportTarget, Span, UnspannedExpr, URL,
+    Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span,
+    UnspannedExpr, URL,
 };
 use crate::{Parsed, Resolved};
 
@@ -179,12 +181,13 @@ impl ImportLocation {
         };
 
         let asloc_ty = make_aslocation_uniontype();
-        let expr = mkexpr(ExprKind::Field(asloc_ty, field_name.into()));
+        let expr =
+            mkexpr(ExprKind::Op(OpKind::Field(asloc_ty, field_name.into())));
         match arg {
-            Some(arg) => mkexpr(ExprKind::App(
+            Some(arg) => mkexpr(ExprKind::Op(OpKind::App(
                 expr,
                 mkexpr(ExprKind::TextLit(arg.into())),
-            )),
+            ))),
             None => expr,
         }
     }
@@ -196,7 +199,7 @@ fn mkexpr(kind: UnspannedExpr) -> Expr {
 
 fn make_aslocation_uniontype() -> Expr {
     let text_type = mkexpr(ExprKind::Builtin(Builtin::Text));
-    let mut union = DupTreeMap::default();
+    let mut union = BTreeMap::default();
     union.insert("Local".into(), Some(text_type.clone()));
     union.insert("Remote".into(), Some(text_type.clone()));
     union.insert("Environment".into(), Some(text_type));
@@ -261,21 +264,21 @@ fn resolve_one_import(
 /// Desugar the first level of the expression.
 fn desugar(expr: &Expr) -> Cow<'_, Expr> {
     match expr.kind() {
-        ExprKind::Completion(ty, compl) => {
+        ExprKind::Op(OpKind::Completion(ty, compl)) => {
             let ty_field_default = Expr::new(
-                ExprKind::Field(ty.clone(), "default".into()),
+                ExprKind::Op(OpKind::Field(ty.clone(), "default".into())),
                 expr.span(),
             );
             let merged = Expr::new(
-                ExprKind::BinOp(
+                ExprKind::Op(OpKind::BinOp(
                     BinOp::RightBiasedRecordMerge,
                     ty_field_default,
                     compl.clone(),
-                ),
+                )),
                 expr.span(),
             );
             let ty_field_type = Expr::new(
-                ExprKind::Field(ty.clone(), "Type".into()),
+                ExprKind::Op(OpKind::Field(ty.clone(), "Type".into())),
                 expr.span(),
             );
             Cow::Owned(Expr::new(
@@ -304,7 +307,7 @@ fn traverse_resolve_expr(
                     .format(),
             )?,
         },
-        ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
+        ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => {
             match traverse_resolve_expr(name_env, l, f) {
                 Ok(l) => l,
                 Err(_) => {
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 89a8027..ec15a1f 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,6 +1,7 @@
+use crate::builtins::Builtin;
 use crate::error::{ErrorBuilder, TypeError};
 use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
-use crate::syntax::{Builtin, Const, Expr, Span};
+use crate::syntax::{Const, Expr, Span};
 
 /// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index c3334b5..361e1b4 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,49 +1,10 @@
-use std::borrow::Cow;
 use std::cmp::max;
-use std::collections::HashMap;
 
+use crate::builtins::{type_of_builtin, Builtin};
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
-use crate::semantics::merge_maps;
-use crate::semantics::{
-    type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv,
-    Type,
-};
-use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span,
-};
-
-fn check_rectymerge(
-    span: &Span,
-    env: &TyEnv,
-    x: Nir,
-    y: Nir,
-) -> Result<(), TypeError> {
-    let kts_x = match x.kind() {
-        NirKind::RecordType(kts) => kts,
-        _ => {
-            return mk_span_err(
-                span.clone(),
-                "RecordTypeMergeRequiresRecordType",
-            )
-        }
-    };
-    let kts_y = match y.kind() {
-        NirKind::RecordType(kts) => kts,
-        _ => {
-            return mk_span_err(
-                span.clone(),
-                "RecordTypeMergeRequiresRecordType",
-            )
-        }
-    };
-    for (k, tx) in kts_x {
-        if let Some(ty) = kts_y.get(k) {
-            // TODO: store Type in RecordType ?
-            check_rectymerge(span, env, tx.clone(), ty.clone())?;
-        }
-    }
-    Ok(())
-}
+use crate::operations::typecheck_operation;
+use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
+use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span};
 
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
@@ -74,8 +35,8 @@ fn type_one_layer(
 ) -> Result<Type, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
-    let ty = match &ekind {
-        ExprKind::Import(..) | ExprKind::Completion(..) => {
+    Ok(match &ekind {
+        ExprKind::Import(..) => {
             unreachable!("This case should have been handled in resolution")
         }
         ExprKind::Var(..)
@@ -89,20 +50,16 @@ fn type_one_layer(
 
         ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
+        ExprKind::Num(num) => Type::from_builtin(match num {
+            NumKind::Bool(_) => Builtin::Bool,
+            NumKind::Natural(_) => Builtin::Natural,
+            NumKind::Integer(_) => Builtin::Integer,
+            NumKind::Double(_) => Builtin::Double,
+        }),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
             typecheck(&t_hir)?.eval_to_type(env)?
         }
-        ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
-        ExprKind::Num(NumKind::Natural(_)) => {
-            Type::from_builtin(Builtin::Natural)
-        }
-        ExprKind::Num(NumKind::Integer(_)) => {
-            Type::from_builtin(Builtin::Integer)
-        }
-        ExprKind::Num(NumKind::Double(_)) => {
-            Type::from_builtin(Builtin::Double)
-        }
         ExprKind::TextLit(interpolated) => {
             let text_type = Type::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
@@ -115,6 +72,16 @@ fn type_one_layer(
             }
             text_type
         }
+        ExprKind::SomeLit(x) => {
+            if x.ty().ty().as_const() != Some(Const::Type) {
+                return span_err("InvalidOptionalType");
+            }
+
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::Optional)
+                .app(t)
+                .to_type(Const::Type)
+        }
         ExprKind::EmptyListLit(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
@@ -138,82 +105,56 @@ fn type_one_layer(
             let t = x.ty().to_nir();
             Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
         }
-        ExprKind::SomeLit(x) => {
-            if x.ty().ty().as_const() != Some(Const::Type) {
-                return span_err("InvalidOptionalType");
-            }
-
-            let t = x.ty().to_nir();
-            Nir::from_builtin(Builtin::Optional)
-                .app(t)
-                .to_type(Const::Type)
-        }
         ExprKind::RecordLit(kvs) => {
-            use std::collections::hash_map::Entry;
-            let mut kts = HashMap::new();
             // An empty record type has type Type
             let mut k = Const::Type;
-            for (x, v) in kvs {
-                // Check for duplicated entries
-                match kts.entry(x.clone()) {
-                    Entry::Occupied(_) => {
-                        return span_err("RecordTypeDuplicateField")
-                    }
-                    Entry::Vacant(e) => e.insert(v.ty().to_nir()),
-                };
-
+            for v in kvs.values() {
                 // Check that the fields have a valid kind
                 match v.ty().ty().as_const() {
                     Some(c) => k = max(k, c),
-                    None => return span_err("InvalidFieldType"),
+                    None => return mk_span_err(v.span(), "InvalidFieldType"),
                 }
             }
 
+            let kts = kvs
+                .iter()
+                .map(|(x, v)| (x.clone(), v.ty().to_nir()))
+                .collect();
+
             Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
         }
         ExprKind::RecordType(kts) => {
-            use std::collections::hash_map::Entry;
-            let mut seen_fields = HashMap::new();
             // An empty record type has type Type
             let mut k = Const::Type;
-
-            for (x, t) in kts {
-                // Check for duplicated entries
-                match seen_fields.entry(x.clone()) {
-                    Entry::Occupied(_) => {
-                        return span_err("RecordTypeDuplicateField")
-                    }
-                    Entry::Vacant(e) => e.insert(()),
-                };
-
+            for t in kts.values() {
                 // Check the type is a Const and compute final type
                 match t.ty().as_const() {
                     Some(c) => k = max(k, c),
-                    None => return span_err("InvalidFieldType"),
+                    None => return mk_span_err(t.span(), "InvalidFieldType"),
                 }
             }
 
             Type::from_const(k)
         }
         ExprKind::UnionType(kts) => {
-            use std::collections::hash_map::Entry;
-            let mut seen_fields = HashMap::new();
             // Check that all types are the same const
             let mut k = None;
-            for (x, t) in kts {
+            for t in kts.values() {
                 if let Some(t) = t {
-                    match (k, t.ty().as_const()) {
-                        (None, Some(k2)) => k = Some(k2),
-                        (Some(k1), Some(k2)) if k1 == k2 => {}
-                        _ => return span_err("InvalidFieldType"),
+                    let c = match t.ty().as_const() {
+                        Some(c) => c,
+                        None => {
+                            return mk_span_err(t.span(), "InvalidVariantType")
+                        }
+                    };
+                    match k {
+                        None => k = Some(c),
+                        Some(k) if k == c => {}
+                        _ => {
+                            return mk_span_err(t.span(), "InvalidVariantType")
+                        }
                     }
                 }
-                match seen_fields.entry(x) {
-                    Entry::Occupied(_) => {
-                        return span_err("UnionTypeDuplicateField")
-                    }
-                    Entry::Vacant(e) => e.insert(()),
-                };
             }
 
             // An empty union type has type Type;
@@ -222,36 +163,7 @@ fn type_one_layer(
 
             Type::from_const(k)
         }
-        ExprKind::Field(scrut, x) => {
-            match scrut.ty().kind() {
-                NirKind::RecordType(kts) => match kts.get(&x) {
-                    Some(val) => Type::new_infer_universe(env, val.clone())?,
-                    None => return span_err("MissingRecordField"),
-                },
-                NirKind::Const(_) => {
-                    let scrut = scrut.eval_to_type(env)?;
-                    match scrut.kind() {
-                        NirKind::UnionType(kts) => match kts.get(x) {
-                            // Constructor has type T -> < x: T, ... >
-                            Some(Some(ty)) => {
-                                Nir::from_kind(NirKind::PiClosure {
-                                    binder: Binder::new(x.clone()),
-                                    annot: ty.clone(),
-                                    closure: Closure::new_constant(
-                                        scrut.to_nir(),
-                                    ),
-                                })
-                                .to_type(scrut.ty())
-                            }
-                            Some(None) => scrut,
-                            None => return span_err("MissingUnionField"),
-                        },
-                        _ => return span_err("NotARecord"),
-                    }
-                }
-                _ => return span_err("NotARecord"),
-            }
-        }
+        ExprKind::Op(op) => typecheck_operation(env, span, op)?,
         ExprKind::Assert(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
@@ -261,430 +173,13 @@ fn type_one_layer(
             }
             t
         }
-        ExprKind::App(f, arg) => {
-            match f.ty().kind() {
-                // TODO: store Type in closure
-                NirKind::PiClosure { annot, closure, .. } => {
-                    if arg.ty().as_nir() != annot {
-                        return mkerr(
-                            ErrorBuilder::new(format!(
-                                "wrong type of function argument"
-                            ))
-                            .span_err(
-                                f.span(),
-                                format!(
-                                    "this expects an argument of type: {}",
-                                    annot.to_expr_tyenv(env),
-                                ),
-                            )
-                            .span_err(
-                                arg.span(),
-                                format!(
-                                    "but this has type: {}",
-                                    arg.ty().to_expr_tyenv(env),
-                                ),
-                            )
-                            .note(format!(
-                                "expected type `{}`\n   found type `{}`",
-                                annot.to_expr_tyenv(env),
-                                arg.ty().to_expr_tyenv(env),
-                            ))
-                            .format(),
-                        );
-                    }
-
-                    let arg_nf = arg.eval(env);
-                    Type::new_infer_universe(env, closure.apply(arg_nf))?
-                }
-                _ => return mkerr(
-                    ErrorBuilder::new(format!(
-                        "expected function, found `{}`",
-                        f.ty().to_expr_tyenv(env)
-                    ))
-                    .span_err(
-                        f.span(),
-                        format!("function application requires a function",),
-                    )
-                    .format(),
-                ),
-            }
-        }
-        ExprKind::BoolIf(x, y, z) => {
-            if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
-                return span_err("InvalidPredicate");
-            }
-            if y.ty().ty().as_const() != Some(Const::Type) {
-                return span_err("IfBranchMustBeTerm");
-            }
-            if y.ty() != z.ty() {
-                return span_err("IfBranchMismatch");
-            }
-
-            y.ty().clone()
-        }
-        ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => {
-            let x_type = x.ty();
-            let y_type = y.ty();
-
-            // Extract the LHS record type
-            let kts_x = match x_type.kind() {
-                NirKind::RecordType(kts) => kts,
-                _ => return span_err("MustCombineRecord"),
-            };
-            // Extract the RHS record type
-            let kts_y = match y_type.kind() {
-                NirKind::RecordType(kts) => kts,
-                _ => return span_err("MustCombineRecord"),
-            };
-
-            // Union the two records, prefering
-            // the values found in the RHS.
-            let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone());
-
-            let u = max(x.ty().ty(), y.ty().ty());
-            Nir::from_kind(NirKind::RecordType(kts)).to_type(u)
-        }
-        ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
-
-            let hir = Hir::new(
-                HirKind::Expr(ExprKind::BinOp(
-                    BinOp::RecursiveRecordTypeMerge,
-                    x.ty().to_hir(env.as_varenv()),
-                    y.ty().to_hir(env.as_varenv()),
-                )),
-                span.clone(),
-            );
-            let x_u = x.ty().ty();
-            let y_u = y.ty().ty();
-            Type::new(hir.eval(env), max(x_u, y_u))
-        }
-        ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
-
-            // A RecordType's type is always a const
-            let xk = x.ty().as_const().unwrap();
-            let yk = y.ty().as_const().unwrap();
-            Type::from_const(max(xk, yk))
-        }
-        ExprKind::BinOp(BinOp::ListAppend, l, r) => {
-            match l.ty().kind() {
-                NirKind::ListType(..) => {}
-                _ => return span_err("BinOpTypeMismatch"),
-            }
-
-            if l.ty() != r.ty() {
-                return span_err("BinOpTypeMismatch");
-            }
-
-            l.ty().clone()
-        }
-        ExprKind::BinOp(BinOp::Equivalence, l, r) => {
-            if l.ty() != r.ty() {
-                return span_err("EquivalenceTypeMismatch");
-            }
-            if l.ty().ty().as_const() != Some(Const::Type) {
-                return span_err("EquivalenceArgumentsMustBeTerms");
-            }
-
-            Type::from_const(Const::Type)
-        }
-        ExprKind::BinOp(o, l, r) => {
-            let t = Type::from_builtin(match o {
-                BinOp::BoolAnd
-                | BinOp::BoolOr
-                | BinOp::BoolEQ
-                | BinOp::BoolNE => Builtin::Bool,
-                BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural,
-                BinOp::TextAppend => Builtin::Text,
-                BinOp::ListAppend
-                | BinOp::RightBiasedRecordMerge
-                | BinOp::RecursiveRecordMerge
-                | BinOp::RecursiveRecordTypeMerge
-                | BinOp::Equivalence => unreachable!(),
-                BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
-            });
-
-            if *l.ty() != t {
-                return span_err("BinOpTypeMismatch");
-            }
-
-            if *r.ty() != t {
-                return span_err("BinOpTypeMismatch");
-            }
-
-            t
-        }
-        ExprKind::Merge(record, union, type_annot) => {
-            let record_type = record.ty();
-            let handlers = match record_type.kind() {
-                NirKind::RecordType(kts) => kts,
-                _ => return span_err("Merge1ArgMustBeRecord"),
-            };
-
-            let union_type = union.ty();
-            let variants = match union_type.kind() {
-                NirKind::UnionType(kts) => Cow::Borrowed(kts),
-                NirKind::OptionalType(ty) => {
-                    let mut kts = HashMap::new();
-                    kts.insert("None".into(), None);
-                    kts.insert("Some".into(), Some(ty.clone()));
-                    Cow::Owned(kts)
-                }
-                _ => return span_err("Merge2ArgMustBeUnionOrOptional"),
-            };
-
-            let mut inferred_type = None;
-            for (x, handler_type) in handlers {
-                let handler_return_type: Type = match variants.get(x) {
-                    // Union alternative with type
-                    Some(Some(variant_type)) => match handler_type.kind() {
-                        NirKind::PiClosure { closure, annot, .. } => {
-                            if variant_type != annot {
-                                return mkerr(
-                                    ErrorBuilder::new(format!(
-                                        "Wrong handler input type"
-                                    ))
-                                    .span_err(
-                                        span,
-                                        format!("in this merge expression",),
-                                    )
-                                    .span_err(
-                                        record.span(),
-                                        format!(
-                                            "the handler for `{}` expects a \
-                                             value of type: `{}`",
-                                            x,
-                                            annot.to_expr_tyenv(env)
-                                        ),
-                                    )
-                                    .span_err(
-                                        union.span(),
-                                        format!(
-                                            "but the corresponding variant \
-                                             has type: `{}`",
-                                            variant_type.to_expr_tyenv(env)
-                                        ),
-                                    )
-                                    .format(),
-                                );
-                            }
-
-                            // TODO: this actually doesn't check anything yet
-                            match closure.remove_binder() {
-                                Ok(v) => {
-                                    Type::new_infer_universe(env, v.clone())?
-                                }
-                                Err(()) => {
-                                    return span_err(
-                                        "MergeReturnTypeIsDependent",
-                                    )
-                                }
-                            }
-                        }
-                        _ => {
-                            return mkerr(
-                                ErrorBuilder::new(format!(
-                                    "merge handler is not a function"
-                                ))
-                                .span_err(
-                                    span,
-                                    format!("in this merge expression"),
-                                )
-                                .span_err(
-                                    record.span(),
-                                    format!(
-                                        "the handler for `{}` has type: `{}`",
-                                        x,
-                                        handler_type.to_expr_tyenv(env)
-                                    ),
-                                )
-                                .span_help(
-                                    union.span(),
-                                    format!(
-                                        "the corresponding variant has type: \
-                                         `{}`",
-                                        variant_type.to_expr_tyenv(env)
-                                    ),
-                                )
-                                .help(format!(
-                                    "a handler for this variant must be a \
-                                     function that takes an input of type: \
-                                     `{}`",
-                                    variant_type.to_expr_tyenv(env)
-                                ))
-                                .format(),
-                            )
-                        }
-                    },
-                    // Union alternative without type
-                    Some(None) => {
-                        Type::new_infer_universe(env, handler_type.clone())?
-                    }
-                    None => return span_err("MergeHandlerMissingVariant"),
-                };
-                match &inferred_type {
-                    None => inferred_type = Some(handler_return_type),
-                    Some(t) => {
-                        if t != &handler_return_type {
-                            return span_err("MergeHandlerTypeMismatch");
-                        }
-                    }
-                }
-            }
-            for x in variants.keys() {
-                if !handlers.contains_key(x) {
-                    return span_err("MergeVariantMissingHandler");
-                }
-            }
-
-            let type_annot = type_annot
-                .as_ref()
-                .map(|t| t.eval_to_type(env))
-                .transpose()?;
-            match (inferred_type, type_annot) {
-                (Some(t1), Some(t2)) => {
-                    if t1 != t2 {
-                        return span_err("MergeAnnotMismatch");
-                    }
-                    t1
-                }
-                (Some(t), None) => t,
-                (None, Some(t)) => t,
-                (None, None) => return span_err("MergeEmptyNeedsAnnotation"),
-            }
-        }
-        ExprKind::ToMap(record, annot) => {
-            if record.ty().ty().as_const() != Some(Const::Type) {
-                return span_err("`toMap` only accepts records of type `Type`");
-            }
-            let record_t = record.ty();
-            let kts = match record_t.kind() {
-                NirKind::RecordType(kts) => kts,
-                _ => {
-                    return span_err("The argument to `toMap` must be a record")
-                }
-            };
-
-            if kts.is_empty() {
-                let annot = if let Some(annot) = annot {
-                    annot
-                } else {
-                    return span_err(
-                        "`toMap` applied to an empty record requires a type \
-                         annotation",
-                    );
-                };
-                let annot_val = annot.eval_to_type(env)?;
-
-                let err_msg = "The type of `toMap x` must be of the form \
-                               `List { mapKey : Text, mapValue : T }`";
-                let arg = match annot_val.kind() {
-                    NirKind::ListType(t) => t,
-                    _ => return span_err(err_msg),
-                };
-                let kts = match arg.kind() {
-                    NirKind::RecordType(kts) => kts,
-                    _ => return span_err(err_msg),
-                };
-                if kts.len() != 2 {
-                    return span_err(err_msg);
-                }
-                match kts.get(&"mapKey".into()) {
-                    Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
-                    _ => return span_err(err_msg),
-                }
-                match kts.get(&"mapValue".into()) {
-                    Some(_) => {}
-                    None => return span_err(err_msg),
-                }
-                annot_val
-            } else {
-                let entry_type = kts.iter().next().unwrap().1.clone();
-                for (_, t) in kts.iter() {
-                    if *t != entry_type {
-                        return span_err(
-                            "Every field of the record must have the same type",
-                        );
-                    }
-                }
-
-                let mut kts = HashMap::new();
-                kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
-                kts.insert("mapValue".into(), entry_type);
-                let output_type: Type = Nir::from_builtin(Builtin::List)
-                    .app(Nir::from_kind(NirKind::RecordType(kts)))
-                    .to_type(Const::Type);
-                if let Some(annot) = annot {
-                    let annot_val = annot.eval_to_type(env)?;
-                    if output_type != annot_val {
-                        return span_err("Annotation mismatch");
-                    }
-                }
-                output_type
-            }
-        }
-        ExprKind::Projection(record, labels) => {
-            let record_type = record.ty();
-            let kts = match record_type.kind() {
-                NirKind::RecordType(kts) => kts,
-                _ => return span_err("ProjectionMustBeRecord"),
-            };
-
-            let mut new_kts = HashMap::new();
-            for l in labels {
-                match kts.get(l) {
-                    None => return span_err("ProjectionMissingEntry"),
-                    Some(t) => {
-                        use std::collections::hash_map::Entry;
-                        match new_kts.entry(l.clone()) {
-                            Entry::Occupied(_) => {
-                                return span_err("ProjectionDuplicateField")
-                            }
-                            Entry::Vacant(e) => e.insert(t.clone()),
-                        }
-                    }
-                };
-            }
-
-            Type::new_infer_universe(
-                env,
-                Nir::from_kind(NirKind::RecordType(new_kts)),
-            )?
-        }
-        ExprKind::ProjectionByExpr(record, selection) => {
-            let record_type = record.ty();
-            let rec_kts = match record_type.kind() {
-                NirKind::RecordType(kts) => kts,
-                _ => return span_err("ProjectionMustBeRecord"),
-            };
-
-            let selection_val = selection.eval_to_type(env)?;
-            let sel_kts = match selection_val.kind() {
-                NirKind::RecordType(kts) => kts,
-                _ => return span_err("ProjectionByExprTakesRecordType"),
-            };
-
-            for (l, sel_ty) in sel_kts {
-                match rec_kts.get(l) {
-                    Some(rec_ty) => {
-                        if rec_ty != sel_ty {
-                            return span_err("ProjectionWrongType");
-                        }
-                    }
-                    None => return span_err("ProjectionMissingEntry"),
-                }
-            }
-
-            selection_val
-        }
-    };
-
-    Ok(ty)
+    })
 }
 
 /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
 /// to compare with.
+// We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use
+// it to handle the annotations in merge/toMap/etc. uniformly.
 pub fn type_with<'hir>(
     env: &TyEnv,
     hir: &'hir Hir,
@@ -780,7 +275,7 @@ pub fn type_with<'hir>(
     Ok(tir)
 }
 
-/// Typecheck an expression and return the expression annotated with types if type-checking
+/// Typecheck an expression and return the expression annotated with its type if type-checking
 /// succeeded, or an error if type-checking failed.
 pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
     type_with(&TyEnv::new(), hir, None)
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 9e935dc..9d216a7 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,8 +1,9 @@
 use std::collections::BTreeMap;
 
+use crate::builtins::Builtin;
 use crate::error::Error;
+use crate::operations::OpKind;
 use crate::semantics::Universe;
-use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::visitor;
 use crate::syntax::*;
 
@@ -36,74 +37,6 @@ impl Const {
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct V(pub Label, pub usize);
 
-// Definition order must match precedence order for
-// pretty-printing to work correctly
-#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum BinOp {
-    /// `x ? y`
-    ImportAlt,
-    /// `x || y`
-    BoolOr,
-    /// `x + y`
-    NaturalPlus,
-    /// `x ++ y`
-    TextAppend,
-    /// `x # y`
-    ListAppend,
-    /// `x && y`
-    BoolAnd,
-    /// `x ∧ y`
-    RecursiveRecordMerge,
-    /// `x ⫽ y`
-    RightBiasedRecordMerge,
-    /// `x ⩓ y`
-    RecursiveRecordTypeMerge,
-    /// `x * y`
-    NaturalTimes,
-    /// `x == y`
-    BoolEQ,
-    /// `x != y`
-    BoolNE,
-    /// x === y
-    Equivalence,
-}
-
-/// Built-ins
-#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
-pub enum Builtin {
-    Bool,
-    Natural,
-    Integer,
-    Double,
-    Text,
-    List,
-    Optional,
-    OptionalNone,
-    NaturalBuild,
-    NaturalFold,
-    NaturalIsZero,
-    NaturalEven,
-    NaturalOdd,
-    NaturalToInteger,
-    NaturalShow,
-    NaturalSubtract,
-    IntegerToDouble,
-    IntegerShow,
-    IntegerNegate,
-    IntegerClamp,
-    DoubleShow,
-    ListBuild,
-    ListFold,
-    ListLength,
-    ListHead,
-    ListLast,
-    ListIndexed,
-    ListReverse,
-    OptionalFold,
-    OptionalBuild,
-    TextShow,
-}
-
 // Each node carries an annotation.
 #[derive(Debug, Clone)]
 pub struct Expr {
@@ -132,57 +65,44 @@ pub enum NumKind {
 // smart pointers.
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum ExprKind<SubExpr> {
+    /// `Type`, `Kind` and `Sort`
     Const(Const),
+    /// Numbers and booleans
     Num(NumKind),
-    ///  `x`
-    ///  `x@n`
-    Var(V),
-    ///  `λ(x : A) -> b`
-    Lam(Label, SubExpr, SubExpr),
-    ///  `A -> B`
-    ///  `∀(x : A) -> B`
-    Pi(Label, SubExpr, SubExpr),
-    ///  `f a`
-    App(SubExpr, SubExpr),
-    ///  `let x     = r in e`
-    ///  `let x : t = r in e`
-    Let(Label, Option<SubExpr>, SubExpr, SubExpr),
-    ///  `x : t`
-    Annot(SubExpr, SubExpr),
-    ///  `assert : t`
-    Assert(SubExpr),
-    /// Built-in values
+    /// Built-in functions and types
     Builtin(Builtin),
-    // Binary operations
-    BinOp(BinOp, SubExpr, SubExpr),
-    ///  `if x then y else z`
-    BoolIf(SubExpr, SubExpr, SubExpr),
     ///  `"Some ${interpolated} text"`
     TextLit(InterpolatedText<SubExpr>),
+    ///  `Some e`
+    SomeLit(SubExpr),
     ///  `[] : t`
     EmptyListLit(SubExpr),
     ///  `[x, y, z]`
     NEListLit(Vec<SubExpr>),
-    ///  `Some e`
-    SomeLit(SubExpr),
     ///  `{ k1 : t1, k2 : t1 }`
-    RecordType(DupTreeMap<Label, SubExpr>),
+    RecordType(BTreeMap<Label, SubExpr>),
     ///  `{ k1 = v1, k2 = v2 }`
     RecordLit(BTreeMap<Label, SubExpr>),
     ///  `< k1 : t1, k2 >`
-    UnionType(DupTreeMap<Label, Option<SubExpr>>),
-    ///  `merge x y : t`
-    Merge(SubExpr, SubExpr, Option<SubExpr>),
-    ///  `toMap x : t`
-    ToMap(SubExpr, Option<SubExpr>),
-    ///  `e.x`
-    Field(SubExpr, Label),
-    ///  `e.{ x, y, z }`
-    Projection(SubExpr, DupTreeSet<Label>),
-    ///  `e.(t)`
-    ProjectionByExpr(SubExpr, SubExpr),
-    ///  `x::y`
-    Completion(SubExpr, SubExpr),
+    UnionType(BTreeMap<Label, Option<SubExpr>>),
+
+    ///  `x`, `x@n`
+    Var(V),
+    ///  `λ(x : A) -> b`
+    Lam(Label, SubExpr, SubExpr),
+    ///  `A -> B`, `∀(x : A) -> B`
+    Pi(Label, SubExpr, SubExpr),
+    ///  `let x : t = r in e`
+    Let(Label, Option<SubExpr>, SubExpr, SubExpr),
+
+    /// Operations
+    Op(OpKind<SubExpr>),
+
+    ///  `x : t`
+    Annot(SubExpr, SubExpr),
+    ///  `assert : t`
+    Assert(SubExpr),
+
     /// `./some/path`
     Import(Import<SubExpr>),
 }
diff --git a/dhall/src/syntax/ast/map.rs b/dhall/src/syntax/ast/map.rs
deleted file mode 100644
index 7a88204..0000000
--- a/dhall/src/syntax/ast/map.rs
+++ /dev/null
@@ -1,282 +0,0 @@
-/// A sorted map that allows multiple values for each key.
-pub use dup_tree_map::DupTreeMap;
-pub use dup_tree_set::DupTreeSet;
-
-mod known_size_iter {
-    pub struct KnownSizeIterator<I> {
-        pub iter: I,
-        pub size: usize,
-    }
-
-    impl<I: Iterator> Iterator for KnownSizeIterator<I> {
-        type Item = I::Item;
-
-        fn next(&mut self) -> Option<Self::Item> {
-            let next = self.iter.next();
-            if next.is_some() {
-                self.size -= 1;
-            }
-            next
-        }
-
-        fn size_hint(&self) -> (usize, Option<usize>) {
-            (self.size, Some(self.size))
-        }
-    }
-
-    // unsafe impl<I: Iterator> iter::TrustedLen for KnownSizeIterator<I> {}
-}
-
-mod tuple {
-    mod sealed {
-        pub trait Sealed {}
-    }
-    pub trait Tuple: sealed::Sealed {
-        type First;
-        type Second;
-    }
-    impl<A, B> sealed::Sealed for (A, B) {}
-    impl<A, B> Tuple for (A, B) {
-        type First = A;
-        type Second = B;
-    }
-}
-
-mod dup_tree_map {
-    use super::known_size_iter::KnownSizeIterator;
-    use super::tuple::Tuple;
-    use smallvec::SmallVec;
-    use std::collections::BTreeMap;
-    use std::iter;
-
-    type OneOrMore<V> = SmallVec<[V; 1]>;
-    type DupTreeMapInternal<K, V> = BTreeMap<K, OneOrMore<V>>;
-
-    #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-    pub struct DupTreeMap<K, V> {
-        map: DupTreeMapInternal<K, V>,
-        size: usize,
-    }
-
-    // Generic types and functions to construct the iterators for this struct.
-    type ZipRepeatIter<T> = iter::Zip<
-        iter::Repeat<<T as Tuple>::First>,
-        <<T as Tuple>::Second as IntoIterator>::IntoIter,
-    >;
-    type DupTreeMapIter<M> = KnownSizeIterator<
-        iter::FlatMap<
-            <M as IntoIterator>::IntoIter,
-            ZipRepeatIter<<M as IntoIterator>::Item>,
-            fn(
-                <M as IntoIterator>::Item,
-            ) -> ZipRepeatIter<<M as IntoIterator>::Item>,
-        >,
-    >;
-
-    fn zip_repeat<K, I>((k, iter): (K, I)) -> ZipRepeatIter<(K, I)>
-    where
-        K: Clone,
-        I: IntoIterator,
-    {
-        iter::repeat(k).zip(iter.into_iter())
-    }
-
-    fn make_map_iter<M, K, I>(map: M, size: usize) -> DupTreeMapIter<M>
-    where
-        M: IntoIterator<Item = (K, I)>,
-        K: Clone,
-        I: IntoIterator,
-    {
-        KnownSizeIterator {
-            iter: map.into_iter().flat_map(zip_repeat),
-            size,
-        }
-    }
-
-    pub type IterMut<'a, K, V> =
-        DupTreeMapIter<&'a mut DupTreeMapInternal<K, V>>;
-    pub type Iter<'a, K, V> = DupTreeMapIter<&'a DupTreeMapInternal<K, V>>;
-    pub type IntoIter<K, V> = DupTreeMapIter<DupTreeMapInternal<K, V>>;
-
-    impl<K: Ord, V> DupTreeMap<K, V> {
-        pub fn new() -> Self {
-            DupTreeMap {
-                map: BTreeMap::new(),
-                size: 0,
-            }
-        }
-
-        pub fn insert(&mut self, key: K, value: V) {
-            self.map.entry(key).or_default().push(value);
-            self.size += 1;
-        }
-
-        pub fn len(&self) -> usize {
-            self.size
-        }
-        pub fn is_empty(&self) -> bool {
-            self.size == 0
-        }
-
-        pub fn iter(&self) -> Iter<'_, K, V> {
-            make_map_iter(&self.map, self.size)
-        }
-
-        pub fn iter_mut(&mut self) -> IterMut<'_, K, V> {
-            make_map_iter(&mut self.map, self.size)
-        }
-    }
-
-    impl<K, V> Default for DupTreeMap<K, V>
-    where
-        K: Ord,
-    {
-        fn default() -> Self {
-            Self::new()
-        }
-    }
-
-    impl<K, V> IntoIterator for DupTreeMap<K, V>
-    where
-        K: Ord + Clone,
-    {
-        type Item = (K, V);
-        type IntoIter = IntoIter<K, V>;
-
-        fn into_iter(self) -> Self::IntoIter {
-            make_map_iter(self.map, self.size)
-        }
-    }
-
-    impl<'a, K, V> IntoIterator for &'a DupTreeMap<K, V>
-    where
-        K: Ord + 'a,
-        V: 'a,
-    {
-        type Item = (&'a K, &'a V);
-        type IntoIter = Iter<'a, K, V>;
-
-        fn into_iter(self) -> Self::IntoIter {
-            self.iter()
-        }
-    }
-
-    impl<'a, K, V> IntoIterator for &'a mut DupTreeMap<K, V>
-    where
-        K: Ord + 'a,
-        V: 'a,
-    {
-        type Item = (&'a K, &'a mut V);
-        type IntoIter = IterMut<'a, K, V>;
-
-        fn into_iter(self) -> Self::IntoIter {
-            self.iter_mut()
-        }
-    }
-
-    impl<K, V> iter::FromIterator<(K, V)> for DupTreeMap<K, V>
-    where
-        K: Ord,
-    {
-        fn from_iter<T>(iter: T) -> Self
-        where
-            T: IntoIterator<Item = (K, V)>,
-        {
-            let mut map = DupTreeMap::new();
-            for (k, v) in iter {
-                map.insert(k, v);
-            }
-            map
-        }
-    }
-}
-
-mod dup_tree_set {
-    use super::tuple::Tuple;
-    use super::DupTreeMap;
-    use std::iter;
-
-    #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-    pub struct DupTreeSet<K> {
-        map: DupTreeMap<K, ()>,
-    }
-
-    type DupTreeSetIter<M> = iter::Map<
-        <M as IntoIterator>::IntoIter,
-        fn(
-            <M as IntoIterator>::Item,
-        ) -> <<M as IntoIterator>::Item as Tuple>::First,
-    >;
-
-    pub type Iter<'a, K> = DupTreeSetIter<&'a DupTreeMap<K, ()>>;
-    pub type IntoIter<K> = DupTreeSetIter<DupTreeMap<K, ()>>;
-
-    fn drop_second<A, B>((a, _): (A, B)) -> A {
-        a
-    }
-
-    impl<K: Ord> DupTreeSet<K> {
-        pub fn new() -> Self {
-            DupTreeSet {
-                map: DupTreeMap::new(),
-            }
-        }
-
-        pub fn len(&self) -> usize {
-            self.map.len()
-        }
-        pub fn is_empty(&self) -> bool {
-            self.map.is_empty()
-        }
-
-        pub fn iter(&self) -> Iter<'_, K> {
-            self.map.iter().map(drop_second)
-        }
-    }
-
-    impl<K> Default for DupTreeSet<K>
-    where
-        K: Ord,
-    {
-        fn default() -> Self {
-            Self::new()
-        }
-    }
-
-    impl<K> IntoIterator for DupTreeSet<K>
-    where
-        K: Ord + Clone,
-    {
-        type Item = K;
-        type IntoIter = IntoIter<K>;
-
-        fn into_iter(self) -> Self::IntoIter {
-            self.map.into_iter().map(drop_second)
-        }
-    }
-
-    impl<'a, K> IntoIterator for &'a DupTreeSet<K>
-    where
-        K: Ord + 'a,
-    {
-        type Item = &'a K;
-        type IntoIter = Iter<'a, K>;
-
-        fn into_iter(self) -> Self::IntoIter {
-            self.iter()
-        }
-    }
-
-    impl<K> iter::FromIterator<K> for DupTreeSet<K>
-    where
-        K: Ord,
-    {
-        fn from_iter<T>(iter: T) -> Self
-        where
-            T: IntoIterator<Item = K>,
-        {
-            let map = iter.into_iter().map(|k| (k, ())).collect();
-            DupTreeSet { map }
-        }
-    }
-}
diff --git a/dhall/src/syntax/ast/mod.rs b/dhall/src/syntax/ast/mod.rs
index 1950154..c341af7 100644
--- a/dhall/src/syntax/ast/mod.rs
+++ b/dhall/src/syntax/ast/mod.rs
@@ -8,5 +8,4 @@ mod span;
 pub use span::*;
 mod text;
 pub use text::*;
-pub mod map;
 pub mod visitor;
diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index 0a0c5ef..7244d0a 100644
--- a/dhall/src/syntax/ast/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -1,22 +1,13 @@
+use itertools::Itertools;
 use std::iter::FromIterator;
 
 use crate::syntax::*;
 
-fn vec<'a, T, U, Err>(
-    x: &'a [T],
-    f: impl FnMut(&'a T) -> Result<U, Err>,
-) -> Result<Vec<U>, Err> {
-    x.iter().map(f).collect()
-}
-
 fn opt<'a, T, U, Err>(
     x: &'a Option<T>,
     f: impl FnOnce(&'a T) -> Result<U, Err>,
 ) -> Result<Option<U>, Err> {
-    Ok(match x {
-        Some(x) => Some(f(x)?),
-        None => None,
-    })
+    x.as_ref().map(f).transpose()
 }
 
 fn dupmap<'a, SE1, SE2, T, Err>(
@@ -30,27 +21,6 @@ where
     x.into_iter().map(|(k, x)| Ok((k.clone(), f(x)?))).collect()
 }
 
-fn optdupmap<'a, SE1, SE2, T, Err>(
-    x: impl IntoIterator<Item = (&'a Label, &'a Option<SE1>)>,
-    mut f: impl FnMut(&'a SE1) -> Result<SE2, Err>,
-) -> Result<T, Err>
-where
-    SE1: 'a,
-    T: FromIterator<(Label, Option<SE2>)>,
-{
-    x.into_iter()
-        .map(|(k, x)| {
-            Ok((
-                k.clone(),
-                match x {
-                    Some(x) => Some(f(x)?),
-                    None => None,
-                },
-            ))
-        })
-        .collect()
-}
-
 pub fn visit_ref<'a, F, SE1, SE2, Err>(
     input: &'a ExprKind<SE1>,
     mut f: F,
@@ -60,54 +30,44 @@ where
 {
     // Can't use closures because of borrowing rules
     macro_rules! expr {
+        () => {
+            |e| Ok(expr!(e))
+        };
         ($e:expr) => {
-            f(None, $e)
+            f(None, $e)?
         };
         ($l:expr, $e:expr) => {
-            f(Some($l), $e)
+            f(Some($l), $e)?
+        };
+    }
+    macro_rules! opt {
+        () => {
+            |e| Ok(opt!(e))
+        };
+        ($e:expr) => {
+            opt($e, |e| Ok(expr!(e)))?
         };
     }
 
     use crate::syntax::ExprKind::*;
     Ok(match input {
         Var(v) => Var(v.clone()),
-        Lam(l, t, e) => {
-            let t = expr!(t)?;
-            let e = expr!(l, e)?;
-            Lam(l.clone(), t, e)
-        }
-        Pi(l, t, e) => {
-            let t = expr!(t)?;
-            let e = expr!(l, e)?;
-            Pi(l.clone(), t, e)
-        }
-        Let(l, t, a, e) => {
-            let t = opt(t, &mut |e| expr!(e))?;
-            let a = expr!(a)?;
-            let e = expr!(l, e)?;
-            Let(l.clone(), t, a, e)
-        }
-        App(f, a) => App(expr!(f)?, expr!(a)?),
-        Annot(x, t) => Annot(expr!(x)?, expr!(t)?),
+        Lam(l, t, e) => Lam(l.clone(), expr!(t), expr!(l, e)),
+        Pi(l, t, e) => Pi(l.clone(), expr!(t), expr!(l, e)),
+        Let(l, t, a, e) => Let(l.clone(), opt!(t), expr!(a), expr!(l, e)),
         Const(k) => Const(*k),
-        Builtin(v) => Builtin(*v),
         Num(n) => Num(n.clone()),
-        TextLit(t) => TextLit(t.traverse_ref(|e| expr!(e))?),
-        BinOp(o, x, y) => BinOp(*o, expr!(x)?, expr!(y)?),
-        BoolIf(b, t, f) => BoolIf(expr!(b)?, expr!(t)?, expr!(f)?),
-        EmptyListLit(t) => EmptyListLit(expr!(t)?),
-        NEListLit(es) => NEListLit(vec(es, |e| expr!(e))?),
-        SomeLit(e) => SomeLit(expr!(e)?),
-        RecordType(kts) => RecordType(dupmap(kts, |e| expr!(e))?),
-        RecordLit(kvs) => RecordLit(dupmap(kvs, |e| expr!(e))?),
-        UnionType(kts) => UnionType(optdupmap(kts, |e| expr!(e))?),
-        Merge(x, y, t) => Merge(expr!(x)?, expr!(y)?, opt(t, |e| expr!(e))?),
-        ToMap(x, t) => ToMap(expr!(x)?, opt(t, |e| expr!(e))?),
-        Field(e, l) => Field(expr!(e)?, l.clone()),
-        Projection(e, ls) => Projection(expr!(e)?, ls.clone()),
-        ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e)?, expr!(x)?),
-        Completion(e, x) => Completion(expr!(e)?, expr!(x)?),
-        Assert(e) => Assert(expr!(e)?),
-        Import(i) => Import(i.traverse_ref(|e| expr!(e))?),
+        Builtin(v) => Builtin(*v),
+        TextLit(t) => TextLit(t.traverse_ref(expr!())?),
+        SomeLit(e) => SomeLit(expr!(e)),
+        EmptyListLit(t) => EmptyListLit(expr!(t)),
+        NEListLit(es) => NEListLit(es.iter().map(expr!()).try_collect()?),
+        RecordType(kts) => RecordType(dupmap(kts, expr!())?),
+        RecordLit(kvs) => RecordLit(dupmap(kvs, expr!())?),
+        UnionType(kts) => UnionType(dupmap(kts, opt!())?),
+        Op(op) => Op(op.traverse_ref(expr!())?),
+        Annot(x, t) => Annot(expr!(x), expr!(t)),
+        Assert(e) => Assert(expr!(e)),
+        Import(i) => Import(i.traverse_ref(expr!())?),
     })
 }
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index 3c93419..195bd0a 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -3,6 +3,7 @@ use serde_cbor::value::value as cbor;
 use std::iter::FromIterator;
 
 use crate::error::DecodeError;
+use crate::operations::OpKind;
 use crate::syntax;
 use crate::syntax::{
     Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget,
@@ -24,9 +25,12 @@ fn rc(x: UnspannedExpr) -> Expr {
 }
 
 fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
+    use crate::builtins::Builtin;
+    use crate::operations::BinOp;
     use cbor::Value::*;
-    use syntax::{BinOp, Builtin, Const};
+    use syntax::Const;
     use ExprKind::*;
+    use OpKind::*;
     Ok(rc(match data {
         String(s) => match Builtin::parse(s) {
             Some(b) => ExprKind::Builtin(b),
@@ -66,7 +70,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
                 let mut f = cbor_value_to_dhall(&f)?;
                 for a in args {
                     let a = cbor_value_to_dhall(&a)?;
-                    f = rc(App(f, a))
+                    f = rc(Op(App(f, a)))
                 }
                 return Ok(f);
             }
@@ -105,7 +109,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
             [U64(3), U64(13), x, y] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let y = cbor_value_to_dhall(&y)?;
-                Completion(x, y)
+                Op(Completion(x, y))
             }
             [U64(3), U64(n), x, y] => {
                 let x = cbor_value_to_dhall(&x)?;
@@ -131,11 +135,14 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
                         ))
                     }
                 };
-                BinOp(op, x, y)
+                Op(BinOp(op, x, y))
             }
             [U64(4), t] => {
                 let t = cbor_value_to_dhall(&t)?;
-                EmptyListLit(rc(App(rc(ExprKind::Builtin(Builtin::List)), t)))
+                EmptyListLit(rc(Op(App(
+                    rc(ExprKind::Builtin(Builtin::List)),
+                    t,
+                ))))
             }
             [U64(4), Null, rest @ ..] => {
                 let rest = rest
@@ -151,26 +158,26 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
             // Old-style optional literals
             [U64(5), t] => {
                 let t = cbor_value_to_dhall(&t)?;
-                App(rc(ExprKind::Builtin(Builtin::OptionalNone)), t)
+                Op(App(rc(ExprKind::Builtin(Builtin::OptionalNone)), t))
             }
             [U64(5), t, x] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let t = cbor_value_to_dhall(&t)?;
                 Annot(
                     rc(SomeLit(x)),
-                    rc(App(rc(ExprKind::Builtin(Builtin::Optional)), t)),
+                    rc(Op(App(rc(ExprKind::Builtin(Builtin::Optional)), t))),
                 )
             }
             [U64(6), x, y] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let y = cbor_value_to_dhall(&y)?;
-                Merge(x, y, None)
+                Op(Merge(x, y, None))
             }
             [U64(6), x, y, z] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let y = cbor_value_to_dhall(&y)?;
                 let z = cbor_value_to_dhall(&z)?;
-                Merge(x, y, Some(z))
+                Op(Merge(x, y, Some(z)))
             }
             [U64(7), Object(map)] => {
                 let map = cbor_map_to_dhall_map(map)?;
@@ -183,13 +190,13 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
             [U64(9), x, String(l)] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let l = Label::from(l.as_str());
-                Field(x, l)
+                Op(Field(x, l))
             }
             [U64(10), x, Array(arr)] => {
                 let x = cbor_value_to_dhall(&x)?;
                 if let [y] = arr.as_slice() {
                     let y = cbor_value_to_dhall(&y)?;
-                    ProjectionByExpr(x, y)
+                    Op(ProjectionByExpr(x, y))
                 } else {
                     return Err(DecodeError::WrongFormatError(
                         "projection-by-expr".to_owned(),
@@ -207,7 +214,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
                         )),
                     })
                     .collect::<Result<_, _>>()?;
-                Projection(x, labels)
+                Op(Projection(x, labels))
             }
             [U64(11), Object(map)] => {
                 let map = cbor_map_to_dhall_opt_map(map)?;
@@ -222,7 +229,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
                 let x = cbor_value_to_dhall(&x)?;
                 let y = cbor_value_to_dhall(&y)?;
                 let z = cbor_value_to_dhall(&z)?;
-                BoolIf(x, y, z)
+                Op(BoolIf(x, y, z))
             }
             [U64(15), U64(x)] => Num(NumKind::Natural(*x as Natural)),
             [U64(16), U64(x)] => Num(NumKind::Integer(*x as Integer)),
@@ -416,12 +423,12 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
             }
             [U64(27), x] => {
                 let x = cbor_value_to_dhall(&x)?;
-                ToMap(x, None)
+                Op(ToMap(x, None))
             }
             [U64(27), x, y] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let y = cbor_value_to_dhall(&y)?;
-                ToMap(x, Some(y))
+                Op(ToMap(x, Some(y)))
             }
             [U64(28), x] => {
                 let x = cbor_value_to_dhall(&x)?;
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index 8d22a9b..b6bbabe 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -2,9 +2,10 @@ use serde_cbor::value::value as cbor;
 use std::collections::BTreeMap;
 use std::vec;
 
+use crate::builtins::Builtin;
 use crate::error::EncodeError;
+use crate::operations::{BinOp, OpKind};
 use crate::syntax;
-use crate::syntax::map::DupTreeMap;
 use crate::syntax::{
     Expr, ExprKind, FilePrefix, Hash, Import, ImportMode, ImportTarget, Label,
     Scheme, V,
@@ -19,8 +20,7 @@ enum Serialize<'a> {
     Expr(&'a Expr),
     CBOR(cbor::Value),
     RecordMap(&'a BTreeMap<Label, Expr>),
-    RecordDupMap(&'a DupTreeMap<Label, Expr>),
-    UnionMap(&'a DupTreeMap<Label, Option<Expr>>),
+    UnionMap(&'a BTreeMap<Label, Option<Expr>>),
 }
 
 macro_rules! count {
@@ -46,11 +46,11 @@ where
 {
     use cbor::Value::{String, I64, U64};
     use std::iter::once;
-    use syntax::Builtin;
     use syntax::ExprKind::*;
     use syntax::NumKind::*;
+    use OpKind::*;
 
-    use self::Serialize::{RecordDupMap, RecordMap, UnionMap};
+    use self::Serialize::{RecordMap, UnionMap};
     fn expr(x: &Expr) -> self::Serialize<'_> {
         self::Serialize::Expr(x)
     }
@@ -70,7 +70,9 @@ where
             let n: f64 = (*n).into();
             ser.serialize_f64(n)
         }
-        BoolIf(x, y, z) => ser_seq!(ser; tag(14), expr(x), expr(y), expr(z)),
+        Op(BoolIf(x, y, z)) => {
+            ser_seq!(ser; tag(14), expr(x), expr(y), expr(z))
+        }
         Var(V(l, n)) if l == &"_".into() => ser.serialize_u64(*n as u64),
         Var(V(l, n)) => ser_seq!(ser; label(l), U64(*n as u64)),
         Lam(l, x, y) if l == &"_".into() => {
@@ -99,7 +101,7 @@ where
             ser_seq.serialize_element(&expr(bound_e))?;
             ser_seq.end()
         }
-        App(_, _) => {
+        Op(App(_, _)) => {
             let (f, args) = collect_nested_applications(e);
             ser.collect_seq(
                 once(tag(0))
@@ -111,8 +113,8 @@ where
         Assert(x) => ser_seq!(ser; tag(19), expr(x)),
         SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
         EmptyListLit(x) => match x.as_ref() {
-            App(f, a) => match f.as_ref() {
-                ExprKind::Builtin(Builtin::List) => {
+            Op(App(f, a)) => match f.as_ref() {
+                ExprKind::Builtin(self::Builtin::List) => {
                     ser_seq!(ser; tag(4), expr(a))
                 }
                 _ => ser_seq!(ser; tag(28), expr(x)),
@@ -129,12 +131,12 @@ where
                 Text(x) => cbor(String(x)),
             })))
         }
-        RecordType(map) => ser_seq!(ser; tag(7), RecordDupMap(map)),
+        RecordType(map) => ser_seq!(ser; tag(7), RecordMap(map)),
         RecordLit(map) => ser_seq!(ser; tag(8), RecordMap(map)),
         UnionType(map) => ser_seq!(ser; tag(11), UnionMap(map)),
-        Field(x, l) => ser_seq!(ser; tag(9), expr(x), label(l)),
-        BinOp(op, x, y) => {
-            use syntax::BinOp::*;
+        Op(Field(x, l)) => ser_seq!(ser; tag(9), expr(x), label(l)),
+        Op(BinOp(op, x, y)) => {
+            use self::BinOp::*;
             let op = match op {
                 BoolOr => 0,
                 BoolAnd => 1,
@@ -152,21 +154,23 @@ where
             };
             ser_seq!(ser; tag(3), U64(op), expr(x), expr(y))
         }
-        Merge(x, y, None) => ser_seq!(ser; tag(6), expr(x), expr(y)),
-        Merge(x, y, Some(z)) => {
+        Op(Merge(x, y, None)) => ser_seq!(ser; tag(6), expr(x), expr(y)),
+        Op(Merge(x, y, Some(z))) => {
             ser_seq!(ser; tag(6), expr(x), expr(y), expr(z))
         }
-        ToMap(x, None) => ser_seq!(ser; tag(27), expr(x)),
-        ToMap(x, Some(y)) => ser_seq!(ser; tag(27), expr(x), expr(y)),
-        Projection(x, ls) => ser.collect_seq(
+        Op(ToMap(x, None)) => ser_seq!(ser; tag(27), expr(x)),
+        Op(ToMap(x, Some(y))) => ser_seq!(ser; tag(27), expr(x), expr(y)),
+        Op(Projection(x, ls)) => ser.collect_seq(
             once(tag(10))
                 .chain(once(expr(x)))
                 .chain(ls.iter().map(label)),
         ),
-        ProjectionByExpr(x, y) => {
+        Op(ProjectionByExpr(x, y)) => {
             ser_seq!(ser; tag(10), expr(x), vec![expr(y)])
         }
-        Completion(x, y) => ser_seq!(ser; tag(3), tag(13), expr(x), expr(y)),
+        Op(Completion(x, y)) => {
+            ser_seq!(ser; tag(3), tag(13), expr(x), expr(y))
+        }
         Import(import) => serialize_import(ser, import),
     }
 }
@@ -260,11 +264,6 @@ impl<'a> serde::ser::Serialize for Serialize<'a> {
         match self {
             Serialize::Expr(e) => serialize_subexpr(ser, e),
             Serialize::CBOR(v) => v.serialize(ser),
-            Serialize::RecordDupMap(map) => {
-                ser.collect_map(map.iter().map(|(k, v)| {
-                    (cbor::Value::String(k.into()), Serialize::Expr(v))
-                }))
-            }
             Serialize::RecordMap(map) => {
                 ser.collect_map(map.iter().map(|(k, v)| {
                     (cbor::Value::String(k.into()), Serialize::Expr(v))
@@ -286,7 +285,7 @@ impl<'a> serde::ser::Serialize for Serialize<'a> {
 fn collect_nested_applications<'a>(e: &'a Expr) -> (&'a Expr, Vec<&'a Expr>) {
     fn go<'a>(e: &'a Expr, vec: &mut Vec<&'a Expr>) -> &'a Expr {
         match e.as_ref() {
-            ExprKind::App(f, a) => {
+            ExprKind::Op(OpKind::App(f, a)) => {
                 vec.push(a);
                 go(f, vec)
             }
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 6f5949f..dcaf5e4 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -1,13 +1,13 @@
 use itertools::Itertools;
 use pest::prec_climber as pcl;
 use pest::prec_climber::PrecClimber;
-use std::collections::BTreeMap;
+use std::collections::{BTreeMap, BTreeSet};
 use std::iter::once;
 use std::rc::Rc;
 
 use pest_consume::{match_nodes, Parser};
 
-use crate::syntax::map::{DupTreeMap, DupTreeSet};
+use crate::operations::OpKind::*;
 use crate::syntax::ExprKind::*;
 use crate::syntax::NumKind::*;
 use crate::syntax::{
@@ -31,50 +31,10 @@ pub type ParseResult<T> = Result<T, ParseError>;
 #[derive(Debug)]
 enum Selector {
     Field(Label),
-    Projection(DupTreeSet<Label>),
+    Projection(BTreeSet<Label>),
     ProjectionByExpr(Expr),
 }
 
-impl crate::syntax::Builtin {
-    pub fn parse(s: &str) -> Option<Self> {
-        use crate::syntax::Builtin::*;
-        match s {
-            "Bool" => Some(Bool),
-            "Natural" => Some(Natural),
-            "Integer" => Some(Integer),
-            "Double" => Some(Double),
-            "Text" => Some(Text),
-            "List" => Some(List),
-            "Optional" => Some(Optional),
-            "None" => Some(OptionalNone),
-            "Natural/build" => Some(NaturalBuild),
-            "Natural/fold" => Some(NaturalFold),
-            "Natural/isZero" => Some(NaturalIsZero),
-            "Natural/even" => Some(NaturalEven),
-            "Natural/odd" => Some(NaturalOdd),
-            "Natural/toInteger" => Some(NaturalToInteger),
-            "Natural/show" => Some(NaturalShow),
-            "Natural/subtract" => Some(NaturalSubtract),
-            "Integer/toDouble" => Some(IntegerToDouble),
-            "Integer/show" => Some(IntegerShow),
-            "Integer/negate" => Some(IntegerNegate),
-            "Integer/clamp" => Some(IntegerClamp),
-            "Double/show" => Some(DoubleShow),
-            "List/build" => Some(ListBuild),
-            "List/fold" => Some(ListFold),
-            "List/length" => Some(ListLength),
-            "List/head" => Some(ListHead),
-            "List/last" => Some(ListLast),
-            "List/indexed" => Some(ListIndexed),
-            "List/reverse" => Some(ListReverse),
-            "Optional/fold" => Some(OptionalFold),
-            "Optional/build" => Some(OptionalBuild),
-            "Text/show" => Some(TextShow),
-            _ => None,
-        }
-    }
-}
-
 fn input_to_span(input: ParseInput) -> Span {
     Span::make(input.user_data().clone(), input.as_pair().as_span())
 }
@@ -128,7 +88,7 @@ fn trim_indent(lines: &mut Vec<ParsedText>) {
 
 /// Insert the expr into the map; in case of collision, create a RecursiveRecordMerge node.
 fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) {
-    use crate::syntax::BinOp::RecursiveRecordMerge;
+    use crate::operations::BinOp::RecursiveRecordMerge;
     use std::collections::btree_map::Entry;
     match map.entry(l) {
         Entry::Vacant(entry) => {
@@ -138,7 +98,7 @@ fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) {
             let dummy = Expr::new(Num(Bool(false)), Span::Artificial);
             let other = entry.insert(dummy);
             entry.insert(Expr::new(
-                BinOp(RecursiveRecordMerge, other, e),
+                Op(BinOp(RecursiveRecordMerge, other, e)),
                 Span::DuplicateRecordFieldsSugar,
             ));
         }
@@ -146,18 +106,21 @@ fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) {
 }
 
 fn desugar_with_expr(x: Expr, labels: &[Label], y: Expr) -> Expr {
-    use crate::syntax::BinOp::RightBiasedRecordMerge;
+    use crate::operations::BinOp::RightBiasedRecordMerge;
     let expr = |k| Expr::new(k, Span::WithSugar);
     match labels {
         [] => y,
         [l, rest @ ..] => {
-            let res =
-                desugar_with_expr(expr(Field(x.clone(), l.clone())), rest, y);
-            expr(BinOp(
+            let res = desugar_with_expr(
+                expr(Op(Field(x.clone(), l.clone()))),
+                rest,
+                y,
+            );
+            expr(Op(BinOp(
                 RightBiasedRecordMerge,
                 x,
                 expr(RecordLit(once((l.clone(), res)).collect())),
-            ))
+            )))
         }
     }
 }
@@ -387,7 +350,7 @@ impl DhallParser {
     #[alias(expression)]
     fn builtin(input: ParseInput) -> ParseResult<Expr> {
         let s = input.as_str();
-        let e = match crate::syntax::Builtin::parse(s) {
+        let e = match crate::builtins::Builtin::parse(s) {
             Some(b) => Builtin(b),
             None => match s {
                 "True" => Num(Bool(true)),
@@ -725,7 +688,7 @@ impl DhallParser {
             },
             [if_(()), expression(cond), expression(left),
                     expression(right)] => {
-                spanned(input, BoolIf(cond, left, right))
+                spanned(input, Op(BoolIf(cond, left, right)))
             },
             [let_binding(bindings).., expression(final_expr)] => {
                 bindings.rev().fold(
@@ -747,13 +710,13 @@ impl DhallParser {
                 spanned(input, Pi("_".into(), typ, body))
             },
             [merge(()), expression(x), expression(y), expression(z)] => {
-                spanned(input, Merge(x, y, Some(z)))
+                spanned(input, Op(Merge(x, y, Some(z))))
             },
             [assert(()), expression(x)] => {
                 spanned(input, Assert(x))
             },
             [toMap(()), expression(x), expression(y)] => {
-                spanned(input, ToMap(x, Some(y)))
+                spanned(input, Op(ToMap(x, Some(y))))
             },
             [expression(e), expression(annot)] => {
                 spanned(input, Annot(e, annot))
@@ -780,7 +743,7 @@ impl DhallParser {
         op: ParseInput,
         r: Expr,
     ) -> ParseResult<Expr> {
-        use crate::syntax::BinOp::*;
+        use crate::operations::BinOp::*;
         use Rule::*;
         let op = match op.as_rule() {
             import_alt => ImportAlt,
@@ -801,7 +764,7 @@ impl DhallParser {
             }
         };
 
-        Ok(spanned_union(l.span(), r.span(), BinOp(op, l, r)))
+        Ok(spanned_union(l.span(), r.span(), Op(BinOp(op, l, r))))
     }
 
     fn Some_(_input: ParseInput) -> ParseResult<()> {
@@ -840,7 +803,7 @@ impl DhallParser {
                         spanned_union(
                             acc.span(),
                             e.span(),
-                            App(acc, e)
+                            Op(App(acc, e))
                         )
                     }
                 )
@@ -855,10 +818,10 @@ impl DhallParser {
                 spanned(input, SomeLit(e))
             },
             [merge(()), expression(x), expression(y)] => {
-                spanned(input, Merge(x, y, None))
+                spanned(input, Op(Merge(x, y, None)))
             },
             [toMap(()), expression(x)] => {
-                spanned(input, ToMap(x, None))
+                spanned(input, Op(ToMap(x, None)))
             },
             [expression(e)] => e,
         ))
@@ -875,7 +838,7 @@ impl DhallParser {
                         spanned_union(
                             acc.span(),
                             e.span(),
-                            Completion(acc, e),
+                            Op(Completion(acc, e)),
                         )
                     }
                 )
@@ -895,9 +858,9 @@ impl DhallParser {
                             acc.span(),
                             e.1,
                             match e.0 {
-                                Selector::Field(l) => Field(acc, l),
-                                Selector::Projection(ls) => Projection(acc, ls),
-                                Selector::ProjectionByExpr(e) => ProjectionByExpr(acc, e)
+                                Selector::Field(l) => Op(Field(acc, l)),
+                                Selector::Projection(ls) => Op(Projection(acc, ls)),
+                                Selector::ProjectionByExpr(e) => Op(ProjectionByExpr(acc, e))
                             }
                         )
                     }
@@ -915,9 +878,20 @@ impl DhallParser {
         Ok((stor, input_to_span(input)))
     }
 
-    fn labels(input: ParseInput) -> ParseResult<DupTreeSet<Label>> {
-        Ok(match_nodes!(input.into_children();
-            [label(ls)..] => ls.collect(),
+    fn labels(input: ParseInput) -> ParseResult<BTreeSet<Label>> {
+        Ok(match_nodes!(input.children();
+            [label(ls)..] => {
+                let mut set = BTreeSet::default();
+                for l in ls {
+                    if set.contains(&l) {
+                        return Err(
+                            input.error(format!("Duplicate field in projection"))
+                        )
+                    }
+                    set.insert(l);
+                }
+                set
+            },
         ))
     }
 
@@ -957,9 +931,26 @@ impl DhallParser {
 
     fn non_empty_record_type(
         input: ParseInput,
-    ) -> ParseResult<DupTreeMap<Label, Expr>> {
-        Ok(match_nodes!(input.into_children();
-            [record_type_entry(entries)..] => entries.collect()
+    ) -> ParseResult<BTreeMap<Label, Expr>> {
+        Ok(match_nodes!(input.children();
+            [record_type_entry(entries)..] => {
+                let mut map = BTreeMap::default();
+                for (l, t) in entries {
+                    use std::collections::btree_map::Entry;
+                    match map.entry(l) {
+                        Entry::Occupied(_) => {
+                            return Err(input.error(
+                                "Duplicate field in record type"
+                                    .to_string(),
+                            ));
+                        }
+                        Entry::Vacant(e) => {
+                            e.insert(t);
+                        }
+                    }
+                }
+                map
+            },
         ))
     }
 
@@ -1008,7 +999,24 @@ impl DhallParser {
     fn union_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
         let map = match_nodes!(input.children();
             [empty_union_type(_)] => Default::default(),
-            [union_type_entry(entries)..] => entries.collect(),
+            [union_type_entry(entries)..] => {
+                let mut map = BTreeMap::default();
+                for (l, t) in entries {
+                    use std::collections::btree_map::Entry;
+                    match map.entry(l) {
+                        Entry::Occupied(_) => {
+                            return Err(input.error(
+                                "Duplicate variant in union type"
+                                    .to_string(),
+                            ));
+                        }
+                        Entry::Vacant(e) => {
+                            e.insert(t);
+                        }
+                    }
+                }
+                map
+            },
         );
         Ok(UnionType(map))
     }
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index 378f408..9e90660 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -1,3 +1,5 @@
+use crate::builtins::Builtin;
+use crate::operations::{BinOp, OpKind};
 use crate::syntax::*;
 use itertools::Itertools;
 use std::fmt::{self, Display};
@@ -5,15 +7,16 @@ use std::fmt::{self, Display};
 // There is a one-to-one correspondence between the formatter and the grammar. Each phase is
 // named after a corresponding grammar group, and the structure of the formatter reflects
 // the relationship between the corresponding grammar rules. This leads to the nice property
-// of automatically getting all the parentheses and precedences right.
+// of automatically getting all the parentheses and precedences right (in a manner dual do Pratt
+// parsing).
 #[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)]
 enum PrintPhase {
     // `expression`
     Base,
     // `operator-expression`
     Operator,
-    // All the operator `*-expression`s
-    BinOp(ast::BinOp),
+    // All the `<operator>-expression`s
+    BinOp(self::BinOp),
     // `application-expression`
     App,
     // `import-expression`
@@ -36,7 +39,8 @@ impl<'a> PhasedExpr<'a> {
 impl UnspannedExpr {
     // Annotate subexpressions with the appropriate phase, defaulting to Base
     fn annotate_with_phases(&self) -> ExprKind<PhasedExpr<'_>> {
-        use crate::syntax::ExprKind::*;
+        use ExprKind::*;
+        use OpKind::*;
         use PrintPhase::*;
         let with_base = self.map_ref(|e| PhasedExpr(e, Base));
         match with_base {
@@ -47,31 +51,33 @@ impl UnspannedExpr {
                     Pi(a, b, c)
                 }
             }
-            Merge(a, b, c) => Merge(
+            Op(Merge(a, b, c)) => Op(Merge(
                 a.phase(PrintPhase::Import),
                 b.phase(PrintPhase::Import),
                 c.map(|x| x.phase(PrintPhase::App)),
-            ),
-            ToMap(a, b) => ToMap(
+            )),
+            Op(ToMap(a, b)) => Op(ToMap(
                 a.phase(PrintPhase::Import),
                 b.map(|x| x.phase(PrintPhase::App)),
-            ),
+            )),
             Annot(a, b) => Annot(a.phase(Operator), b),
-            ExprKind::BinOp(op, a, b) => ExprKind::BinOp(
+            Op(OpKind::BinOp(op, a, b)) => Op(OpKind::BinOp(
                 op,
                 a.phase(PrintPhase::BinOp(op)),
                 b.phase(PrintPhase::BinOp(op)),
-            ),
+            )),
             SomeLit(e) => SomeLit(e.phase(PrintPhase::Import)),
-            ExprKind::App(f, a) => ExprKind::App(
+            Op(OpKind::App(f, a)) => Op(OpKind::App(
                 f.phase(PrintPhase::App),
                 a.phase(PrintPhase::Import),
-            ),
-            Field(a, b) => Field(a.phase(Primitive), b),
-            Projection(e, ls) => Projection(e.phase(Primitive), ls),
-            ProjectionByExpr(a, b) => ProjectionByExpr(a.phase(Primitive), b),
-            Completion(a, b) => {
-                Completion(a.phase(Primitive), b.phase(Primitive))
+            )),
+            Op(Field(a, b)) => Op(Field(a.phase(Primitive), b)),
+            Op(Projection(e, ls)) => Op(Projection(e.phase(Primitive), ls)),
+            Op(ProjectionByExpr(a, b)) => {
+                Op(ProjectionByExpr(a.phase(Primitive), b))
+            }
+            Op(Completion(a, b)) => {
+                Op(Completion(a.phase(Primitive), b.phase(Primitive)))
             }
             ExprKind::Import(a) => {
                 ExprKind::Import(a.map_ref(|x| x.phase(PrintPhase::Import)))
@@ -85,22 +91,24 @@ impl UnspannedExpr {
         f: &mut fmt::Formatter,
         phase: PrintPhase,
     ) -> Result<(), fmt::Error> {
-        use crate::syntax::ExprKind::*;
+        use ExprKind::*;
+        use OpKind::*;
 
         let needs_paren = match self {
             Lam(_, _, _)
-            | BoolIf(_, _, _)
             | Pi(_, _, _)
             | Let(_, _, _, _)
-            | EmptyListLit(_)
             | SomeLit(_)
-            | Merge(_, _, _)
-            | ToMap(_, _)
+            | EmptyListLit(_)
+            | Op(BoolIf(_, _, _))
+            | Op(Merge(_, _, _))
+            | Op(ToMap(_, _))
             | Annot(_, _) => phase > PrintPhase::Base,
-            // Precedence is magically handled by the ordering of BinOps.
-            ExprKind::BinOp(op, _, _) => phase > PrintPhase::BinOp(*op),
-            ExprKind::App(_, _) => phase > PrintPhase::App,
-            Completion(_, _) => phase > PrintPhase::Import,
+            // Precedence is magically handled by the ordering of BinOps. This is reverse Pratt
+            // parsing.
+            Op(BinOp(op, _, _)) => phase > PrintPhase::BinOp(*op),
+            Op(App(_, _)) => phase > PrintPhase::App,
+            Op(Completion(_, _)) => phase > PrintPhase::Import,
             _ => false,
         };
 
@@ -143,12 +151,10 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::syntax::ExprKind::*;
         match self {
+            Var(a) => a.fmt(f)?,
             Lam(a, b, c) => {
                 write!(f, "λ({} : {}) → {}", a, b, c)?;
             }
-            BoolIf(a, b, c) => {
-                write!(f, "if {} then {} else {}", a, b, c)?;
-            }
             Pi(a, b, c) if &String::from(a) == "_" => {
                 write!(f, "{} → {}", b, c)?;
             }
@@ -162,14 +168,62 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
                 }
                 write!(f, " = {} in {}", c, d)?;
             }
+            Const(k) => k.fmt(f)?,
+            Builtin(v) => v.fmt(f)?,
+            Num(a) => a.fmt(f)?,
+            TextLit(a) => a.fmt(f)?,
+            SomeLit(e) => {
+                write!(f, "Some {}", e)?;
+            }
             EmptyListLit(t) => {
                 write!(f, "[] : {}", t)?;
             }
             NEListLit(es) => {
                 fmt_list("[", ", ", "]", es, f, Display::fmt)?;
             }
-            SomeLit(e) => {
-                write!(f, "Some {}", e)?;
+            RecordLit(a) if a.is_empty() => f.write_str("{=}")?,
+            RecordLit(a) => fmt_list("{ ", ", ", " }", a, f, |(k, v), f| {
+                write!(f, "{} = {}", k, v)
+            })?,
+            RecordType(a) if a.is_empty() => f.write_str("{}")?,
+            RecordType(a) => fmt_list("{ ", ", ", " }", a, f, |(k, t), f| {
+                write!(f, "{} : {}", k, t)
+            })?,
+            UnionType(a) => fmt_list("< ", " | ", " >", a, f, |(k, v), f| {
+                write!(f, "{}", k)?;
+                if let Some(v) = v {
+                    write!(f, ": {}", v)?;
+                }
+                Ok(())
+            })?,
+            Op(op) => {
+                op.fmt(f)?;
+            }
+            Annot(a, b) => {
+                write!(f, "{} : {}", a, b)?;
+            }
+            Assert(a) => {
+                write!(f, "assert : {}", a)?;
+            }
+            Import(a) => a.fmt(f)?,
+        }
+        Ok(())
+    }
+}
+
+/// Generic instance that delegates to subexpressions
+impl<SE: Display + Clone> Display for OpKind<SE> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use OpKind::*;
+        match self {
+            App(a, b) => {
+                write!(f, "{} {}", a, b)?;
+            }
+            BinOp(op, a, b) => {
+                write!(f, "{} {} {}", a, op, b)?;
+            }
+            BoolIf(a, b, c) => {
+                write!(f, "if {} then {} else {}", a, b, c)?;
             }
             Merge(a, b, c) => {
                 write!(f, "merge {} {}", a, b)?;
@@ -183,41 +237,9 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
                     write!(f, " : {}", b)?;
                 }
             }
-            Annot(a, b) => {
-                write!(f, "{} : {}", a, b)?;
-            }
-            Assert(a) => {
-                write!(f, "assert : {}", a)?;
-            }
-            ExprKind::BinOp(op, a, b) => {
-                write!(f, "{} {} {}", a, op, b)?;
-            }
-            ExprKind::App(a, b) => {
-                write!(f, "{} {}", a, b)?;
-            }
             Field(a, b) => {
                 write!(f, "{}.{}", a, b)?;
             }
-            Var(a) => a.fmt(f)?,
-            Const(k) => k.fmt(f)?,
-            Builtin(v) => v.fmt(f)?,
-            Num(a) => a.fmt(f)?,
-            TextLit(a) => a.fmt(f)?,
-            RecordType(a) if a.is_empty() => f.write_str("{}")?,
-            RecordType(a) => fmt_list("{ ", ", ", " }", a, f, |(k, t), f| {
-                write!(f, "{} : {}", k, t)
-            })?,
-            RecordLit(a) if a.is_empty() => f.write_str("{=}")?,
-            RecordLit(a) => fmt_list("{ ", ", ", " }", a, f, |(k, v), f| {
-                write!(f, "{} = {}", k, v)
-            })?,
-            UnionType(a) => fmt_list("< ", " | ", " >", a, f, |(k, v), f| {
-                write!(f, "{}", k)?;
-                if let Some(v) = v {
-                    write!(f, ": {}", v)?;
-                }
-                Ok(())
-            })?,
             Projection(e, ls) => {
                 write!(f, "{}.", e)?;
                 fmt_list("{ ", ", ", " }", ls, f, Display::fmt)?;
@@ -228,7 +250,6 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
             Completion(a, b) => {
                 write!(f, "{}::{}", a, b)?;
             }
-            Import(a) => a.fmt(f)?,
         }
         Ok(())
     }
@@ -315,7 +336,7 @@ impl Display for Const {
 
 impl Display for BinOp {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        use crate::syntax::BinOp::*;
+        use BinOp::*;
         f.write_str(match self {
             BoolOr => "||",
             TextAppend => "++",
@@ -363,7 +384,7 @@ impl Display for Label {
         let is_reserved = match s.as_str() {
             "let" | "in" | "if" | "then" | "else" | "Type" | "Kind"
             | "Sort" | "True" | "False" | "Some" => true,
-            _ => crate::syntax::Builtin::parse(&s).is_some(),
+            _ => Builtin::parse(&s).is_some(),
         };
         if !is_reserved && s.chars().all(|c| c.is_ascii_alphanumeric()) {
             write!(f, "{}", s)
@@ -461,45 +482,6 @@ impl<SubExpr: Display> Display for Import<SubExpr> {
     }
 }
 
-impl Display for Builtin {
-    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        use crate::syntax::Builtin::*;
-        f.write_str(match *self {
-            Bool => "Bool",
-            Natural => "Natural",
-            Integer => "Integer",
-            Double => "Double",
-            Text => "Text",
-            List => "List",
-            Optional => "Optional",
-            OptionalNone => "None",
-            NaturalBuild => "Natural/build",
-            NaturalFold => "Natural/fold",
-            NaturalIsZero => "Natural/isZero",
-            NaturalEven => "Natural/even",
-            NaturalOdd => "Natural/odd",
-            NaturalToInteger => "Natural/toInteger",
-            NaturalShow => "Natural/show",
-            NaturalSubtract => "Natural/subtract",
-            IntegerToDouble => "Integer/toDouble",
-            IntegerNegate => "Integer/negate",
-            IntegerClamp => "Integer/clamp",
-            IntegerShow => "Integer/show",
-            DoubleShow => "Double/show",
-            ListBuild => "List/build",
-            ListFold => "List/fold",
-            ListLength => "List/length",
-            ListHead => "List/head",
-            ListLast => "List/last",
-            ListIndexed => "List/indexed",
-            ListReverse => "List/reverse",
-            OptionalFold => "Optional/fold",
-            OptionalBuild => "Optional/build",
-            TextShow => "Text/show",
-        })
-    }
-}
-
 impl Display for Scheme {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::syntax::Scheme::*;
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 5bcdb1c..468d550 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -225,7 +225,7 @@ impl TestFile {
             if Self::force_update() {
                 self.write_ui(x)?;
             } else {
-                assert_eq_pretty_str!(msg, expected);
+                assert_eq_pretty_str!(expected, msg);
             }
         }
         Ok(())
diff --git a/dhall/tests/type-inference/failure/mixedUnions.txt b/dhall/tests/type-inference/failure/mixedUnions.txt
index a6ca913..2b307d0 100644
--- a/dhall/tests/type-inference/failure/mixedUnions.txt
+++ b/dhall/tests/type-inference/failure/mixedUnions.txt
@@ -1,6 +1,6 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:1
+Type error: error: InvalidVariantType
+ --> <current file>:1:28
   |
 1 | < Left : Natural | Right : Type >
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |                            ^^^^ InvalidVariantType
   |
diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt
index 7dcbe4f..9a243c3 100644
--- a/dhall/tests/type-inference/failure/recordOfKind.txt
+++ b/dhall/tests/type-inference/failure/recordOfKind.txt
@@ -1,6 +1,6 @@
 Type error: error: InvalidFieldType
- --> <current file>:1:1
+ --> <current file>:1:7
   |
 1 | { a = Kind }
-  | ^^^^^^^^^^^^ InvalidFieldType
+  |       ^^^^ InvalidFieldType
   |
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
index fa8b153..a83bb4f 100644
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
@@ -1,6 +1,6 @@
 Type error: error: InvalidFieldType
- --> <current file>:1:1
+ --> <current file>:1:17
   |
 1 | { x = Type, y = Kind }
-  | ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |                 ^^^^ InvalidFieldType
   |
diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt
index 05c3eed..7b35481 100644
--- a/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt
@@ -1,6 +1,6 @@
-Type error: error: ProjectionDuplicateField
- --> <current file>:1:1
+ --> 1:11
   |
-1 | { x = 1 }.{ x, x }
-  | ^^^^^^^^^^^^^^^^^^ ProjectionDuplicateField
+1 | { x = 1 }.{ x, x }␊
+  |           ^------^
   |
+  = Duplicate field in projection
diff --git a/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt
index d8bec44..aced8a9 100644
--- a/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt
@@ -1,6 +1,6 @@
-Type error: error: RecordTypeDuplicateField
- --> <current file>:1:1
+ --> 1:3
   |
-1 | { x: Natural, x: Natural }
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeDuplicateField
+1 | { x: Natural, x: Natural }␊
+  |   ^--------------------^
   |
+  = Duplicate field in record type
diff --git a/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt b/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt
index 81815a2..c6c274c 100644
--- a/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt
@@ -1,6 +1,6 @@
 Type error: error: InvalidFieldType
- --> <current file>:1:1
+ --> <current file>:1:7
   |
 1 | { x : True }
-  | ^^^^^^^^^^^^ InvalidFieldType
+  |       ^^^^ InvalidFieldType
   |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
index 146bf7f..6a6da80 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -1,6 +1,6 @@
 Type error: error: InvalidFieldType
- --> <current file>:1:16
+ --> <current file>:1:22
   |
 1 | { x = Bool } ⫽ { x = Kind }
-  |                ^^^^^^^^^^^^ InvalidFieldType
+  |                      ^^^^ InvalidFieldType
   |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
index 71914e1..322e7f4 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -1,6 +1,6 @@
 Type error: error: InvalidFieldType
- --> <current file>:1:15
+ --> <current file>:1:21
   |
 1 | { x = {=} } ⫽ { x = Kind }
-  |               ^^^^^^^^^^^^ InvalidFieldType
+  |                     ^^^^ InvalidFieldType
   |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt
index 84bfe4d..9984693 100644
--- a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt
@@ -1,6 +1,6 @@
-Type error: error: UnionTypeDuplicateField
- --> <current file>:1:1
+ --> 1:2
   |
-1 | <x | x>
-  | ^^^^^^^ UnionTypeDuplicateField
+1 | <x | x>␊
+  |  ^---^
   |
+  = Duplicate variant in union type
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt
index eb20b12..fdf6dc0 100644
--- a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt
@@ -1,6 +1,6 @@
-Type error: error: UnionTypeDuplicateField
- --> <current file>:1:1
+ --> 1:2
   |
-1 | <x | x: Natural>
-  | ^^^^^^^^^^^^^^^^ UnionTypeDuplicateField
+1 | <x | x: Natural>␊
+  |  ^------------^
   |
+  = Duplicate variant in union type
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
index 44ce7a3..ae6c845 100644
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt
@@ -1,6 +1,6 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:1
+Type error: error: InvalidVariantType
+ --> <current file>:1:18
   |
 1 | < x : Bool | y : Type >
-  | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |                  ^^^^ InvalidVariantType
   |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
index 01f706d..faf81a9 100644
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt
@@ -1,6 +1,6 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:1
+Type error: error: InvalidVariantType
+ --> <current file>:1:18
   |
 1 | < x : Kind | y : Type >
-  | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |                  ^^^^ InvalidVariantType
   |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
index 496462d..bbfb1f3 100644
--- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt
@@ -1,6 +1,6 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:1
+Type error: error: InvalidVariantType
+ --> <current file>:1:18
   |
 1 | < x : Kind | y : Bool >
-  | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+  |                  ^^^^ InvalidVariantType
   |
diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt b/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt
index 450a3dd..cedf06e 100644
--- a/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt
+++ b/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt
@@ -1,6 +1,6 @@
-Type error: error: InvalidFieldType
- --> <current file>:1:1
+Type error: error: InvalidVariantType
+ --> <current file>:1:7
   |
 1 | < x : True >
-  | ^^^^^^^^^^^^ InvalidFieldType
+  |       ^^^^ InvalidVariantType
   |