Extract operation-related code to a new module

13 files changed, 900 insertions, 882 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 98ad4f0..e00177c 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -11,6 +11,7 @@
 mod tests;
 
 pub mod error;
+pub mod operations;
 pub mod semantics;
 pub mod syntax;
 
diff --git a/dhall/src/operations.rs b/dhall/src/operations.rs
new file mode 100644
index 0000000..363cd10
--- /dev/null
+++ b/dhall/src/operations.rs
@@ -0,0 +1,865 @@
+use itertools::Itertools;
+use std::borrow::Cow;
+use std::cmp::max;
+use std::collections::HashMap;
+
+use crate::error::{ErrorBuilder, TypeError};
+use crate::semantics::{
+    merge_maps, mk_span_err, mkerr, ret_kind, ret_op, ret_ref, Binder, Closure,
+    Hir, HirKind, Nir, NirKind, Ret, TextLit, Tir, TyEnv, Type,
+};
+use crate::syntax::map::DupTreeSet;
+use crate::syntax::{
+    trivial_result, BinOp, Builtin, Const, ExprKind, Label, NumKind, Span,
+};
+
+/// 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, DupTreeSet<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))))
+    }
+}
+
+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) => {
+                        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(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")
+        }
+    })
+}
+
+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(
+                            Some((field.clone(), r.clone()))
+                                .into_iter()
+                                .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(
+                            Some((field.clone(), r.clone()))
+                                .into_iter()
+                                .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(
+                            Some((field.clone(), r.clone()))
+                                .into_iter()
+                                .collect(),
+                        )),
+                    ))),
+                    field.clone(),
+                )),
+                None => normalize_field(x, field),
+            },
+            _ => nothing_to_do(),
+        },
+        _ => nothing_to_do(),
+    }
+}
+
+pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
+    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()))
+            }
+            _ => 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/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 45be448..f65e8d1 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,3 +1,4 @@
+use crate::operations::OpKind;
 use crate::semantics::{
     skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv,
 };
@@ -5,8 +6,8 @@ use crate::syntax::map::DupTreeMap;
 use crate::syntax::Const::Type;
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
-    InterpolatedTextContents, Label, NaiveDouble, NumKind, OpKind, Span,
-    UnspannedExpr, V,
+    InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr,
+    V,
 };
 use std::collections::HashMap;
 use std::convert::TryInto;
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 88123d8..5c67c02 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -1,6 +1,7 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
+use crate::operations::OpKind;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder,
@@ -8,7 +9,7 @@ use crate::semantics::{
 };
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
-    NumKind, OpKind, Span,
+    NumKind, Span,
 };
 use crate::ToExprOptions;
 
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c0e41cb..d042f3f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -1,11 +1,9 @@
-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, Label, NumKind, OpKind,
-};
+use crate::syntax::{ExprKind, InterpolatedTextContents};
 
 pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
     match f.kind() {
@@ -83,306 +81,21 @@ where
     kvs
 }
 
-type Ret = NirKind;
+pub type Ret = NirKind;
 
-fn ret_nir(x: Nir) -> Ret {
+pub fn ret_nir(x: Nir) -> Ret {
     ret_ref(&x)
 }
-fn ret_kind(x: NirKind) -> Ret {
+pub fn ret_kind(x: NirKind) -> Ret {
     x
 }
-fn ret_ref(x: &Nir) -> Ret {
+pub fn ret_ref(x: &Nir) -> Ret {
     x.kind().clone()
 }
-fn ret_op(x: OpKind<Nir>) -> Ret {
+pub fn ret_op(x: OpKind<Nir>) -> Ret {
     NirKind::Op(x)
 }
 
-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(
-                            Some((field.clone(), r.clone()))
-                                .into_iter()
-                                .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(
-                            Some((field.clone(), r.clone()))
-                                .into_iter()
-                                .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(
-                            Some((field.clone(), r.clone()))
-                                .into_iter()
-                                .collect(),
-                        )),
-                    ))),
-                    field.clone(),
-                )),
-                None => normalize_field(x, field),
-            },
-            _ => nothing_to_do(),
-        },
-        _ => nothing_to_do(),
-    }
-}
-
-fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
-    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()))
-            }
-            _ => 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")
-        }
-    }
-}
-
 pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
     use NirKind::{
         Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType,
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 3e0022f..bbcd240 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -6,12 +6,13 @@ use url::Url;
 
 use crate::error::ErrorBuilder;
 use crate::error::{Error, ImportError};
+use crate::operations::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, OpKind, Span, UnspannedExpr, URL,
+    ImportTarget, Span, UnspannedExpr, URL,
 };
 use crate::{Parsed, Resolved};
 
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 427b39d..7481f07 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,51 +1,15 @@
-use std::borrow::Cow;
 use std::cmp::max;
 use std::collections::HashMap;
 
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
-use crate::semantics::merge_maps;
+use crate::operations::typecheck_operation;
 use crate::semantics::{
-    type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv,
-    Type,
+    type_of_builtin, Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, OpKind,
-    Span,
+    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(())
-}
-
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
         Const::Type
