Use Rc consistently everywhere

7 files changed, 695 insertions, 583 deletions

diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 08bdba4..2279a51 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -1,7 +1,7 @@
 use dhall_core::*;
 use itertools::*;
-use std::rc::Rc;
 use serde_cbor::value::value as cbor;
+use std::rc::Rc;
 
 type ParsedExpr = Rc<Expr<X, Import>>;
 
@@ -22,7 +22,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
     use cbor::Value::*;
     use dhall_core::{BinOp, Builtin, Const};
     use Expr::*;
-    let e = match data {
+    Ok(rc(match data {
         String(s) => match Builtin::parse(s) {
             Some(b) => Expr::Builtin(b),
             None => match s.as_str() {
@@ -198,7 +198,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
                 let expr = cbor_value_to_dhall(expr)?;
                 return Ok(bindings
                     .into_iter()
-                    .fold(expr, |acc, (x, t, v)| bx(Let(x, t, v, acc))));
+                    .fold(expr, |acc, (x, t, v)| rc(Let(x, t, v, acc))));
             }
             [U64(26), x, y] => {
                 let x = cbor_value_to_dhall(&x)?;
@@ -208,8 +208,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
             _ => Err(DecodeError::WrongFormatError)?,
         },
         _ => Err(DecodeError::WrongFormatError)?,
-    };
-    Ok(bx(e))
+    }))
 }
 
 fn cbor_map_to_dhall_map(
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 3328d99..41953e3 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -1,5 +1,6 @@
 use std::error::Error;
 use std::io::{self, Read};
+use std::rc::Rc;
 use term_painter::ToStyle;
 
 use dhall::*;
@@ -65,9 +66,9 @@ fn main() {
         }
     };
 
-    let expr: Expr<_, _> = imports::panic_imports(&expr);
+    let expr: Rc<Expr<_, _>> = rc(imports::panic_imports(&expr));
 
