Remove the pervasive Label type parameter

Closes #1

8 files changed, 134 insertions, 204 deletions

diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index 3b8ba6d..007ed47 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -8,9 +8,7 @@ use std::io::Read;
 use std::path::Path;
 use std::path::PathBuf;
 
-pub fn panic_imports<S: Clone>(
-    expr: &Expr<Label, S, Import>,
-) -> Expr<Label, S, X> {
+pub fn panic_imports<S: Clone>(expr: &Expr<S, Import>) -> Expr<S, X> {
     let no_import = |i: &Import| -> X { panic!("ahhh import: {:?}", i) };
     expr.map_embed(&no_import)
 }
@@ -24,7 +22,7 @@ pub enum ImportRoot {
 fn resolve_import(
     import: &Import,
     root: &ImportRoot,
-) -> Result<Expr<Label, X, X>, DhallError> {
+) -> Result<Expr<X, X>, DhallError> {
     use self::ImportRoot::*;
     use dhall_core::FilePrefix::*;
     use dhall_core::ImportLocation::*;
@@ -71,13 +69,13 @@ impl fmt::Display for DhallError {
 pub fn load_dhall_file(
     f: &Path,
     resolve_imports: bool,
-) -> Result<Expr<Label, X, X>, DhallError> {
+) -> Result<Expr<X, X>, DhallError> {
     let mut buffer = String::new();
     File::open(f)?.read_to_string(&mut buffer)?;
     let expr = parser::parse_expr(&*buffer)?;
     let expr = if resolve_imports {
         let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
-        let resolve = |import: &Import| -> Expr<Label, X, X> {
+        let resolve = |import: &Import| -> Expr<X, X> {
             resolve_import(import, &root).unwrap()
         };
         let expr = expr.map_embed(&resolve).squash_embed();
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 349af3d..edc6baf 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -65,7 +65,7 @@ fn main() {
         }
     };
 
-    let expr: Expr<Label, _, _> = imports::panic_imports(&expr);
+    let expr: Expr<_, _> = imports::panic_imports(&expr);
 
     let type_expr = match typecheck::type_of(&expr) {
         Err(e) => {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 6344c52..b2ee0f6 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -12,7 +12,7 @@ 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<S, T, A>(e: &Expr<Label, S, A>) -> Expr<Label, T, A>
+pub fn normalize<S, T, A>(e: &Expr<S, A>) -> Expr<T, A>
 where
     S: Clone + fmt::Debug,
     T: Clone + fmt::Debug,
@@ -93,7 +93,7 @@ where
                     normalize(&dhall_expr!(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_expr!(cons y ys)
@@ -130,7 +130,7 @@ 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_expr!(just y)
                     });
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 0dbb2f9..28982fc 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -29,8 +29,8 @@ fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
     }
 }
 
-fn match_vars<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, ctx: &[(L, L)]) -> bool {
-    let xxs: Option<(&(L, L), &[(L, L)])> = ctx.split_first();
+fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool {
+    let xxs: Option<(&(Label, Label), &[(Label, Label)])> = ctx.split_first();
     match (vl, vr, xxs) {
         (V(xL, nL), V(xR, nR), None) => xL == xR && nL == nR,
         (V(xL, 0), V(xR, 0), Some(((xL2, xR2), _)))
@@ -46,15 +46,15 @@ fn match_vars<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, ctx: &[(L, L)]) -> bool {
     }
 }
 
-fn prop_equal<S, T>(eL0: &Expr<Label, S, X>, eR0: &Expr<Label, T, X>) -> bool
+fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &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<Label, S, X>,
-        er: &Expr<Label, T, X>,
+        el: &Expr<S, X>,
+        er: &Expr<T, X>,
     ) -> bool
     where
         S: Clone + ::std::fmt::Debug,
@@ -144,16 +144,16 @@ where
 }
 
 fn op2_type<S, EF>(
-    ctx: &Context<Label, Expr<Label, S, X>>,
-    e: &Expr<Label, S, X>,
+    ctx: &Context<Label, Expr<S, X>>,
+    e: &Expr<S, X>,
     t: core::Builtin,
     ef: EF,
-    l: &Expr<Label, S, X>,
-    r: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<S>>
+    l: &Expr<S, X>,
+    r: &Expr<S, X>,
+) -> Result<Expr<S, X>, TypeError<S>>
 where
     S: Clone + ::std::fmt::Debug,
-    EF: FnOnce(Expr<Label, S, X>, Expr<Label, S, X>) -> TypeMessage<S>,
+    EF: FnOnce(Expr<S, X>, Expr<S, X>) -> TypeMessage<S>,
 {
     let tl = normalize(&type_with(ctx, l)?);
     match tl {
@@ -177,9 +177,9 @@ 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<Label, S, X>>,
-    e: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<S>>
+    ctx: &Context<Label, Expr<S, X>>,
+    e: &Expr<S, X>,
+) -> Result<Expr<S, X>, TypeError<S>>
 where
     S: Clone + ::std::fmt::Debug,
 {
@@ -416,7 +416,7 @@ where
         }
         ListLit(ref t, ref xs) => {
             let mut iter = xs.iter().enumerate();
-            let t: Box<Expr<_, _, _>> = match t {
+            let t: Box<Expr<_, _>> = match t {
                 Some(t) => t.clone(),
                 None => {
                     let (_, first_x) = iter.next().unwrap();
@@ -486,7 +486,7 @@ where
             pi("_", app(List, "a"), app(Optional, "a")),
         )),
         Builtin(ListIndexed) => {
-            let mut m: BTreeMap<Label, Expr<Label, _, _>> = BTreeMap::new();
+            let mut m: BTreeMap<Label, Expr<_, _>> = BTreeMap::new();
             m.insert("index".into(), Builtin(Natural));
             m.insert("value".into(), Var(V("a".into(), 0)));
             Ok(pi(
@@ -502,7 +502,7 @@ where
         )),
         OptionalLit(ref t, ref xs) => {
             let mut iter = xs.iter();
-            let t: Box<Expr<_, _, _>> = match t {
+            let t: Box<Expr<_, _>> = match t {
                 Some(t) => t.clone(),
                 None => {
                     let first_x = iter.next().unwrap();
@@ -707,8 +707,8 @@ where
 /// 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<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<S>> {
+    e: &Expr<S, X>,
+) -> Result<Expr<S, X>, TypeError<S>> {
     let ctx = Context::new();
     type_with(&ctx, e) //.map(|e| e.into_owned())
 }
@@ -717,83 +717,59 @@ pub fn type_of<S: Clone + ::std::fmt::Debug>(
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(Expr<Label, S, X>),
-    InvalidOutputType(Expr<Label, S, X>),
-    NotAFunction(Expr<Label, S, X>, Expr<Label, S, X>),
-    TypeMismatch(
-        Expr<Label, S, X>,
-        Expr<Label, S, X>,
-        Expr<Label, S, X>,
-        Expr<Label, S, X>,
-    ),
-    AnnotMismatch(Expr<Label, S, X>, Expr<Label, S, X>, Expr<Label, S, X>),
+    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>),
     Untyped,
-    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>,
-    ),
+    InvalidListElement(usize, Expr<S, X>, Expr<S, X>, Expr<S, X>),
+    InvalidListType(Expr<S, X>),
+    InvalidOptionalElement(Expr<S, X>, Expr<S, X>, Expr<S, X>),
     InvalidOptionalLiteral(usize),
-    InvalidOptionalType(Expr<Label, S, X>),
-    InvalidPredicate(Expr<Label, S, X>, Expr<Label, S, X>),
-    IfBranchMismatch(
-        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>,
-    ),
-    InvalidField(Label, Expr<Label, S, X>),
-    InvalidFieldType(Label, Expr<Label, S, X>),
-    InvalidAlternative(Label, Expr<Label, S, X>),
-    InvalidAlternativeType(Label, Expr<Label, S, X>),
+    InvalidOptionalType(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>),
     DuplicateAlternative(Label),
-    MustCombineARecord(Expr<Label, S, X>, Expr<Label, S, X>),
+    MustCombineARecord(Expr<S, X>, Expr<S, X>),
     FieldCollision(Label),
-    MustMergeARecord(Expr<Label, S, X>, Expr<Label, S, X>),
-    MustMergeUnion(Expr<Label, S, X>, Expr<Label, S, X>),
+    MustMergeARecord(Expr<S, X>, Expr<S, X>),
+    MustMergeUnion(Expr<S, X>, Expr<S, X>),
     UnusedHandler(HashSet<Label>),
     MissingHandler(HashSet<Label>),
-    HandlerInputTypeMismatch(Label, Expr<Label, S, X>, Expr<Label, S, X>),
-    HandlerOutputTypeMismatch(Label, Expr<Label, S, X>, Expr<Label, S, X>),
-    HandlerNotAFunction(Label, Expr<Label, S, X>),
-    NotARecord(Label, Expr<Label, S, X>, Expr<Label, S, X>),
-    MissingField(Label, 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>),
+    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>),
 }
 
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError<S> {
-    pub context: Context<Label, Expr<Label, S, X>>,
-    pub current: Expr<Label, S, X>,
+    pub context: Context<Label, Expr<S, X>>,
+    pub current: Expr<S, X>,
     pub type_message: TypeMessage<S>,
 }
 
 impl<S: Clone> TypeError<S> {
     pub fn new(
-        context: &Context<Label, Expr<Label, S, X>>,
-        current: &Expr<Label, S, X>,
+        context: &Context<Label, Expr<S, X>>,
+        current: &Expr<S, X>,
         type_message: TypeMessage<S>,
     ) -> Self {
         TypeError {
diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs
index 10c4f5c..9ed48e0 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -73,9 +73,7 @@ pub enum ExpectedResult {
     Failure,
 }
 
-pub fn read_dhall_file<'i>(
-    file_path: &str,
-) -> Result<Expr<Label, X, X>, DhallError> {
+pub fn read_dhall_file<'i>(file_path: &str) -> Result<Expr<X, X>, DhallError> {
     load_dhall_file(&PathBuf::from(file_path), true)
 }
 
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 7eaf08e..89fb6b9 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -1,7 +1,6 @@
 #![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
@@ -139,8 +138,8 @@ impl Label {
 /// Zero indices are omitted when pretty-printing `Var`s and non-zero indices
 /// appear as a numeric suffix.
 ///
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub struct V<Label>(pub Label, pub usize);
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct V(pub Label, pub usize);
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub enum BinOp {
@@ -172,52 +171,40 @@ pub enum BinOp {
 
 /// Syntax tree for expressions
 #[derive(Debug, Clone, PartialEq)]
-pub enum Expr<Label, Note, Embed> {
+pub enum Expr<Note, Embed> {
     ///  `Const c                                  ~  c`
     Const(Const),
     ///  `Var (V x 0)                              ~  x`<br>
     ///  `Var (V x n)                              ~  x@n`
-    Var(V<Label>),
+    Var(V),
     ///  `Lam x     A b                            ~  λ(x : A) -> b`
-    Lam(
-        Label,
-        Box<Expr<Label, Note, Embed>>,
-        Box<Expr<Label, Note, Embed>>,
-    ),
+    Lam(Label, Box<Expr<Note, Embed>>, Box<Expr<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<Note, Embed>>, Box<Expr<Note, Embed>>),
     ///  `App f A                                  ~  f A`
-    App(Box<Expr<Label, Note, Embed>>, Box<Expr<Label, Note, Embed>>),
+    App(Box<Expr<Note, Embed>>, Box<Expr<Note, Embed>>),
     ///  `Let x Nothing  r e  ~  let x     = r in e`
     ///  `Let x (Just t) r e  ~  let x : t = r in e`
     Let(
         Label,
-        Option<Box<Expr<Label, Note, Embed>>>,
-        Box<Expr<Label, Note, Embed>>,
-        Box<Expr<Label, Note, Embed>>,
+        Option<Box<Expr<Note, Embed>>>,
+        Box<Expr<Note, Embed>>,
+        Box<Expr<Note, Embed>>,
     ),
     ///  `Annot x t                                ~  x : t`
-    Annot(Box<Expr<Label, Note, Embed>>, Box<Expr<Label, Note, Embed>>),
+    Annot(Box<Expr<Note, Embed>>, Box<Expr<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<Note, Embed>>, Box<Expr<Note, Embed>>),
     ///  `BoolLit b                                ~  b`
     BoolLit(bool),
     ///  `BoolIf x y z                             ~  if x then y else z`
     BoolIf(
-        Box<Expr<Label, Note, Embed>>,
-        Box<Expr<Label, Note, Embed>>,
-        Box<Expr<Label, Note, Embed>>,
+        Box<Expr<Note, Embed>>,
+        Box<Expr<Note, Embed>>,
+        Box<Expr<Note, Embed>>,
     ),
     ///  `NaturalLit n                             ~  +n`
     NaturalLit(Natural),
@@ -228,38 +215,32 @@ 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<Note, Embed>>>, Vec<Expr<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<Note, Embed>>>, Vec<Expr<Note, Embed>>),
     ///  `Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }`
-    Record(BTreeMap<Label, Expr<Label, Note, Embed>>),
+    Record(BTreeMap<Label, Expr<Note, Embed>>),
     ///  `RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }`
-    RecordLit(BTreeMap<Label, Expr<Label, Note, Embed>>),
+    RecordLit(BTreeMap<Label, Expr<Note, Embed>>),
     ///  `Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1, k2 : t2 >`
-    Union(BTreeMap<Label, Expr<Label, Note, Embed>>),
+    Union(BTreeMap<Label, Expr<Note, Embed>>),
     ///  `UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1, k2 : t2, k3 : t3 >`
     UnionLit(
         Label,
-        Box<Expr<Label, Note, Embed>>,
-        BTreeMap<Label, Expr<Label, Note, Embed>>,
+        Box<Expr<Note, Embed>>,
+        BTreeMap<Label, Expr<Note, Embed>>,
     ),
     ///  `Merge x y t                              ~  merge x y : t`
     Merge(
-        Box<Expr<Label, Note, Embed>>,
-        Box<Expr<Label, Note, Embed>>,
-        Option<Box<Expr<Label, Note, Embed>>>,
+        Box<Expr<Note, Embed>>,
+        Box<Expr<Note, Embed>>,
+        Option<Box<Expr<Note, Embed>>>,
     ),
     ///  `Field e x                                ~  e.x`
-    Field(Box<Expr<Label, Note, Embed>>, Label),
+    Field(Box<Expr<Note, Embed>>, Label),
     /// Annotation on the AST. Unused for now but could hold e.g. file location information
-    Note(Note, Box<Expr<Label, Note, Embed>>),
+    Note(Note, Box<Expr<Note, Embed>>),
     /// Embeds an import or the result of resolving the import
     Embed(Embed),
 }
@@ -296,49 +277,43 @@ pub enum Builtin {
     TextShow,
 }
 
-impl From<Label> for V<Label> {
+impl From<Label> for V {
     fn from(s: Label) -> Self {
         V(s, 0)
     }
 }
 
-impl From<&'static str> for V<Label> {
+impl From<&'static str> for V {
     fn from(s: &'static str) -> Self {
         V(s.into(), 0)
     }
 }
 
-impl<'i, S, A> From<&'i str> for Expr<&'i str, S, A> {
-    fn from(s: &'i str) -> Self {
-        Expr::Var(V(s, 0))
-    }
-}
-
-impl<S, A> From<&'static str> for Expr<Label, S, A> {
+impl<S, A> From<&'static str> for Expr<S, A> {
     fn from(s: &'static str) -> Self {
         Expr::Var(V(s.into(), 0))
     }
 }
 
-impl<Label, S, A> From<Builtin> for Expr<Label, S, A> {
+impl<S, A> From<Builtin> for Expr<S, A> {
     fn from(t: Builtin) -> Self {
         Expr::Builtin(t)
     }
 }
 
-impl<S, A> Expr<Label, S, A> {
+impl<S, A> Expr<S, A> {
     pub fn map_shallow<T, B, F1, F2, F3, F4>(
         &self,
         map_expr: F1,
         map_note: F2,
         map_embed: F3,
         map_label: F4,
-    ) -> Expr<Label, T, B>
+    ) -> Expr<T, B>
     where
         A: Clone,
         T: Clone,
         S: Clone,
-        F1: Fn(&Self) -> Expr<Label, T, B>,
+        F1: Fn(&Self) -> Expr<T, B>,
         F2: FnOnce(&S) -> T,
         F3: FnOnce(&A) -> B,
         F4: Fn(&Label) -> Label,
@@ -346,15 +321,13 @@ impl<S, A> Expr<Label, S, A> {
         map_shallow(self, map_expr, map_note, map_embed, map_label)
     }
 
-    pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr<Label, S, B>
+    pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr<S, B>
     where
         A: Clone,
         S: Clone,
         F: Fn(&A) -> B,
     {
-        let recurse = |e: &Expr<Label, S, A>| -> Expr<Label, S, B> {
-            e.map_embed(map_embed)
-        };
+        let recurse = |e: &Expr<S, A>| -> Expr<S, B> { e.map_embed(map_embed) };
         self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone())
     }
 
@@ -390,8 +363,8 @@ impl<S, A> Expr<Label, S, A> {
     }
 }
 
-impl<S: Clone, A: Clone> Expr<Label, S, Expr<Label, S, A>> {
-    pub fn squash_embed(&self) -> Expr<Label, S, A> {
+impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> {
+    pub fn squash_embed(&self) -> Expr<S, A> {
         match self {
             Expr::Embed(e) => e.clone(),
             e => e.map_shallow(
@@ -414,7 +387,7 @@ impl<S: Clone, A: Clone> Expr<Label, S, Expr<Label, S, A>> {
 //  you add a new constructor to the syntax tree without adding a matching
 //  case the corresponding builder.
 
-impl<Label: Display, S, A: Display> Display for Expr<Label, S, A> {
+impl<S, A: Display> Display for Expr<S, A> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         // buildExprA
         use crate::Expr::*;
@@ -430,7 +403,7 @@ impl<Label: Display, S, A: Display> Display for Expr<Label, S, A> {
     }
 }
 
-impl<Label: Display, S, A: Display> Expr<Label, S, A> {
+impl<S, A: Display> Expr<S, A> {
     fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::Expr::*;
         match self {
@@ -726,7 +699,7 @@ impl Builtin {
     }
 }
 
-impl<Label: Display> Display for V<Label> {
+impl Display for V {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let V(ref x, ref n) = *self;
         x.fmt(f)?;
@@ -737,19 +710,19 @@ impl<Label: Display> Display for V<Label> {
     }
 }
 
-pub fn pi<S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<Label, S, A>
+pub fn pi<S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<S, A>
 where
     Name: Into<Label>,
-    Et: Into<Expr<Label, S, A>>,
-    Ev: Into<Expr<Label, S, A>>,
+    Et: Into<Expr<S, A>>,
+    Ev: Into<Expr<S, A>>,
 {
     Expr::Pi(var.into(), bx(ty.into()), bx(value.into()))
 }
 
-pub fn app<Label, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<Label, S, A>
+pub fn app<S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<S, A>
 where
-    Ef: Into<Expr<Label, S, A>>,
-    Ex: Into<Expr<Label, S, A>>,
+    Ef: Into<Expr<S, A>>,
+    Ex: Into<Expr<S, A>>,
 {
     Expr::App(bx(f.into()), bx(x.into()))
 }
@@ -783,24 +756,23 @@ fn add_ui(u: usize, i: isize) -> usize {
 }
 
 pub fn map_shallow<S, T, A, B, F1, F2, F3, F4>(
-    e: &Expr<Label, S, A>,
+    e: &Expr<S, A>,
     map: F1,
     map_note: F2,
     map_embed: F3,
     map_label: F4,
-) -> Expr<Label, T, B>
+) -> Expr<T, B>
 where
     A: Clone,
     S: Clone,
     T: Clone,
-    F1: Fn(&Expr<Label, S, A>) -> Expr<Label, T, B>,
+    F1: Fn(&Expr<S, A>) -> Expr<T, B>,
     F2: FnOnce(&S) -> T,
     F3: FnOnce(&A) -> B,
     F4: Fn(&Label) -> Label,
 {
     use crate::Expr::*;
-    let bxmap =
-        |x: &Expr<Label, S, A>| -> Box<Expr<Label, T, B>> { bx(map(x)) };
+    let bxmap = |x: &Expr<S, A>| -> Box<Expr<T, B>> { bx(map(x)) };
     let opt = |x| map_opt_box(x, &map);
     match *e {
         Const(k) => Const(k),
@@ -959,11 +931,7 @@ where
 /// descend into a lambda or let expression that binds a variable of the same
 /// name in order to avoid shifting the bound variables by mistake.
 ///
-pub fn shift<S, T, A: Clone>(
-    d: isize,
-    v: &V<Label>,
-    e: &Expr<Label, S, A>,
-) -> Expr<Label, T, A> {
+pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> {
     use crate::Expr::*;
     let V(x, n) = v;
     match e {
@@ -1039,15 +1007,12 @@ pub fn shift<S, T, A: Clone>(
 fn shift_op2<S, T, A, F>(
     f: F,
     d: isize,
-    v: &V<Label>,
-    a: &Expr<Label, S, A>,
-    b: &Expr<Label, S, A>,
-) -> Expr<Label, T, A>
+    v: &V,
+    a: &Expr<S, A>,
+    b: &Expr<S, A>,
+) -> Expr<T, A>
 where
-    F: FnOnce(
-        Box<Expr<Label, T, A>>,
-        Box<Expr<Label, T, A>>,
-    ) -> Expr<Label, T, A>,
+    F: FnOnce(Box<Expr<T, A>>, Box<Expr<T, A>>) -> Expr<T, A>,
     A: Clone,
 {
     map_op2(f, |x| bx(shift(d, v, x)), a, b)
@@ -1059,11 +1024,7 @@ where
 /// subst x C B  ~  B[x := C]
 /// ```
 ///
-pub fn subst<S, T, A>(
-    v: &V<Label>,
-    e: &Expr<Label, S, A>,
-    b: &Expr<Label, T, A>,
-) -> Expr<Label, S, A>
+pub fn subst<S, T, A>(v: &V, e: &Expr<S, A>, b: &Expr<T, A>) -> Expr<S, A>
 where
     S: Clone,
     A: Clone,
@@ -1150,16 +1111,13 @@ where
 
 fn subst_op2<S, T, A, F>(
     f: F,
-    v: &V<Label>,
-    e: &Expr<Label, S, A>,
-    a: &Expr<Label, T, A>,
-    b: &Expr<Label, T, A>,
-) -> Expr<Label, S, A>
+    v: &V,
+    e: &Expr<S, A>,
+    a: &Expr<T, A>,
+    b: &Expr<T, A>,
+) -> Expr<S, A>
 where
-    F: FnOnce(
-        Box<Expr<Label, S, A>>,
-        Box<Expr<Label, S, A>>,
-    ) -> Expr<Label, S, A>,
+    F: FnOnce(Box<Expr<S, A>>, Box<Expr<S, A>>) -> Expr<S, A>,
     S: Clone,
     A: Clone,
 {
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 7073a93..2fa005a 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -8,7 +8,7 @@ use dhall_parser::{DhallParser, Rule};
 use crate::core;
 use crate::core::*;
 
-pub type ParsedExpr = Expr<Label, X, Import>;
+pub type ParsedExpr = Expr<X, Import>;
 pub type BoxExpr = Box<ParsedExpr>;
 
 pub type ParseError = pest::error::Error<Rule>;
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index f633544..780b621 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -8,7 +8,7 @@ use quote::quote;
 #[proc_macro]
 pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let input_str = input.to_string();
-    let expr: Box<Expr<_, X, Import>> = parser::parse_expr(&input_str).unwrap();
+    let expr: Box<Expr<X, Import>> = parser::parse_expr(&input_str).unwrap();
     let no_import =
         |_: &Import| -> X { panic!("Don't use import in dhall!()") };
     let expr = expr.map_embed(&no_import);
@@ -19,7 +19,7 @@ pub fn dhall_expr(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(
-    expr: &Expr<Label, X, X>,
+    expr: &Expr<X, X>,
     ctx: &Context<Label, ()>,
 ) -> TokenStream {
     use dhall_core::Expr::*;
@@ -75,7 +75,7 @@ fn dhall_to_tokenstream(
 
 // Returns an expression of type Box<Expr<_, _>>
 fn dhall_to_tokenstream_bx(
-    expr: &Expr<Label, X, X>,
+    expr: &Expr<X, X>,
     ctx: &Context<Label, ()>,
 ) -> TokenStream {
     use dhall_core::Expr::*;
@@ -93,7 +93,7 @@ fn dhall_to_tokenstream_bx(
                     // TODO: insert appropriate shifts ?
                     let v: TokenStream = s.parse().unwrap();
                     quote! { {
-                        let x: Box<Expr<_, _, _>> = #v.clone();
+                        let x: Box<Expr<_, _>> = #v.clone();
                         x
                     } }
                 }