Slowly propagate the new type parameter throughout the codebase

8 files changed, 298 insertions, 178 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 4e183b4..6372768 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -43,7 +43,7 @@ impl fmt::Display for DhallError {
 pub fn load_dhall_file<'i, 'a: 'i>(
     f: &Path,
     source_pool: &'a mut Vec<String>,
-    resolve_imports: bool,
+    _resolve_imports: bool,
 ) -> Result<Expr<'i, X, X>, DhallError> {
     source_pool.push(String::new());
     let mut buffer = source_pool.last_mut().unwrap();
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 493f9be..dbe80a3 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -89,5 +89,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 246a3c0..d3766d5 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -12,7 +12,9 @@ use std::fmt;
 /// However, `normalize` will not fail if the expression is ill-typed and will
 /// leave ill-typed sub-expressions unevaluated.
 ///
-pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
+pub fn normalize<Label: StringLike, S, T, A>(
+    e: &Expr_<Label, S, A>,
+) -> Expr_<Label, T, A>
 where
     S: Clone + fmt::Debug,
     T: Clone + fmt::Debug,
@@ -24,9 +26,9 @@ where
     match e {
         // Matches that don't normalize everything right away
         Let(f, _, r, b) => {
-            let r2 = shift::<_, S, _>(1, V(f, 0), r);
-            let b2 = subst(V(f, 0), &r2, b);
-            let b3 = shift::<_, T, _>(-1, V(f, 0), &b2);
+            let r2 = shift::<Label, _, S, _>(1, V(f.clone(), 0), r);
+            let b2 = subst::<Label, _, S, _>(V(f.clone(), 0), &r2, b);
+            let b3 = shift::<Label, _, T, _>(-1, V(f.clone(), 0), &b2);
             normalize(&b3)
         }
         BoolIf(b, t, f) => match normalize(b) {
@@ -36,16 +38,16 @@ where
         },
         Annot(x, _) => normalize(x),
         Note(_, e) => normalize(e),
-        App(f, a) => match normalize::<S, T, A>(f) {
+        App(f, a) => match normalize::<Label, S, T, A>(f) {
             Lam(x, _A, b) => {
                 // Beta reduce
                 let vx0 = V(x, 0);
-                let a2 = shift::<S, S, A>(1, vx0, a);
-                let b2 = subst::<S, T, A>(vx0, &a2, &b);
-                let b3 = shift::<S, T, A>(-1, vx0, &b2);
+                let a2 = shift::<Label, S, S, A>(1, vx0, a);
+                let b2 = subst::<Label, S, T, A>(vx0, &a2, &b);
+                let b3 = shift::<Label, S, T, A>(-1, vx0, &b2);
                 normalize(&b3)
             }
-            f2 => match (f2, normalize::<S, T, A>(a)) {
+            f2 => match (f2, normalize::<Label, S, T, A>(a)) {
                 // fold/build fusion for `List`
                 (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) |
                 (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) |
@@ -87,13 +89,14 @@ where
                 (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
                 (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize),
                 (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
-                (App(box Builtin(ListBuild), a0), k) => {
-                    let k = bx(k);
-                    let a1 = bx(shift(1, V("a", 0), &a0));
-                    normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)))
-                }
+                // TODO: restore when handling variables generically fixed
+                // (App(box Builtin(ListBuild), a0), k) => {
+                //     let k = bx(k);
+                //     let a1 = bx(shift(1, V("a", 0), &a0));
+                //     normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)))
+                // }
                 (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
-                    let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| {
+                    let e2: Expr_<_, _, _> = xs.into_iter().rev().fold(nil, |y, ys| {
                         let y = bx(y);
                         let ys = bx(ys);
                         dhall!(cons y ys)
@@ -130,23 +133,29 @@ where
                               ]
             */
                 (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => {
-                    let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _| {
+                    let e2: Expr_<_, _, _> = xs.into_iter().fold(nothing, |y, _| {
                         let y = bx(y);
                         dhall!(just y)
                     });
                     normalize(&e2)
                 }
-                (App(box Builtin(OptionalBuild), a0), g) => {
-                    let g = bx(g);
-                    normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)))
-                }
+                // TODO: restore when handling variables generically fixed
+                // (App(box Builtin(OptionalBuild), a0), g) => {
+                //     let g = bx(g);
+                //     normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)))
+                // }
                 (f2, a2) => app(f2, a2),
             },
         },
 
         // Normalize everything else before matching
         e => {
-            match e.map_shallow(normalize, |_| unreachable!(), |x| x.clone()) {
+            match e.map_shallow(
+                normalize,
+                |_| unreachable!(),
+                |x| x.clone(),
+                |x| x.clone(),
+            ) {
                 BinOp(BoolAnd, box BoolLit(x), box BoolLit(y)) => {
                     BoolLit(x && y)
                 }
@@ -180,7 +189,7 @@ where
                     ListLit(t, xs.chain(ys).collect())
                 }
                 Merge(_x, _y, _t) => unimplemented!(),
-                Field(box RecordLit(kvs), x) => match kvs.get(x) {
+                Field(box RecordLit(kvs), x) => match kvs.get(&x) {
                     Some(r) => r.clone(),
                     None => Field(bx(RecordLit(kvs)), x),
                 },
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 23ab7a6..c2a2ca3 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -10,7 +10,7 @@ use dhall_core::core::Builtin::*;
 use dhall_core::core::Const::*;
 use dhall_core::core::Expr_::*;
 use dhall_core::core::{app, pi};
-use dhall_core::core::{bx, shift, subst, Expr, V, X};
+use dhall_core::core::{bx, shift, subst, Expr, Expr_, V, X};
 
 use self::TypeMessage::*;
 
@@ -155,7 +155,7 @@ fn op2_type<'i, S, EF>(
 ) -> Result<Expr<'i, S, X>, TypeError<'i, S>>
 where
     S: Clone + ::std::fmt::Debug + 'i,
-    EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>,
+    EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<&'i str, S>,
 {
     let tl = normalize(&type_with(ctx, l)?);
     match tl {
@@ -189,7 +189,7 @@ where
     use dhall_core::Expr_;
     match *e {
         Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
-        Var(V(x, n)) => {
+        Var(V(ref x, n)) => {
             ctx.lookup(x, n)
                 .cloned()
                 //.map(Cow::Borrowed)
@@ -206,7 +206,7 @@ where
             Ok(p)
         }
         Pi(x, ref tA, ref tB) => {
-            let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
+            let tA2 = normalize::<_, S, S, X>(&type_with(ctx, tA)?);
             let kA = match tA2 {
                 Const(k) => k,
                 _ => {
@@ -253,9 +253,9 @@ where
             let tA2 = type_with(ctx, a)?;
             if prop_equal(&tA, &tA2) {
                 let vx0 = V(x, 0);
-                let a2 = shift::<S, S, X>(1, vx0, a);
+                let a2 = shift::<&str, S, S, X>(1, vx0, a);
                 let tB2 = subst(vx0, &a2, &tB);
-                let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
+                let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2);
                 Ok(tB3)
             } else {
                 let nf_A = normalize(&tA);
@@ -269,7 +269,7 @@ where
         }
         Let(f, ref mt, ref r, ref b) => {
             let tR = type_with(ctx, r)?;
-            let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
+            let ttR = normalize::<_, S, S, X>(&type_with(ctx, &tR)?);
             let kR = match ttR {
                 Const(k) => k,
                 // Don't bother to provide a `let`-specific version of this error
@@ -279,7 +279,7 @@ where
 
             let ctx2 = ctx.insert(f, tR.clone());
             let tB = type_with(&ctx2, b)?;
-            let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
+            let ttB = normalize::<_, S, S, X>(&type_with(ctx, &tB)?);
             let kB = match ttB {
                 Const(k) => k,
                 // Don't bother to provide a `let`-specific version of this error
@@ -426,7 +426,7 @@ where
                 }
             };
 
-            let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
+            let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?);
             match s {
                 Const(Type) => {}
                 _ => return Err(TypeError::new(ctx, e, InvalidListType(*t))),
@@ -512,7 +512,7 @@ where
                 }
             };
 
-            let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
+            let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?);
             match s {
                 Const(Type) => {}
                 _ => {
@@ -561,7 +561,7 @@ where
         | 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)?);
+                let s = normalize::<_, S, S, X>(&type_with(ctx, t)?);
                 match s {
                     Const(Type) => {}
                     _ => {
@@ -580,7 +580,7 @@ where
                 .iter()
                 .map(|(&k, v)| {
                     let t = type_with(ctx, v)?;
-                    let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
+                    let s = normalize::<_, S, S, X>(&type_with(ctx, &t)?);
                     match s {
                         Const(Type) => {}
                         _ => {
@@ -717,57 +717,71 @@ pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(
 
 /// The specific type error
 #[derive(Debug)]
-pub enum TypeMessage<'i, S> {
+pub enum TypeMessage<Label, S> {
     UnboundVariable,
-    InvalidInputType(Expr<'i, S, X>),
-    InvalidOutputType(Expr<'i, S, X>),
-    NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidInputType(Expr_<Label, S, X>),
+    InvalidOutputType(Expr_<Label, S, X>),
+    NotAFunction(Expr_<Label, S, X>, Expr_<Label, S, X>),
     TypeMismatch(
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
     ),
-    AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    AnnotMismatch(Expr_<Label, S, X>, Expr_<Label, S, X>, Expr_<Label, S, X>),
     Untyped,
-    InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
-    InvalidListType(Expr<'i, S, X>),
-    InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidListElement(
+        usize,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+    ),
+    InvalidListType(Expr_<Label, S, X>),
+    InvalidOptionalElement(
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+    ),
     InvalidOptionalLiteral(usize),
-    InvalidOptionalType(Expr<'i, S, X>),
-    InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>),
+    InvalidOptionalType(Expr_<Label, S, X>),
+    InvalidPredicate(Expr_<Label, S, X>, Expr_<Label, S, X>),
     IfBranchMismatch(
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
-        Expr<'i, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+    ),
+    IfBranchMustBeTerm(
+        bool,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
+        Expr_<Label, S, X>,
     ),
-    IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
-    InvalidField(String, Expr<'i, S, X>),
-    InvalidFieldType(String, Expr<'i, S, X>),
-    InvalidAlternative(String, Expr<'i, S, X>),
-    InvalidAlternativeType(String, Expr<'i, S, X>),
+    InvalidField(String, Expr_<Label, S, X>),
+    InvalidFieldType(String, Expr_<Label, S, X>),
+    InvalidAlternative(String, Expr_<Label, S, X>),
+    InvalidAlternativeType(String, Expr_<Label, S, X>),
     DuplicateAlternative(String),
-    MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>),
+    MustCombineARecord(Expr_<Label, S, X>, Expr_<Label, S, X>),
     FieldCollision(String),
-    MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>),
-    MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>),
+    MustMergeARecord(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    MustMergeUnion(Expr_<Label, S, X>, Expr_<Label, S, X>),
     UnusedHandler(HashSet<String>),
     MissingHandler(HashSet<String>),
-    HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
-    HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
-    HandlerNotAFunction(String, Expr<'i, S, X>),
-    NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>),
-    MissingField(String, Expr<'i, S, X>),
-    CantAnd(Expr<'i, S, X>, Expr<'i, S, X>),
-    CantOr(Expr<'i, S, X>, Expr<'i, S, X>),
-    CantEQ(Expr<'i, S, X>, Expr<'i, S, X>),
-    CantNE(Expr<'i, S, X>, Expr<'i, S, X>),
-    CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>),
-    CantAdd(Expr<'i, S, X>, Expr<'i, S, X>),
-    CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>),
-    NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>),
-    NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>),
+    HandlerInputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+    HandlerOutputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+    HandlerNotAFunction(String, Expr_<Label, S, X>),
+    NotARecord(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+    MissingField(String, Expr_<Label, S, X>),
+    CantAnd(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantOr(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantEQ(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantNE(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantTextAppend(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantAdd(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    CantMultiply(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    NoDependentLet(Expr_<Label, S, X>, Expr_<Label, S, X>),
+    NoDependentTypes(Expr_<Label, S, X>, Expr_<Label, S, X>),
 }
 
 /// A structured type error that includes context
@@ -775,14 +789,14 @@ pub enum TypeMessage<'i, S> {
 pub struct TypeError<'i, S> {
     pub context: Context<&'i str, Expr<'i, S, X>>,
     pub current: Expr<'i, S, X>,
-    pub type_message: TypeMessage<'i, S>,
+    pub type_message: TypeMessage<&'i str, S>,
 }
 
 impl<'i, S: Clone> TypeError<'i, S> {
     pub fn new(
         context: &Context<&'i str, Expr<'i, S, X>>,
         current: &Expr<'i, S, X>,
-        type_message: TypeMessage<'i, S>,
+        type_message: TypeMessage<&'i str, S>,
     ) -> Self {
         TypeError {
             context: context.clone(),
@@ -792,7 +806,7 @@ impl<'i, S: Clone> TypeError<'i, S> {
     }
 }
 
-impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
+impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<&'i str, S> {
     fn description(&self) -> &str {
         match *self {
             UnboundVariable => "Unbound variable",
@@ -805,7 +819,7 @@ impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
     }
 }
 
-impl<'i, S> fmt::Display for TypeMessage<'i, S> {
+impl<'i, S> fmt::Display for TypeMessage<&'i str, S> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         match *self {
             UnboundVariable => {
diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs
index ef518ed..b27b850 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -61,8 +61,8 @@ macro_rules! make_spec_test {
 }
 
 use dhall::*;
-use dhall_core::*;
 use dhall_core::parser::*;
+use dhall_core::*;
 use std::fs::File;
 use std::io::Read;
 use std::path::PathBuf;
@@ -114,8 +114,8 @@ pub fn run_test(base_path: &str, feature: Feature, expected: ExpectedResult) {
             let expected = read_dhall_file(&expected_file_path, &mut expected_buffer).unwrap();
 
             assert_eq_!(
-                normalize::<_, X, _>(&expr),
-                normalize::<_, X, _>(&expected)
+                normalize::<_, _, X, _>(&expr),
+                normalize::<_, _, X, _>(&expected)
             );
         }
         _ => unimplemented!(),
diff --git a/dhall_core/src/context.rs b/dhall_core/src/context.rs
index 412d3f0..877843d 100644
--- a/dhall_core/src/context.rs
+++ b/dhall_core/src/context.rs
@@ -31,8 +31,8 @@ impl<K: Hash + Eq + Clone, T> Context<K, T> {
     /// lookup k n (insert k v c) = lookup k (n - 1) c  -- 1 <= n
     /// lookup k n (insert j v c) = lookup k  n      c  -- k /= j
     /// ```
-    pub fn lookup<'a>(&'a self, k: K, n: usize) -> Option<&'a T> {
-        self.0.get(&k).and_then(|v| v.get(v.len() - 1 - n))
+    pub fn lookup<'a>(&'a self, k: &K, n: usize) -> Option<&'a T> {
+        self.0.get(k).and_then(|v| v.get(v.len() - 1 - n))
     }
 
     pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<K, U> {
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index cbf0654..d832a18 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -1,6 +1,7 @@
 #![allow(non_snake_case)]
 use std::collections::BTreeMap;
 use std::fmt::{self, Display};
+use std::hash::Hash;
 use std::path::PathBuf;
 
 /// Constants for a pure type system
@@ -144,12 +145,23 @@ pub enum Expr_<Label, Note, Embed> {
     ///  `Var (V x n)                              ~  x@n`
     Var(V<Label>),
     ///  `Lam x     A b                            ~  λ(x : A) -> b`
-    Lam(Label, Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>),
+    Lam(
+        Label,
+        Box<Expr_<Label, Note, Embed>>,
+        Box<Expr_<Label, Note, Embed>>,
+    ),
     ///  `Pi "_" A B                               ~        A  -> B`
     ///  `Pi x   A B                               ~  ∀(x : A) -> B`
-    Pi(Label, Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>),
+    Pi(
+        Label,
+        Box<Expr_<Label, Note, Embed>>,
+        Box<Expr_<Label, Note, Embed>>,
+    ),
     ///  `App f A                                  ~  f A`
-    App(Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>),
+    App(
+        Box<Expr_<Label, Note, Embed>>,
+        Box<Expr_<Label, 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(
@@ -159,11 +171,18 @@ pub enum Expr_<Label, Note, Embed> {
         Box<Expr_<Label, Note, Embed>>,
     ),
     ///  `Annot x t                                ~  x : t`
-    Annot(Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>),
+    Annot(
+        Box<Expr_<Label, Note, Embed>>,
+        Box<Expr_<Label, Note, Embed>>,
+    ),
     /// Built-in values
     Builtin(Builtin),
     // Binary operations
-    BinOp(BinOp, Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>),
+    BinOp(
+        BinOp,
+        Box<Expr_<Label, Note, Embed>>,
+        Box<Expr_<Label, Note, Embed>>,
+    ),
     ///  `BoolLit b                                ~  b`
     BoolLit(bool),
     ///  `BoolIf x y z                             ~  if x then y else z`
@@ -181,10 +200,16 @@ pub enum Expr_<Label, Note, Embed> {
     ///  `TextLit t                                ~  t`
     TextLit(Builder),
     ///  `ListLit t [x, y, z]                      ~  [x, y, z] : List t`
-    ListLit(Option<Box<Expr_<Label, Note, Embed>>>, Vec<Expr_<Label, Note, Embed>>),
+    ListLit(
+        Option<Box<Expr_<Label, Note, Embed>>>,
+        Vec<Expr_<Label, Note, Embed>>,
+    ),
     ///  `OptionalLit t [e]                        ~  [e] : Optional t`
     ///  `OptionalLit t []                         ~  []  : Optional t`
-    OptionalLit(Option<Box<Expr_<Label, Note, Embed>>>, Vec<Expr_<Label, Note, Embed>>),
+    OptionalLit(
+        Option<Box<Expr_<Label, Note, Embed>>>,
+        Vec<Expr_<Label, Note, Embed>>,
+    ),
     ///  `Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }`
     Record(BTreeMap<Label, Expr_<Label, Note, Embed>>),
     ///  `RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }`
@@ -243,8 +268,26 @@ pub enum Builtin {
     TextShow,
 }
 
-impl<'i> From<&'i str> for V<&'i str> {
-    fn from(s: &'i str) -> Self {
+pub trait StringLike:
+    Display + fmt::Debug + Clone + Copy + Hash + Ord + Eq + Into<String> + Default
+{
+}
+
+impl<T> StringLike for T where
+    T: Display
+        + fmt::Debug
+        + Clone
+        + Copy
+        + Hash
+        + Ord
+        + Eq
+        + Into<String>
+        + Default
+{
+}
+
+impl<Label> From<Label> for V<Label> {
+    fn from(s: Label) -> Self {
         V(s, 0)
     }
 }
@@ -255,39 +298,43 @@ impl<'i, S, A> From<&'i str> for Expr<'i, S, A> {
     }
 }
 
-impl<'i, S, A> From<Builtin> for Expr<'i, S, A> {
+impl<L, S, A> From<Builtin> for Expr_<L, S, A> {
     fn from(t: Builtin) -> Self {
         Expr_::Builtin(t)
     }
 }
 
-impl<'i, S, A> Expr<'i, S, A> {
-    pub fn map_shallow<T, B, F1, F2, F3>(
+impl<Label: StringLike, S, A> Expr_<Label, S, A> {
+    pub fn map_shallow<T, B, Label2, F1, F2, F3, F4>(
         &self,
         map_expr: F1,
         map_note: F2,
         map_embed: F3,
-    ) -> Expr<'i, T, B>
+        map_label: F4,
+    ) -> Expr_<Label2, T, B>
     where
         A: Clone,
         T: Clone,
         S: Clone,
-        F1: Fn(&Self) -> Expr<'i, T, B>,
+        Label2: StringLike,
+        F1: Fn(&Self) -> Expr_<Label2, T, B>,
         F2: FnOnce(&S) -> T,
         F3: FnOnce(&A) -> B,
+        F4: Fn(&Label) -> Label2,
     {
-        map_shallow(self, map_expr, map_note, map_embed)
+        map_shallow(self, map_expr, map_note, map_embed, map_label)
     }
 
-    pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr<'i, S, B>
+    pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr_<Label, S, B>
     where
         A: Clone,
         S: Clone,
         F: Fn(&A) -> B,
     {
-        let recurse =
-            |e: &Expr<'i, S, A>| -> Expr<'i, S, B> { e.map_embed(map_embed) };
-        map_shallow(self, recurse, |x| x.clone(), map_embed)
+        let recurse = |e: &Expr_<Label, S, A>| -> Expr_<Label, S, B> {
+            e.map_embed(map_embed)
+        };
+        self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone())
     }
 
     pub fn bool_lit(&self) -> Option<bool> {
@@ -312,6 +359,14 @@ impl<'i, S, A> Expr<'i, S, A> {
     }
 }
 
+// impl<'i, S: Clone, A: Clone> Expr_<&'i str, S, A> {
+//     pub fn to_owned(&self) -> Expr_<String, S, A> {
+//         let recurse =
+//             |e: &Expr_<&'i str, S, A>| -> Expr_<String, S, A> { e.to_owned() };
+//         self.map_shallow(recurse, |x| x.clone(), |x| x.clone(), |x| x.to_owned())
+//     }
+// }
+
 //  There is a one-to-one correspondence between the formatters in this section
 //  and the grammar in grammar.lalrpop.  Each formatter is named after the
 //  corresponding grammar rule and the relationship between formatters exactly matches
@@ -322,7 +377,7 @@ impl<'i, S, A> Expr<'i, S, A> {
 //  you add a new constructor to the syntax tree without adding a matching
 //  case the corresponding builder.
 
-impl<'i, S, A: Display> Display for Expr<'i, S, A> {
+impl<Label: Display, S, A: Display> Display for Expr_<Label, S, A> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         // buildExprA
         use crate::Expr_::*;
@@ -338,11 +393,11 @@ impl<'i, S, A: Display> Display for Expr<'i, S, A> {
     }
 }
 
-impl<'i, S, A: Display> Expr<'i, S, A> {
+impl<Label: Display, S, A: Display> Expr_<Label, S, A> {
     fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::Expr_::*;
         match self {
-            &Lam(a, ref b, ref c) => {
+            &Lam(ref a, ref b, ref c) => {
                 write!(f, "λ({} : ", a)?;
                 b.fmt(f)?;
                 write!(f, ") → ")?;
@@ -356,24 +411,25 @@ impl<'i, S, A: Display> Expr<'i, S, A> {
                 write!(f, " else ")?;
                 c.fmt_c(f)
             }
-            &Pi("_", ref b, ref c) => {
-                b.fmt_c(f)?;
-                write!(f, " → ")?;
-                c.fmt_b(f)
-            }
-            &Pi(a, ref b, ref c) => {
+            // TODO: wait for decision on label types
+            // &Pi("_", ref b, ref c) => {
+            //     b.fmt_c(f)?;
+            //     write!(f, " → ")?;
+            //     c.fmt_b(f)
+            // }
+            &Pi(ref a, ref b, ref c) => {
                 write!(f, "∀({} : ", a)?;
                 b.fmt(f)?;
                 write!(f, ") → ")?;
                 c.fmt_b(f)
             }
-            &Let(a, None, ref c, ref d) => {
+            &Let(ref a, None, ref c, ref d) => {
                 write!(f, "let {} = ", a)?;
                 c.fmt(f)?;
                 write!(f, ") → ")?;
                 d.fmt_b(f)
             }
-            &Let(a, Some(ref b), ref c, ref d) => {
+            &Let(ref a, Some(ref b), ref c, ref d) => {
                 write!(f, "let {} : ", a)?;
                 b.fmt(f)?;
                 write!(f, " = ")?;
@@ -488,7 +544,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> {
     fn fmt_e(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::Expr_::*;
         match self {
-            &Field(ref a, b) => {
+            &Field(ref a, ref b) => {
                 a.fmt_e(f)?;
                 write!(f, ".{}", b)
             }
@@ -499,7 +555,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> {
 
     fn fmt_f(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::Expr_::*;
-        match self {
+        match &self {
             &Var(a) => a.fmt(f),
             &Const(k) => k.fmt(f),
             &Builtin(v) => v.fmt(f),
@@ -521,7 +577,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> {
                 write!(f, "{} = {}", k, v)
             }),
             &Union(ref _a) => f.write_str("Union"),
-            &UnionLit(_a, ref _b, ref _c) => f.write_str("UnionLit"),
+            &UnionLit(ref _a, ref _b, ref _c) => f.write_str("UnionLit"),
             &Embed(ref a) => a.fmt(f),
             &Note(_, ref b) => b.fmt_f(f),
             a => write!(f, "({})", a),
@@ -633,34 +689,34 @@ impl Builtin {
     }
 }
 
-impl<'i> Display for V<&'i str> {
+impl<Label: Display> Display for V<Label> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        let V(x, n) = *self;
-        f.write_str(x)?;
-        if n != 0 {
+        let V(ref x, ref n) = *self;
+        x.fmt(f)?;
+        if *n != 0 {
             write!(f, "@{}", n)?;
         }
         Ok(())
     }
 }
 
-pub fn pi<'i, S, A, Name, Et, Ev>(
+pub fn pi<Label, S, A, Name, Et, Ev>(
     var: Name,
     ty: Et,
     value: Ev,
-) -> Expr<'i, S, A>
+) -> Expr_<Label, S, A>
 where
-    Name: Into<&'i str>,
-    Et: Into<Expr<'i, S, A>>,
-    Ev: Into<Expr<'i, S, A>>,
+    Name: Into<Label>,
+    Et: Into<Expr_<Label, S, A>>,
+    Ev: Into<Expr_<Label, S, A>>,
 {
     Expr_::Pi(var.into(), bx(ty.into()), bx(value.into()))
 }
 
-pub fn app<'i, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<'i, S, A>
+pub fn app<Label, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr_<Label, S, A>
 where
-    Ef: Into<Expr<'i, S, A>>,
-    Ex: Into<Expr<'i, S, A>>,
+    Ef: Into<Expr_<Label, S, A>>,
+    Ex: Into<Expr_<Label, S, A>>,
 {
     Expr_::App(bx(f.into()), bx(x.into()))
 }
@@ -693,30 +749,37 @@ fn add_ui(u: usize, i: isize) -> usize {
     }
 }
 
-pub fn map_shallow<'i, S, T, A, B, F1, F2, F3>(
-    e: &Expr<'i, S, A>,
+pub fn map_shallow<Label1, Label2, S, T, A, B, F1, F2, F3, F4>(
+    e: &Expr_<Label1, S, A>,
     map: F1,
     map_note: F2,
     map_embed: F3,
-) -> Expr<'i, T, B>
+    map_label: F4,
+) -> Expr_<Label2, T, B>
 where
     A: Clone,
     S: Clone,
     T: Clone,
-    F1: Fn(&Expr<'i, S, A>) -> Expr<'i, T, B>,
+    Label1: StringLike,
+    Label2: StringLike,
+    F1: Fn(&Expr_<Label1, S, A>) -> Expr_<Label2, T, B>,
     F2: FnOnce(&S) -> T,
     F3: FnOnce(&A) -> B,
+    F4: Fn(&Label1) -> Label2,
 {
     use crate::Expr_::*;
-    let bxmap = |x: &Expr<'i, S, A>| -> Box<Expr<'i, T, B>> { bx(map(x)) };
+    let bxmap =
+        |x: &Expr_<Label1, S, A>| -> Box<Expr_<Label2, T, B>> { bx(map(x)) };
     let opt = |x| map_opt_box(x, &map);
     match *e {
         Const(k) => Const(k),
-        Var(v) => Var(v),
-        Lam(x, ref t, ref b) => Lam(x, bxmap(t), bxmap(b)),
-        Pi(x, ref t, ref b) => Pi(x, bxmap(t), bxmap(b)),
+        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)),
         App(ref f, ref a) => App(bxmap(f), bxmap(a)),
-        Let(l, ref t, ref a, ref b) => Let(l, opt(t), bxmap(a), bxmap(b)),
+        Let(ref l, ref t, ref a, ref b) => {
+            Let(map_label(l), opt(t), bxmap(a), bxmap(b))
+        }
         Annot(ref x, ref t) => Annot(bxmap(x), bxmap(t)),
         Builtin(v) => Builtin(v),
         BoolLit(b) => BoolLit(b),
@@ -734,27 +797,49 @@ where
             let es = es.iter().map(&map).collect();
             OptionalLit(opt(t), es)
         }
-        Record(ref kts) => Record(map_record_value(kts, map)),
-        RecordLit(ref kvs) => RecordLit(map_record_value(kvs, map)),
-        Union(ref kts) => Union(map_record_value(kts, map)),
-        UnionLit(k, ref v, ref kvs) => {
-            UnionLit(k, bxmap(v), map_record_value(kvs, map))
+        Record(ref kts) => {
+            Record(map_record_value_and_keys(kts, map, map_label))
+        }
+        RecordLit(ref kvs) => {
+            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, map, map_label),
+        ),
         Merge(ref x, ref y, ref t) => Merge(bxmap(x), bxmap(y), opt(t)),
-        Field(ref r, x) => Field(bxmap(r), x),
+        Field(ref r, ref x) => Field(bxmap(r), map_label(x)),
         Note(ref n, ref e) => Note(map_note(n), bxmap(e)),
         Embed(ref a) => Embed(map_embed(a)),
     }
 }
 
-pub fn map_record_value<'a, I, K, V, U, F>(it: I, mut f: F) -> BTreeMap<K, U>
+pub fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
 where
     I: IntoIterator<Item = (&'a K, &'a V)>,
     K: Eq + Ord + Copy + 'a,
     V: 'a,
     F: FnMut(&V) -> U,
 {
-    it.into_iter().map(|(&k, v)| (k, f(v))).collect()
+    map_record_value_and_keys(it, f, |&x| x)
+}
+
+pub fn map_record_value_and_keys<'a, I, K, L, V, U, F, G>(
+    it: I,
+    mut f: F,
+    mut g: G,
+) -> BTreeMap<L, U>
+where
+    I: IntoIterator<Item = (&'a K, &'a V)>,
+    K: Eq + Ord + 'a,
+    L: Eq + Ord + 'a,
+    V: 'a,
+    F: FnMut(&V) -> U,
+    G: FnMut(&K) -> L,
+{
+    it.into_iter().map(|(k, v)| (g(k), f(v))).collect()
 }
 
 pub fn map_opt_box<T, U, F>(x: &Option<Box<T>>, f: F) -> Option<Box<U>>
@@ -843,11 +928,16 @@ 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<'i, S, T, A: Clone>(
+pub fn shift<Label, S, T, A: Clone>(
     d: isize,
-    v: V<&'i str>,
-    e: &Expr<'i, S, A>,
-) -> Expr<'i, T, A> {
+    v: V<Label>,
+    e: &Expr_<Label, S, A>,
+) -> Expr_<Label, T, A>
+where
+    Label: Copy,
+    Label: Ord,
+    Label: PartialEq,
+{
     use crate::Expr_::*;
     let V(x, n) = v;
     match *e {
@@ -922,16 +1012,22 @@ pub fn shift<'i, S, T, A: Clone>(
     }
 }
 
-fn shift_op2<'i, S, T, A, F>(
+fn shift_op2<Label, S, T, A, F>(
     f: F,
     d: isize,
-    v: V<&'i str>,
-    a: &Expr<'i, S, A>,
-    b: &Expr<'i, S, A>,
-) -> Expr<'i, T, A>
+    v: V<Label>,
+    a: &Expr_<Label, S, A>,
+    b: &Expr_<Label, S, A>,
+) -> Expr_<Label, T, A>
 where
-    F: FnOnce(Box<Expr<'i, T, A>>, Box<Expr<'i, T, A>>) -> Expr<'i, T, A>,
+    F: FnOnce(
+        Box<Expr_<Label, T, A>>,
+        Box<Expr_<Label, T, A>>,
+    ) -> Expr_<Label, T, A>,
     A: Clone,
+    Label: Copy,
+    Label: Ord,
+    Label: PartialEq,
 {
     map_op2(f, |x| bx(shift(d, v, x)), a, b)
 }
@@ -942,11 +1038,11 @@ where
 /// subst x C B  ~  B[x := C]
 /// ```
 ///
-pub fn subst<'i, S, T, A>(
-    v: V<&'i str>,
-    e: &Expr<'i, S, A>,
-    b: &Expr<'i, T, A>,
-) -> Expr<'i, S, A>
+pub fn subst<Label: StringLike, S, T, A>(
+    v: V<Label>,
+    e: &Expr_<Label, S, A>,
+    b: &Expr_<Label, T, A>,
+) -> Expr_<Label, S, A>
 where
     S: Clone,
     A: Clone,
@@ -965,7 +1061,7 @@ where
             let n2 = if x == y { n + 1 } else { n };
             let tB2 = subst(V(x, n2), &shift(1, V(y, 0), e), tB);
             let tA2 = subst(V(x, n), e, tA);
-            pi(y, tA2, tB2)
+            Pi(y, bx(tA2), bx(tB2))
         }
         App(ref f, ref a) => {
             let f2 = subst(v, e, f);
@@ -1028,15 +1124,18 @@ where
     }
 }
 
-fn subst_op2<'i, S, T, A, F>(
+fn subst_op2<Label: StringLike, S, T, A, F>(
     f: F,
-    v: V<&'i str>,
-    e: &Expr<'i, S, A>,
-    a: &Expr<'i, T, A>,
-    b: &Expr<'i, T, A>,
-) -> Expr<'i, S, A>
+    v: V<Label>,
+    e: &Expr_<Label, S, A>,
+    a: &Expr_<Label, T, A>,
+    b: &Expr_<Label, T, A>,
+) -> Expr_<Label, S, A>
 where
-    F: FnOnce(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>) -> Expr<'i, S, A>,
+    F: FnOnce(
+        Box<Expr_<Label, S, A>>,
+        Box<Expr_<Label, S, A>>,
+    ) -> Expr_<Label, S, A>,
     S: Clone,
     A: Clone,
 {
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index 1cc62d0..7f2e295 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -4,8 +4,6 @@ use dhall_core::*;
 use proc_macro2::Literal;
 use proc_macro2::TokenStream;
 use quote::quote;
-use std::fmt::Debug;
-use std::hash::Hash;
 
 #[proc_macro]
 pub fn dhall(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
@@ -20,7 +18,7 @@ pub fn dhall(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
 
 // Returns an expression of type Expr<_, _>. Expects input variables
 // to be of type Box<Expr<_, _>> (future-proof for structural sharing).
-fn dhall_to_tokenstream<L: Eq + Hash + Clone + Debug + Into<String>>(
+fn dhall_to_tokenstream<L: StringLike>(
     expr: &Expr_<L, X, X>,
     ctx: &Context<L, ()>,
 ) -> TokenStream {
@@ -34,7 +32,7 @@ fn dhall_to_tokenstream<L: Eq + Hash + Clone + Debug + Into<String>>(
             let t = dhall_to_tokenstream_bx(t, ctx);
             let b = dhall_to_tokenstream_bx(b, &ctx.insert(x.clone(), ()));
             let x = Literal::string(&x.clone().into());
-            quote! { Lam(#x, #t, #b) }
+            quote! { Lam(#x.to_owned().into(), #t, #b) }
         }
         App(f, a) => {
             let f = dhall_to_tokenstream_bx(f, ctx);
@@ -76,18 +74,18 @@ fn dhall_to_tokenstream<L: Eq + Hash + Clone + Debug + Into<String>>(
 }
 
 // Returns an expression of type Box<Expr<_, _>>
-fn dhall_to_tokenstream_bx<L: Eq + Hash + Clone + Debug + Into<String>>(
+fn dhall_to_tokenstream_bx<L: StringLike>(
     expr: &Expr_<L, X, X>,
     ctx: &Context<L, ()>,
 ) -> TokenStream {
     use dhall_core::Expr_::*;
     match expr {
         Var(V(s, n)) => {
-            match ctx.lookup(s.clone(), *n) {
+            match ctx.lookup(&s, *n) {
                 // Non-free variable; interpolates as itself
                 Some(()) => {
                     let s: String = s.clone().into();
-                    quote! { bx(Var(V(#s, #n))) }
+                    quote! { bx(Var(V(#s.to_owned().into(), #n))) }
                 }
                 // Free variable; interpolates as a rust variable
                 None => {
@@ -95,7 +93,7 @@ fn dhall_to_tokenstream_bx<L: Eq + Hash + Clone + Debug + Into<String>>(
                     // TODO: insert appropriate shifts ?
                     let v: TokenStream = s.parse().unwrap();
                     quote! { {
-                        let x: Box<Expr<_, _>> = #v.clone();
+                        let x: Box<Expr_<_, _, _>> = #v.clone();
                         x
                     } }
                 }