-    let type_expr = match typecheck::type_of(&expr) {
+    let type_expr = match typecheck::type_of(expr.clone()) {
         Err(e) => {
             let explain = ::std::env::args().any(|s| s == "--explain");
             if !explain {
@@ -89,5 +90,5 @@ fn main() {
 
     println!("{}", type_expr);
     println!();
-    println!("{}", normalize::<_, X, _>(&expr));
+    println!("{}", normalize::<_, X, _>(expr));
 }
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 40112f1..fccc938 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use std::rc::Rc;
 /// Is identical to normalize on primitive types, but not on more complex
 /// types like functions and records.
 /// This allows normalization to be lazy.
-pub fn normalize_whnf<S, A>(e: &Expr<S, A>) -> Expr<S, A>
+pub fn normalize_whnf<S, A>(e: &SubExpr<S, A>) -> SubExpr<S, A>
 where
     S: Clone + fmt::Debug,
     A: Clone + fmt::Debug,
@@ -17,158 +17,204 @@ where
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
     use dhall_core::Expr::*;
-    match e {
+    rc(match e.as_ref() {
         Let(f, _, r, b) => {
             let vf0 = &V(f.clone(), 0);
             let r2 = shift::<_, S, _>(1, vf0, r);
             let b2 = subst::<_, S, _>(vf0, &r2, b);
             let b3 = shift::<_, S, _>(-1, vf0, &b2);
-            normalize_whnf(&b3)
+            return normalize_whnf(&b3);
         }
-        Annot(x, _) => normalize_whnf(x),
-        Note(_, e) => normalize_whnf(e),
-        App(f, args) => match (normalize_whnf(f), args.as_slice()) {
-            (f, []) => f,
-            (App(f, args1), args2) => normalize_whnf(&App(
-                f.clone(),
-                args1.iter().chain(args2.iter()).cloned().collect(),
-            )),
-            (Lam(ref x, _, ref b), [a, rest..]) => {
-                // Beta reduce
-                let vx0 = &V(x.clone(), 0);
-                let a2 = shift::<S, S, A>(1, vx0, a);
-                let b2 = subst::<S, S, A>(vx0, &a2, &b);
-                let b3 = shift::<S, S, A>(-1, vx0, &b2);
-                normalize_whnf(&App(bx(b3), rest.to_vec()))
-            }
-            // TODO: this is more normalization than needed
-            (Builtin(b), args) => match (
-                b,
-                args.iter()
-                    .map(|x| normalize_whnf(&*x))
-                    .collect::<Vec<Expr<_, _>>>()
-                    .as_slice(),
-            ) {
-                (OptionalSome, [a]) => OptionalLit(None, Some(bx(a.clone()))),
-                (OptionalNone, [a]) => OptionalLit(Some(bx(a.clone())), None),
-                (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0),
-                (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0),
-                (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0),
-                (NaturalToInteger, [NaturalLit(n)]) => IntegerLit(*n as isize),
-                (NaturalShow, [NaturalLit(n)]) => TextLit(n.to_string().into()),
-                (ListLength, [_, ListLit(_, ys)]) => NaturalLit(ys.len()),
-                (ListHead, [_, ListLit(t, ys)]) => {
-                    OptionalLit(t.clone(), ys.iter().cloned().next())
-                }
-                (ListLast, [_, ListLit(t, ys)]) => {
-                    OptionalLit(t.clone(), ys.iter().cloned().last())
-                }
-                (ListReverse, [_, ListLit(t, ys)]) => {
-                    let xs = ys.iter().rev().cloned().collect();
-                    ListLit(t.clone(), xs)
+        Annot(x, _) => return normalize_whnf(x),
+        Note(_, e) => return normalize_whnf(e),
+        App(f, args) => {
+            let f = normalize_whnf(f);
+            match (f.as_ref(), args.as_slice()) {
+                (_, []) => return f,
+                (App(f, args1), args2) => {
+                    return normalize_whnf(&rc(App(
+                        f.clone(),
+                        args1.iter().chain(args2.iter()).cloned().collect(),
+                    )))
                 }
-                (ListBuild, [a0, g]) => {
-                    // fold/build fusion
-                    let g = match g {
-                        App(f, args) => match (&**f, args.as_slice()) {
-                            (Builtin(ListFold), [_, x, rest..]) => {
-                                return normalize_whnf(&App(
-                                    x.clone(),
-                                    rest.to_vec(),
-                                ))
-                            }
-                            (_, args) => App(f.clone(), args.to_vec()),
-                        },
-                        g => g.clone(),
-                    };
-                    let g = bx(g);
-                    let a0 = bx(a0.clone());
-                    let a1 = bx(shift(1, &V("a".into(), 0), &a0));
-                    normalize_whnf(
-                        &dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)),
-                    )
+                (Lam(ref x, _, ref b), [a, rest..]) => {
+                    // Beta reduce
+                    let vx0 = &V(x.clone(), 0);
+                    let a2 = shift::<S, S, A>(1, vx0, a);
+                    let b2 = subst::<S, S, A>(vx0, &a2, &b);
+                    let b3 = shift::<S, S, A>(-1, vx0, &b2);
+                    return normalize_whnf(&rc(App(b3, rest.to_vec())));
                 }
-                (OptionalBuild, [a0, g]) => {
-                    // fold/build fusion
-                    let g = match g {
-                        App(f, args) => match (&**f, args.as_slice()) {
-                            (Builtin(OptionalFold), [_, x, rest..]) => {
-                                return normalize_whnf(&App(
-                                    x.clone(),
-                                    rest.to_vec(),
-                                ))
+                // TODO: this is more normalization than needed
+                (Builtin(b), args) => {
+                    let args = args
+                        .iter()
+                        .map(|x| normalize_whnf(x))
+                        .collect::<Vec<Rc<Expr<_, _>>>>();
+
+                    match (
+                        b,
+                        args.iter()
+                            .map(Rc::as_ref)
+                            .collect::<Vec<_>>()
+                            .as_slice(),
+                    ) {
+                        (OptionalSome, [_]) => {
+                            OptionalLit(None, Some(Rc::clone(&args[0])))
+                        }
+                        (OptionalNone, [_]) => {
+                            OptionalLit(Some(Rc::clone(&args[0])), None)
+                        }
+                        (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0),
+                        (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0),
+                        (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0),
+                        (NaturalToInteger, [NaturalLit(n)]) => {
+                            IntegerLit(*n as isize)
+                        }
+                        (NaturalShow, [NaturalLit(n)]) => {
+                            TextLit(n.to_string().into())
+                        }
+                        (ListLength, [_, ListLit(_, ys)]) => {
+                            NaturalLit(ys.len())
+                        }
+                        (ListHead, [_, ListLit(t, ys)]) => {
+                            OptionalLit(t.clone(), ys.iter().cloned().next())
+                        }
+                        (ListLast, [_, ListLit(t, ys)]) => {
+                            OptionalLit(t.clone(), ys.iter().cloned().last())
+                        }
+                        (ListReverse, [_, ListLit(t, ys)]) => {
+                            let xs = ys.iter().rev().cloned().collect();
+                            ListLit(t.clone(), xs)
+                        }
+                        (ListBuild, [_, _]) => {
+                            // fold/build fusion
+                            let g = Rc::clone(&args[1]);
+                            let g = match g.as_ref() {
+                                App(f, args) => {
+                                    match (f.as_ref(), args.as_slice()) {
+                                        (Builtin(ListFold), [_, x, rest..]) => {
+                                            return normalize_whnf(&rc(App(
+                                                x.clone(),
+                                                rest.to_vec(),
+                                            )))
+                                        }
+                                        (_, args) => {
+                                            rc(App(f.clone(), args.to_vec()))
+                                        }
+                                    }
+                                }
+                                _ => g,
+                            };
+                            let a0 = Rc::clone(&args[0]);
+                            let a1 = shift(1, &V("a".into(), 0), &a0);
+                            return normalize_whnf(
+                                &dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)),
+                            );
+                        }
+                        (OptionalBuild, [_, _]) => {
+                            // fold/build fusion
+                            let g = Rc::clone(&args[1]);
+                            let g = match g.as_ref() {
+                                App(f, args) => {
+                                    match (f.as_ref(), args.as_slice()) {
+                                        (
+                                            Builtin(OptionalFold),
+                                            [_, x, rest..],
+                                        ) => {
+                                            return normalize_whnf(&rc(App(
+                                                x.clone(),
+                                                rest.to_vec(),
+                                            )))
+                                        }
+                                        (_, args) => {
+                                            rc(App(f.clone(), args.to_vec()))
+                                        }
+                                    }
+                                }
+                                _ => g,
+                            };
+                            let a0 = Rc::clone(&args[0]);
+                            return normalize_whnf(
+                                &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)),
+                            );
+                        }
+                        (ListFold, [_, ListLit(_, xs), _, _, _]) => {
+                            let e2: Rc<Expr<_, _>> = xs.iter().rev().fold(
+                                Rc::clone(&args[4]),
+                                |acc, x| {
+                                    let x = x.clone();
+                                    let acc = acc.clone();
+                                    let cons = Rc::clone(&args[3]);
+                                    dhall_expr!(cons x acc)
+                                },
+                            );
+                            return normalize_whnf(&e2);
+                        }
+                        // // fold/build fusion
+                        // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
+                        //     normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+                        // }
+                        (
+                            OptionalFold,
+                            [_, OptionalLit(_, Some(x)), _, _, _],
+                        ) => {
+                            let x = x.clone();
+                            let just = Rc::clone(&args[3]);
+                            return normalize_whnf(&dhall_expr!(just x));
+                        }
+                        (
+                            OptionalFold,
+                            [_, OptionalLit(_, None), _, _, nothing],
+                        ) => (*nothing).clone(),
+                        // // fold/build fusion
+                        // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
+                        //     normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+                        // }
+                        (NaturalBuild, [App(f, args)]) => {
+                            match (f.as_ref(), args.as_slice()) {
+                                // fold/build fusion
+                                (Builtin(NaturalFold), [x, rest..]) => {
+                                    return normalize_whnf(&rc(App(
+                                        x.clone(),
+                                        rest.to_vec(),
+                                    )))
+                                }
+                                (_, args) => app(
+                                    Builtin(NaturalBuild),
+                                    vec![bx(App(f.clone(), args.to_vec()))],
+                                ),
                             }
-                            (_, args) => App(f.clone(), args.to_vec()),
-                        },
-                        g => g.clone(),
-                    };
-                    let g = bx(g);
-                    let a0 = bx(a0.clone());
-                    normalize_whnf(
-                        &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)),
-                    )
-                }
-                (ListFold, [_, ListLit(_, xs), _, cons, nil]) => {
-                    let e2: Expr<_, _> =
-                        xs.iter().rev().fold((*nil).clone(), |acc, x| {
-                            let x = (x).clone();
-                            let acc = bx((acc).clone());
-                            let cons = bx((cons).clone());
-                            dhall_expr!(cons x acc)
-                        });
-                    normalize_whnf(&e2)
-                }
-                // // fold/build fusion
-                // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
-                //     normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
-                // }
-                (OptionalFold, [_, OptionalLit(_, Some(x)), _, just, _]) => {
-                    let x = x.clone();
-                    let just = bx(just.clone());
-                    normalize_whnf(&dhall_expr!(just x))
-                }
-                (OptionalFold, [_, OptionalLit(_, None), _, _, nothing]) => {
-                    (*nothing).clone()
-                }
-                // // fold/build fusion
-                // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
-                //     normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
-                // }
-                (NaturalBuild, [App(f, args)]) => {
-                    match (&**f, args.as_slice()) {
-                        // fold/build fusion
-                        (Builtin(NaturalFold), [x, rest..]) => {
-                            normalize_whnf(&App(x.clone(), rest.to_vec()))
                         }
-                        (_, args) => app(
-                            Builtin(NaturalBuild),
-                            vec![bx(App(f.clone(), args.to_vec()))],
-                        ),
-                    }
-                }
-                (NaturalFold, [App(f, args)]) => {
-                    match (&**f, args.as_slice()) {
-                        // fold/build fusion
-                        (Builtin(NaturalBuild), [x, rest..]) => {
-                            normalize_whnf(&App(x.clone(), rest.to_vec()))
+                        (NaturalFold, [App(f, args)]) => {
+                            match (f.as_ref(), args.as_slice()) {
+                                // fold/build fusion
+                                (Builtin(NaturalBuild), [x, rest..]) => {
+                                    return normalize_whnf(&rc(App(
+                                        x.clone(),
+                                        rest.to_vec(),
+                                    )))
+                                }
+                                (_, args) => app(
+                                    Builtin(NaturalFold),
+                                    vec![bx(App(f.clone(), args.to_vec()))],
+                                ),
+                            }
                         }
-                        (_, args) => app(
-                            Builtin(NaturalFold),
-                            vec![bx(App(f.clone(), args.to_vec()))],
-                        ),
+                        (b, _) => App(rc(Builtin(*b)), args),
                     }
                 }
-                (b, args) => {
-                    App(bx(Builtin(b)), args.iter().cloned().map(bx).collect())
-                }
-            },
-            (f, args) => App(bx(f), args.to_vec()),
-        },
-        BoolIf(b, t, f) => match normalize_whnf(b) {
-            BoolLit(true) => normalize_whnf(t),
-            BoolLit(false) => normalize_whnf(f),
-            b2 => BoolIf(bx(b2), t.clone(), f.clone()),
-        },
+                (_, args) => App(f, args.to_vec()),
+            }
+        }
+        BoolIf(b, t, f) => {
+            let b = normalize_whnf(b);
+            match b.as_ref() {
+                BoolLit(true) => return normalize_whnf(t),
+                BoolLit(false) => return normalize_whnf(f),
+                _ => BoolIf(b, t.clone(), f.clone()),
+            }
+        }
         OptionalLit(t, es) => {
             if !es.is_none() {
                 OptionalLit(None, es.clone())
@@ -176,36 +222,52 @@ where
                 OptionalLit(t.clone(), es.clone())
             }
         }
-        BinOp(o, x, y) => match (o, normalize_whnf(&x), normalize_whnf(&y)) {
-            (BoolAnd, BoolLit(x), BoolLit(y)) => BoolLit(x && y),
-            (BoolOr, BoolLit(x), BoolLit(y)) => BoolLit(x || y),
-            (BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y),
-            (BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y),
-            (NaturalPlus, NaturalLit(x), NaturalLit(y)) => NaturalLit(x + y),
-            (NaturalTimes, NaturalLit(x), NaturalLit(y)) => NaturalLit(x * y),
-            (TextAppend, TextLit(x), TextLit(y)) => TextLit(x + y),
-            (ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => {
-                // Drop type annotation if the result is nonempty
-                let t = if xs.is_empty() && ys.is_empty() {
-                    t1.or(t2)
-                } else {
-                    None
-                };
-                let xs = xs.into_iter();
-                let ys = ys.into_iter();
-                ListLit(t, xs.chain(ys).collect())
+        BinOp(o, x, y) => {
+            let x = normalize_whnf(x);
+            let y = normalize_whnf(y);
+            match (o, x.as_ref(), y.as_ref()) {
+                (BoolAnd, BoolLit(x), BoolLit(y)) => BoolLit(*x && *y),
+                (BoolOr, BoolLit(x), BoolLit(y)) => BoolLit(*x || *y),
+                (BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y),
+                (BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y),
+                (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+                    NaturalLit(x + y)
+                }
+                (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+                    NaturalLit(x * y)
+                }
+                // TODO: interpolation
+                (TextAppend, TextLit(x), TextLit(y)) => {
+                    TextLit(x.clone() + y.clone())
+                }
+                (ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => {
+                    let t1: Option<Rc<_>> = t1.as_ref().map(Rc::clone);
+                    let t2: Option<Rc<_>> = t2.as_ref().map(Rc::clone);
+                    // Drop type annotation if the result is nonempty
+                    let t = if xs.is_empty() && ys.is_empty() {
+                        t1.or(t2)
+                    } else {
+                        None
+                    };
+                    let xs = xs.into_iter().cloned();
+                    let ys = ys.into_iter().cloned();
+                    ListLit(t, xs.chain(ys).collect())
+                }
+                (o, _, _) => BinOp(*o, x, y),
+            }
+        }
+        Field(e, x) => {
+            let e = normalize_whnf(e);
+            match (e.as_ref(), x) {
+                (RecordLit(kvs), x) => match kvs.get(&x) {
+                    Some(r) => return normalize_whnf(r),
+                    None => Field(e, x.clone()),
+                },
+                (_, x) => Field(e, x.clone()),
             }
-            (o, x, y) => BinOp(*o, bx(x), bx(y)),
-        },
-        Field(e, x) => match (normalize_whnf(&e), x) {
-            (RecordLit(kvs), x) => match kvs.get(&x) {
-                Some(r) => normalize_whnf(r),
-                None => Field(bx(RecordLit(kvs)), x.clone()),
-            },
-            (e, x) => Field(bx(e), x.clone()),
-        },
-        e => e.clone(),
-    }
+        }
+        _ => return Rc::clone(e),
+    })
 }
 
 /// Reduce an expression to its normal form, performing beta reduction
@@ -217,16 +279,16 @@ where
 /// However, `normalize` will not fail if the expression is ill-typed and will
 /// leave ill-typed sub-expressions unevaluated.
 ///
-pub fn normalize<S, T, A>(e: &Expr<S, A>) -> Expr<T, A>
+pub fn normalize<S, T, A>(e: SubExpr<S, A>) -> SubExpr<T, A>
 where
     S: Clone + fmt::Debug,
     T: Clone + fmt::Debug,
     A: Clone + fmt::Debug,
 {
-    normalize_whnf(e).map_shallow(
-        normalize,
+    rc(normalize_whnf(&e).map_shallow_rc(
+        |x| normalize(Rc::clone(x)),
         |_| unreachable!(),
         |x| x.clone(),
         |x| x.clone(),
-    )
+    ))
 }
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f5670f7..d6195a5 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -4,13 +4,13 @@ use std::collections::HashSet;
 use std::fmt;
 use std::rc::Rc;
 
-use crate::normalize;
+use crate::normalize::normalize;
 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, shift, subst, Expr, Label, V, X};
+use dhall_core::core::{bx, rc, shift, subst, Expr, Label, V, X};
 use dhall_generator::dhall_expr;
 
 use self::TypeMessage::*;
@@ -18,11 +18,11 @@ use self::TypeMessage::*;
 fn axiom<S: Clone>(c: core::Const) -> Result<core::Const, TypeError<S>> {
     match c {
         Type => Ok(Kind),
-        Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)),
+        Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)),
     }
 }
 
-fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
+fn rule(a: &core::Const, b: &core::Const) -> Result<core::Const, ()> {
     match (a, b) {
         (Type, Kind) => Err(()),
         (Kind, Kind) => Ok(Kind),
@@ -47,30 +47,30 @@ fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool {
     }
 }
 
-fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
+fn prop_equal<S, T>(eL0: Rc<Expr<S, X>>, eR0: Rc<Expr<T, X>>) -> bool
 where
     S: Clone + ::std::fmt::Debug,
     T: Clone + ::std::fmt::Debug,
 {
     fn go<S, T>(
         ctx: &mut Vec<(Label, Label)>,
-        el: &Expr<S, X>,
-        er: &Expr<T, X>,
+        el: Rc<Expr<S, X>>,
+        er: Rc<Expr<T, X>>,
     ) -> bool
     where
         S: Clone + ::std::fmt::Debug,
         T: Clone + ::std::fmt::Debug,
     {
-        match (el, er) {
+        match (el.as_ref(), er.as_ref()) {
             (&Const(Type), &Const(Type)) | (&Const(Kind), &Const(Kind)) => true,
-            (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx),
+            (&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, tL, tR);
+                let eq1 = go(ctx, Rc::clone(tL), Rc::clone(tR));
                 if eq1 {
                     //State.put ((xL, xR):ctx)
                     ctx.push((xL.clone(), xR.clone()));
-                    let eq2 = go(ctx, bL, bR);
+                    let eq2 = go(ctx, Rc::clone(bL), Rc::clone(bR));
                     //State.put ctx
                     let _ = ctx.pop();
                     eq2
@@ -79,8 +79,10 @@ where
                 }
             }
             (&App(ref fL, ref aL), &App(ref fR, ref aR)) => {
-                if go(ctx, fL, fR) {
-                    aL.iter().zip(aR.iter()).all(|(aL, aR)| go(ctx, aL, aR))
+                if go(ctx, Rc::clone(fL), Rc::clone(fR)) {
+                    aL.iter()
+                        .zip(aR.iter())
+                        .all(|(aL, aR)| go(ctx, Rc::clone(aL), Rc::clone(aR)))
                 } else {
                     false
                 }
@@ -112,10 +114,9 @@ where
                 }
                 true
                 */
-                !ktsL0
-                    .iter()
-                    .zip(ktsR0.iter())
-                    .any(|((kL, tL), (kR, tR))| kL != kR || !go(ctx, tL, tR))
+                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
+                    kL != kR || !go(ctx, Rc::clone(tL), Rc::clone(tR))
+                })
             }
             (&Union(ref ktsL0), &Union(ref ktsR0)) => {
                 if ktsL0.len() != ktsR0.len() {
@@ -132,40 +133,39 @@ where
                         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, tL, tR))
+                !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| {
+                    kL != kR || !go(ctx, Rc::clone(tL), Rc::clone(tR))
+                })
             }
             (_, _) => false,
         }
     }
     let mut ctx = vec![];
-    go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
+    go::<S, T>(&mut ctx, normalize(eL0), normalize(eR0))
 }
 
 fn op2_type<S, EF>(
-    ctx: &Context<Label, Expr<S, X>>,
-    e: &Expr<S, X>,
+    ctx: &Context<Label, Rc<Expr<S, X>>>,
+    e: Rc<Expr<S, X>>,
     t: core::Builtin,
     ef: EF,
-    l: &Expr<S, X>,
-    r: &Expr<S, X>,
+    l: &Rc<Expr<S, X>>,
+    r: &Rc<Expr<S, X>>,
 ) -> Result<Expr<S, X>, TypeError<S>>
 where
     S: Clone + ::std::fmt::Debug,
-    EF: FnOnce(Expr<S, X>, Expr<S, X>) -> TypeMessage<S>,
+    EF: FnOnce(Rc<Expr<S, X>>, Rc<Expr<S, X>>) -> TypeMessage<S>,
 {
-    let tl = normalize(&type_with(ctx, l)?);
-    match tl {
+    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))),
+        _ => return Err(TypeError::new(ctx, e, ef(l.clone(), tl))),
     }
 
-    let tr = normalize(&type_with(ctx, r)?);
-    match tr {
+    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))),
+        _ => return Err(TypeError::new(ctx, e, ef(r.clone(), tr))),
     }
 
     Ok(Builtin(t))
