Improve ergonomics of typechecking

1 files changed, 248 insertions, 354 deletions

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 15629a9..26ab360 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -5,24 +5,24 @@ use std::fmt;
 use std::rc::Rc;
 
 use crate::normalize::normalize;
+use dhall_core;
 use dhall_core::context::Context;
-use dhall_core::core;
-use dhall_core::core::Builtin::*;
-use dhall_core::core::Const::*;
-use dhall_core::core::Expr::*;
-use dhall_core::core::{bx, rc, shift, subst, Expr, Label, V, X};
+use dhall_core::*;
 use dhall_generator::dhall_expr;
 
 use self::TypeMessage::*;
 
-fn axiom<S>(c: core::Const) -> Result<core::Const, TypeError<S>> {
+fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
+    use dhall_core::Const::*;
+    use dhall_core::Expr::*;
     match c {
         Type => Ok(Kind),
         Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)),
     }
 }
 
-fn rule(a: &core::Const, b: &core::Const) -> Result<core::Const, ()> {
+fn rule(a: Const, b: Const) -> Result<Const, ()> {
+    use dhall_core::Const::*;
     match (a, b) {
         (Type, Kind) => Err(()),
         (Kind, Kind) => Ok(Kind),
@@ -31,46 +31,51 @@ fn rule(a: &core::Const, b: &core::Const) -> Result<core::Const, ()> {
 }
 
 fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool {
-    let xxs: Option<(&(Label, Label), &[(Label, Label)])> = ctx.split_first();
-    match (vl, vr, xxs) {
-        (V(xL, nL), V(xR, nR), None) => xL == xR && nL == nR,
-        (V(xL, 0), V(xR, 0), Some(((xL2, xR2), _)))
-            if xL == xL2 && xR == xR2 =>
-        {
-            true
-        }
-        (V(xL, nL), V(xR, nR), Some(((xL2, xR2), xs))) => {
-            let nL2 = if xL == xL2 { nL - 1 } else { *nL };
-            let nR2 = if xR == xR2 { nR - 1 } else { *nR };
-            match_vars(&V(xL.clone(), nL2), &V(xR.clone(), nR2), xs)
+    let mut vl = vl.clone();
+    let mut vr = vr.clone();
+    let mut ctx = ctx.to_vec();
+    ctx.reverse();
+    while let Some((xL2, xR2)) = &ctx.pop() {
+        match (&vl, &vr) {
+            (V(xL, 0), V(xR, 0)) if xL == xL2 && xR == xR2 => return true,
+            (V(xL, nL), V(xR, nR)) => {
+                let nL2 = if xL == xL2 { nL - 1 } else { *nL };
+                let nR2 = if xR == xR2 { nR - 1 } else { *nR };
+                vl = V(xL.clone(), nL2);
+                vr = V(xR.clone(), nR2);
+            }
         }
     }
+    vl == vr
 }
 
-fn prop_equal<S, T>(eL0: Rc<Expr<S, X>>, eR0: Rc<Expr<T, X>>) -> bool
+// Takes normalized expressions as input
+fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
 where
     S: ::std::fmt::Debug,
     T: ::std::fmt::Debug,
 {
+    use dhall_core::Expr::*;
     fn go<S, T>(
         ctx: &mut Vec<(Label, Label)>,
-        el: Rc<Expr<S, X>>,
-        er: Rc<Expr<T, X>>,
+        el: &Expr<S, X>,
+        er: &Expr<T, X>,
     ) -> bool
     where
         S: ::std::fmt::Debug,
         T: ::std::fmt::Debug,
     {
-        match (el.as_ref(), er.as_ref()) {
-            (&Const(Type), &Const(Type)) | (&Const(Kind), &Const(Kind)) => true,
+        match (el, er) {
+            (&Const(a), &Const(b)) => a == b,
+            (&Builtin(a), &Builtin(b)) => a == b,
             (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, ctx),
             (&Pi(ref xL, ref tL, ref bL), &Pi(ref xR, ref tR, ref bR)) => {
                 //ctx <- State.get
-                let eq1 = go(ctx, Rc::clone(tL), Rc::clone(tR));
+                let eq1 = go(ctx, tL.as_ref(), tR.as_ref());
                 if eq1 {
                     //State.put ((xL, xR):ctx)
                     ctx.push((xL.clone(), xR.clone()));
-                    let eq2 = go(ctx, Rc::clone(bL), Rc::clone(bR));
+                    let eq2 = go(ctx, bL.as_ref(), bR.as_ref());
                     //State.put ctx
                     let _ = ctx.pop();
                     eq2
@@ -79,96 +84,100 @@ where
                 }
             }
             (&App(ref fL, ref aL), &App(ref fR, ref aR)) => {
-                if go(ctx, Rc::clone(fL), Rc::clone(fR)) {
-                    aL.iter()
+                go(ctx, fL.as_ref(), fR.as_ref())
+                    && aL.len() == aR.len()
+                    && aL
+                        .iter()
                         .zip(aR.iter())
-                        .all(|(aL, aR)| go(ctx, Rc::clone(aL), Rc::clone(aR)))
-                } else {
-                    false
-                }
+                        .all(|(aL, aR)| go(ctx, aL.as_ref(), aR.as_ref()))
             }
-            (&Builtin(a), &Builtin(b)) => a == b,
             (&Record(ref ktsL0), &Record(ref ktsR0)) => {
-                if ktsL0.len() != ktsR0.len() {
-                    return false;
-                }
-                /*
-                let go ((kL, tL):ktsL) ((kR, tR):ktsR)
-                        | kL == kR = do
-                            b <- go tL tR
-                            if b
-                                then go ktsL ktsR
-                                else return False
-                    go [] [] = return True
-                    go _  _  = return False
-                */
-                /*
-                for ((kL, tL), (kR, tR)) in ktsL0.iter().zip(ktsR0.iter()) {
-                    if kL == kR {
-                        if !go(ctx, tL, tR) {
-                            return false;
-                        }
-                    } else {
-                        return false;
-                    }
-                }
-                true
-                */
-                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
-                    kL != kR || !go(ctx, Rc::clone(tL), Rc::clone(tR))
-                })
+                ktsL0.len() == ktsR0.len()
+                    && ktsL0.iter().zip(ktsR0.iter()).all(
+                        |((kL, tL), (kR, tR))| {
+                            kL == kR && go(ctx, tL.as_ref(), tR.as_ref())
+                        },
+                    )
             }
             (&Union(ref ktsL0), &Union(ref ktsR0)) => {
-                if ktsL0.len() != ktsR0.len() {
-                    return false;
-                }
-                /*
-                    let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
-                            | kL == kR = do
-                                b <- go tL tR
-                                if b
-                                    then loop ktsL ktsR
-                                    else return False
-                        loop [] [] = return True
-                        loop _  _  = return False
-                    loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0)
-                */
-                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
-                    kL != kR || !go(ctx, Rc::clone(tL), Rc::clone(tR))
-                })
+                ktsL0.len() == ktsR0.len()
+                    && ktsL0.iter().zip(ktsR0.iter()).all(
+                        |((kL, tL), (kR, tR))| {
+                            kL == kR && go(ctx, tL.as_ref(), tR.as_ref())
+                        },
+                    )
             }
             (_, _) => false,
         }
     }
     let mut ctx = vec![];
-    go::<S, T>(&mut ctx, normalize(eL0), normalize(eR0))
+    go::<S, T>(&mut ctx, eL0, eR0)
 }
 
-fn op2_type<S, EF>(
-    ctx: &Context<Label, Rc<Expr<S, X>>>,
-    e: Rc<Expr<S, X>>,
-    t: core::Builtin,
-    ef: EF,
-    l: &Rc<Expr<S, X>>,
-    r: &Rc<Expr<S, X>>,
-) -> Result<Expr<S, X>, TypeError<S>>
-where
-    S: ::std::fmt::Debug,
-    EF: FnOnce(Rc<Expr<S, X>>, Rc<Expr<S, X>>) -> TypeMessage<S>,
-{
-    let tl = normalize(type_with(ctx, l.clone())?);
-    match *tl {
-        Builtin(lt) if lt == t => {}
-        _ => return Err(TypeError::new(ctx, e, ef(l.clone(), tl))),
-    }
-
-    let tr = normalize(type_with(ctx, r.clone())?);
-    match *tr {
-        Builtin(rt) if rt == t => {}
-        _ => return Err(TypeError::new(ctx, e, ef(r.clone(), tr))),
+fn type_of_builtin<S>(b: Builtin) -> Rc<Expr<S, X>> {
+    use dhall_core::Builtin::*;
+    use dhall_core::Const::*;
+    use dhall_core::Expr::*;
+    match b {
+        Bool | Natural | Integer | Double | Text => dhall_expr!(Type),
+        List | Optional => dhall_expr!(
+            Type -> Type
+        ),
+        NaturalFold => dhall_expr!(
+            Natural ->
+            forall (natural: Type) ->
+            forall (succ: natural -> natural) ->
+            forall (zero: natural) ->
+            natural
+        ),
+        NaturalBuild => dhall_expr!(
+            (forall (natural: Type) ->
+                forall (succ: natural -> natural) ->
+                forall (zero: natural) ->
+                natural) ->
+            Natural
+        ),
+        NaturalIsZero | NaturalEven | NaturalOdd => dhall_expr!(
+            Natural -> Bool
+        ),
+        ListBuild => dhall_expr!(
+            forall (a: Type) ->
+            (forall (list: Type) ->
+                forall (cons: a -> list -> list) ->
+                forall (nil: list) ->
+                list) ->
+            List a
+        ),
+        ListFold => dhall_expr!(
+            forall (a: Type) ->
+            List a ->
+            forall (list: Type) ->
+            forall (cons: a -> list -> list) ->
+            forall (nil: list) ->
+            list
+        ),
+        ListLength => dhall_expr!(forall (a: Type) -> List a -> Natural),
+        ListHead | ListLast => {
+            dhall_expr!(forall (a: Type) -> List a -> Optional a)
+        }
+        ListIndexed => dhall_expr!(
+            forall (a: Type) ->
+            List a ->
+            List { index: Natural, value: a }
+        ),
+        ListReverse => dhall_expr!(
+            forall (a: Type) -> List a -> List a
+        ),
+        OptionalFold => dhall_expr!(
+            forall (a: Type) ->
+            Optional a ->
+            forall (optional: Type) ->
+            forall (just: a -> optional) ->
+            forall (nothing: optional) ->
+            optional
+        ),
+        _ => panic!("Unimplemented typecheck case: {:?}", b),
     }
-
-    Ok(Builtin(t))
 }
 
 /// Type-check an expression and return the expression'i type if type-checking
@@ -185,17 +194,31 @@ where
     S: ::std::fmt::Debug,
 {
     use dhall_core::BinOp::*;
+    use dhall_core::Builtin::*;
+    use dhall_core::Const::*;
     use dhall_core::Expr;
+    use dhall_core::Expr::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
-    match *e {
-        Const(c) => axiom(c).map(Const),
-        Var(V(ref x, n)) => {
+    let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref()
+    {
+        Const(k) => Ok(*k),
+        _ => Err(mkerr(msg)),
+    };
+    let ensure_is_type =
+        |x: SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref() {
+            Const(Type) => Ok(()),
+            _ => Err(mkerr(msg)),
+        };
+
+    match e.as_ref() {
+        Const(c) => axiom(*c).map(Const),
+        Var(V(x, n)) => {
             return ctx
-                .lookup(x, n)
+                .lookup(x, *n)
                 .cloned()
                 .ok_or_else(|| mkerr(UnboundVariable))
         }
-        Lam(ref x, ref tA, ref b) => {
+        Lam(x, tA, b) => {
             let ctx2 = ctx
                 .insert(x.clone(), tA.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
@@ -204,21 +227,16 @@ where
             let _ = type_with(ctx, p.clone())?;
             return Ok(p);
         }
-        Pi(ref x, ref tA, ref tB) => {
-            let tA2 = normalize(type_with(ctx, tA.clone())?);
-            let kA = match tA2.as_ref() {
-                Const(k) => k,
-                _ => {
-                    return Err(mkerr(InvalidInputType(tA.clone())));
-                }
-            };
+        Pi(x, tA, tB) => {
+            let tA2 = normalized_type_with(ctx, tA.clone())?;
+            let kA = ensure_const(&tA2, InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = normalize(type_with(&ctx2, tB.clone())?);
+            let tB = normalized_type_with(&ctx2, tB.clone())?;
             let kB = match tB.as_ref() {
-                Const(k) => k,
+                Const(k) => *k,
                 _ => {
                     return Err(TypeError::new(
                         &ctx2,
@@ -230,19 +248,19 @@ where
 
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(tA.clone(), tB))),
-                Ok(k) => Ok(Const(k)),
+                Ok(_) => Ok(Const(kB)),
             }
         }
-        App(ref f, ref args) => {
+        App(f, args) => {
             // Recurse on args
             let (a, tf) = match args.split_last() {
                 None => return type_with(ctx, f.clone()),
                 Some((a, args)) => (
                     a,
-                    normalize(type_with(
+                    normalized_type_with(
                         ctx,
                         rc(App(f.clone(), args.to_vec())),
-                    )?),
+                    )?,
                 ),
             };
             let (x, tA, tB) = match tf.as_ref() {
@@ -251,116 +269,79 @@ where
                     return Err(mkerr(NotAFunction(f.clone(), tf)));
                 }
             };
-            let tA2 = type_with(ctx, a.clone())?;
-            if prop_equal(tA.clone(), tA2.clone()) {
+            let tA = normalize(Rc::clone(tA));
+            let tA2 = normalized_type_with(ctx, a.clone())?;
+            if prop_equal(tA.as_ref(), tA2.as_ref()) {
                 let vx0 = &V(x.clone(), 0);
                 let a2 = shift(1, vx0, a);
                 let tB2 = subst(vx0, &a2, &tB);
                 let tB3 = shift(-1, vx0, &tB2);
                 return Ok(tB3);
             } else {
-                let nf_A = normalize(tA.clone());
-                let nf_A2 = normalize(tA2);
-                Err(mkerr(TypeMismatch(f.clone(), nf_A, a.clone(), nf_A2)))
+                Err(mkerr(TypeMismatch(f.clone(), tA, a.clone(), tA2)))
             }
         }
-        Let(ref f, ref mt, ref r, ref b) => {
-            let tR = type_with(ctx, r.clone())?;
-            let ttR = normalize(type_with(ctx, tR.clone())?);
-            let kR = match ttR.as_ref() {
-                Const(k) => k,
-                // Don't bother to provide a `let`-specific version of this error
-                // message because this should never happen anyway
-                _ => return Err(mkerr(InvalidInputType(tR))),
+        Let(f, mt, r, b) => {
+            let r = if let Some(t) = mt {
+                rc(Annot(Rc::clone(r), Rc::clone(t)))
+            } else {
+                Rc::clone(r)
             };
 
+            let tR = type_with(ctx, r)?;
+            let ttR = normalized_type_with(ctx, tR.clone())?;
+            // Don't bother to provide a `let`-specific version of this error
+            // message because this should never happen anyway
+            let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?;
+
             let ctx2 = ctx.insert(f.clone(), tR.clone());
             let tB = type_with(&ctx2, b.clone())?;
-            let ttB = normalize(type_with(ctx, tB.clone())?);
-            let kB = match ttB.as_ref() {
-                Const(k) => k,
-                // Don't bother to provide a `let`-specific version of this error
-                // message because this should never happen anyway
-                _ => return Err(mkerr(InvalidOutputType(tB))),
-            };
+            let ttB = normalized_type_with(ctx, tB.clone())?;
+            // Don't bother to provide a `let`-specific version of this error
+            // message because this should never happen anyway
+            let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?;
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(tR, tB)));
             }
 
-            if let Some(ref t) = *mt {
-                let nf_t = normalize(t.clone());
-                let nf_tR = normalize(tR);
-                if !prop_equal(nf_tR.clone(), nf_t.clone()) {
-                    return Err(mkerr(AnnotMismatch(r.clone(), nf_t, nf_tR)));
-                }
-            }
-
             return Ok(tB);
         }
-        Annot(ref x, ref t) => {
+        Annot(x, t) => {
             // This is mainly just to check that `t` is not `Kind`
             let _ = type_with(ctx, t.clone())?;
 
-            let t2 = type_with(ctx, x.clone())?;
-            if prop_equal(t.clone(), t2.clone()) {
+            let t2 = normalized_type_with(ctx, x.clone())?;
+            let t = normalize(t.clone());
+            if prop_equal(t.as_ref(), t2.as_ref()) {
                 return Ok(t.clone());
             } else {
-                let nf_t = normalize(t.clone());
-                let nf_t2 = normalize(t2);
-                Err(mkerr(AnnotMismatch(x.clone(), nf_t, nf_t2)))
+                Err(mkerr(AnnotMismatch(x.clone(), t, t2)))
             }
         }
-        BoolLit(_) => Ok(Builtin(Bool)),
-        BinOp(BoolAnd, ref l, ref r) => {
-            op2_type(ctx, e.clone(), Bool, CantAnd, l, r)
-        }
-        BinOp(BoolOr, ref l, ref r) => {
-            op2_type(ctx, e.clone(), Bool, CantOr, l, r)
-        }
-        BinOp(BoolEQ, ref l, ref r) => {
-            op2_type(ctx, e.clone(), Bool, CantEQ, l, r)
-        }
-        BinOp(BoolNE, ref l, ref r) => {
-            op2_type(ctx, e.clone(), Bool, CantNE, l, r)
-        }
-        BoolIf(ref x, ref y, ref z) => {
-            let tx = normalize(type_with(ctx, x.clone())?);
+        BoolIf(x, y, z) => {
+            let tx = normalized_type_with(ctx, x.clone())?;
             match tx.as_ref() {
                 Builtin(Bool) => {}
                 _ => {
                     return Err(mkerr(InvalidPredicate(x.clone(), tx)));
                 }
             }
-            let ty = normalize(type_with(ctx, y.clone())?);
-            let tty = normalize(type_with(ctx, ty.clone())?);
-            match tty.as_ref() {
-                Const(Type) => {}
-                _ => {
-                    return Err(mkerr(IfBranchMustBeTerm(
-                        true,
-                        y.clone(),
-                        ty,
-                        tty,
-                    )));
-                }
-            }
+            let ty = normalized_type_with(ctx, y.clone())?;
+            let tty = normalized_type_with(ctx, ty.clone())?;
+            ensure_is_type(
+                tty.clone(),
+                IfBranchMustBeTerm(true, y.clone(), ty.clone(), tty.clone()),
+            )?;
 
-            let tz = normalize(type_with(ctx, z.clone())?);
-            let ttz = normalize(type_with(ctx, tz.clone())?);
-            match ttz.as_ref() {
-                Const(Type) => {}
-                _ => {
-                    return Err(mkerr(IfBranchMustBeTerm(
-                        false,
-                        z.clone(),
-                        tz,
-                        ttz,
-                    )));
-                }
-            }
+            let tz = normalized_type_with(ctx, z.clone())?;
+            let ttz = normalized_type_with(ctx, tz.clone())?;
+            ensure_is_type(
+                ttz.clone(),
+                IfBranchMustBeTerm(false, z.clone(), tz.clone(), ttz.clone()),
+            )?;
 
-            if !prop_equal(ty.clone(), tz.clone()) {
+            if !prop_equal(ty.as_ref(), tz.as_ref()) {
                 return Err(mkerr(IfBranchMismatch(
                     y.clone(),
                     z.clone(),
@@ -370,43 +351,7 @@ where
             }
             return Ok(ty);
         }
-        NaturalLit(_) => Ok(Builtin(Natural)),
-        Builtin(NaturalFold) => {
-            return Ok(dhall_expr!(
-                Natural ->
-                forall (natural: Type) ->
-                forall (succ: natural -> natural) ->
-                forall (zero: natural) ->
-                natural
-            ))
-        }
-        Builtin(NaturalBuild) => {
-            return Ok(dhall_expr!(
-                (forall (natural: Type) ->
-                    forall (succ: natural -> natural) ->
-                    forall (zero: natural) ->
-                    natural) ->
-                Natural
-            ))
-        }
-        Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => {
-            return Ok(dhall_expr!(
-                Natural -> Bool
-            ))
-        }
-        BinOp(NaturalPlus, ref l, ref r) => {
-            op2_type(ctx, e.clone(), Natural, CantAdd, l, r)
-        }
-        BinOp(NaturalTimes, ref l, ref r) => {
-            op2_type(ctx, e.clone(), Natural, CantMultiply, l, r)
-        }
-        IntegerLit(_) => Ok(Builtin(Integer)),
-        DoubleLit(_) => Ok(Builtin(Double)),
-        TextLit(_) => Ok(Builtin(Text)),
-        BinOp(TextAppend, ref l, ref r) => {
-            op2_type(ctx, e.clone(), Text, CantTextAppend, l, r)
-        }
-        ListLit(ref t, ref xs) => {
+        ListLit(t, xs) => {
             let mut iter = xs.iter().enumerate();
             let t: Rc<Expr<_, _>> = match t {
                 Some(t) => t.clone(),
@@ -416,65 +361,18 @@ where
                 }
             };
 
-            let s = normalize(type_with(ctx, t.clone())?);
-            match s.as_ref() {
-                Const(Type) => {}
-                _ => return Err(mkerr(InvalidListType(t))),
-            }
+            let s = normalized_type_with(ctx, t.clone())?;
+            ensure_is_type(s, InvalidListType(t.clone()))?;
+            let t = normalize(t);
             for (i, x) in iter {
-                let t2 = type_with(ctx, x.clone())?;
-                if !prop_equal(t.clone(), t2.clone()) {
-                    let nf_t = normalize(t);
-                    let nf_t2 = normalize(t2);
-                    return Err(mkerr(InvalidListElement(
-                        i,
-                        nf_t,
-                        x.clone(),
-                        nf_t2,
-                    )));
+                let t2 = normalized_type_with(ctx, x.clone())?;
+                if !prop_equal(t.as_ref(), t2.as_ref()) {
+                    return Err(mkerr(InvalidListElement(i, t, x.clone(), t2)));
                 }
             }
             return Ok(dhall_expr!(List t));
         }
-        Builtin(ListBuild) => {
-            return Ok(dhall_expr!(
-                forall (a: Type) ->
-                (forall (list: Type) ->
-                    forall (cons: a -> list -> list) ->
-                    forall (nil: list) ->
-                    list) ->
-                List a
-            ))
-        }
-        Builtin(ListFold) => {
-            return Ok(dhall_expr!(
-                forall (a: Type) ->
-                List a ->
-                forall (list: Type) ->
-                forall (cons: a -> list -> list) ->
-                forall (nil: list) ->
-                list
-            ))
-        }
-        Builtin(ListLength) => {
-            return Ok(dhall_expr!(forall (a: Type) -> List a -> Natural))
-        }
-        Builtin(ListHead) | Builtin(ListLast) => {
-            return Ok(dhall_expr!(forall (a: Type) -> List a -> Optional a))
-        }
-        Builtin(ListIndexed) => {
-            return Ok(dhall_expr!(
-                forall (a: Type) ->
-                List a ->
-                List { index: Natural, value: a }
-            ))
-        }
-        Builtin(ListReverse) => {
-            return Ok(dhall_expr!(
-                forall (a: Type) -> List a -> List a
-            ))
-        }
-        OptionalLit(ref t, ref xs) => {
+        OptionalLit(t, xs) => {
             let mut iter = xs.iter();
             let t: Rc<Expr<_, _>> = match t {
                 Some(t) => t.clone(),
@@ -484,83 +382,44 @@ where
                 }
             };
 
-            let s = normalize(type_with(ctx, t.clone())?);
-            match s.as_ref() {
-                Const(Type) => {}
-                _ => {
-                    return Err(mkerr(InvalidOptionalType(t)));
-                }
-            }
+            let s = normalized_type_with(ctx, t.clone())?;
+            ensure_is_type(s, InvalidOptionalType(t.clone()))?;
+            let t = normalize(t);
             for x in iter {
-                let t2 = type_with(ctx, x.clone())?;
-                if !prop_equal(t.clone(), t2.clone()) {
-                    let nf_t = normalize(t);
-                    let nf_t2 = normalize(t2);
+                let t2 = normalized_type_with(ctx, x.clone())?;
+                if !prop_equal(t.as_ref(), t2.as_ref()) {
                     return Err(mkerr(InvalidOptionalElement(
-                        nf_t,
+                        t,
                         x.clone(),
-                        nf_t2,
+                        t2,
                     )));
                 }
             }
             return Ok(dhall_expr!(Optional t));
         }
-        Builtin(OptionalFold) => {
-            return Ok(dhall_expr!(
-                forall (a: Type) ->
-                Optional a ->
-                forall (optional: Type) ->
-                forall (just: a -> optional) ->
-                forall (nothing: optional) ->
-                optional
-            ))
-        }
-        Builtin(List) | Builtin(Optional) => {
-            return Ok(dhall_expr!(
-                Type -> Type
-            ))
-        }
-        Builtin(Bool) | Builtin(Natural) | Builtin(Integer)
-        | Builtin(Double) | Builtin(Text) => Ok(Const(Type)),
-        Record(ref kts) => {
+        Record(kts) => {
             for (k, t) in kts {
-                let s = normalize(type_with(ctx, t.clone())?);
-                match s.as_ref() {
-                    Const(Type) => {}
-                    _ => {
-                        return Err(mkerr(InvalidFieldType(
-                            k.clone(),
-                            t.clone(),
-                        )));
-                    }
-                }
+                let s = normalized_type_with(ctx, t.clone())?;
+                ensure_is_type(s, InvalidFieldType(k.clone(), t.clone()))?;
             }
             Ok(Const(Type))
         }
-        RecordLit(ref kvs) => {
+        RecordLit(kvs) => {
             let kts = kvs
                 .iter()
                 .map(|(k, v)| {
                     let t = type_with(ctx, v.clone())?;
-                    let s = normalize(type_with(ctx, t.clone())?);
-                    match s.as_ref() {
-                        Const(Type) => {}
-                        _ => {
-                            return Err(mkerr(InvalidField(
-                                k.clone(),
-                                v.clone(),
-                            )));
-                        }
-                    }
+                    let s = normalized_type_with(ctx, t.clone())?;
+                    ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
                     Ok((k.clone(), t))
                 })
                 .collect::<Result<_, _>>()?;
             Ok(Record(kts))
         }
-        Field(ref r, ref x) => {
-            let t = normalize(type_with(ctx, r.clone())?);
+        Field(r, x) => {
+            let t = normalized_type_with(ctx, r.clone())?;
             match t.as_ref() {
-                Record(ref kts) => {
+                Record(kts) => {
                     return kts.get(x).cloned().ok_or_else(|| {
                         mkerr(MissingField(x.clone(), t.clone()))
                     })
@@ -568,12 +427,53 @@ where
                 _ => Err(mkerr(NotARecord(x.clone(), r.clone(), t.clone()))),
             }
         }
-        Embed(p) => match p {},
+        Builtin(b) => return Ok(type_of_builtin(*b)),
+        BoolLit(_) => Ok(Builtin(Bool)),
+        NaturalLit(_) => Ok(Builtin(Natural)),
+        IntegerLit(_) => Ok(Builtin(Integer)),
+        DoubleLit(_) => Ok(Builtin(Double)),
+        TextLit(_) => Ok(Builtin(Text)),
+        BinOp(o, l, r) => {
+            let t = match o {
+                BoolAnd => Bool,
+                BoolOr => Bool,
+                BoolEQ => Bool,
+                BoolNE => Bool,
+                NaturalPlus => Natural,
+                NaturalTimes => Natural,
+                TextAppend => Text,
+                _ => panic!("Unimplemented typecheck case: {:?}", e),
+            };
+            let tl = normalized_type_with(ctx, l.clone())?;
+            match tl.as_ref() {
+                Builtin(lt) if *lt == t => {}
+                _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone(), tl))),
+            }
+
+            let tr = normalized_type_with(ctx, r.clone())?;
+            match tr.as_ref() {
+                Builtin(rt) if *rt == t => {}
+                _ => return Err(mkerr(BinOpTypeMismatch(*o, r.clone(), tr))),
+            }
+
+            Ok(Builtin(t))
+        }
+        Embed(p) => match *p {},
         _ => panic!("Unimplemented typecheck case: {:?}", e),
     }
     .map(rc)
 }
 
+pub fn normalized_type_with<S>(
+    ctx: &Context<Label, Rc<Expr<S, X>>>,
+    e: Rc<Expr<S, X>>,
+) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+where
+    S: ::std::fmt::Debug,
+{
+    Ok(normalize(type_with(ctx, e)?))
+}
+
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
@@ -628,13 +528,7 @@ pub enum TypeMessage<S> {
     HandlerNotAFunction(Label, Rc<Expr<S, X>>),
     NotARecord(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     MissingField(Label, Rc<Expr<S, X>>),
-    CantAnd(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    CantOr(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    CantEQ(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    CantNE(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    CantTextAppend(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    CantAdd(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    CantMultiply(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    BinOpTypeMismatch(BinOp, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     NoDependentLet(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     NoDependentTypes(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
 }
@@ -676,11 +570,11 @@ impl<S: fmt::Debug> ::std::error::Error for TypeMessage<S> {
 
 impl<S> fmt::Display for TypeMessage<S> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        match *self {
+        match self {
             UnboundVariable => {
                 f.write_str(include_str!("errors/UnboundVariable.txt"))
             }
-            TypeMismatch(ref e0, ref e1, ref e2, ref e3) => {
+            TypeMismatch(e0, e1, e2, e3) => {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
                     .replace("$txt0", &format!("{}", e0))