Use Rc consistently everywhere

4 files changed, 545 insertions, 427 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,
         }
     }