@@ -178,55 +178,54 @@ where
 /// is not necessary for just type-checking.  If you actually care about the
 /// returned type then you may want to `normalize` it afterwards.
 pub fn type_with<S>(
-    ctx: &Context<Label, Expr<S, X>>,
-    e: &Expr<S, X>,
-) -> Result<Expr<S, X>, TypeError<S>>
+    ctx: &Context<Label, Rc<Expr<S, X>>>,
+    e: Rc<Expr<S, X>>,
+) -> Result<Rc<Expr<S, X>>, TypeError<S>>
 where
     S: Clone + ::std::fmt::Debug,
 {
     use dhall_core::BinOp::*;
     use dhall_core::Expr;
     match *e {
-        Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
+        Const(c) => axiom(c).map(Const),
         Var(V(ref x, n)) => {
-            ctx.lookup(x, n)
+            return ctx
+                .lookup(x, n)
                 .cloned()
-                //.map(Cow::Borrowed)
-                .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable))
+                .ok_or_else(|| TypeError::new(ctx, e.clone(), UnboundVariable))
         }
         Lam(ref x, ref tA, ref b) => {
             let ctx2 = ctx
-                .insert(x.clone(), (**tA).clone())
-                .map(|e| core::shift(1, &V(x.clone(), 0), e));
-            let tB = type_with(&ctx2, b)?;
-            let p = Pi(x.clone(), tA.clone(), bx(tB));
-            let _ = type_with(ctx, &p)?;
-            //Ok(Cow::Owned(p))
-            Ok(p)
+                .insert(x.clone(), tA.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);
         }
         Pi(ref x, ref tA, ref tB) => {
-            let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
-            let kA = match tA2 {
+            let tA2 = normalize::<S, S, X>(type_with(ctx, tA.clone())?);
+            let kA = match tA2.as_ref() {
                 Const(k) => k,
                 _ => {
                     return Err(TypeError::new(
                         ctx,
-                        e,
-                        InvalidInputType((**tA).clone()),
+                        e.clone(),
+                        InvalidInputType(tA.clone()),
                     ));
                 }
             };
 
             let ctx2 = ctx
-                .insert(x.clone(), (**tA).clone())
-                .map(|e| core::shift(1, &V(x.clone(), 0), e));
-            let tB = normalize(&type_with(&ctx2, tB)?);
-            let kB = match tB {
+                .insert(x.clone(), tA.clone())
+                .map(|e| shift(1, &V(x.clone(), 0), e));
+            let tB = normalize(type_with(&ctx2, tB.clone())?);
+            let kB = match tB.as_ref() {
                 Const(k) => k,
                 _ => {
                     return Err(TypeError::new(
                         &ctx2,
-                        e,
+                        e.clone(),
                         InvalidOutputType(tB),
                     ));
                 }
@@ -235,184 +234,212 @@ where
             match rule(kA, kB) {
                 Err(()) => Err(TypeError::new(
                     ctx,
-                    e,
-                    NoDependentTypes((**tA).clone(), tB),
+                    e.clone(),
+                    NoDependentTypes(tA.clone(), tB),
                 )),
                 Ok(k) => Ok(Const(k)),
             }
         }
         App(ref f, ref args) => {
             let (a, args) = match args.split_last() {
-                None => return type_with(ctx, f),
+                None => return type_with(ctx, f.clone()),
                 Some(x) => x,
             };
             let tf =
-                normalize(&type_with(ctx, &App(f.clone(), args.to_vec()))?);
-            let (x, tA, tB) = match tf {
+                normalize(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(TypeError::new(
                         ctx,
-                        e,
-                        NotAFunction((**f).clone(), tf),
+                        e.clone(),
+                        NotAFunction(f.clone(), tf),
                     ));
                 }
             };
-            let tA2 = type_with(ctx, a)?;
-            if prop_equal(&tA, &tA2) {
-                let vx0 = &V(x, 0);
+            let tA2 = type_with(ctx, a.clone())?;
+            if prop_equal(tA.clone(), tA2.clone()) {
+                let vx0 = &V(x.clone(), 0);
                 let a2 = shift::<S, S, X>(1, vx0, a);
                 let tB2 = subst(vx0, &a2, &tB);
                 let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
-                Ok(tB3)
+                return Ok(tB3);
             } else {
-                let nf_A = normalize(&tA);
-                let nf_A2 = normalize(&tA2);
+                let nf_A = normalize(tA.clone());
+                let nf_A2 = normalize(tA2);
                 Err(TypeError::new(
                     ctx,
-                    e,
-                    TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2),
+                    e.clone(),
+                    TypeMismatch(f.clone(), nf_A, a.clone(), nf_A2),
                 ))
             }
         }
         Let(ref f, ref mt, ref r, ref b) => {
-            let tR = type_with(ctx, r)?;
-            let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
-            let kR = match ttR {
+            let tR = type_with(ctx, r.clone())?;
+            let ttR = normalize::<S, S, X>(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(TypeError::new(ctx, e, InvalidInputType(tR))),
+                _ => {
+                    return Err(TypeError::new(
+                        ctx,
+                        e.clone(),
+                        InvalidInputType(tR),
+                    ))
+                }
             };
 
             let ctx2 = ctx.insert(f.clone(), tR.clone());
-            let tB = type_with(&ctx2, b)?;
-            let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
-            let kB = match ttB {
+            let tB = type_with(&ctx2, b.clone())?;
+            let ttB = normalize::<S, S, X>(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(TypeError::new(ctx, e, InvalidOutputType(tB))),
+                _ => {
+                    return Err(TypeError::new(
+                        ctx,
+                        e.clone(),
+                        InvalidOutputType(tB),
+                    ))
+                }
             };
 
             if let Err(()) = rule(kR, kB) {
-                return Err(TypeError::new(ctx, e, NoDependentLet(tR, tB)));
+                return Err(TypeError::new(
+                    ctx,
+                    e.clone(),
+                    NoDependentLet(tR, tB),
+                ));
             }
 
             if let Some(ref t) = *mt {
-                let nf_t = normalize(t);
-                let nf_tR = normalize(&tR);
-                if !prop_equal(&nf_tR, &nf_t) {
+                let nf_t = normalize(t.clone());
+                let nf_tR = normalize(tR);
+                if !prop_equal(nf_tR.clone(), nf_t.clone()) {
                     return Err(TypeError::new(
                         ctx,
-                        e,
-                        AnnotMismatch((**r).clone(), nf_t, nf_tR),
+                        e.clone(),
+                        AnnotMismatch(r.clone(), nf_t, nf_tR),
                     ));
                 }
             }
 
-            Ok(tB)
+            return Ok(tB);
         }
         Annot(ref x, ref t) => {
             // This is mainly just to check that `t` is not `Kind`
-            let _ = type_with(ctx, t)?;
+            let _ = type_with(ctx, t.clone())?;
 
-            let t2 = type_with(ctx, x)?;
-            if prop_equal(t, &t2) {
-                Ok((**t).clone())
+            let t2 = type_with(ctx, x.clone())?;
+            if prop_equal(t.clone(), t2.clone()) {
+                return Ok(t.clone());
             } else {
-                let nf_t = normalize(t);
-                let nf_t2 = normalize(&t2);
+                let nf_t = normalize(t.clone());
+                let nf_t2 = normalize(t2);
                 Err(TypeError::new(
                     ctx,
-                    e,
-                    AnnotMismatch((**x).clone(), nf_t, nf_t2),
+                    e.clone(),
+                    AnnotMismatch(x.clone(), nf_t, nf_t2),
                 ))
             }
         }
         BoolLit(_) => Ok(Builtin(Bool)),
-        BinOp(BoolAnd, ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r),
-        BinOp(BoolOr, ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r),
-        BinOp(BoolEQ, ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r),
-        BinOp(BoolNE, ref l, ref r) => op2_type(ctx, e, Bool, CantNE, l, r),
+        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)?);
-            match tx {
+            let tx = normalize(type_with(ctx, x.clone())?);
+            match tx.as_ref() {
                 Builtin(Bool) => {}
                 _ => {
                     return Err(TypeError::new(
                         ctx,
-                        e,
-                        InvalidPredicate((**x).clone(), tx),
+                        e.clone(),
+                        InvalidPredicate(x.clone(), tx),
                     ));
                 }
             }
-            let ty = normalize(&type_with(ctx, y)?);
-            let tty = normalize(&type_with(ctx, &ty)?);
-            match tty {
+            let ty = normalize(type_with(ctx, y.clone())?);
+            let tty = normalize(type_with(ctx, ty.clone())?);
+            match tty.as_ref() {
                 Const(Type) => {}
                 _ => {
                     return Err(TypeError::new(
                         ctx,
-                        e,
-                        IfBranchMustBeTerm(true, (**y).clone(), ty, tty),
+                        e.clone(),
+                        IfBranchMustBeTerm(true, y.clone(), ty, tty),
                     ));
                 }
             }
 
-            let tz = normalize(&type_with(ctx, z)?);
-            let ttz = normalize(&type_with(ctx, &tz)?);
-            match ttz {
+            let tz = normalize(type_with(ctx, z.clone())?);
+            let ttz = normalize(type_with(ctx, tz.clone())?);
+            match ttz.as_ref() {
                 Const(Type) => {}
                 _ => {
                     return Err(TypeError::new(
                         ctx,
-                        e,
-                        IfBranchMustBeTerm(false, (**z).clone(), tz, ttz),
+                        e.clone(),
+                        IfBranchMustBeTerm(false, z.clone(), tz, ttz),
                     ));
                 }
             }
 
-            if !prop_equal(&ty, &tz) {
+            if !prop_equal(ty.clone(), tz.clone()) {
                 return Err(TypeError::new(
                     ctx,
-                    e,
-                    IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz),
+                    e.clone(),
+                    IfBranchMismatch(y.clone(), z.clone(), ty, tz),
                 ));
             }
-            Ok(ty)
+            return Ok(ty);
         }
         NaturalLit(_) => Ok(Builtin(Natural)),
-        Builtin(NaturalFold) => Ok(dhall_expr!(
-            Natural ->
-            forall (natural: Type) ->
-            forall (succ: natural -> natural) ->
-            forall (zero: natural) ->
-            natural
-        )),
-        Builtin(NaturalBuild) => Ok(dhall_expr!(
-            (forall (natural: Type) ->
+        Builtin(NaturalFold) => {
+            return Ok(dhall_expr!(
+                Natural ->
+                forall (natural: Type) ->
                 forall (succ: natural -> natural) ->
                 forall (zero: natural) ->
-                natural) ->
-            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) => {
-            Ok(dhall_expr!(
+            return Ok(dhall_expr!(
                 Natural -> Bool
             ))
         }
         BinOp(NaturalPlus, ref l, ref r) => {
-            op2_type(ctx, e, Natural, CantAdd, l, r)
+            op2_type(ctx, e.clone(), Natural, CantAdd, l, r)
         }
         BinOp(NaturalTimes, ref l, ref r) => {
-            op2_type(ctx, e, Natural, CantMultiply, l, 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, Text, CantTextAppend, l, r)
+            op2_type(ctx, e.clone(), Text, CantTextAppend, l, r)
         }
         ListLit(ref t, ref xs) => {
             let mut iter = xs.iter().enumerate();
@@ -420,117 +447,135 @@ where
                 Some(t) => t.clone(),
                 None => {
                     let (_, first_x) = iter.next().unwrap();
-                    bx(type_with(ctx, first_x)?)
+                    type_with(ctx, first_x.clone())?
                 }
             };
 
-            let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
-            match s {
+            let s = normalize::<_, S, _>(type_with(ctx, t.clone())?);
+            match s.as_ref() {
                 Const(Type) => {}
-                _ => return Err(TypeError::new(ctx, e, InvalidListType(t))),
+                _ => {
+                    return Err(TypeError::new(
+                        ctx,
+                        e.clone(),
+                        InvalidListType(t),
+                    ))
+                }
             }
             for (i, x) in iter {
-                let t2 = type_with(ctx, x)?;
-                if !prop_equal(&t, &t2) {
-                    let nf_t = normalize(&t);
-                    let nf_t2 = normalize(&t2);
+                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(TypeError::new(
                         ctx,
-                        e,
-                        InvalidListElement(i, nf_t, (**x).clone(), nf_t2),
+                        e.clone(),
+                        InvalidListElement(i, nf_t, x.clone(), nf_t2),
                     ));
                 }
             }
-            Ok(dhall_expr!(List t))
+            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(ListBuild) => Ok(dhall_expr!(
-            forall (a: Type) ->
-            (forall (list: Type) ->
+        Builtin(ListFold) => {
+            return Ok(dhall_expr!(
+                forall (a: Type) ->
+                List a ->
+                forall (list: Type) ->
                 forall (cons: a -> list -> list) ->
                 forall (nil: list) ->
-                list) ->
-            List a
-        )),
-        Builtin(ListFold) => Ok(dhall_expr!(
-            forall (a: Type) ->
-            List a ->
-            forall (list: Type) ->
-            forall (cons: a -> list -> list) ->
-            forall (nil: list) ->
-            list
-        )),
+                list
+            ))
+        }
         Builtin(ListLength) => {
-            Ok(dhall_expr!(forall (a: Type) -> List a -> Natural))
+            return Ok(dhall_expr!(forall (a: Type) -> List a -> Natural))
         }
         Builtin(ListHead) | Builtin(ListLast) => {
-            Ok(dhall_expr!(forall (a: Type) -> List a -> Optional a))
-        }
-        Builtin(ListIndexed) => Ok(dhall_expr!(
-            forall (a: Type) ->
-            List a ->
-            List { index: Natural, value: a }
-        )),
-        Builtin(ListReverse) => Ok(dhall_expr!(
-            forall (a: Type) -> List a -> List a
-        )),
+            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) => {
             let mut iter = xs.iter();
             let t: Rc<Expr<_, _>> = match t {
                 Some(t) => t.clone(),
                 None => {
                     let x = iter.next().unwrap();
-                    bx(type_with(ctx, x)?)
+                    type_with(ctx, x.clone())?
                 }
             };
 
-            let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
-            match s {
+            let s = normalize::<_, S, _>(type_with(ctx, t.clone())?);
+            match s.as_ref() {
                 Const(Type) => {}
                 _ => {
                     return Err(TypeError::new(
                         ctx,
-                        e,
+                        e.clone(),
                         InvalidOptionalType(t),
                     ));
                 }
             }
             for x in iter {
-                let t2 = type_with(ctx, x)?;
-                if !prop_equal(&t, &t2) {
-                    let nf_t = normalize(&t);
-                    let nf_t2 = normalize(&t2);
+                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(TypeError::new(
                         ctx,
-                        e,
-                        InvalidOptionalElement(nf_t, (**x).clone(), nf_t2),
+                        e.clone(),
+                        InvalidOptionalElement(nf_t, x.clone(), nf_t2),
                     ));
                 }
             }
-            Ok(dhall_expr!(Optional t))
-        }
-        Builtin(OptionalFold) => Ok(dhall_expr!(
-            forall (a: Type) ->
-            Optional a ->
-            forall (optional: Type) ->
-            forall (just: a -> optional) ->
-            forall (nothing: optional) ->
-            optional
-        )),
-        Builtin(List) | Builtin(Optional) => Ok(dhall_expr!(
-            Type -> Type
-        )),
+            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) => {
             for (k, t) in kts {
-                let s = normalize::<S, S, X>(&type_with(ctx, t)?);
-                match s {
+                let s = normalize::<S, S, X>(type_with(ctx, t.clone())?);
+                match s.as_ref() {
                     Const(Type) => {}
                     _ => {
                         return Err(TypeError::new(
                             ctx,
-                            e,
-                            InvalidFieldType((*k).clone(), (**t).clone()),
+                            e.clone(),
+                            InvalidFieldType(k.clone(), t.clone()),
                         ));
                     }
                 }
@@ -541,19 +586,19 @@ where
             let kts = kvs
                 .iter()
                 .map(|(k, v)| {
-                    let t = type_with(ctx, v)?;
-                    let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
-                    match s {
+                    let t = type_with(ctx, v.clone())?;
+                    let s = normalize::<S, S, X>(type_with(ctx, t.clone())?);
+                    match s.as_ref() {
                         Const(Type) => {}
                         _ => {
                             return Err(TypeError::new(
                                 ctx,
-                                e,
-                                InvalidField((*k).clone(), (**v).clone()),
+                                e.clone(),
+                                InvalidField(k.clone(), v.clone()),
                             ));
                         }
                     }
-                    Ok(((*k).clone(), bx(t)))
+                    Ok((k.clone(), t))
                 })
                 .collect::<Result<_, _>>()?;
             Ok(Record(kts))
@@ -640,21 +685,21 @@ where
             return t
             */
         Field(ref r, ref x) => {
-            let t = normalize(&type_with(ctx, r)?);
-            match t {
+            let t = normalize(type_with(ctx, r.clone())?);
+            match t.as_ref() {
                 Record(ref kts) => {
-                    kts.get(x).map(|x| &**x).cloned().ok_or_else(|| {
+                    return kts.get(x).cloned().ok_or_else(|| {
                         TypeError::new(
                             ctx,
-                            e,
-                            MissingField((*x).clone(), t.clone()),
+                            e.clone(),
+                            MissingField(x.clone(), t.clone()),
                         )
                     })
                 }
                 _ => Err(TypeError::new(
                     ctx,
-                    e,
-                    NotARecord((*x).clone(), (**r).clone(), t.clone()),
+                    e.clone(),
+                    NotARecord(x.clone(), r.clone(), t.clone()),
                 )),
             }
         }
@@ -667,14 +712,15 @@ where
         Embed(p) => match p {},
         _ => panic!("Unimplemented typecheck case: {:?}", e),
     }
+    .map(rc)
 }
 
 /// `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.
 pub fn type_of<S: Clone + ::std::fmt::Debug>(
-    e: &Expr<S, X>,
-) -> Result<Expr<S, X>, TypeError<S>> {
+    e: Rc<Expr<S, X>>,
+) -> Result<Rc<Expr<S, X>>, TypeError<S>> {
     let ctx = Context::new();
     type_with(&ctx, e) //.map(|e| e.into_owned())
 }
@@ -683,64 +729,74 @@ pub fn type_of<S: Clone + ::std::fmt::Debug>(
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(Expr<S, X>),
-    InvalidOutputType(Expr<S, X>),
-    NotAFunction(Expr<S, X>, Expr<S, X>),
-    TypeMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>),
-    AnnotMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>),
+    InvalidInputType(Rc<Expr<S, X>>),
+    InvalidOutputType(Rc<Expr<S, X>>),
+    NotAFunction(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    TypeMismatch(
+        Rc<Expr<S, X>>,
+        Rc<Expr<S, X>>,
+        Rc<Expr<S, X>>,
+        Rc<Expr<S, X>>,
+    ),
+    AnnotMismatch(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     Untyped,
-    InvalidListElement(usize, Expr<S, X>, Expr<S, X>, Expr<S, X>),
+    InvalidListElement(usize, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     InvalidListType(Rc<Expr<S, X>>),
-    InvalidOptionalElement(Expr<S, X>, Expr<S, X>, Expr<S, X>),
+    InvalidOptionalElement(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     InvalidOptionalLiteral(usize),
     InvalidOptionalType(Rc<Expr<S, X>>),
-    InvalidPredicate(Expr<S, X>, Expr<S, X>),
-    IfBranchMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>),
-    IfBranchMustBeTerm(bool, Expr<S, X>, Expr<S, X>, Expr<S, X>),
-    InvalidField(Label, Expr<S, X>),
-    InvalidFieldType(Label, Expr<S, X>),
-    InvalidAlternative(Label, Expr<S, X>),
-    InvalidAlternativeType(Label, Expr<S, X>),
+    InvalidPredicate(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    IfBranchMismatch(
+        Rc<Expr<S, X>>,
+        Rc<Expr<S, X>>,
+        Rc<Expr<S, X>>,
+        Rc<Expr<S, X>>,
+    ),
+    IfBranchMustBeTerm(bool, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    InvalidField(Label, Rc<Expr<S, X>>),
+    InvalidFieldType(Label, Rc<Expr<S, X>>),
+    InvalidAlternative(Label, Rc<Expr<S, X>>),
+    InvalidAlternativeType(Label, Rc<Expr<S, X>>),
     DuplicateAlternative(Label),
-    MustCombineARecord(Expr<S, X>, Expr<S, X>),
+    MustCombineARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     FieldCollision(Label),
-    MustMergeARecord(Expr<S, X>, Expr<S, X>),
-    MustMergeUnion(Expr<S, X>, Expr<S, X>),
+    MustMergeARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    MustMergeUnion(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
     UnusedHandler(HashSet<Label>),
     MissingHandler(HashSet<Label>),
-    HandlerInputTypeMismatch(Label, Expr<S, X>, Expr<S, X>),
-    HandlerOutputTypeMismatch(Label, Expr<S, X>, Expr<S, X>),
-    HandlerNotAFunction(Label, Expr<S, X>),
-    NotARecord(Label, Expr<S, X>, Expr<S, X>),
-    MissingField(Label, Expr<S, X>),
-    CantAnd(Expr<S, X>, Expr<S, X>),
-    CantOr(Expr<S, X>, Expr<S, X>),
-    CantEQ(Expr<S, X>, Expr<S, X>),
-    CantNE(Expr<S, X>, Expr<S, X>),
-    CantTextAppend(Expr<S, X>, Expr<S, X>),
-    CantAdd(Expr<S, X>, Expr<S, X>),
-    CantMultiply(Expr<S, X>, Expr<S, X>),
-    NoDependentLet(Expr<S, X>, Expr<S, X>),
-    NoDependentTypes(Expr<S, X>, Expr<S, X>),
+    HandlerInputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    HandlerOutputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    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>>),
+    NoDependentLet(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    NoDependentTypes(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
 }
 
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError<S> {
-    pub context: Context<Label, Expr<S, X>>,
-    pub current: Expr<S, X>,
+    pub context: Context<Label, Rc<Expr<S, X>>>,
+    pub current: Rc<Expr<S, X>>,
     pub type_message: TypeMessage<S>,
 }
 
 impl<S: Clone> TypeError<S> {
     pub fn new(
-        context: &Context<Label, Expr<S, X>>,
-        current: &Expr<S, X>,
+        context: &Context<Label, Rc<Expr<S, X>>>,
+        current: Rc<Expr<S, X>>,
         type_message: TypeMessage<S>,
     ) -> Self {
         TypeError {
             context: context.clone(),
-            current: current.clone(),
+            current: current,
             type_message,
         }
     }
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index b60262b..4d64fea 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -97,25 +97,25 @@ pub fn run_test(base_path: &str, feature: Feature) {
         Normalization => {
             let expr_file_path = base_path.clone() + "A.dhall";
             let expected_file_path = base_path + "B.dhall";
-            let expr = read_dhall_file(&expr_file_path).unwrap();
-            let expected = read_dhall_file(&expected_file_path).unwrap();
+            let expr = rc(read_dhall_file(&expr_file_path).unwrap());
+            let expected = rc(read_dhall_file(&expected_file_path).unwrap());
 
             assert_eq_display!(
-                normalize::<_, X, _>(&expr),
-                normalize::<_, X, _>(&expected)
+                normalize::<_, X, _>(expr),
+                normalize::<_, X, _>(expected)
             );
         }
         TypecheckFailure => {
             let file_path = base_path + ".dhall";
-            let expr = read_dhall_file(&file_path).unwrap();
-            typecheck::type_of(&expr).unwrap_err();
+            let expr = rc(read_dhall_file(&file_path).unwrap());
+            typecheck::type_of(expr).unwrap_err();
         }
         TypecheckSuccess => {
             let expr_file_path = base_path.clone() + "A.dhall";
             let expected_file_path = base_path + "B.dhall";
-            let expr = read_dhall_file(&expr_file_path).unwrap();
-            let expected = read_dhall_file(&expected_file_path).unwrap();
-            typecheck::type_of(&Expr::Annot(bx(expr), bx(expected))).unwrap();
+            let expr = rc(read_dhall_file(&expr_file_path).unwrap());
+            let expected = rc(read_dhall_file(&expected_file_path).unwrap());
+            typecheck::type_of(rc(Expr::Annot(expr, expected))).unwrap();
         }
     }
 }
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index f5da1df..eba6a42 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -290,6 +290,8 @@ impl<N: Clone, E: Clone> Add for InterpolatedText<N, E> {
     }
 }
 
+pub type SubExpr<Note, Embed> = Rc<Expr<Note, Embed>>;
+
 /// Syntax tree for expressions
 #[derive(Debug, Clone, PartialEq)]
 pub enum Expr<Note, Embed> {
@@ -299,33 +301,33 @@ pub enum Expr<Note, Embed> {
     ///  `Var (V x n)                              ~  x@n`
     Var(V),
     ///  `Lam x     A b                            ~  λ(x : A) -> b`
-    Lam(Label, Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+    Lam(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
     ///  `Pi "_" A B                               ~        A  -> B`
     ///  `Pi x   A B                               ~  ∀(x : A) -> B`
-    Pi(Label, Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+    Pi(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
     ///  `App f A                                  ~  f A`
-    App(Rc<Expr<Note, Embed>>, Vec<Rc<Expr<Note, Embed>>>),
+    App(SubExpr<Note, Embed>, Vec<SubExpr<Note, Embed>>),
     ///  `Let x Nothing  r e  ~  let x     = r in e`
     ///  `Let x (Just t) r e  ~  let x : t = r in e`
     Let(
         Label,
-        Option<Rc<Expr<Note, Embed>>>,
-        Rc<Expr<Note, Embed>>,
-        Rc<Expr<Note, Embed>>,
+        Option<SubExpr<Note, Embed>>,
+        SubExpr<Note, Embed>,
+        SubExpr<Note, Embed>,
     ),
     ///  `Annot x t                                ~  x : t`
-    Annot(Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+    Annot(SubExpr<Note, Embed>, SubExpr<Note, Embed>),
     /// Built-in values
     Builtin(Builtin),
     // Binary operations
-    BinOp(BinOp, Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+    BinOp(BinOp, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
     ///  `BoolLit b                                ~  b`
     BoolLit(bool),
     ///  `BoolIf x y z                             ~  if x then y else z`
     BoolIf(
-        Rc<Expr<Note, Embed>>,
-        Rc<Expr<Note, Embed>>,
-        Rc<Expr<Note, Embed>>,
+        SubExpr<Note, Embed>,
+        SubExpr<Note, Embed>,
+        SubExpr<Note, Embed>,
     ),
     ///  `NaturalLit n                             ~  +n`
     NaturalLit(Natural),
@@ -336,35 +338,32 @@ pub enum Expr<Note, Embed> {
     ///  `TextLit t                                ~  t`
     TextLit(InterpolatedText<Note, Embed>),
     ///  `ListLit t [x, y, z]                      ~  [x, y, z] : List t`
-    ListLit(Option<Rc<Expr<Note, Embed>>>, Vec<Rc<Expr<Note, Embed>>>),
+    ListLit(Option<SubExpr<Note, Embed>>, Vec<SubExpr<Note, Embed>>),
     ///  `OptionalLit t [e]                        ~  [e] : Optional t`
     ///  `OptionalLit t []                         ~  []  : Optional t`
-    OptionalLit(
-        Option<Rc<Expr<Note, Embed>>>,
-        Option<Rc<Expr<Note, Embed>>>,
-    ),
+    OptionalLit(Option<SubExpr<Note, Embed>>, Option<SubExpr<Note, Embed>>),
     ///  `Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }`
-    Record(BTreeMap<Label, Rc<Expr<Note, Embed>>>),
+    Record(BTreeMap<Label, SubExpr<Note, Embed>>),
     ///  `RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }`
-    RecordLit(BTreeMap<Label, Rc<Expr<Note, Embed>>>),
+    RecordLit(BTreeMap<Label, SubExpr<Note, Embed>>),
     ///  `Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1, k2 : t2 >`
-    Union(BTreeMap<Label, Rc<Expr<Note, Embed>>>),
+    Union(BTreeMap<Label, SubExpr<Note, Embed>>),
     ///  `UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1, k2 : t2, k3 : t3 >`
     UnionLit(
         Label,
-        Rc<Expr<Note, Embed>>,
-        BTreeMap<Label, Rc<Expr<Note, Embed>>>,
+        SubExpr<Note, Embed>,
+        BTreeMap<Label, SubExpr<Note, Embed>>,
     ),
     ///  `Merge x y t                              ~  merge x y : t`
     Merge(
-        Rc<Expr<Note, Embed>>,
-        Rc<Expr<Note, Embed>>,
-        Option<Rc<Expr<Note, Embed>>>,
+        SubExpr<Note, Embed>,
+        SubExpr<Note, Embed>,
+        Option<SubExpr<Note, Embed>>,
     ),
     ///  `Field e x                                ~  e.x`
-    Field(Rc<Expr<Note, Embed>>, Label),
+    Field(SubExpr<Note, Embed>, Label),
     /// Annotation on the AST. Unused for now but could hold e.g. file location information
-    Note(Note, Rc<Expr<Note, Embed>>),
+    Note(Note, SubExpr<Note, Embed>),
     /// Embeds an import or the result of resolving the import
     Embed(Embed),
 }
@@ -444,6 +443,31 @@ impl<S, A> Expr<S, A> {
         F3: FnOnce(&A) -> B,
         F4: Fn(&Label) -> Label,
     {
+        map_shallow(
+            self,
+            |x| rc(map_expr(x.as_ref())),
+            map_note,
+            map_embed,
+            map_label,
+        )
+    }
+
+    pub fn map_shallow_rc<T, B, F1, F2, F3, F4>(
+        &self,
+        map_expr: F1,
+        map_note: F2,
+        map_embed: F3,
+        map_label: F4,
+    ) -> Expr<T, B>
+    where
+        A: Clone,
+        T: Clone,
+        S: Clone,
+        F1: Fn(&SubExpr<S, A>) -> SubExpr<T, B>,
+        F2: FnOnce(&S) -> T,
+        F3: FnOnce(&A) -> B,
+        F4: Fn(&Label) -> Label,
+    {
         map_shallow(self, map_expr, map_note, map_embed, map_label)
     }
 
@@ -852,10 +876,7 @@ pub fn app<S, A, Ef>(f: Ef, x: Vec<Rc<Expr<S, A>>>) -> Expr<S, A>
 where
     Ef: Into<Expr<S, A>>,
 {
-    Expr::App(
-        bx(f.into()),
-        x,
-    )
+    Expr::App(bx(f.into()), x)
 }
 
 pub type Double = f64;
@@ -900,58 +921,55 @@ where
     A: Clone,
     S: Clone,
     T: Clone,
-    F1: Fn(&Expr<S, A>) -> Expr<T, B>,
+    F1: Fn(&SubExpr<S, A>) -> SubExpr<T, B>,
     F2: FnOnce(&S) -> T,
     F3: FnOnce(&A) -> B,
     F4: Fn(&Label) -> Label,
 {
     use crate::Expr::*;
-    let bxmap = |x: &Expr<S, A>| -> Rc<Expr<T, B>> { bx(map(x)) };
-    let bxbxmap = |x: &Rc<Expr<S, A>>| -> Rc<Expr<T, B>> { bx(map(&**x)) };
-    let opt = |x| map_opt_box(x, &map);
+    let map = &map;
+    let opt = |x: &Option<_>| x.as_ref().map(&map);
     match *e {
         Const(k) => Const(k),
         Var(V(ref x, n)) => Var(V(map_label(x), n)),
-        Lam(ref x, ref t, ref b) => Lam(map_label(x), bxmap(t), bxmap(b)),
-        Pi(ref x, ref t, ref b) => Pi(map_label(x), bxmap(t), bxmap(b)),
+        Lam(ref x, ref t, ref b) => Lam(map_label(x), map(t), map(b)),
+        Pi(ref x, ref t, ref b) => Pi(map_label(x), map(t), map(b)),
         App(ref f, ref args) => {
-            let args = args.iter().map(bxbxmap).collect();
-            App(bxmap(f), args)
+            let args = args.iter().map(map).collect();
+            App(map(f), args)
         }
         Let(ref l, ref t, ref a, ref b) => {
-            Let(map_label(l), opt(t), bxmap(a), bxmap(b))
+            Let(map_label(l), opt(t), map(a), map(b))
         }
-        Annot(ref x, ref t) => Annot(bxmap(x), bxmap(t)),
+        Annot(ref x, ref t) => Annot(map(x), map(t)),
         Builtin(v) => Builtin(v),
         BoolLit(b) => BoolLit(b),
-        BoolIf(ref b, ref t, ref f) => BoolIf(bxmap(b), bxmap(t), bxmap(f)),
+        BoolIf(ref b, ref t, ref f) => BoolIf(map(b), map(t), map(f)),
         NaturalLit(n) => NaturalLit(n),
         IntegerLit(n) => IntegerLit(n),
         DoubleLit(n) => DoubleLit(n),
-        TextLit(ref t) => TextLit(t.map(&bxbxmap)),
-        BinOp(o, ref x, ref y) => BinOp(o, bxmap(x), bxmap(y)),
+        TextLit(ref t) => TextLit(t.map(&map)),
+        BinOp(o, ref x, ref y) => BinOp(o, map(x), map(y)),
         ListLit(ref t, ref es) => {
-            let es = es.iter().map(&bxbxmap).collect();
+            let es = es.iter().map(&map).collect();
             ListLit(opt(t), es)
         }
         OptionalLit(ref t, ref es) => OptionalLit(opt(t), opt(es)),
         Record(ref kts) => {
-            Record(map_record_value_and_keys(kts, bxbxmap, map_label))
+            Record(map_record_value_and_keys(kts, map, map_label))
         }
         RecordLit(ref kvs) => {
-            RecordLit(map_record_value_and_keys(kvs, bxbxmap, map_label))
-        }
-        Union(ref kts) => {
-            Union(map_record_value_and_keys(kts, bxbxmap, map_label))
+            RecordLit(map_record_value_and_keys(kvs, map, map_label))
         }
+        Union(ref kts) => Union(map_record_value_and_keys(kts, map, map_label)),
         UnionLit(ref k, ref v, ref kvs) => UnionLit(
             map_label(k),
-            bxmap(v),
-            map_record_value_and_keys(kvs, bxbxmap, map_label),
+            map(v),
+            map_record_value_and_keys(kvs, map, map_label),
         ),
-        Merge(ref x, ref y, ref t) => Merge(bxmap(x), bxmap(y), opt(t)),
-        Field(ref r, ref x) => Field(bxmap(r), map_label(x)),
-        Note(ref n, ref e) => Note(map_note(n), bxmap(e)),
+        Merge(ref x, ref y, ref t) => Merge(map(x), map(y), opt(t)),
+        Field(ref r, ref x) => Field(map(r), map_label(x)),
+        Note(ref n, ref e) => Note(map_note(n), map(e)),
         Embed(ref a) => Embed(map_embed(a)),
     }
 }
@@ -982,13 +1000,6 @@ where
     it.into_iter().map(|(k, v)| (g(k), f(v))).collect()
 }
 
-pub fn map_opt_box<T, U, F>(x: &Option<Rc<T>>, f: F) -> Option<Rc<U>>
-where
-    F: FnOnce(&T) -> U,
-{
-    x.as_ref().map(|x| x.as_ref()).map(f).map(bx)
-}
-
 fn map_op2<T, U, V, F, G>(f: F, g: G, a: T, b: T) -> V
 where
     F: FnOnce(U, U) -> V,
@@ -1068,10 +1079,14 @@ where
 /// descend into a lambda or let expression that binds a variable of the same
 /// name in order to avoid shifting the bound variables by mistake.
 ///
-pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> {
+pub fn shift<S, T, A: Clone>(
+    d: isize,
+    v: &V,
+    e: &Rc<Expr<S, A>>,
+) -> Rc<Expr<T, A>> {
     use crate::Expr::*;
     let V(x, n) = v;
-    match e {
+    rc(match e.as_ref() {
         Const(a) => Const(*a),
         Var(V(x2, n2)) => {
             let n3 = if x == x2 && n <= n2 {
@@ -1085,80 +1100,68 @@ pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> {
             let n2 = if x == x2 { n + 1 } else { *n };
             let tA2 = shift(d, v, tA);
             let b2 = shift(d, &V(x.clone(), n2), b);
-            Lam(x2.clone(), bx(tA2), bx(b2))
+            Lam(x2.clone(), tA2, b2)
         }
         Pi(x2, tA, tB) => {
             let n2 = if x == x2 { n + 1 } else { *n };
             let tA2 = shift(d, v, tA);
             let tB2 = shift(d, &V(x.clone(), n2), tB);
-            Pi(x2.clone(), bx(tA2), bx(tB2))
+            Pi(x2.clone(), tA2, tB2)
         }
         App(f, args) => {
             let f = shift(d, v, f);
-            let args = args.iter().map(|a| bx(shift(d, v, a))).collect();
-            app(f, args)
+            let args = args.iter().map(|a| shift(d, v, a)).collect();
+            App(f, args)
         }
         Let(f, mt, r, e) => {
             let n2 = if x == f { n + 1 } else { *n };
             let e2 = shift(d, &V(x.clone(), n2), e);
-            let mt2 = mt.as_ref().map(|t| bx(shift(d, v, t)));
+            let mt2 = mt.as_ref().map(|t| shift(d, v, t));
             let r2 = shift(d, v, r);
-            Let(f.clone(), mt2, bx(r2), bx(e2))
+            Let(f.clone(), mt2, r2, e2)
         }
-        Annot(a, b) => shift_op2(Annot, d, v, a, b),
+        Annot(a, b) => map_op2(Annot, |x| shift(d, v, x), a, b),
         Builtin(v) => Builtin(*v),
         BoolLit(a) => BoolLit(*a),
-        BinOp(o, a, b) => shift_op2(|x, y| BinOp(*o, x, y), d, v, a, b),
+        BinOp(o, a, b) => {
+            map_op2(|x, y| BinOp(*o, x, y), |x| shift(d, v, x), a, b)
+        }
         BoolIf(a, b, c) => {
-            BoolIf(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
+            BoolIf(shift(d, v, a), shift(d, v, b), shift(d, v, c))
         }
         NaturalLit(a) => NaturalLit(*a),
         IntegerLit(a) => IntegerLit(*a),
         DoubleLit(a) => DoubleLit(*a),
-        TextLit(a) => TextLit(a.map(|e| bx(shift(d, v, &*e)))),
+        TextLit(a) => TextLit(a.map(|e| shift(d, v, &*e))),
         ListLit(t, es) => ListLit(
-            t.as_ref().map(|t| bx(shift(d, v, t))),
-            es.iter().map(|e| bx(shift(d, v, e))).collect(),
+            t.as_ref().map(|t| shift(d, v, t)),
+            es.iter().map(|e| shift(d, v, e)).collect(),
         ),
         OptionalLit(t, e) => OptionalLit(
-            t.as_ref().map(|t| bx(shift(d, v, t))),
-            e.as_ref().map(|t| bx(shift(d, v, t))),
+            t.as_ref().map(|t| shift(d, v, t)),
+            e.as_ref().map(|t| shift(d, v, t)),
         ),
-        Record(a) => Record(map_record_value(a, |val| bx(shift(d, v, &*val)))),
+        Record(a) => Record(map_record_value(a, |val| shift(d, v, &*val))),
         RecordLit(a) => {
-            RecordLit(map_record_value(a, |val| bx(shift(d, v, &*val))))
+            RecordLit(map_record_value(a, |val| shift(d, v, &*val)))
         }
-        Union(a) => Union(map_record_value(a, |val| bx(shift(d, v, &*val)))),
+        Union(a) => Union(map_record_value(a, |val| shift(d, v, &*val))),
         UnionLit(k, uv, a) => UnionLit(
             k.clone(),
-            bx(shift(d, v, uv)),
-            map_record_value(a, |val| bx(shift(d, v, &*val))),
+            shift(d, v, uv),
+            map_record_value(a, |val| shift(d, v, &*val)),
         ),
         Merge(a, b, c) => Merge(
-            bx(shift(d, v, a)),
-            bx(shift(d, v, b)),
-            c.as_ref().map(|c| bx(shift(d, v, c))),
+            shift(d, v, a),
+            shift(d, v, b),
+            c.as_ref().map(|c| shift(d, v, c)),
         ),
-        Field(a, b) => Field(bx(shift(d, v, a)), b.clone()),
-        Note(_, b) => shift(d, v, b),
+        Field(a, b) => Field(shift(d, v, a), b.clone()),
+        Note(_, b) => return shift(d, v, b),
         // The Dhall compiler enforces that all embedded values are closed expressions
         // and `shift` does nothing to a closed expression
         Embed(p) => Embed(p.clone()),
-    }
-}
-
-fn shift_op2<S, T, A, F>(
-    f: F,
-    d: isize,
-    v: &V,
-    a: &Expr<S, A>,
-    b: &Expr<S, A>,
-) -> Expr<T, A>
-where
-    F: FnOnce(Rc<Expr<T, A>>, Rc<Expr<T, A>>) -> Expr<T, A>,
-    A: Clone,
-{
-    map_op2(f, |x| bx(shift(d, v, x)), a, b)
+    })
 }
 
 /// Substitute all occurrences of a variable with an expression
@@ -1167,37 +1170,41 @@ where
 /// subst x C B  ~  B[x := C]
 /// ```
 ///
-pub fn subst<S, T, A>(v: &V, e: &Expr<S, A>, b: &Expr<T, A>) -> Expr<S, A>
+pub fn subst<S, T, A>(
+    v: &V,
+    e: &Rc<Expr<S, A>>,
+    b: &Rc<Expr<T, A>>,
+) -> Rc<Expr<S, A>>
 where
     S: Clone,
     A: Clone,
 {
     use crate::Expr::*;
     let V(x, n) = v;
-    match b {
+    rc(match b.as_ref() {
         Const(a) => Const(*a),
         Lam(y, tA, b) => {
             let n2 = if x == y { n + 1 } else { *n };
             let b2 =
                 subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), b);
             let tA2 = subst(v, e, tA);
-            Lam(y.clone(), bx(tA2), bx(b2))
+            Lam(y.clone(), tA2, b2)
         }
         Pi(y, tA, tB) => {
             let n2 = if x == y { n + 1 } else { *n };
             let tB2 =
                 subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), tB);
             let tA2 = subst(v, e, tA);
-            Pi(y.clone(), bx(tA2), bx(tB2))
+            Pi(y.clone(), tA2, tB2)
         }
         App(f, args) => {
             let f2 = subst(v, e, f);
-            let args = args.iter().map(|a| bx(subst(v, e, a))).collect();
-            app(f2, args)
+            let args = args.iter().map(|a| subst(v, e, a)).collect();
+            App(f2, args)
         }
         Var(v2) => {
             if v == v2 {
-                e.clone()
+                return e.clone();
             } else {
                 Var(v2.clone())
             }
@@ -1206,63 +1213,50 @@ where
             let n2 = if x == f { n + 1 } else { *n };
             let b2 =
                 subst(&V(x.clone(), n2), &shift(1, &V(f.clone(), 0), e), b);
-            let mt2 = mt.as_ref().map(|t| bx(subst(v, e, t)));
+            let mt2 = mt.as_ref().map(|t| subst(v, e, t));
             let r2 = subst(v, e, r);
-            Let(f.clone(), mt2, bx(r2), bx(b2))
+            Let(f.clone(), mt2, r2, b2)
         }
-        Annot(a, b) => subst_op2(Annot, v, e, a, b),
+        Annot(a, b) => map_op2(Annot, |x| subst(v, e, x), a, b),
         Builtin(v) => Builtin(*v),
         BoolLit(a) => BoolLit(*a),
-        BinOp(o, a, b) => subst_op2(|x, y| BinOp(*o, x, y), v, e, a, b),
+        BinOp(o, a, b) => {
+            map_op2(|x, y| BinOp(*o, x, y), |x| subst(v, e, x), a, b)
+        }
         BoolIf(a, b, c) => {
-            BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
+            BoolIf(subst(v, e, a), subst(v, e, b), subst(v, e, c))
         }
         NaturalLit(a) => NaturalLit(*a),
         IntegerLit(a) => IntegerLit(*a),
         DoubleLit(a) => DoubleLit(*a),
-        TextLit(a) => TextLit(a.map(|b| bx(subst(v, e, &*b)))),
+        TextLit(a) => TextLit(a.map(|b| subst(v, e, &*b))),
         ListLit(a, b) => {
-            let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
-            let b2 = b.iter().map(|be| bx(subst(v, e, be))).collect();
+            let a2 = a.as_ref().map(|a| subst(v, e, a));
+            let b2 = b.iter().map(|be| subst(v, e, be)).collect();
             ListLit(a2, b2)
         }
         OptionalLit(a, b) => {
-            let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
-            let b2 = b.as_ref().map(|a| bx(subst(v, e, a)));
+            let a2 = a.as_ref().map(|a| subst(v, e, a));
+            let b2 = b.as_ref().map(|a| subst(v, e, a));
             OptionalLit(a2, b2)
         }
-        Record(kts) => Record(map_record_value(kts, |t| bx(subst(v, e, &*t)))),
+        Record(kts) => Record(map_record_value(kts, |t| subst(v, e, &*t))),
         RecordLit(kvs) => {
-            RecordLit(map_record_value(kvs, |val| bx(subst(v, e, &*val))))
+            RecordLit(map_record_value(kvs, |val| subst(v, e, &*val)))
         }
-        Union(kts) => Union(map_record_value(kts, |t| bx(subst(v, e, &*t)))),
+        Union(kts) => Union(map_record_value(kts, |t| subst(v, e, &*t))),
         UnionLit(k, uv, kvs) => UnionLit(
             k.clone(),
-            bx(subst(v, e, uv)),
-            map_record_value(kvs, |val| bx(subst(v, e, &*val))),
+            subst(v, e, uv),
+            map_record_value(kvs, |val| subst(v, e, &*val)),
         ),
         Merge(a, b, c) => Merge(
-            bx(subst(v, e, a)),
-            bx(subst(v, e, b)),
-            c.as_ref().map(|c| bx(subst(v, e, c))),
+            subst(v, e, a),
+            subst(v, e, b),
+            c.as_ref().map(|c| subst(v, e, c)),
         ),
-        Field(a, b) => Field(bx(subst(v, e, a)), b.clone()),
-        Note(_, b) => subst(v, e, b),
+        Field(a, b) => Field(subst(v, e, a), b.clone()),
+        Note(_, b) => return subst(v, e, b),
         Embed(p) => Embed(p.clone()),
-    }
-}
-
-fn subst_op2<S, T, A, F>(
-    f: F,
-    v: &V,
-    e: &Expr<S, A>,
-    a: &Expr<T, A>,
-    b: &Expr<T, A>,
-) -> Expr<S, A>
-where
-    F: FnOnce(Rc<Expr<S, A>>, Rc<Expr<S, A>>) -> Expr<S, A>,
-    S: Clone,
-    A: Clone,
-{
-    map_op2(f, |x| bx(subst(v, e, x)), a, b)
+    })
 }
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index 26be4c4..9c0aacf 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -13,11 +13,11 @@ pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let no_import =
         |_: &Import| -> X { panic!("Don't use import in dhall!()") };
     let expr = expr.map_embed(&no_import);
-    let output = dhall_to_tokenstream(&expr, &Context::new());
+    let output = dhall_to_tokenstream_bx(&expr, &Context::new());
     output.into()
 }
 
-// Returns an expression of type Expr<_, _>. Expects input variables
+// Returns an expression of type Expr<_, _>. Expects interpolated variables
 // to be of type Rc<Expr<_, _>>.
 fn dhall_to_tokenstream(
     expr: &Expr<X, X>,