Merge branch 'improve_typecheck_code'

10 files changed, 543 insertions, 263 deletions

diff --git a/README.md b/README.md
index 6ba1bfc..599d48b 100644
--- a/README.md
+++ b/README.md
@@ -12,7 +12,7 @@ This language is defined by a [standard](https://github.com/dhall-lang/dhall-lan
 - Parsing: 100%
 - Imports: 0%
 - Normalization: 74%
-- Typechecking: 78%
+- Typechecking: 66%
 
 You can see what's missing from the commented out tests in `dhall/tests`.
 
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 0270103..103fd29 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -14,6 +14,8 @@ mod dhall_type;
 pub mod imports;
 pub mod typecheck;
 pub use crate::dhall_type::*;
+pub use dhall_generator::expr;
+pub use dhall_generator::subexpr;
 pub use dhall_generator::Type;
 
 pub use crate::imports::*;
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 145de63..e63b032 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,7 +6,7 @@ use crate::normalize::normalize;
 use dhall_core;
 use dhall_core::context::Context;
 use dhall_core::*;
-use dhall_generator::dhall_expr;
+use dhall_generator as dhall;
 
 use self::TypeMessage::*;
 
@@ -112,31 +112,31 @@ where
     go::<S, T>(&mut ctx, eL0, eR0)
 }
 
-fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
+fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
     use dhall_core::Builtin::*;
     match b {
-        Bool | Natural | Integer | Double | Text => dhall_expr!(Type),
-        List | Optional => dhall_expr!(
+        Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
+        List | Optional => dhall::expr!(
             Type -> Type
         ),
-        NaturalFold => dhall_expr!(
+        NaturalFold => dhall::expr!(
             Natural ->
             forall (natural: Type) ->
             forall (succ: natural -> natural) ->
             forall (zero: natural) ->
             natural
         ),
-        NaturalBuild => dhall_expr!(
+        NaturalBuild => dhall::expr!(
             (forall (natural: Type) ->
                 forall (succ: natural -> natural) ->
                 forall (zero: natural) ->
                 natural) ->
             Natural
         ),
-        NaturalIsZero | NaturalEven | NaturalOdd => dhall_expr!(
+        NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!(
             Natural -> Bool
         ),
-        ListBuild => dhall_expr!(
+        ListBuild => dhall::expr!(
             forall (a: Type) ->
             (forall (list: Type) ->
                 forall (cons: a -> list -> list) ->
@@ -144,7 +144,7 @@ fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
                 list) ->
             List a
         ),
-        ListFold => dhall_expr!(
+        ListFold => dhall::expr!(
             forall (a: Type) ->
             List a ->
             forall (list: Type) ->
@@ -152,19 +152,19 @@ fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
             forall (nil: list) ->
             list
         ),
-        ListLength => dhall_expr!(forall (a: Type) -> List a -> Natural),
+        ListLength => dhall::expr!(forall (a: Type) -> List a -> Natural),
         ListHead | ListLast => {
-            dhall_expr!(forall (a: Type) -> List a -> Optional a)
+            dhall::expr!(forall (a: Type) -> List a -> Optional a)
         }
-        ListIndexed => dhall_expr!(
+        ListIndexed => dhall::expr!(
             forall (a: Type) ->
             List a ->
             List { index: Natural, value: a }
         ),
-        ListReverse => dhall_expr!(
+        ListReverse => dhall::expr!(
             forall (a: Type) -> List a -> List a
         ),
-        OptionalFold => dhall_expr!(
+        OptionalFold => dhall::expr!(
             forall (a: Type) ->
             Optional a ->
             forall (optional: Type) ->
@@ -176,12 +176,29 @@ fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
     }
 }
 
-/// Type-check an expression and return the expression'i type if type-checking
-/// suceeds or an error if type-checking fails
+fn ensure_equal<'a, S, F1, F2>(
+    x: &'a Expr<S, X>,
+    y: &'a Expr<S, X>,
+    mkerr: F1,
+    mkmsg: F2,
+) -> Result<(), TypeError<S>>
+where
+    S: std::fmt::Debug,
+    F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
+    F2: FnOnce() -> TypeMessage<S>,
+{
+    if prop_equal(x, y) {
+        Ok(())
+    } else {
+        Err(mkerr(mkmsg()))
+    }
+}
+
+/// Type-check an expression and return the expression's type if type-checking
+/// succeeds or an error if type-checking fails
 ///
-/// `type_with` does not necessarily normalize the type since full normalization
-/// is not necessary for just type-checking.  If you actually care about the
-/// returned type then you may want to `normalize` it afterwards.
+/// `type_with` normalizes the type since while type-checking. It expects the
+/// context to contain only normalized expressions.
 pub fn type_with<S>(
     ctx: &Context<Label, SubExpr<S, X>>,
     e: SubExpr<S, X>,
@@ -205,31 +222,25 @@ where
             _ => Err(mkerr(msg)),
         };
 
-    match e.as_ref() {
-        Const(c) => axiom(*c).map(Const),
-        Var(V(x, n)) => {
-            return ctx
-                .lookup(x, *n)
-                .cloned()
-                .ok_or_else(|| mkerr(UnboundVariable))
-        }
-        Lam(x, tA, b) => {
+    let ret = match e.as_ref() {
+        Lam(x, t, b) => {
+            let t2 = normalize(SubExpr::clone(t));
             let ctx2 = ctx
-                .insert(x.clone(), tA.clone())
+                .insert(x.clone(), t2.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, b.clone())?;
-            let p = rc(Pi(x.clone(), tA.clone(), tB));
-            let _ = type_with(ctx, p.clone())?;
-            return Ok(p);
+            let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?;
+            Ok(Pi(x.clone(), t2, tB))
         }
         Pi(x, tA, tB) => {
-            let tA2 = normalized_type_with(ctx, tA.clone())?;
-            let kA = ensure_const(&tA2, InvalidInputType(tA.clone()))?;
+            let ttA = type_with(ctx, tA.clone())?;
+            let tA = normalize(SubExpr::clone(tA));
+            let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = normalized_type_with(&ctx2, tB.clone())?;
+            let tB = type_with(&ctx2, tB.clone())?;
             let kB = match tB.as_ref() {
                 Const(k) => *k,
                 _ => {
@@ -246,33 +257,6 @@ where
                 Ok(_) => Ok(Const(kB)),
             }
         }
-        App(f, args) => {
-            // Recurse on args
-            let (a, tf) = match args.split_last() {
-                None => return type_with(ctx, f.clone()),
-                Some((a, args)) => (
-                    a,
-                    normalized_type_with(
-                        ctx,
-                        rc(App(f.clone(), args.to_vec())),
-                    )?,
-                ),
-            };
-            let (x, tA, tB) = match tf.as_ref() {
-                Pi(x, tA, tB) => (x, tA, tB),
-                _ => {
-                    return Err(mkerr(NotAFunction(f.clone(), tf)));
-                }
-            };
-            let tA = normalize(SubExpr::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);
-                return Ok(subst_shift(vx0, &a, &tB));
-            } else {
-                Err(mkerr(TypeMismatch(f.clone(), tA, a.clone(), tA2)))
-            }
-        }
         Let(f, mt, r, b) => {
             let r = if let Some(t) = mt {
                 rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
@@ -281,14 +265,14 @@ where
             };
 
             let tR = type_with(ctx, r)?;
-            let ttR = normalized_type_with(ctx, tR.clone())?;
+            let ttR = 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 = normalized_type_with(ctx, tB.clone())?;
+            let ttB = 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()))?;
@@ -297,162 +281,174 @@ where
                 return Err(mkerr(NoDependentLet(tR, tB)));
             }
 
-            return Ok(tB);
-        }
-        Annot(x, t) => {
-            // This is mainly just to check that `t` is not `Kind`
-            let _ = type_with(ctx, t.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 {
-                Err(mkerr(AnnotMismatch(x.clone(), t, t2)))
-            }
+            Ok(tB.unroll())
         }
-        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)));
+        _ => match e
+            .as_ref()
+            .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))?
+        {
+            Lam(_, _, _) => unreachable!(),
+            Pi(_, _, _) => unreachable!(),
+            Let(_, _, _, _) => unreachable!(),
+            Const(c) => axiom(c).map(Const),
+            Var(V(x, n)) => match ctx.lookup(&x, n) {
+                Some(e) => Ok(e.unroll()),
+                None => Err(mkerr(UnboundVariable)),
+            },
+            App((f, mut tf), args) => {
+                let mut iter = args.into_iter();
+                let mut seen_args: Vec<SubExpr<_, _>> = vec![];
+                while let Some((a, ta)) = iter.next() {
+                    seen_args.push(a.clone());
+                    let (x, tx, tb) = match tf.as_ref() {
+                        Pi(x, tx, tb) => (x, tx, tb),
+                        _ => {
+                            return Err(mkerr(NotAFunction(
+                                rc(App(f.clone(), seen_args)),
+                                tf,
+                            )));
+                        }
+                    };
+                    ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || {
+                        TypeMismatch(
+                            rc(App(f.clone(), seen_args.clone())),
+                            tx.clone(),
+                            a.clone(),
+                            ta.clone(),
+                        )
+                    })?;
+                    tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb));
                 }
+                Ok(tf.unroll())
             }
-            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()),
-            )?;
+            Annot((x, tx), (t, _)) => {
+                let t = normalize(t.clone());
+                ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || {
+                    AnnotMismatch(x.clone(), t.clone(), tx.clone())
+                })?;
+                Ok(t.unroll())
+            }
+            BoolIf((x, tx), (y, ty), (z, tz)) => {
+                ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || {
+                    InvalidPredicate(x.clone(), tx.clone())
+                })?;
+                let tty = type_with(ctx, ty.clone())?;
+                ensure_is_type(
+                    tty.clone(),
+                    IfBranchMustBeTerm(
+                        true,
+                        y.clone(),
+                        ty.clone(),
+                        tty.clone(),
+                    ),
+                )?;
 
