Factor out operations in typecheck

2 files changed, 438 insertions, 417 deletions

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 8f3fcb2..28d08b9 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -66,206 +66,263 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
     )
 }
 
-/// When all sub-expressions have been typed, check the remaining toplevel
-/// layer.
-fn type_one_layer(
+fn type_of_binop(
     env: &TyEnv,
-    ekind: ExprKind<Tir<'_>>,
     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};
 
-    let ty = match &ekind {
-        ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => {
-            unreachable!("This case should have been handled in resolution")
-        }
-        ExprKind::Var(..)
-        | ExprKind::Const(Const::Sort)
-        | ExprKind::Lam(..)
-        | ExprKind::Pi(..)
-        | ExprKind::Let(..)
-        | ExprKind::Annot(..) => {
-            unreachable!("This case should have been handled in type_with")
-        }
+    Ok(match op {
+        RightBiasedRecordMerge => {
+            let x_type = l.ty();
+            let y_type = r.ty();
 
-        ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
-        ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
-        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)
+            // 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)
         }
-        ExprKind::TextLit(interpolated) => {
-            let text_type = Type::from_builtin(Builtin::Text);
-            for contents in interpolated.iter() {
-                use InterpolatedTextContents::Expr;
-                if let Expr(x) = contents {
-                    if *x.ty() != text_type {
-                        return span_err("InvalidTextInterpolation");
-                    }
-                }
-            }
-            text_type
+        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))
         }
-        ExprKind::EmptyListLit(t) => {
-            let t = t.eval_to_type(env)?;
-            match t.kind() {
-                NirKind::ListType(..) => {}
-                _ => return span_err("InvalidListType"),
-            };
-            t
+        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))
         }
-        ExprKind::NEListLit(xs) => {
-            let mut iter = xs.iter();
-            let x = iter.next().unwrap();
-            for y in iter {
-                if x.ty() != y.ty() {
-                    return span_err("InvalidListElement");
-                }
+        ListAppend => {
+            match l.ty().kind() {
+                ListType(..) => {}
+                _ => return span_err("BinOpTypeMismatch"),
             }
-            if x.ty().ty().as_const() != Some(Const::Type) {
-                return span_err("InvalidListType");
+
+            if l.ty() != r.ty() {
+                return span_err("BinOpTypeMismatch");
             }
 
-            let t = x.ty().to_nir();
-            Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
+            l.ty().clone()
         }
-        ExprKind::SomeLit(x) => {
-            if x.ty().ty().as_const() != Some(Const::Type) {
-                return span_err("InvalidOptionalType");
+        Equivalence => {
+            if l.ty() != r.ty() {
+                return span_err("EquivalenceTypeMismatch");
+            }
+            if l.ty().ty().as_const() != Some(Const::Type) {
+                return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
-            let t = x.ty().to_nir();
-            Nir::from_builtin(Builtin::Optional)
-                .app(t)
-                .to_type(Const::Type)
+            Type::from_const(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()),
-                };
+        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"),
+            });
 
-                // 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"),
-                }
+            if *l.ty() != t {
+                return span_err("BinOpTypeMismatch");
             }
 
-            Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
+            if *r.ty() != t {
+                return span_err("BinOpTypeMismatch");
+            }
+
+            t
         }
-        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(()),
-                };
+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};
 
-                // 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"),
-                }
-            }
+    let record_type = scrut.ty();
+    let handlers = match record_type.kind() {
+        RecordType(kts) => kts,
+        _ => return span_err("Merge1ArgMustBeRecord"),
+    };
 
-            Type::from_const(k)
+    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)
         }
-        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 {
-                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"),
-                    }
-                }
-                match seen_fields.entry(x) {
-                    Entry::Occupied(_) => {
-                        return span_err("UnionTypeDuplicateField")
-                    }
-                    Entry::Vacant(e) => e.insert(()),
-                };
-            }
+        _ => return span_err("Merge2ArgMustBeUnionOrOptional"),
+    };
 
-            // An empty union type has type Type;
-            // an union type with only unary variants also has type Type
-            let k = k.unwrap_or(Const::Type);
+    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(),
+                        );
+                    }
 
-            Type::from_const(k)
-        }
-        ExprKind::Op(OpKind::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"),
+                    // 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 span_err("NotARecord"),
+                _ => {
+                    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");
+                }
             }
         }
-        ExprKind::Assert(t) => {
-            let t = t.eval_to_type(env)?;
-            match t.kind() {
-                NirKind::Equivalence(x, y) if x == y => {}
-                NirKind::Equivalence(..) => return span_err("AssertMismatch"),
-                _ => return span_err("AssertMustTakeEquivalence"),
+    }
+    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");
             }
-            t
+            t1
         }