@@ -66,477 +30,6 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
     )
 }
 
-fn type_of_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 type_of_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"),
-    })
-}
-
-fn type_of_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) => type_of_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) => {
-            type_of_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) => {
-                        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(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")
-        }
-    })
-}
-
 /// When all sub-expressions have been typed, check the remaining toplevel
 /// layer.
 fn type_one_layer(
@@ -690,7 +183,7 @@ fn type_one_layer(
 
             Type::from_const(k)
         }
-        ExprKind::Op(op) => type_of_operation(env, span, op)?,
+        ExprKind::Op(op) => typecheck_operation(env, span, op)?,
         ExprKind::Assert(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 51e9ea7..62734bf 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::error::Error;
+use crate::operations::OpKind;
 use crate::semantics::Universe;
-use crate::syntax::map::{DupTreeMap, DupTreeSet};
+use crate::syntax::map::DupTreeMap;
 use crate::syntax::visitor;
 use crate::syntax::*;
 
@@ -126,29 +127,6 @@ pub enum NumKind {
     Double(Double),
 }
 
-/// 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, DupTreeSet<Label>),
-    ///  `e.(t)`
-    ProjectionByExpr(SubExpr, SubExpr),
-    ///  `x::y`
-    Completion(SubExpr, SubExpr),
-}
-
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
@@ -249,45 +227,6 @@ impl<SE> ExprKind<SE> {
     }
 }
 
-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))))
-    }
-}
-
 impl Expr {
     pub fn as_ref(&self) -> &UnspannedExpr {
         &self.kind
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index b183f6c..f062089 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -3,10 +3,11 @@ 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,
-    Integer, InterpolatedText, Label, Natural, NumKind, OpKind, Scheme, Span,
+    Integer, InterpolatedText, Label, Natural, NumKind, Scheme, Span,
     UnspannedExpr, URL, V,
 };
 type DecodedExpr = Expr;
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index f2bc6f1..cef2af8 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -3,11 +3,12 @@ use std::collections::BTreeMap;
 use std::vec;
 
 use crate::error::EncodeError;
+use crate::operations::OpKind;
 use crate::syntax;
 use crate::syntax::map::DupTreeMap;
 use crate::syntax::{
     Expr, ExprKind, FilePrefix, Hash, Import, ImportMode, ImportTarget, Label,
-    OpKind, Scheme, V,
+    Scheme, V,
 };
 
 pub fn encode(expr: &Expr) -> Result<Vec<u8>, EncodeError> {
@@ -49,7 +50,7 @@ where
     use syntax::Builtin;
     use syntax::ExprKind::*;
     use syntax::NumKind::*;
-    use syntax::OpKind::*;
+    use OpKind::*;
 
     use self::Serialize::{RecordDupMap, RecordMap, UnionMap};
     fn expr(x: &Expr) -> self::Serialize<'_> {
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index ab9bc24..8d76225 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -7,10 +7,10 @@ use std::rc::Rc;
 
 use pest_consume::{match_nodes, Parser};
 
+use crate::operations::OpKind::*;
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::ExprKind::*;
 use crate::syntax::NumKind::*;
-use crate::syntax::OpKind::*;
 use crate::syntax::{
     Double, Expr, FilePath, FilePrefix, Hash, ImportMode, ImportTarget,
     Integer, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble,
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index d655489..a85f435 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -1,3 +1,4 @@
+use crate::operations::OpKind;
 use crate::syntax::*;
 use itertools::Itertools;
 use std::fmt::{self, Display};
@@ -37,8 +38,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 crate::syntax::OpKind::*;
+        use ExprKind::*;
+        use OpKind::*;
         use PrintPhase::*;
         let with_base = self.map_ref(|e| PhasedExpr(e, Base));
         match with_base {
@@ -89,8 +90,8 @@ impl UnspannedExpr {
         f: &mut fmt::Formatter,
         phase: PrintPhase,
     ) -> Result<(), fmt::Error> {
-        use crate::syntax::ExprKind::*;
-        use crate::syntax::OpKind::*;
+        use ExprKind::*;
+        use OpKind::*;
 
         let needs_paren = match self {
             Lam(_, _, _)
@@ -212,7 +213,7 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
 /// 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 crate::syntax::OpKind::*;
+        use OpKind::*;
         match self {
             App(a, b) => {
                 write!(f, "{} {}", a, b)?;
diff --git a/serde_dhall/src/value.rs b/serde_dhall/src/value.rs
index 587349c..e8f333e 100644
--- a/serde_dhall/src/value.rs
+++ b/serde_dhall/src/value.rs
@@ -1,7 +1,8 @@
 use std::collections::{BTreeMap, HashMap};
 
+use dhall::operations::OpKind;
 use dhall::semantics::{Hir, HirKind, Nir, NirKind};
-use dhall::syntax::{Builtin, Expr, ExprKind, NumKind, OpKind, Span};
+use dhall::syntax::{Builtin, Expr, ExprKind, NumKind, Span};
 
 use crate::{Error, ErrorKind, FromDhall, Result, Sealed};