-            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()),
-            )?;
+                let ttz = type_with(ctx, tz.clone())?;
+                ensure_is_type(
+                    ttz.clone(),
+                    IfBranchMustBeTerm(
+                        false,
+                        z.clone(),
+                        tz.clone(),
+                        ttz.clone(),
+                    ),
+                )?;
 
-            if !prop_equal(ty.as_ref(), tz.as_ref()) {
-                return Err(mkerr(IfBranchMismatch(
-                    y.clone(),
-                    z.clone(),
-                    ty,
-                    tz,
-                )));
+                ensure_equal(ty.as_ref(), tz.as_ref(), mkerr, || {
+                    IfBranchMismatch(
+                        y.clone(),
+                        z.clone(),
+                        ty.clone(),
+                        tz.clone(),
+                    )
+                })?;
+                Ok(ty.unroll())
             }
-            return Ok(ty);
-        }
-        EmptyListLit(t) => {
-            let s = normalized_type_with(ctx, t.clone())?;
-            ensure_is_type(s, InvalidListType(t.clone()))?;
-            let t = normalize(SubExpr::clone(t));
-            return Ok(dhall_expr!(List t));
-        }
-        NEListLit(xs) => {
-            let mut iter = xs.iter().enumerate();
-            let (_, first_x) = iter.next().unwrap();
-            let t = type_with(ctx, first_x.clone())?;
-
-            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 = normalized_type_with(ctx, x.clone())?;
-                if !prop_equal(t.as_ref(), t2.as_ref()) {
-                    return Err(mkerr(InvalidListElement(i, t, x.clone(), t2)));
+            EmptyListLit((t, tt)) => {
+                ensure_is_type(tt, InvalidListType(t.clone()))?;
+                let t = normalize(SubExpr::clone(t));
+                Ok(dhall::expr!(List t))
+            }
+            NEListLit(xs) => {
+                let mut iter = xs.into_iter().enumerate();
+                let (_, (_, t)) = iter.next().unwrap();
+                let s = type_with(ctx, t.clone())?;
+                ensure_is_type(s, InvalidListType(t.clone()))?;
+                for (i, (y, ty)) in iter {
+                    ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || {
+                        InvalidListElement(i, t.clone(), y.clone(), ty.clone())
+                    })?;
                 }
+                Ok(dhall::expr!(List t))
             }
-            return Ok(dhall_expr!(List t));
-        }
-        EmptyOptionalLit(t) => {
-            let s = normalized_type_with(ctx, t.clone())?;
-            ensure_is_type(s, InvalidOptionalType(t.clone()))?;
-            let t = normalize(t.clone());
-            return Ok(dhall_expr!(Optional t));
-        }
-        NEOptionalLit(x) => {
-            let t: SubExpr<_, _> = type_with(ctx, x.clone())?;
-            let s = normalized_type_with(ctx, t.clone())?;
-            ensure_is_type(s, InvalidOptionalType(t.clone()))?;
-            let t = normalize(t);
-            return Ok(dhall_expr!(Optional t));
-        }
-        RecordType(kts) => {
-            for (k, t) in kts {
-                let s = normalized_type_with(ctx, t.clone())?;
-                ensure_is_type(s, InvalidFieldType(k.clone(), t.clone()))?;
+            EmptyOptionalLit((t, tt)) => {
+                ensure_is_type(tt, InvalidOptionalType(t.clone()))?;
+                let t = normalize(t.clone());
+                Ok(dhall::expr!(Optional t))
             }
-            Ok(Const(Type))
-        }
-        RecordLit(kvs) => {
-            let kts = kvs
-                .iter()
-                .map(|(k, v)| {
-                    let t = type_with(ctx, 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(RecordType(kts))
-        }
-        Field(r, x) => {
-            let t = normalized_type_with(ctx, r.clone())?;
-            match t.as_ref() {
-                RecordType(kts) => {
-                    return kts.get(x).cloned().ok_or_else(|| {
-                        mkerr(MissingField(x.clone(), t.clone()))
-                    })
+            NEOptionalLit((_, t)) => {
+                let s = type_with(ctx, t.clone())?;
+                ensure_is_type(s, InvalidOptionalType(t.clone()))?;
+                Ok(dhall::expr!(Optional t))
+            }
+            RecordType(kts) => {
+                for (k, (t, tt)) in kts {
+                    ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
                 }
-                _ => Err(mkerr(NotARecord(x.clone(), r.clone(), t.clone()))),
+                Ok(Const(Type))
             }
-        }
-        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))),
+            RecordLit(kvs) => {
+                let kts = kvs
+                    .into_iter()
+                    .map(|(k, (v, t))| {
+                        let s = type_with(ctx, t.clone())?;
+                        ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
+                        Ok((k.clone(), t))
+                    })
+                    .collect::<Result<_, _>>()?;
+                Ok(RecordType(kts))
             }
+            Field((r, tr), x) => match tr.as_ref() {
+                RecordType(kts) => match kts.get(&x) {
+                    Some(e) => Ok(e.unroll()),
+                    None => Err(mkerr(MissingField(x.clone(), tr.clone()))),
+                },
+                _ => Err(mkerr(NotARecord(x.clone(), r.clone(), tr.clone()))),
+            },
+            Builtin(b) => Ok(type_of_builtin(b)),
+            BoolLit(_) => Ok(Builtin(Bool)),
+            NaturalLit(_) => Ok(Builtin(Natural)),
+            IntegerLit(_) => Ok(Builtin(Integer)),
+            DoubleLit(_) => Ok(Builtin(Double)),
+            // TODO: check type of interpolations
+            TextLit(_) => Ok(Builtin(Text)),
+            BinOp(o, (l, tl), (r, tr)) => {
+                let t = Builtin(match o {
+                    BoolAnd => Bool,
+                    BoolOr => Bool,
+                    BoolEQ => Bool,
+                    BoolNE => Bool,
+                    NaturalPlus => Natural,
+                    NaturalTimes => Natural,
+                    TextAppend => Text,
+                    _ => panic!("Unimplemented typecheck case: {:?}", e),
+                });
 
-            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))),
-            }
+                ensure_equal(tl.as_ref(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, l.clone(), tl.clone())
+                })?;
 