-        ExprKind::Op(OpKind::App(f, arg)) => {
+        (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
-                NirKind::PiClosure { annot, closure, .. } => {
+                PiClosure { annot, closure, .. } => {
                     if arg.ty().as_nir() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
@@ -310,7 +367,8 @@ fn type_one_layer(
                 ),
             }
         }
-        ExprKind::Op(OpKind::BoolIf(x, y, z)) => {
+        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");
             }
@@ -323,245 +381,16 @@ fn type_one_layer(
 
             y.ty().clone()
         }
-        ExprKind::Op(OpKind::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)
+        Merge(record, scrut, type_annot) => {
+            type_of_merge(env, span, record, scrut, type_annot.as_ref())?
         }
-        ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => {
-            check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
-
-            let hir = Hir::new(
-                HirKind::Expr(ExprKind::Op(OpKind::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::Op(OpKind::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::Op(OpKind::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::Op(OpKind::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::Op(OpKind::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::Op(OpKind::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::Op(OpKind::ToMap(record, annot)) => {
+        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,
+                RecordType(kts) => kts,
                 _ => {
                     return span_err("The argument to `toMap` must be a record")
                 }
@@ -581,11 +410,11 @@ fn type_one_layer(
                 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,
+                    ListType(t) => t,
                     _ => return span_err(err_msg),
                 };
                 let kts = match arg.kind() {
-                    NirKind::RecordType(kts) => kts,
+                    RecordType(kts) => kts,
                     _ => return span_err(err_msg),
                 };
                 if kts.len() != 2 {
@@ -614,7 +443,7 @@ fn type_one_layer(
                 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)))
+                    .app(Nir::from_kind(RecordType(kts)))
                     .to_type(Const::Type);
                 if let Some(annot) = annot {
                     let annot_val = annot.eval_to_type(env)?;
@@ -625,10 +454,36 @@ fn type_one_layer(
                 output_type
             }
         }
-        ExprKind::Op(OpKind::Projection(record, labels)) => {
+        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() {
-                NirKind::RecordType(kts) => kts,
+                RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
@@ -648,21 +503,18 @@ fn type_one_layer(
                 };
             }
 
-            Type::new_infer_universe(
-                env,
-                Nir::from_kind(NirKind::RecordType(new_kts)),
-            )?
+            Type::new_infer_universe(env, Nir::from_kind(RecordType(new_kts)))?
         }
-        ExprKind::Op(OpKind::ProjectionByExpr(record, selection)) => {
+        ProjectionByExpr(record, selection) => {
             let record_type = record.ty();
             let rec_kts = match record_type.kind() {
-                NirKind::RecordType(kts) => kts,
+                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,
+                RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
             };
 
@@ -679,13 +531,182 @@ fn type_one_layer(
 
             selection_val
         }
-    };
+        Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
+        }
+    })
+}
 
-    Ok(ty)
+/// When all sub-expressions have been typed, check the remaining toplevel
+/// layer.
+fn type_one_layer(
+    env: &TyEnv,
+    ekind: ExprKind<Tir<'_>>,
+    span: Span,
+) -> Result<Type, TypeError> {
+    let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+
+    Ok(match &ekind {
+        ExprKind::Import(..) => {
+            unreachable!("This case should have been handled in resolution")
+        }
+        ExprKind::Var(..)
+        | ExprKind::Const(Const::Sort)
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..)
+        | ExprKind::Annot(..) => {
+            unreachable!("This case should have been handled in type_with")
+        }
+
+        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::TextLit(interpolated) => {
+            let text_type = Type::from_builtin(Builtin::Text);
+            for contents in interpolated.iter() {
+                use InterpolatedTextContents::Expr;
+                if let Expr(x) = contents {
+                    if *x.ty() != text_type {
+                        return span_err("InvalidTextInterpolation");
+                    }
+                }
+            }
+            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() {
+                NirKind::ListType(..) => {}
+                _ => return span_err("InvalidListType"),
+            };
+            t
+        }
+        ExprKind::NEListLit(xs) => {
+            let mut iter = xs.iter();
+            let x = iter.next().unwrap();
+            for y in iter {
+                if x.ty() != y.ty() {
+                    return span_err("InvalidListElement");
+                }
+            }
+            if x.ty().ty().as_const() != Some(Const::Type) {
+                return span_err("InvalidListType");
+            }
+
+            let t = x.ty().to_nir();
+            Nir::from_builtin(Builtin::List).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()),
+                };
+
+                // 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"),
+                }
+            }
+
+            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(()),
+                };
+
+                // 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"),
+                }
+            }
+
+            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 {
+                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"),
+                    }
+                }
+                match seen_fields.entry(x) {
+                    Entry::Occupied(_) => {
+                        return span_err("UnionTypeDuplicateField")
+                    }
+                    Entry::Vacant(e) => e.insert(()),
+                };
+            }
+
+            // An empty union type has type Type;
+            // an union type with only unary variants also has type Type
+            let k = k.unwrap_or(Const::Type);
+
+            Type::from_const(k)
+        }
+        ExprKind::Op(op) => type_of_operation(env, span, op)?,
+        ExprKind::Assert(t) => {
+            let t = t.eval_to_type(env)?;
+            match t.kind() {
+                NirKind::Equivalence(x, y) if x == y => {}
+                NirKind::Equivalence(..) => return span_err("AssertMismatch"),
+                _ => return span_err("AssertMustTakeEquivalence"),
+            }
+            t
+        }
+    })
 }
 
 /// `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,
@@ -781,7 +802,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 51426ce..51e9ea7 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -161,10 +161,10 @@ pub enum ExprKind<SubExpr> {
     Num(NumKind),
     /// Built-in functions and types
     Builtin(Builtin),
-    ///  `Some e`
-    SomeLit(SubExpr),
     ///  `"Some ${interpolated} text"`
     TextLit(InterpolatedText<SubExpr>),
+    ///  `Some e`
+    SomeLit(SubExpr),
     ///  `[] : t`
     EmptyListLit(SubExpr),
     ///  `[x, y, z]`