-            Ok(Builtin(t))
-        }
-        Embed(p) => match *p {},
-        _ => panic!("Unimplemented typecheck case: {:?}", e),
-    }
-    .map(rc)
-}
+                ensure_equal(tr.as_ref(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, r.clone(), tr.clone())
+                })?;
 
-pub fn normalized_type_with<S>(
-    ctx: &Context<Label, SubExpr<S, X>>,
-    e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>>
-where
-    S: ::std::fmt::Debug + Clone,
-{
-    Ok(normalize(type_with(ctx, e)?))
+                Ok(t)
+            }
+            Embed(p) => match p {},
+            _ => panic!("Unimplemented typecheck case: {:?}", e),
+        },
+    }?;
+    Ok(rc(ret))
 }
 
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index 325b80f..397a8ee 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -40,6 +40,8 @@ pub enum Feature {
     Normalization,
     TypecheckSuccess,
     TypecheckFailure,
+    TypeInferenceSuccess,
+    TypeInferenceFailure,
 }
 
 pub fn read_dhall_file<'i>(file_path: &str) -> Result<Expr<X, X>, DhallError> {
@@ -60,6 +62,8 @@ pub fn run_test(base_path: &str, feature: Feature) {
         Normalization => "normalization/success/",
         TypecheckSuccess => "typecheck/success/",
         TypecheckFailure => "typecheck/failure/",
+        TypeInferenceSuccess => "type-inference/success/",
+        TypeInferenceFailure => "type-inference/failure/",
     };
     let base_path =
         "../dhall-lang/tests/".to_owned() + base_path_prefix + base_path;
@@ -113,5 +117,17 @@ pub fn run_test(base_path: &str, feature: Feature) {
             let expected = rc(read_dhall_file(&expected_file_path).unwrap());
             typecheck::type_of(rc(ExprF::Annot(expr, expected))).unwrap();
         }
+        TypeInferenceFailure => {
+            let file_path = base_path + ".dhall";
+            let expr = rc(read_dhall_file(&file_path).unwrap());
+            typecheck::type_of(expr).unwrap_err();
+        }
+        TypeInferenceSuccess => {
+            let expr_file_path = base_path.clone() + "A.dhall";
+            let expected_file_path = base_path + "B.dhall";
+            let expr = rc(read_dhall_file(&expr_file_path).unwrap());
+            let expected = rc(read_dhall_file(&expected_file_path).unwrap());
+            assert_eq_display!(typecheck::type_of(expr).unwrap(), expected);
+        }
     }
 }
diff --git a/dhall/tests/typecheck.rs b/dhall/tests/typecheck.rs
index 0cd6ddf..367765c 100644
--- a/dhall/tests/typecheck.rs
+++ b/dhall/tests/typecheck.rs
@@ -13,6 +13,17 @@ macro_rules! tc_failure {
     };
 }
 
+macro_rules! ti_success {
+    ($name:ident, $path:expr) => {
+        make_spec_test!(TypeInferenceSuccess, $name, $path);
+    };
+}
+// macro_rules! ti_failure {
+//     ($name:ident, $path:expr) => {
+//         make_spec_test!(TypeInferenceFailure, $name, $path);
+//     };
+// }
+
 // tc_success!(spec_typecheck_success_accessEncodedType, "accessEncodedType");
 // tc_success!(spec_typecheck_success_accessType, "accessType");
 tc_success!(spec_typecheck_success_prelude_Bool_and_0, "prelude/Bool/and/0");
@@ -145,8 +156,8 @@ tc_success!(spec_typecheck_success_prelude_Optional_unzip_0, "prelude/Optional/u
 tc_success!(spec_typecheck_success_prelude_Optional_unzip_1, "prelude/Optional/unzip/1");
 tc_success!(spec_typecheck_success_prelude_Text_concat_0, "prelude/Text/concat/0");
 tc_success!(spec_typecheck_success_prelude_Text_concat_1, "prelude/Text/concat/1");
-tc_success!(spec_typecheck_success_prelude_Text_concatMap_0, "prelude/Text/concatMap/0");
-tc_success!(spec_typecheck_success_prelude_Text_concatMap_1, "prelude/Text/concatMap/1");
+// tc_success!(spec_typecheck_success_prelude_Text_concatMap_0, "prelude/Text/concatMap/0");
+// tc_success!(spec_typecheck_success_prelude_Text_concatMap_1, "prelude/Text/concatMap/1");
 // tc_success!(spec_typecheck_success_prelude_Text_concatMapSep_0, "prelude/Text/concatMapSep/0");
 // tc_success!(spec_typecheck_success_prelude_Text_concatMapSep_1, "prelude/Text/concatMapSep/1");
 // tc_success!(spec_typecheck_success_prelude_Text_concatSep_0, "prelude/Text/concatSep/0");
@@ -166,3 +177,125 @@ tc_success!(spec_typecheck_success_prelude_Text_concatMap_1, "prelude/Text/conca
 // tc_failure!(spec_typecheck_failure_combineMixedRecords, "combineMixedRecords");
 // tc_failure!(spec_typecheck_failure_duplicateFields, "duplicateFields");
 tc_failure!(spec_typecheck_failure_hurkensParadox, "hurkensParadox");
+
+// ti_success!(spec_typeinference_success_simple_alternativesAreTypes, "simple/alternativesAreTypes");
+// ti_success!(spec_typeinference_success_simple_kindParameter, "simple/kindParameter");
+ti_success!(spec_typeinference_success_unit_Bool, "unit/Bool");
+ti_success!(spec_typeinference_success_unit_Double, "unit/Double");
+ti_success!(spec_typeinference_success_unit_DoubleLiteral, "unit/DoubleLiteral");
+// ti_success!(spec_typeinference_success_unit_DoubleShow, "unit/DoubleShow");
+ti_success!(spec_typeinference_success_unit_False, "unit/False");
+ti_success!(spec_typeinference_success_unit_Function, "unit/Function");
+ti_success!(spec_typeinference_success_unit_FunctionApplication, "unit/FunctionApplication");
+ti_success!(spec_typeinference_success_unit_FunctionNamedArg, "unit/FunctionNamedArg");
+// ti_success!(spec_typeinference_success_unit_FunctionTypeKindKind, "unit/FunctionTypeKindKind");
+// ti_success!(spec_typeinference_success_unit_FunctionTypeKindTerm, "unit/FunctionTypeKindTerm");
+// ti_success!(spec_typeinference_success_unit_FunctionTypeKindType, "unit/FunctionTypeKindType");
+ti_success!(spec_typeinference_success_unit_FunctionTypeTermTerm, "unit/FunctionTypeTermTerm");
+ti_success!(spec_typeinference_success_unit_FunctionTypeTypeTerm, "unit/FunctionTypeTypeTerm");
+ti_success!(spec_typeinference_success_unit_FunctionTypeTypeType, "unit/FunctionTypeTypeType");
+ti_success!(spec_typeinference_success_unit_FunctionTypeUsingArgument, "unit/FunctionTypeUsingArgument");
+ti_success!(spec_typeinference_success_unit_If, "unit/If");
+ti_success!(spec_typeinference_success_unit_IfNormalizeArguments, "unit/IfNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_Integer, "unit/Integer");
+ti_success!(spec_typeinference_success_unit_IntegerLiteral, "unit/IntegerLiteral");
+// ti_success!(spec_typeinference_success_unit_IntegerShow, "unit/IntegerShow");
+// ti_success!(spec_typeinference_success_unit_IntegerToDouble, "unit/IntegerToDouble");
+// ti_success!(spec_typeinference_success_unit_Kind, "unit/Kind");
+ti_success!(spec_typeinference_success_unit_Let, "unit/Let");
+// ti_success!(spec_typeinference_success_unit_LetNestedTypeSynonym, "unit/LetNestedTypeSynonym");
+// ti_success!(spec_typeinference_success_unit_LetTypeSynonym, "unit/LetTypeSynonym");
+ti_success!(spec_typeinference_success_unit_LetWithAnnotation, "unit/LetWithAnnotation");
+ti_success!(spec_typeinference_success_unit_List, "unit/List");
+ti_success!(spec_typeinference_success_unit_ListBuild, "unit/ListBuild");
+ti_success!(spec_typeinference_success_unit_ListFold, "unit/ListFold");
+ti_success!(spec_typeinference_success_unit_ListHead, "unit/ListHead");
+ti_success!(spec_typeinference_success_unit_ListIndexed, "unit/ListIndexed");
+ti_success!(spec_typeinference_success_unit_ListLast, "unit/ListLast");
+ti_success!(spec_typeinference_success_unit_ListLength, "unit/ListLength");
+ti_success!(spec_typeinference_success_unit_ListLiteralEmpty, "unit/ListLiteralEmpty");
+ti_success!(spec_typeinference_success_unit_ListLiteralNormalizeArguments, "unit/ListLiteralNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_ListLiteralOne, "unit/ListLiteralOne");
+ti_success!(spec_typeinference_success_unit_ListReverse, "unit/ListReverse");
+// ti_success!(spec_typeinference_success_unit_MergeEmptyUnion, "unit/MergeEmptyUnion");
+// ti_success!(spec_typeinference_success_unit_MergeOne, "unit/MergeOne");
+// ti_success!(spec_typeinference_success_unit_MergeOneWithAnnotation, "unit/MergeOneWithAnnotation");
+ti_success!(spec_typeinference_success_unit_Natural, "unit/Natural");
+ti_success!(spec_typeinference_success_unit_NaturalBuild, "unit/NaturalBuild");
+ti_success!(spec_typeinference_success_unit_NaturalEven, "unit/NaturalEven");
+ti_success!(spec_typeinference_success_unit_NaturalFold, "unit/NaturalFold");
+ti_success!(spec_typeinference_success_unit_NaturalIsZero, "unit/NaturalIsZero");
+ti_success!(spec_typeinference_success_unit_NaturalLiteral, "unit/NaturalLiteral");
+ti_success!(spec_typeinference_success_unit_NaturalOdd, "unit/NaturalOdd");
+// ti_success!(spec_typeinference_success_unit_NaturalShow, "unit/NaturalShow");
+// ti_success!(spec_typeinference_success_unit_NaturalToInteger, "unit/NaturalToInteger");
+// ti_success!(spec_typeinference_success_unit_None, "unit/None");
+ti_success!(spec_typeinference_success_unit_OldOptionalNone, "unit/OldOptionalNone");
+// ti_success!(spec_typeinference_success_unit_OldOptionalTrue, "unit/OldOptionalTrue");
+ti_success!(spec_typeinference_success_unit_OperatorAnd, "unit/OperatorAnd");
+ti_success!(spec_typeinference_success_unit_OperatorAndNormalizeArguments, "unit/OperatorAndNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_OperatorEqual, "unit/OperatorEqual");
+ti_success!(spec_typeinference_success_unit_OperatorEqualNormalizeArguments, "unit/OperatorEqualNormalizeArguments");
+// ti_success!(spec_typeinference_success_unit_OperatorListConcatenate, "unit/OperatorListConcatenate");
+// ti_success!(spec_typeinference_success_unit_OperatorListConcatenateNormalizeArguments, "unit/OperatorListConcatenateNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_OperatorNotEqual, "unit/OperatorNotEqual");
+ti_success!(spec_typeinference_success_unit_OperatorNotEqualNormalizeArguments, "unit/OperatorNotEqualNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_OperatorOr, "unit/OperatorOr");
+ti_success!(spec_typeinference_success_unit_OperatorOrNormalizeArguments, "unit/OperatorOrNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_OperatorPlus, "unit/OperatorPlus");
+ti_success!(spec_typeinference_success_unit_OperatorPlusNormalizeArguments, "unit/OperatorPlusNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_OperatorTextConcatenate, "unit/OperatorTextConcatenate");
+ti_success!(spec_typeinference_success_unit_OperatorTextConcatenateNormalizeArguments, "unit/OperatorTextConcatenateNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_OperatorTimes, "unit/OperatorTimes");
+ti_success!(spec_typeinference_success_unit_OperatorTimesNormalizeArguments, "unit/OperatorTimesNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_Optional, "unit/Optional");
+// ti_success!(spec_typeinference_success_unit_OptionalBuild, "unit/OptionalBuild");
+ti_success!(spec_typeinference_success_unit_OptionalFold, "unit/OptionalFold");
+ti_success!(spec_typeinference_success_unit_RecordEmpty, "unit/RecordEmpty");
+// ti_success!(spec_typeinference_success_unit_RecordOneKind, "unit/RecordOneKind");
+// ti_success!(spec_typeinference_success_unit_RecordOneType, "unit/RecordOneType");
+ti_success!(spec_typeinference_success_unit_RecordOneValue, "unit/RecordOneValue");
+// ti_success!(spec_typeinference_success_unit_RecordProjectionEmpty, "unit/RecordProjectionEmpty");
+// ti_success!(spec_typeinference_success_unit_RecordProjectionKind, "unit/RecordProjectionKind");
+// ti_success!(spec_typeinference_success_unit_RecordProjectionType, "unit/RecordProjectionType");
+// ti_success!(spec_typeinference_success_unit_RecordProjectionValue, "unit/RecordProjectionValue");
+// ti_success!(spec_typeinference_success_unit_RecordSelectionKind, "unit/RecordSelectionKind");
+// ti_success!(spec_typeinference_success_unit_RecordSelectionType, "unit/RecordSelectionType");
+ti_success!(spec_typeinference_success_unit_RecordSelectionValue, "unit/RecordSelectionValue");
+ti_success!(spec_typeinference_success_unit_RecordType, "unit/RecordType");
+ti_success!(spec_typeinference_success_unit_RecordTypeEmpty, "unit/RecordTypeEmpty");
+// ti_success!(spec_typeinference_success_unit_RecordTypeKind, "unit/RecordTypeKind");
+// ti_success!(spec_typeinference_success_unit_RecordTypeType, "unit/RecordTypeType");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordMergeLhsEmpty, "unit/RecursiveRecordMergeLhsEmpty");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordMergeRecursively, "unit/RecursiveRecordMergeRecursively");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordMergeRecursivelyTypes, "unit/RecursiveRecordMergeRecursivelyTypes");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordMergeRhsEmpty, "unit/RecursiveRecordMergeRhsEmpty");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordMergeTwo, "unit/RecursiveRecordMergeTwo");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordMergeTwoKinds, "unit/RecursiveRecordMergeTwoKinds");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordMergeTwoTypes, "unit/RecursiveRecordMergeTwoTypes");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordTypeMergeRecursively, "unit/RecursiveRecordTypeMergeRecursively");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordTypeMergeRecursivelyTypes, "unit/RecursiveRecordTypeMergeRecursivelyTypes");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordTypeMergeRhsEmpty, "unit/RecursiveRecordTypeMergeRhsEmpty");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordTypeMergeTwo, "unit/RecursiveRecordTypeMergeTwo");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordTypeMergeTwoKinds, "unit/RecursiveRecordTypeMergeTwoKinds");
+// ti_success!(spec_typeinference_success_unit_RecursiveRecordTypeMergeTwoTypes, "unit/RecursiveRecordTypeMergeTwoTypes");
+// ti_success!(spec_typeinference_success_unit_RightBiasedRecordMergeRhsEmpty, "unit/RightBiasedRecordMergeRhsEmpty");
+// ti_success!(spec_typeinference_success_unit_RightBiasedRecordMergeTwo, "unit/RightBiasedRecordMergeTwo");
+// ti_success!(spec_typeinference_success_unit_RightBiasedRecordMergeTwoDifferent, "unit/RightBiasedRecordMergeTwoDifferent");
+// ti_success!(spec_typeinference_success_unit_RightBiasedRecordMergeTwoKinds, "unit/RightBiasedRecordMergeTwoKinds");
+// ti_success!(spec_typeinference_success_unit_RightBiasedRecordMergeTwoTypes, "unit/RightBiasedRecordMergeTwoTypes");
+ti_success!(spec_typeinference_success_unit_SomeTrue, "unit/SomeTrue");
+ti_success!(spec_typeinference_success_unit_Text, "unit/Text");
+ti_success!(spec_typeinference_success_unit_TextLiteral, "unit/TextLiteral");
+ti_success!(spec_typeinference_success_unit_TextLiteralNormalizeArguments, "unit/TextLiteralNormalizeArguments");
+ti_success!(spec_typeinference_success_unit_TextLiteralWithInterpolation, "unit/TextLiteralWithInterpolation");
+// ti_success!(spec_typeinference_success_unit_TextShow, "unit/TextShow");
+ti_success!(spec_typeinference_success_unit_True, "unit/True");
+ti_success!(spec_typeinference_success_unit_Type, "unit/Type");
+ti_success!(spec_typeinference_success_unit_TypeAnnotation, "unit/TypeAnnotation");
+// ti_success!(spec_typeinference_success_unit_UnionConstructorField, "unit/UnionConstructorField");
+// ti_success!(spec_typeinference_success_unit_UnionOne, "unit/UnionOne");
+// ti_success!(spec_typeinference_success_unit_UnionTypeEmpty, "unit/UnionTypeEmpty");
+// ti_success!(spec_typeinference_success_unit_UnionTypeKind, "unit/UnionTypeKind");
+// ti_success!(spec_typeinference_success_unit_UnionTypeOne, "unit/UnionTypeOne");
+// ti_success!(spec_typeinference_success_unit_UnionTypeType, "unit/UnionTypeType");
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index a9033f3..a56c5a3 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -12,6 +12,13 @@ pub type Double = NaiveDouble;
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub enum X {}
 
+pub fn trivial_result<T>(x: Result<T, X>) -> T {
+    match x {
+        Ok(x) => x,
+        Err(e) => match e {},
+    }
+}
+
 /// Double with bitwise equality
 #[derive(Debug, Copy, Clone)]
 pub struct NaiveDouble(f64);
@@ -362,83 +369,122 @@ impl<SE, L, N, E> ExprF<SE, L, N, E> {
     }
 
     #[inline(always)]
-    pub fn map<SE2, L2, N2, E2, F1, F2, F3, F4, F5>(
+    pub fn traverse<SE2, L2, N2, E2, Err, F1, F2, F3, F4, F5>(
         self,
         map_subexpr: F1,
         map_under_binder: F2,
         map_note: F3,
         map_embed: F4,
         mut map_label: F5,
-    ) -> ExprF<SE2, L2, N2, E2>
+    ) -> Result<ExprF<SE2, L2, N2, E2>, Err>
     where
         L: Ord,
         L2: Ord,
-        F1: FnMut(SE) -> SE2,
-        F2: FnOnce(&L, SE) -> SE2,
-        F3: FnOnce(N) -> N2,
-        F4: FnOnce(E) -> E2,
-        F5: FnMut(L) -> L2,
+        F1: FnMut(SE) -> Result<SE2, Err>,
+        F2: FnOnce(&L, SE) -> Result<SE2, Err>,
+        F3: FnOnce(N) -> Result<N2, Err>,
+        F4: FnOnce(E) -> Result<E2, Err>,
+        F5: FnMut(L) -> Result<L2, Err>,
     {
         let mut map = map_subexpr;
-        fn vec<T, U, F: FnMut(T) -> U>(x: Vec<T>, f: F) -> Vec<U> {
+        fn vec<T, U, Err, F: FnMut(T) -> Result<U, Err>>(
+            x: Vec<T>,
+            f: F,
+        ) -> Result<Vec<U>, Err> {
             x.into_iter().map(f).collect()
         }
-        fn btmap<K, L, T, U, FK, FV>(
+        fn opt<T, U, Err, F: FnOnce(T) -> Result<U, Err>>(
+            x: Option<T>,
+            f: F,
+        ) -> Result<Option<U>, Err> {
+            Ok(match x {
+                Some(x) => Some(f(x)?),
+                None => None,
+            })
+        }
+        fn btmap<K, L, T, U, Err, FK, FV>(
             x: BTreeMap<K, T>,
             mut fk: FK,
             mut fv: FV,
-        ) -> BTreeMap<L, U>
+        ) -> Result<BTreeMap<L, U>, Err>
         where
             K: Ord,
             L: Ord,
-            FK: FnMut(K) -> L,
-            FV: FnMut(T) -> U,
+            FK: FnMut(K) -> Result<L, Err>,
+            FV: FnMut(T) -> Result<U, Err>,
         {
-            x.into_iter().map(|(k, v)| (fk(k), fv(v))).collect()
+            x.into_iter().map(|(k, v)| Ok((fk(k)?, fv(v)?))).collect()
         }
 
         use crate::ExprF::*;
-        match self {
-            Var(V(l, n)) => Var(V(map_label(l), n)),
+        Ok(match self {
+            Var(V(l, n)) => Var(V(map_label(l)?, n)),
             Lam(l, t, b) => {
-                let b = map_under_binder(&l, b);
-                Lam(map_label(l), map(t), b)
+                let b = map_under_binder(&l, b)?;
+                Lam(map_label(l)?, map(t)?, b)
             }
             Pi(l, t, b) => {
-                let b = map_under_binder(&l, b);
-                Pi(map_label(l), map(t), b)
+                let b = map_under_binder(&l, b)?;
+                Pi(map_label(l)?, map(t)?, b)
             }
             Let(l, t, a, b) => {
-                let b = map_under_binder(&l, b);
-                Let(map_label(l), t.map(&mut map), map(a), b)
+                let b = map_under_binder(&l, b)?;
+                Let(map_label(l)?, opt(t, &mut map)?, map(a)?, b)
             }
-            App(f, args) => App(map(f), vec(args, map)),
-            Annot(x, t) => Annot(map(x), map(t)),
+            App(f, args) => App(map(f)?, vec(args, map)?),
+            Annot(x, t) => Annot(map(x)?, map(t)?),
             Const(k) => Const(k),
             Builtin(v) => Builtin(v),
             BoolLit(b) => BoolLit(b),
             NaturalLit(n) => NaturalLit(n),
             IntegerLit(n) => IntegerLit(n),
             DoubleLit(n) => DoubleLit(n),
-            TextLit(t) => TextLit(t.map(map)),
-            BinOp(o, x, y) => BinOp(o, map(x), map(y)),
-            BoolIf(b, t, f) => BoolIf(map(b), map(t), map(f)),
-            EmptyListLit(t) => EmptyListLit(map(t)),
-            NEListLit(es) => NEListLit(vec(es, map)),
-            EmptyOptionalLit(t) => EmptyOptionalLit(map(t)),
-            NEOptionalLit(e) => NEOptionalLit(map(e)),
-            RecordType(kts) => RecordType(btmap(kts, map_label, map)),
-            RecordLit(kvs) => RecordLit(btmap(kvs, map_label, map)),
-            UnionType(kts) => UnionType(btmap(kts, map_label, map)),
+            TextLit(t) => TextLit(t.traverse(map)?),
+            BinOp(o, x, y) => BinOp(o, map(x)?, map(y)?),
+            BoolIf(b, t, f) => BoolIf(map(b)?, map(t)?, map(f)?),
+            EmptyListLit(t) => EmptyListLit(map(t)?),
+            NEListLit(es) => NEListLit(vec(es, map)?),
+            EmptyOptionalLit(t) => EmptyOptionalLit(map(t)?),
+            NEOptionalLit(e) => NEOptionalLit(map(e)?),
+            RecordType(kts) => RecordType(btmap(kts, map_label, map)?),
+            RecordLit(kvs) => RecordLit(btmap(kvs, map_label, map)?),
+            UnionType(kts) => UnionType(btmap(kts, map_label, map)?),
             UnionLit(k, v, kvs) => {
-                UnionLit(map_label(k), map(v), btmap(kvs, map_label, map))
+                UnionLit(map_label(k)?, map(v)?, btmap(kvs, map_label, map)?)
             }
-            Merge(x, y, t) => Merge(map(x), map(y), t.map(map)),
-            Field(e, l) => Field(map(e), map_label(l)),
-            Projection(e, ls) => Projection(map(e), vec(ls, map_label)),
-            Note(n, e) => Note(map_note(n), map(e)),
-            Embed(a) => Embed(map_embed(a)),
-        }
+            Merge(x, y, t) => Merge(map(x)?, map(y)?, opt(t, map)?),
+            Field(e, l) => Field(map(e)?, map_label(l)?),
+            Projection(e, ls) => Projection(map(e)?, vec(ls, map_label)?),
+            Note(n, e) => Note(map_note(n)?, map(e)?),
+            Embed(a) => Embed(map_embed(a)?),
+        })
+    }
+
+    #[inline(always)]
+    pub fn map<SE2, L2, N2, E2, F1, F2, F3, F4, F5>(
+        self,
+        mut map_subexpr: F1,
+        map_under_binder: F2,
+        map_note: F3,
+        map_embed: F4,
+        mut map_label: F5,
+    ) -> ExprF<SE2, L2, N2, E2>
+    where
+        L: Ord,
+        L2: Ord,
+        F1: FnMut(SE) -> SE2,
+        F2: FnOnce(&L, SE) -> SE2,
+        F3: FnOnce(N) -> N2,
+        F4: FnOnce(E) -> E2,
+        F5: FnMut(L) -> L2,
+    {
+        trivial_result(self.traverse(
+            |x| Ok(map_subexpr(x)),
+            |l, x| Ok(map_under_binder(l, x)),
+            |x| Ok(map_note(x)),
+            |x| Ok(map_embed(x)),
+            |x| Ok(map_label(x)),
+        ))
     }
 
     #[inline(always)]
@@ -490,6 +536,27 @@ impl<SE, L, N, E> ExprF<SE, L, N, E> {
         )
     }
 
+    #[inline(always)]
+    pub fn traverse_ref_simple<'a, SE2, Err, F1>(
+        &'a self,
+        map_subexpr: F1,
+    ) -> Result<ExprF<SE2, L, N, E>, Err>
+    where
+        L: Ord,
+        L: Clone,
+        N: Clone,
+        E: Clone,
+        F1: Fn(&'a SE) -> Result<SE2, Err>,
+    {
+        self.as_ref().traverse(
+            &map_subexpr,
+            |_, e| map_subexpr(e),
+            |x| Ok(N::clone(x)),
+            |x| Ok(E::clone(x)),
+            |x| Ok(L::clone(x)),
+        )
+    }
+
     // #[inline(always)]
     // pub fn zip<SE2, L2, N2, E2>(
     //     self,
diff --git a/dhall_core/src/text.rs b/dhall_core/src/text.rs
index 9500f32..7c0e2b4 100644
--- a/dhall_core/src/text.rs
+++ b/dhall_core/src/text.rs
@@ -34,18 +34,28 @@ pub enum InterpolatedTextContents<SubExpr> {
 }
 
 impl<SubExpr> InterpolatedText<SubExpr> {
-    pub fn map<SubExpr2, F>(self, mut f: F) -> InterpolatedText<SubExpr2>
+    pub fn traverse<SubExpr2, E, F>(
+        self,
+        mut f: F,
+    ) -> Result<InterpolatedText<SubExpr2>, E>
     where
-        F: FnMut(SubExpr) -> SubExpr2,
+        F: FnMut(SubExpr) -> Result<SubExpr2, E>,
     {
-        InterpolatedText {
+        Ok(InterpolatedText {
             head: self.head.clone(),
             tail: self
                 .tail
                 .into_iter()
-                .map(|(e, s)| (f(e), s.clone()))
-                .collect(),
-        }
+                .map(|(e, s)| Ok((f(e)?, s.clone())))
+                .collect::<Result<_, _>>()?,
+        })
+    }
+
+    pub fn map<SubExpr2, F>(self, mut f: F) -> InterpolatedText<SubExpr2>
+    where
+        F: FnMut(SubExpr) -> SubExpr2,
+    {
+        crate::trivial_result(self.traverse(|e| Ok(f(e))))
     }
 
     pub fn as_ref(&self) -> InterpolatedText<&SubExpr> {
diff --git a/dhall_generator/src/dhall_expr.rs b/dhall_generator/src/dhall_expr.rs
index 9da23b6..d0c5733 100644
--- a/dhall_generator/src/dhall_expr.rs
+++ b/dhall_generator/src/dhall_expr.rs
@@ -5,19 +5,29 @@ use proc_macro2::TokenStream;
 use quote::quote;
 use std::collections::BTreeMap;
 
-pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
+pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let input_str = input.to_string();
     let expr: SubExpr<X, Import> = parse_expr(&input_str).unwrap();
     let no_import =
-        |_: &Import| -> X { panic!("Don't use import in dhall!()") };
-    let expr = rc(expr.as_ref().map_embed(&no_import));
-    let output = quote_subexpr(&expr, &Context::new());
+        |_: &Import| -> X { panic!("Don't use import in dhall::expr!()") };
+    let expr = expr.as_ref().map_embed(&no_import);
+    let output = quote_expr(&expr, &Context::new());
+    output.into()
+}
+
+pub fn subexpr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
+    let input_str = input.to_string();
+    let expr: SubExpr<X, Import> = parse_expr(&input_str).unwrap();
+    let no_import =
+        |_: &Import| -> X { panic!("Don't use import in dhall::subexpr!()") };
+    let expr = expr.as_ref().map_embed(&no_import);
+    let output = quote_subexpr(&rc(expr), &Context::new());
     output.into()
 }
 
 // Returns an expression of type ExprF<T, _, _>, where T is the
 // type of the subexpressions after interpolation.
-pub fn quote_expr<TS>(expr: ExprF<TS, Label, X, X>) -> TokenStream
+pub fn quote_exprf<TS>(expr: ExprF<TS, Label, X, X>) -> TokenStream
 where
     TS: quote::ToTokens + std::fmt::Debug,
 {
@@ -134,7 +144,42 @@ fn quote_subexpr(
                 }
             }
         }
-        e => bx(quote_expr(e)),
+        e => bx(quote_exprf(e)),
+    }
+}
+
+// Returns an expression of type Expr<_, _>. Expects interpolated variables
+// to be of type SubExpr<_, _>.
+fn quote_expr(expr: &Expr<X, X>, ctx: &Context<Label, ()>) -> TokenStream {
+    use dhall_core::ExprF::*;
+    match expr.map_ref(
+        |e| quote_subexpr(e, ctx),
+        |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())),
+        |_| unreachable!(),
+        |_| unreachable!(),
+        |l| l.clone(),
+    ) {
+        Var(V(ref s, n)) => {
+            match ctx.lookup(s, n) {
+                // Non-free variable; interpolates as itself
+                Some(()) => {
+                    let s: String = s.into();
+                    let var = quote! { dhall_core::V(#s.into(), #n) };
+                    quote! { dhall_core::ExprF::Var(#var) }
+                }
+                // Free variable; interpolates as a rust variable
+                None => {
+                    let s: String = s.into();
+                    // TODO: insert appropriate shifts ?
+                    let v: TokenStream = s.parse().unwrap();
+                    quote! { {
+                        let x: dhall_core::SubExpr<_, _> = #v.clone();
+                        x.unroll()
+                    } }
+                }
+            }
+        }
+        e => quote_exprf(e),
     }
 }
 
diff --git a/dhall_generator/src/dhall_type.rs b/dhall_generator/src/dhall_type.rs
index ec023bc..3b1d1c9 100644
--- a/dhall_generator/src/dhall_type.rs
+++ b/dhall_generator/src/dhall_type.rs
@@ -48,7 +48,7 @@ pub fn derive_for_struct(
         })
         .collect();
     let record =
-        crate::dhall_expr::quote_expr(dhall_core::ExprF::RecordType(fields));
+        crate::dhall_expr::quote_exprf(dhall_core::ExprF::RecordType(fields));
     Ok(quote! { dhall_core::rc(#record) })
 }
 
@@ -93,7 +93,7 @@ pub fn derive_for_enum(
         .collect::<Result<_, Error>>()?;
 
     let union =
-        crate::dhall_expr::quote_expr(dhall_core::ExprF::UnionType(variants));
+        crate::dhall_expr::quote_exprf(dhall_core::ExprF::UnionType(variants));
     Ok(quote! { dhall_core::rc(#union) })
 }
 
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index d720b67..f31faa4 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -5,9 +5,20 @@ mod dhall_type;
 
 use proc_macro::TokenStream;
 
+// Deprecated
 #[proc_macro]
 pub fn dhall_expr(input: TokenStream) -> TokenStream {
-    dhall_expr::dhall_expr(input)
+    subexpr(input)
+}
+
+#[proc_macro]
+pub fn expr(input: TokenStream) -> TokenStream {
+    dhall_expr::expr(input)
+}
+
+#[proc_macro]
+pub fn subexpr(input: TokenStream) -> TokenStream {
+    dhall_expr::subexpr(input)
 }
 
 #[proc_macro_derive(Type)]