From 4c159640e5ee77ffa48b85a5bffa56350cf933ef Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 17:59:05 +0200
Subject: Make SubExpr generic in the variable labels type

---
 dhall/src/binary.rs             |  22 +++--
 dhall/src/expr.rs               |  32 ++++---
 dhall/src/normalize.rs          |  48 +++++-----
 dhall/src/serde.rs              |   2 +-
 dhall/src/traits/static_type.rs |  14 +--
 dhall/src/typecheck.rs          |  65 +++++++------
 dhall/tests/traits.rs           |   4 +-
 dhall_proc_macros/src/quote.rs  |  62 ++++++------
 dhall_syntax/src/core.rs        | 207 +++++++++++++++++++++-------------------
 dhall_syntax/src/parser.rs      |  24 +++--
 dhall_syntax/src/printer.rs     |  44 +++++----
 dhall_syntax/src/visitor.rs     | 130 ++++++++++++-------------
 12 files changed, 351 insertions(+), 303 deletions(-)

diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 9c31d4c..0d9f28a 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -2,7 +2,7 @@ use dhall_syntax::*;
 use itertools::*;
 use serde_cbor::value::value as cbor;
 
-type ParsedExpr = SubExpr<X, Import>;
+type ParsedExpr = SubExpr<Label, X, Import>;
 
 #[derive(Debug)]
 pub enum DecodeError {
@@ -18,28 +18,32 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
 }
 
 fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
-    use cbor::Value::*;
+    use cbor::Value::{Array, Bool, Null, Object, String, F64, I64, U64};
     use dhall_syntax::{BinOp, Builtin, Const};
-    use ExprF::*;
+    use ExprF::{
+        Annot, App, BoolIf, BoolLit, DoubleLit, Embed, EmptyListLit, Field,
+        IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit, OldOptionalLit, Pi,
+        RecordLit, RecordType, SomeLit, TextLit, UnionLit, UnionType,
+    };
     Ok(rc(match data {
         String(s) => match Builtin::parse(s) {
             Some(b) => ExprF::Builtin(b),
             None => match s.as_str() {
                 "True" => BoolLit(true),
                 "False" => BoolLit(false),
-                "Type" => Const(Const::Type),
-                "Kind" => Const(Const::Kind),
-                "Sort" => Const(Const::Sort),
+                "Type" => ExprF::Const(Const::Type),
+                "Kind" => ExprF::Const(Const::Kind),
+                "Sort" => ExprF::Const(Const::Sort),
                 _ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?,
             },
         },
-        U64(n) => Var(V(Label::from("_"), *n as usize)),
+        U64(n) => ExprF::Var(Var(Label::from("_"), *n as usize)),
         F64(x) => DoubleLit((*x).into()),
         Bool(b) => BoolLit(*b),
         Array(vec) => match vec.as_slice() {
             [String(l), U64(n)] => {
                 let l = Label::from(l.as_str());
-                Var(V(l, *n as usize))
+                ExprF::Var(Var(l, *n as usize))
             }
             [U64(0), f, args..] => {
                 let mut f = cbor_value_to_dhall(&f)?;
@@ -92,7 +96,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
                         Err(DecodeError::WrongFormatError("binop".to_owned()))?
                     }
                 };
-                BinOp(op, x, y)
+                ExprF::BinOp(op, x, y)
             }
             [U64(4), t] => {
                 let t = cbor_value_to_dhall(&t)?;
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 5bde68f..efc3928 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -23,15 +23,17 @@ macro_rules! derive_other_traits {
     };
 }
 
+type OutputSubExpr = SubExpr<Label, X, X>;
+
 #[derive(Debug, Clone)]
 pub(crate) struct Parsed(
-    pub(crate) SubExpr<Span, Import>,
+    pub(crate) SubExpr<Label, Span, Import>,
     pub(crate) ImportRoot,
 );
 derive_other_traits!(Parsed);
 
 #[derive(Debug, Clone)]
-pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>);
+pub(crate) struct Resolved(pub(crate) SubExpr<Label, Span, Normalized>);
 derive_other_traits!(Resolved);
 
 pub(crate) use self::typed::TypedInternal;
@@ -57,12 +59,12 @@ impl std::fmt::Display for Normalized {
 }
 
 mod typed {
-    use super::{Type, Typed};
+    use super::{OutputSubExpr, Type, Typed};
     use crate::normalize::{Thunk, Value};
     use crate::typecheck::{
         TypeError, TypeInternal, TypeMessage, TypecheckContext,
     };
-    use dhall_syntax::{Const, Label, SubExpr, V, X};
+    use dhall_syntax::{Const, Label, Var};
     use std::borrow::Cow;
 
     #[derive(Debug, Clone)]
@@ -90,7 +92,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+        pub(crate) fn to_expr(&self) -> OutputSubExpr {
             self.to_value().normalize_to_expr()
         }
 
@@ -129,7 +131,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.shift(delta, var),
@@ -139,7 +141,11 @@ mod typed {
             }
         }
 
-        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+        pub(crate) fn subst_shift(
+            &self,
+            var: &Var<Label>,
+            val: &Typed,
+        ) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.subst_shift(var, val),
@@ -158,7 +164,7 @@ mod typed {
 ///
 /// For a more general notion of "type", see [Type].
 #[derive(Debug, Clone)]
-pub struct SimpleType(pub(crate) SubExpr<X, X>);
+pub struct SimpleType(pub(crate) OutputSubExpr);
 derive_other_traits!(SimpleType);
 
 pub(crate) use crate::typecheck::TypeInternal;
@@ -178,16 +184,16 @@ impl std::fmt::Display for Type {
 
 // Exposed for the macros
 #[doc(hidden)]
-impl From<SimpleType> for SubExpr<X, X> {
-    fn from(x: SimpleType) -> SubExpr<X, X> {
+impl From<SimpleType> for OutputSubExpr {
+    fn from(x: SimpleType) -> OutputSubExpr {
         x.0
     }
 }
 
 // Exposed for the macros
 #[doc(hidden)]
-impl From<SubExpr<X, X>> for SimpleType {
-    fn from(x: SubExpr<X, X>) -> SimpleType {
+impl From<OutputSubExpr> for SimpleType {
+    fn from(x: OutputSubExpr) -> SimpleType {
         SimpleType(x)
     }
 }
@@ -204,7 +210,7 @@ impl Normalized {
     pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
         Normalized(TypedInternal::from_thunk_and_type(th, t))
     }
-    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+    pub(crate) fn to_expr(&self) -> OutputSubExpr {
         self.0.to_expr()
     }
     pub(crate) fn to_value(&self) -> Value {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 8ae746d..3de12ee 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,13 +6,13 @@ use dhall_proc_macros as dhall;
 use dhall_syntax::context::Context;
 use dhall_syntax::{
     rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
-    InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X,
+    InterpolatedTextContents, Label, Natural, Span, SubExpr, Var, X,
 };
 
 use crate::expr::{Normalized, Type, Typed, TypedInternal};
 
-type InputSubExpr = SubExpr<Span, Normalized>;
-type OutputSubExpr = SubExpr<X, X>;
+type InputSubExpr = SubExpr<Label, Span, Normalized>;
+type OutputSubExpr = SubExpr<Label, X, X>;
 
 impl Typed {
     /// Reduce an expression to its normal form, performing beta reduction
@@ -38,11 +38,11 @@ impl Typed {
         Normalized(internal)
     }
 
-    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         Typed(self.0.shift(delta, var))
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
         Typed(self.0.subst_shift(var, val))
     }
 
@@ -58,11 +58,11 @@ impl Typed {
 #[derive(Debug, Clone)]
 enum EnvItem {
     Thunk(Thunk),
-    Skip(V<Label>),
+    Skip(Var<Label>),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         use EnvItem::*;
         match self {
             Thunk(e) => Thunk(e.shift(delta, var)),
@@ -70,7 +70,7 @@ impl EnvItem {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
             EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -93,8 +93,8 @@ impl NormalizationContext {
                 .insert(x.clone(), EnvItem::Skip(x.into())),
         ))
     }
-    fn lookup(&self, var: &V<Label>) -> Value {
-        let V(x, n) = var;
+    fn lookup(&self, var: &Var<Label>) -> Value {
+        let Var(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Thunk(t)) => t.to_value(),
             Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
@@ -118,11 +118,11 @@ impl NormalizationContext {
         NormalizationContext(Rc::new(ctx))
     }
 
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
     }
 
-    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
         NormalizationContext(Rc::new(
             self.0.map(|_, e| e.subst_shift(var, val)),
         ))
@@ -144,7 +144,7 @@ pub(crate) enum Value {
     NaturalSuccClosure,
     Pi(Label, TypeThunk, TypeThunk),
 
-    Var(V<Label>),
+    Var(Var<Label>),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -403,7 +403,7 @@ impl Value {
         Value::AppliedBuiltin(b, vec![])
     }
 
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -500,7 +500,7 @@ impl Value {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -616,7 +616,7 @@ mod thunk {
         OutputSubExpr, Value,
     };
     use crate::expr::Typed;
-    use dhall_syntax::{Label, V};
+    use dhall_syntax::{Label, Var};
     use std::cell::{Ref, RefCell};
     use std::rc::Rc;
 
@@ -693,7 +693,7 @@ mod thunk {
             }
         }
 
-        fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -707,7 +707,7 @@ mod thunk {
             }
         }
 
-        fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+        fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -805,11 +805,15 @@ mod thunk {
             apply_any(self.clone(), th)
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
             self.0.borrow().shift(delta, var).into_thunk()
         }
 
-        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+        pub(crate) fn subst_shift(
+            &self,
+            var: &Var<Label>,
+            val: &Typed,
+        ) -> Self {
             self.0.borrow().subst_shift(var, val).into_thunk()
         }
     }
@@ -855,14 +859,14 @@ impl TypeThunk {
         self.normalize_nf().normalize_to_expr()
     }
 
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
             TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs
index 96bc765..bc76c49 100644
--- a/dhall/src/serde.rs
+++ b/dhall/src/serde.rs
@@ -11,7 +11,7 @@ impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T {
     }
 }
 
-struct Deserializer<'a>(Cow<'a, SubExpr<X, X>>);
+struct Deserializer<'a>(Cow<'a, SubExpr<Label, X, X>>);
 
 impl serde::de::Error for Error {
     fn custom<T>(msg: T) -> Self
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index f90b8df..c3f323b 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -32,7 +32,7 @@ pub trait SimpleStaticType {
     fn get_simple_static_type() -> SimpleType;
 }
 
-fn mktype(x: SubExpr<X, X>) -> SimpleType {
+fn mktype(x: SubExpr<Label, X, X>) -> SimpleType {
     x.into()
 }
 
@@ -106,22 +106,22 @@ impl SimpleStaticType for String {
 
 impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) {
     fn get_simple_static_type() -> SimpleType {
-        let ta: SubExpr<_, _> = A::get_simple_static_type().into();
-        let tb: SubExpr<_, _> = B::get_simple_static_type().into();
+        let ta: SubExpr<_, _, _> = A::get_simple_static_type().into();
+        let tb: SubExpr<_, _, _> = B::get_simple_static_type().into();
         mktype(dhall::subexpr!({ _1: ta, _2: tb }))
     }
 }
 
 impl<T: SimpleStaticType> SimpleStaticType for Option<T> {
     fn get_simple_static_type() -> SimpleType {
-        let t: SubExpr<_, _> = T::get_simple_static_type().into();
+        let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
         mktype(dhall::subexpr!(Optional t))
     }
 }
 
 impl<T: SimpleStaticType> SimpleStaticType for Vec<T> {
     fn get_simple_static_type() -> SimpleType {
-        let t: SubExpr<_, _> = T::get_simple_static_type().into();
+        let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
         mktype(dhall::subexpr!(List t))
     }
 }
@@ -142,8 +142,8 @@ impl<T: SimpleStaticType, E: SimpleStaticType> SimpleStaticType
     for std::result::Result<T, E>
 {
     fn get_simple_static_type() -> SimpleType {
-        let tt: SubExpr<_, _> = T::get_simple_static_type().into();
-        let te: SubExpr<_, _> = E::get_simple_static_type().into();
+        let tt: SubExpr<_, _, _> = T::get_simple_static_type().into();
+        let te: SubExpr<_, _, _> = E::get_simple_static_type().into();
         mktype(dhall::subexpr!(< Ok: tt | Err: te>))
     }
 }
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8b7f011..63041bb 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -14,13 +14,16 @@ use dhall_syntax::*;
 
 use self::TypeMessage::*;
 
+type InputSubExpr = SubExpr<Label, Span, Normalized>;
+type OutputSubExpr = SubExpr<Label, X, X>;
+
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError> {
         type_of(self.0)
     }
     pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
-        let expr: SubExpr<_, _> = self.0;
-        let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd();
+        let expr = self.0;
+        let ty = ty.to_expr().embed_absurd().note_absurd();
         type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
     }
     /// Pretends this expression has been typechecked. Use with care.
@@ -43,7 +46,7 @@ impl Typed {
 }
 
 impl Normalized {
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         Normalized(self.0.shift(delta, var))
     }
     pub(crate) fn to_type(self) -> Type {
@@ -55,7 +58,7 @@ impl Type {
     pub(crate) fn to_normalized(&self) -> Normalized {
         self.0.to_normalized()
     }
-    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+    pub(crate) fn to_expr(&self) -> OutputSubExpr {
         self.0.to_expr()
     }
     pub(crate) fn to_value(&self) -> Value {
@@ -73,10 +76,10 @@ impl Type {
     fn internal_whnf(&self) -> Option<Value> {
         self.0.whnf()
     }
-    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         Type(self.0.shift(delta, var))
     }
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
         Type(self.0.subst_shift(var, val))
     }
 
@@ -124,7 +127,7 @@ impl TypeInternal {
     fn to_normalized(&self) -> Normalized {
         self.to_typed().normalize()
     }
-    fn to_expr(&self) -> SubExpr<X, X> {
+    fn to_expr(&self) -> OutputSubExpr {
         self.to_normalized().to_expr()
     }
     fn to_value(&self) -> Value {
@@ -148,14 +151,14 @@ impl TypeInternal {
             _ => None,
         }
     }
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.shift(delta, var))),
             Const(c) => Const(*c),
         }
     }
-    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -173,12 +176,12 @@ impl PartialEq for TypeInternal {
 
 #[derive(Debug, Clone)]
 pub(crate) enum EnvItem {
-    Type(V<Label>, Type),
+    Type(Var<Label>, Type),
     Value(Normalized),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
         use EnvItem::*;
         match self {
             Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
@@ -205,8 +208,8 @@ impl TypecheckContext {
     pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self {
         TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t)))
     }
-    pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> {
-        let V(x, n) = var;
+    pub(crate) fn lookup(&self, var: &Var<Label>) -> Option<Cow<'_, Type>> {
+        let Var(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)),
             Some(EnvItem::Value(t)) => Some(t.get_type()?),
@@ -238,8 +241,12 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
     }
 }
 
-fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
-    let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr);
+fn match_vars(
+    vl: &Var<Label>,
+    vr: &Var<Label>,
+    ctx: &[(&Label, &Label)],
+) -> bool {
+    let (Var(xL, mut nL), Var(xR, mut nR)) = (vl, vr);
     for &(xL2, xR2) in ctx {
         match (nL, nR) {
             (0, 0) if xL == xL2 && xR == xR2 => return true,
@@ -265,8 +272,8 @@ where
     use dhall_syntax::ExprF::*;
     fn go<'a, S, T>(
         ctx: &mut Vec<(&'a Label, &'a Label)>,
-        el: &'a SubExpr<S, X>,
-        er: &'a SubExpr<T, X>,
+        el: &'a SubExpr<Label, S, X>,
+        er: &'a SubExpr<Label, T, X>,
     ) -> bool
     where
         S: ::std::fmt::Debug,
@@ -350,9 +357,9 @@ fn type_of_const(c: Const) -> Result<Type, TypeError> {
     }
 }
 
-fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
+fn type_of_builtin(b: Builtin) -> InputSubExpr {
     use dhall_syntax::Builtin::*;
-    match b {
+    rc(match b {
         Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
         List | Optional => dhall::expr!(
             Type -> Type
@@ -432,7 +439,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
         OptionalNone => dhall::expr!(
             forall (A: Type) -> Optional A
         ),
-    }
+    })
+    .note_absurd()
 }
 
 macro_rules! ensure_equal {
@@ -619,10 +627,7 @@ impl TypeIntermediate {
 
 /// Takes an expression that is meant to contain a Type
 /// and turn it into a type, typechecking it along the way.
-fn mktype(
-    ctx: &TypecheckContext,
-    e: SubExpr<Span, Normalized>,
-) -> Result<Type, TypeError> {
+fn mktype(ctx: &TypecheckContext, e: InputSubExpr) -> Result<Type, TypeError> {
     Ok(type_with(ctx, e)?.to_type())
 }
 
@@ -645,7 +650,7 @@ enum Ret {
 /// succeeded, or an error if type-checking failed
 fn type_with(
     ctx: &TypecheckContext,
-    e: SubExpr<Span, Normalized>,
+    e: InputSubExpr,
 ) -> Result<Typed, TypeError> {
     use dhall_syntax::ExprF::{
         Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
@@ -756,7 +761,7 @@ fn type_last_layer(
                 mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
             });
 
-            Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
+            Ok(RetType(tb.subst_shift(&x.into(), &a)))
         }
         Annot(x, t) => {
             let t = t.to_type();
@@ -937,9 +942,7 @@ fn type_last_layer(
             }
         }
         Const(c) => Ok(RetTyped(const_to_typed(c))),
-        Builtin(b) => {
-            Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?))
-        }
+        Builtin(b) => Ok(RetType(mktype(ctx, type_of_builtin(b))?)),
         BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
         IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
@@ -998,7 +1001,7 @@ fn type_last_layer(
 /// `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.
-fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
+fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
     let ctx = TypecheckContext::new();
     let e = type_with(&ctx, e)?;
     // Ensure `e` has a type (i.e. `e` is not `Sort`)
@@ -1009,7 +1012,7 @@ fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
 /// The specific type error
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
-    UnboundVariable(V<Label>),
+    UnboundVariable(Var<Label>),
     InvalidInputType(Normalized),
     InvalidOutputType(Normalized),
     NotAFunction(Typed),
diff --git a/dhall/tests/traits.rs b/dhall/tests/traits.rs
index 6604c06..cf68d7d 100644
--- a/dhall/tests/traits.rs
+++ b/dhall/tests/traits.rs
@@ -1,11 +1,11 @@
 #![feature(proc_macro_hygiene)]
 use dhall::de::SimpleStaticType;
 use dhall_proc_macros;
-use dhall_syntax::{SubExpr, X};
+use dhall_syntax::{Label, SubExpr, X};
 
 #[test]
 fn test_static_type() {
-    fn mktype(x: SubExpr<X, X>) -> dhall::expr::SimpleType {
+    fn mktype(x: SubExpr<Label, X, X>) -> dhall::expr::SimpleType {
         x.into()
     }
 
diff --git a/dhall_proc_macros/src/quote.rs b/dhall_proc_macros/src/quote.rs
index eaf4946..d0deaad 100644
--- a/dhall_proc_macros/src/quote.rs
+++ b/dhall_proc_macros/src/quote.rs
@@ -7,7 +7,7 @@ use std::collections::BTreeMap;
 
 pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let input_str = input.to_string();
-    let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote();
+    let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote();
     let no_import =
         |_: &Import| -> X { panic!("Don't use import in dhall::expr!()") };
     let expr = expr.map_embed(no_import);
@@ -17,7 +17,7 @@ pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
 
 pub fn subexpr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let input_str = input.to_string();
-    let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote();
+    let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote();
     let no_import =
         |_: &Import| -> X { panic!("Don't use import in dhall::subexpr!()") };
     let expr = expr.map_embed(no_import);
@@ -31,60 +31,59 @@ pub fn quote_exprf<TS>(expr: ExprF<TS, Label, X>) -> TokenStream
 where
     TS: quote::ToTokens + std::fmt::Debug,
 {
-    use dhall_syntax::ExprF::*;
     match expr {
-        Var(_) => unreachable!(),
-        Pi(x, t, b) => {
+        ExprF::Var(_) => unreachable!(),
+        ExprF::Pi(x, t, b) => {
             let x = quote_label(&x);
             quote! { dhall_syntax::ExprF::Pi(#x, #t, #b) }
         }
-        Lam(x, t, b) => {
+        ExprF::Lam(x, t, b) => {
             let x = quote_label(&x);
             quote! { dhall_syntax::ExprF::Lam(#x, #t, #b) }
         }
-        App(f, a) => {
+        ExprF::App(f, a) => {
             quote! { dhall_syntax::ExprF::App(#f, #a) }
         }
-        Annot(x, t) => {
+        ExprF::Annot(x, t) => {
             quote! { dhall_syntax::ExprF::Annot(#x, #t) }
         }
-        Const(c) => {
+        ExprF::Const(c) => {
             let c = quote_const(c);
             quote! { dhall_syntax::ExprF::Const(#c) }
         }
-        Builtin(b) => {
+        ExprF::Builtin(b) => {
             let b = quote_builtin(b);
             quote! { dhall_syntax::ExprF::Builtin(#b) }
         }
-        BinOp(o, a, b) => {
+        ExprF::BinOp(o, a, b) => {
             let o = quote_binop(o);
             quote! { dhall_syntax::ExprF::BinOp(#o, #a, #b) }
         }
-        NaturalLit(n) => {
+        ExprF::NaturalLit(n) => {
             quote! { dhall_syntax::ExprF::NaturalLit(#n) }
         }
-        BoolLit(b) => {
+        ExprF::BoolLit(b) => {
             quote! { dhall_syntax::ExprF::BoolLit(#b) }
         }
-        SomeLit(x) => {
+        ExprF::SomeLit(x) => {
             quote! { dhall_syntax::ExprF::SomeLit(#x) }
         }
-        EmptyListLit(t) => {
+        ExprF::EmptyListLit(t) => {
             quote! { dhall_syntax::ExprF::EmptyListLit(#t) }
         }
-        NEListLit(es) => {
+        ExprF::NEListLit(es) => {
             let es = quote_vec(es);
             quote! { dhall_syntax::ExprF::NEListLit(#es) }
         }
-        RecordType(m) => {
+        ExprF::RecordType(m) => {
             let m = quote_map(m);
             quote! { dhall_syntax::ExprF::RecordType(#m) }
         }
-        RecordLit(m) => {
+        ExprF::RecordLit(m) => {
             let m = quote_map(m);
             quote! { dhall_syntax::ExprF::RecordLit(#m) }
         }
-        UnionType(m) => {
+        ExprF::UnionType(m) => {
             let m = quote_opt_map(m);
             quote! { dhall_syntax::ExprF::UnionType(#m) }
         }
@@ -95,22 +94,21 @@ where
 // Returns an expression of type SubExpr<_, _>. Expects interpolated variables
 // to be of type SubExpr<_, _>.
 fn quote_subexpr(
-    expr: &SubExpr<X, X>,
+    expr: &SubExpr<Label, X, X>,
     ctx: &Context<Label, ()>,
 ) -> TokenStream {
-    use dhall_syntax::ExprF::*;
     match expr.as_ref().map_ref_with_special_handling_of_binders(
         |e| quote_subexpr(e, ctx),
         |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())),
         |_| unreachable!(),
         Label::clone,
     ) {
-        Var(V(ref s, n)) => {
+        ExprF::Var(Var(ref s, n)) => {
             match ctx.lookup(s, n) {
                 // Non-free variable; interpolates as itself
                 Some(()) => {
                     let s: String = s.into();
-                    let var = quote! { dhall_syntax::V(#s.into(), #n) };
+                    let var = quote! { dhall_syntax::Var(#s.into(), #n) };
                     rc(quote! { dhall_syntax::ExprF::Var(#var) })
                 }
                 // Free variable; interpolates as a rust variable
@@ -119,7 +117,7 @@ fn quote_subexpr(
                     // TODO: insert appropriate shifts ?
                     let v: TokenStream = s.parse().unwrap();
                     quote! { {
-                        let x: dhall_syntax::SubExpr<_, _> = #v.clone();
+                        let x: dhall_syntax::SubExpr<_, _, _> = #v.clone();
                         x
                     } }
                 }
@@ -129,22 +127,24 @@ fn quote_subexpr(
     }
 }
 
-// Returns an expression of type Expr<_, _>. Expects interpolated variables
-// to be of type SubExpr<_, _>.
-fn quote_expr(expr: &Expr<X, X>, ctx: &Context<Label, ()>) -> TokenStream {
-    use dhall_syntax::ExprF::*;
+// Returns an expression of type Expr<_, _, _>. Expects interpolated variables
+// to be of type SubExpr<_, _, _>.
+fn quote_expr(
+    expr: &Expr<Label, X, X>,
+    ctx: &Context<Label, ()>,
+) -> TokenStream {
     match expr.map_ref_with_special_handling_of_binders(
         |e| quote_subexpr(e, ctx),
         |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())),
         |_| unreachable!(),
         Label::clone,
     ) {
-        Var(V(ref s, n)) => {
+        ExprF::Var(Var(ref s, n)) => {
             match ctx.lookup(s, n) {
                 // Non-free variable; interpolates as itself
                 Some(()) => {
                     let s: String = s.into();
-                    let var = quote! { dhall_syntax::V(#s.into(), #n) };
+                    let var = quote! { dhall_syntax::Var(#s.into(), #n) };
                     quote! { dhall_syntax::ExprF::Var(#var) }
                 }
                 // Free variable; interpolates as a rust variable
@@ -153,7 +153,7 @@ fn quote_expr(expr: &Expr<X, X>, ctx: &Context<Label, ()>) -> TokenStream {
                     // TODO: insert appropriate shifts ?
                     let v: TokenStream = s.parse().unwrap();
                     quote! { {
-                        let x: dhall_syntax::SubExpr<_, _> = #v.clone();
+                        let x: dhall_syntax::SubExpr<_, _, _> = #v.clone();
                         x.unroll()
                     } }
                 }
diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index a186d19..c8a2425 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,19 +60,7 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct V<Label>(pub Label, pub usize);
-
-// This is only for the specific `Label` type, not generic
-impl From<Label> for V<Label> {
-    fn from(x: Label) -> V<Label> {
-        V(x, 0)
-    }
-}
-impl<'a> From<&'a Label> for V<Label> {
-    fn from(x: &'a Label) -> V<Label> {
-        V(x.clone(), 0)
-    }
-}
+pub struct Var<Label>(pub Label, pub usize);
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -137,44 +125,52 @@ pub enum Builtin {
     TextShow,
 }
 
-pub type ParsedExpr = SubExpr<X, Import>;
-pub type ResolvedExpr = SubExpr<X, X>;
+pub type ParsedExpr = SubExpr<Label, X, Import>;
+pub type ResolvedExpr = SubExpr<Label, X, X>;
 pub type DhallExpr = ResolvedExpr;
 
 // Each node carries an annotation. In practice it's either X (no annotation) or a Span.
 #[derive(Debug)]
-pub struct SubExpr<Note, Embed>(Rc<(Expr<Note, Embed>, Option<Note>)>);
+pub struct SubExpr<VarLabel, Note, Embed>(
+    Rc<(Expr<VarLabel, Note, Embed>, Option<Note>)>,
+);
 
-impl<Note, Embed: PartialEq> std::cmp::PartialEq for SubExpr<Note, Embed> {
+impl<VarLabel: PartialEq, Note, Embed: PartialEq> std::cmp::PartialEq
+    for SubExpr<VarLabel, Note, Embed>
+{
     fn eq(&self, other: &Self) -> bool {
         self.0.as_ref().0 == other.0.as_ref().0
     }
 }
 
-impl<Note, Embed: Eq> std::cmp::Eq for SubExpr<Note, Embed> {}
+impl<VarLabel: Eq, Note, Embed: Eq> std::cmp::Eq
+    for SubExpr<VarLabel, Note, Embed>
+{
+}
 
-pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Embed>;
+pub type Expr<VarLabel, Note, Embed> =
+    ExprF<SubExpr<VarLabel, Note, Embed>, VarLabel, Embed>;
 
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
 // smart pointers.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ExprF<SubExpr, Label, Embed> {
+pub enum ExprF<SubExpr, VarLabel, Embed> {
     Const(Const),
     ///  `x`
     ///  `x@n`
-    Var(V<Label>),
+    Var(Var<VarLabel>),
     ///  `λ(x : A) -> b`
-    Lam(Label, SubExpr, SubExpr),
+    Lam(VarLabel, SubExpr, SubExpr),
     ///  `A -> B`
     ///  `∀(x : A) -> B`
-    Pi(Label, SubExpr, SubExpr),
+    Pi(VarLabel, SubExpr, SubExpr),
     ///  `f a`
     App(SubExpr, SubExpr),
     ///  `let x     = r in e`
     ///  `let x : t = r in e`
-    Let(Label, Option<SubExpr>, SubExpr, SubExpr),
+    Let(VarLabel, Option<SubExpr>, SubExpr, SubExpr),
     ///  `x : t`
     Annot(SubExpr, SubExpr),
     /// Built-in values
@@ -235,11 +231,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_under_binder: impl FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> Result<ExprF<SE2, L2, E2>, Err> {
         self.visit(visitor::TraverseRefWithBindersVisitor {
             visit_subexpr,
             visit_under_binder,
@@ -253,11 +245,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> Result<ExprF<SE2, L2, E2>, Err> {
         self.visit(visitor::TraverseRefVisitor {
             visit_subexpr,
             visit_embed,
@@ -271,11 +259,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_under_binder: impl FnMut(&'a L, &'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> ExprF<SE2, L2, E2> {
         trivial_result(self.traverse_ref_with_special_handling_of_binders(
             |x| Ok(map_subexpr(x)),
             |l, x| Ok(map_under_binder(l, x)),
@@ -289,11 +273,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> ExprF<SE2, L2, E2> {
         trivial_result(self.traverse_ref(
             |x| Ok(map_subexpr(x)),
             |x| Ok(map_embed(x)),
@@ -306,7 +286,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
     ) -> Result<ExprF<SE2, L, E>, Err>
     where
-        L: Ord + Clone,
+        L: Clone,
         E: Clone,
     {
         self.traverse_ref(
@@ -321,26 +301,31 @@ impl<SE, L, E> ExprF<SE, L, E> {
         map_subexpr: impl Fn(&'a SE) -> SE2,
     ) -> ExprF<SE2, L, E>
     where
-        L: Ord + Clone,
+        L: Clone,
         E: Clone,
     {
         self.map_ref(map_subexpr, E::clone, L::clone)
     }
 }
 
-impl<N, E> Expr<N, E> {
+impl<L, N, E> Expr<L, N, E> {
     fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<Expr<N, E2>, Err>
+    ) -> Result<Expr<L, N, E2>, Err>
     where
+        L: Clone,
         N: Clone,
     {
         self.visit(&mut visitor::TraverseEmbedVisitor(visit_embed))
     }
 
-    fn map_embed<E2>(&self, mut map_embed: impl FnMut(&E) -> E2) -> Expr<N, E2>
+    fn map_embed<E2>(
+        &self,
+        mut map_embed: impl FnMut(&E) -> E2,
+    ) -> Expr<L, N, E2>
     where
+        L: Clone,
         N: Clone,
     {
         trivial_result(self.traverse_embed(|x| Ok(map_embed(x))))
@@ -348,52 +333,52 @@ impl<N, E> Expr<N, E> {
 
     pub fn squash_embed<E2>(
         &self,
-        f: impl FnMut(&E) -> SubExpr<N, E2>,
-    ) -> SubExpr<N, E2>
+        f: impl FnMut(&E) -> SubExpr<L, N, E2>,
+    ) -> SubExpr<L, N, E2>
     where
+        L: Clone,
         N: Clone,
     {
         trivial_result(self.visit(&mut visitor::SquashEmbedVisitor(f)))
     }
 }
 
-impl<E: Clone> Expr<X, E> {
-    pub fn note_absurd<N>(&self) -> Expr<N, E> {
+impl<L: Clone, E: Clone> Expr<L, X, E> {
+    pub fn note_absurd<N>(&self) -> Expr<L, N, E> {
         self.visit(&mut visitor::NoteAbsurdVisitor)
     }
 }
 
-impl<N: Clone> Expr<N, X> {
-    pub fn embed_absurd<E>(&self) -> Expr<N, E> {
+impl<L: Clone, N: Clone> Expr<L, N, X> {
+    pub fn embed_absurd<E>(&self) -> Expr<L, N, E> {
         self.visit(&mut visitor::EmbedAbsurdVisitor)
     }
 }
 
-impl<N, E> SubExpr<N, E> {
-    pub fn as_ref(&self) -> &Expr<N, E> {
+impl<V, N, E> SubExpr<V, N, E> {
+    pub fn as_ref(&self) -> &Expr<V, N, E> {
         &self.0.as_ref().0
     }
 
-    pub fn new(x: Expr<N, E>, n: N) -> Self {
+    pub fn new(x: Expr<V, N, E>, n: N) -> Self {
         SubExpr(Rc::new((x, Some(n))))
     }
 
-    pub fn from_expr_no_note(x: Expr<N, E>) -> Self {
+    pub fn from_expr_no_note(x: Expr<V, N, E>) -> Self {
         SubExpr(Rc::new((x, None)))
     }
 
-    pub fn unnote(&self) -> SubExpr<X, E>
+    pub fn unnote(&self) -> SubExpr<V, X, E>
     where
+        V: Clone,
         E: Clone,
     {
         SubExpr::from_expr_no_note(
             self.as_ref().visit(&mut visitor::UnNoteVisitor),
         )
     }
-}
 
-impl<N: Clone, E> SubExpr<N, E> {
-    pub fn rewrap<E2>(&self, x: Expr<N, E2>) -> SubExpr<N, E2>
+    pub fn rewrap<E2>(&self, x: Expr<V, N, E2>) -> SubExpr<V, N, E2>
     where
         N: Clone,
     {
@@ -403,8 +388,9 @@ impl<N: Clone, E> SubExpr<N, E> {
     pub fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<SubExpr<N, E2>, Err>
+    ) -> Result<SubExpr<V, N, E2>, Err>
     where
+        V: Clone,
         N: Clone,
     {
         Ok(self.rewrap(self.as_ref().traverse_embed(visit_embed)?))
@@ -413,8 +399,9 @@ impl<N: Clone, E> SubExpr<N, E> {
     pub fn map_embed<E2>(
         &self,
         map_embed: impl FnMut(&E) -> E2,
-    ) -> SubExpr<N, E2>
+    ) -> SubExpr<V, N, E2>
     where
+        V: Clone,
         N: Clone,
     {
         self.rewrap(self.as_ref().map_embed(map_embed))
@@ -423,8 +410,12 @@ impl<N: Clone, E> SubExpr<N, E> {
     pub fn map_subexprs_with_special_handling_of_binders<'a>(
         &'a self,
         map_expr: impl FnMut(&'a Self) -> Self,
-        map_under_binder: impl FnMut(&'a Label, &'a Self) -> Self,
-    ) -> Self {
+        map_under_binder: impl FnMut(&'a V, &'a Self) -> Self,
+    ) -> Self
+    where
+        V: Clone,
+        N: Clone,
+    {
         match self.as_ref() {
             ExprF::Embed(_) => SubExpr::clone(self),
             // This calls ExprF::map_ref
@@ -432,7 +423,7 @@ impl<N: Clone, E> SubExpr<N, E> {
                 map_expr,
                 map_under_binder,
                 |_| unreachable!(),
-                Label::clone,
+                V::clone,
             )),
         }
     }
@@ -441,26 +432,34 @@ impl<N: Clone, E> SubExpr<N, E> {
     /// capture by shifting variable indices
     /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
     /// for details
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    pub fn shift(&self, delta: isize, var: &Var<V>) -> Self
+    where
+        V: Clone + PartialEq,
+        N: Clone,
+    {
         match self.as_ref() {
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.shift(delta, var),
-                |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
+                |x: &V, e| e.shift(delta, &var.shift(1, &Var::new(x.clone()))),
             ),
         }
     }
 
-    pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
+    pub fn subst_shift(&self, var: &Var<V>, val: &Self) -> Self
+    where
+        V: Clone + PartialEq,
+        N: Clone,
+    {
         match self.as_ref() {
             ExprF::Var(v) if v == var => val.clone(),
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.subst_shift(var, val),
-                |x: &Label, e| {
+                |x: &V, e| {
                     e.subst_shift(
-                        &var.shift(1, &x.into()),
-                        &val.shift(1, &x.into()),
+                        &var.shift(1, &Var::new(x.clone())),
+                        &val.shift(1, &Var::new(x.clone())),
                     )
                 },
             ),
@@ -468,26 +467,26 @@ impl<N: Clone, E> SubExpr<N, E> {
     }
 }
 
-impl<N: Clone> SubExpr<N, X> {
-    pub fn embed_absurd<T>(&self) -> SubExpr<N, T> {
+impl<L: Clone, N: Clone> SubExpr<L, N, X> {
+    pub fn embed_absurd<T>(&self) -> SubExpr<L, N, T> {
         self.rewrap(self.as_ref().embed_absurd())
     }
 }
 
-impl<E: Clone> SubExpr<X, E> {
-    pub fn note_absurd<N>(&self) -> SubExpr<N, E> {
+impl<L: Clone, E: Clone> SubExpr<L, X, E> {
+    pub fn note_absurd<N>(&self) -> SubExpr<L, N, E> {
         SubExpr::from_expr_no_note(self.as_ref().note_absurd())
     }
 }
 
-impl<N, E> Clone for SubExpr<N, E> {
+impl<L, N, E> Clone for SubExpr<L, N, E> {
     fn clone(&self) -> Self {
         SubExpr(Rc::clone(&self.0))
     }
 }
 
 // Should probably rename this
-pub fn rc<E>(x: Expr<X, E>) -> SubExpr<X, E> {
+pub fn rc<L, E>(x: Expr<L, X, E>) -> SubExpr<L, X, E> {
     SubExpr::from_expr_no_note(x)
 }
 
@@ -501,18 +500,35 @@ fn add_ui(u: usize, i: isize) -> usize {
     }
 }
 
-impl<Label: PartialEq + Clone> V<Label> {
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        let V(x, n) = var;
-        let V(y, m) = self;
+impl<L> Var<L> {
+    fn new(x: L) -> Self {
+        Var(x, 0)
+    }
+}
+impl<L: PartialEq + Clone> Var<L> {
+    pub fn shift(&self, delta: isize, var: &Var<L>) -> Self {
+        let Var(x, n) = var;
+        let Var(y, m) = self;
         if x == y && n <= m {
-            V(y.clone(), add_ui(*m, delta))
+            Var(y.clone(), add_ui(*m, delta))
         } else {
-            V(y.clone(), *m)
+            Var(y.clone(), *m)
         }
     }
 }
 
+// This is only for the specific `Label` type, not generic
+impl From<Label> for Var<Label> {
+    fn from(x: Label) -> Var<Label> {
+        Var(x, 0)
+    }
+}
+impl<'a> From<&'a Label> for Var<Label> {
+    fn from(x: &'a Label) -> Var<Label> {
+        Var(x.clone(), 0)
+    }
+}
+
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
@@ -520,9 +536,9 @@ impl<Label: PartialEq + Clone> V<Label> {
 ///
 pub fn shift<N, E>(
     delta: isize,
-    var: &V<Label>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+    var: &Var<Label>,
+    in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
 where
     N: Clone,
 {
@@ -531,8 +547,8 @@ where
 
 pub fn shift0_multiple<N, E>(
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+    in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
 where
     N: Clone,
 {
@@ -542,16 +558,15 @@ where
 fn shift0_multiple_inner<N, E>(
     ctx: &Context<Label, ()>,
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+    in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
 where
     N: Clone,
 {
-    use crate::ExprF::*;
     match in_expr.as_ref() {
-        Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
+        ExprF::Var(Var(y, m)) if ctx.lookup(y, *m).is_none() => {
             let delta = deltas.get(y).unwrap_or(&0);
-            in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
+            in_expr.rewrap(ExprF::Var(Var(y.clone(), add_ui(*m, *delta))))
         }
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| shift0_multiple_inner(ctx, deltas, e),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 83ccc1e..bdef553 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -8,7 +8,13 @@ use std::rc::Rc;
 
 use dhall_generated_parser::{DhallParser, Rule};
 
-use crate::ExprF::*;
+use crate::ExprF::{
+    Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit, Embed,
+    EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit,
+    OldOptionalLit, Pi, Projection, RecordLit, RecordType, SomeLit, TextLit,
+    UnionLit, UnionType,
+};
+
 use crate::*;
 
 // This file consumes the parse tree generated by pest and turns it into
@@ -16,10 +22,10 @@ use crate::*;
 // their own crate because they are quite general and useful. For now they
 // are here and hopefully you can figure out how they work.
 
-type ParsedExpr = Expr<Span, Import>;
-type ParsedSubExpr = SubExpr<Span, Import>;
-type ParsedText = InterpolatedText<SubExpr<Span, Import>>;
-type ParsedTextContents = InterpolatedTextContents<SubExpr<Span, Import>>;
+type ParsedExpr = Expr<Label, Span, Import>;
+type ParsedSubExpr = SubExpr<Label, Span, Import>;
+type ParsedText = InterpolatedText<ParsedSubExpr>;
+type ParsedTextContents = InterpolatedTextContents<ParsedSubExpr>;
 
 pub type ParseError = pest::error::Error<Rule>;
 
@@ -504,17 +510,17 @@ make_parser! {
 
     rule!(identifier<ParsedSubExpr> as expression; span; children!(
         [variable(v)] => {
-            spanned(span, Var(v))
+            spanned(span, ExprF::Var(v))
         },
         [builtin(e)] => e,
     ));
 
-    rule!(variable<V<Label>>; children!(
+    rule!(variable<Var<Label>>; children!(
         [label(l), natural_literal(idx)] => {
-            V(l, idx)
+            Var(l, idx)
         },
         [label(l)] => {
-            V(l, 0)
+            Var(l, 0)
         },
     ));
 
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index e3b180b..9cc1b46 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,7 +3,9 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
+impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
+    for ExprF<SE, L, E>
+{
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
         match self {
@@ -13,9 +15,10 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            Pi(a, b, c) if &String::from(a) == "_" => {
-                write!(f, "{} → {}", b, c)?;
-            }
+            // TODO: arrow type
+            // Pi(a, b, c) if &String::from(a) == "_" => {
+            //     write!(f, "{} → {}", b, c)?;
+            // }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -124,21 +127,25 @@ enum PrintPhase {
 // Wraps an Expr with a phase, so that phase selsction can be done
 // separate from the actual printing
 #[derive(Clone)]
-struct PhasedExpr<'a, S, A>(&'a SubExpr<S, A>, PrintPhase);
+struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
 
-impl<'a, S: Clone, A: Display + Clone> Display for PhasedExpr<'a, S, A> {
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for PhasedExpr<'a, L, S, A>
+{
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, S: Clone, A: Display + Clone> PhasedExpr<'a, S, A> {
-    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, S, A> {
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
+    PhasedExpr<'a, L, S, A>
+{
+    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<S: Clone, A: Display + Clone> Expr<S, A> {
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -172,11 +179,12 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                if &String::from(&a) == "_" {
-                    Pi(a, b.phase(Operator), c)
-                } else {
-                    Pi(a, b, c)
-                }
+                // TODO: arrow type
+                // if &String::from(&a) == "_" {
+                //     Pi(a, b.phase(Operator), c)
+                // } else {
+                Pi(a, b, c)
+                // }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -212,7 +220,9 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
     }
 }
 
-impl<S: Clone, A: Display + Clone> Display for SubExpr<S, A> {
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for SubExpr<L, S, A>
+{
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
     }
@@ -474,9 +484,9 @@ impl Display for Scheme {
     }
 }
 
-impl<Label: Display> Display for V<Label> {
+impl<Label: Display> Display for Var<Label> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        let V(x, n) = self;
+        let Var(x, n) = self;
         x.fmt(f)?;
         if *n != 0 {
             write!(f, "@{}", n)?;
diff --git a/dhall_syntax/src/visitor.rs b/dhall_syntax/src/visitor.rs
index 7fdf217..a8e5a8c 100644
--- a/dhall_syntax/src/visitor.rs
+++ b/dhall_syntax/src/visitor.rs
@@ -48,8 +48,6 @@ pub trait ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>: Sized {
 impl<'a, T, Ret, SE1, L1, E1>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, Result<Ret, T::Error>> for T
 where
-    L1: Ord,
-    T::L2: Ord,
     T: ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> Result<Ret, T::Error> {
@@ -69,31 +67,27 @@ where
             })
         }
         fn btmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<L, SE>,
+            x: &'a BTreeMap<Label, SE>,
             mut v: V,
-        ) -> Result<BTreeMap<V::L2, V::SE2>, V::Error>
+        ) -> Result<BTreeMap<Label, V::SE2>, V::Error>
         where
-            L: Ord,
-            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
-                .map(|(k, x)| Ok((v.visit_label(k)?, v.visit_subexpr(x)?)))
+                .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
                 .collect()
         }
         fn btoptmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<L, Option<SE>>,
+            x: &'a BTreeMap<Label, Option<SE>>,
             mut v: V,
-        ) -> Result<BTreeMap<V::L2, Option<V::SE2>>, V::Error>
+        ) -> Result<BTreeMap<Label, Option<V::SE2>>, V::Error>
         where
-            L: Ord,
-            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
                 .map(|(k, x)| {
                     Ok((
-                        v.visit_label(k)?,
+                        k.clone(),
                         match x {
                             Some(x) => Some(v.visit_subexpr(x)?),
                             None => None,
@@ -104,9 +98,14 @@ where
         }
 
         let mut v = self;
-        use crate::ExprF::*;
+        use crate::ExprF::{
+            Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit,
+            Embed, EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit,
+            NaturalLit, OldOptionalLit, Pi, Projection, RecordLit, RecordType,
+            SomeLit, TextLit, UnionLit, UnionType,
+        };
         T::visit_resulting_exprf(match input {
-            Var(V(l, n)) => Var(V(v.visit_label(l)?, *n)),
+            ExprF::Var(Var(l, n)) => ExprF::Var(Var(v.visit_label(l)?, *n)),
             Lam(l, t, e) => {
                 let t = v.visit_subexpr(t)?;
                 let (l, e) = v.visit_binder(l, e)?;
@@ -150,20 +149,16 @@ where
             RecordType(kts) => RecordType(btmap(kts, v)?),
             RecordLit(kvs) => RecordLit(btmap(kvs, v)?),
             UnionType(kts) => UnionType(btoptmap(kts, v)?),
-            UnionLit(k, x, kts) => UnionLit(
-                v.visit_label(k)?,
-                v.visit_subexpr(x)?,
-                btoptmap(kts, v)?,
-            ),
+            UnionLit(l, x, kts) => {
+                UnionLit(l.clone(), v.visit_subexpr(x)?, btoptmap(kts, v)?)
+            }
             Merge(x, y, t) => Merge(
                 v.visit_subexpr(x)?,
                 v.visit_subexpr(y)?,
                 opt(t, |e| v.visit_subexpr(e))?,
             ),
-            Field(e, l) => Field(v.visit_subexpr(e)?, v.visit_label(l)?),
-            Projection(e, ls) => {
-                Projection(v.visit_subexpr(e)?, vec(ls, |l| v.visit_label(l))?)
-            }
+            Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
+            Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
             Embed(a) => return v.visit_embed_squash(a),
         })
     }
@@ -314,8 +309,6 @@ where
 impl<'a, T, SE1, SE2, L1, L2, E1, E2>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, ExprF<SE2, L2, E2>> for T
 where
-    L1: Ord,
-    L2: Ord,
     T: ExprFInFallibleVisitor<'a, SE1, SE2, L1, L2, E1, E2>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> ExprF<SE2, L2, E2> {
@@ -337,8 +330,6 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
-    L: Ord,
-    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F2: FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
     F4: FnOnce(&'a E) -> Result<E2, Err>,
@@ -377,8 +368,6 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
-    L: Ord,
-    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F3: FnOnce(&'a E) -> Result<E2, Err>,
     F4: FnMut(&'a L) -> Result<L2, Err>,
@@ -398,10 +387,11 @@ where
 
 pub struct TraverseEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, N, E, E2, Err, F1>
-    ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, Label, Label, E, E2>
+impl<'a, 'b, L, N, E, E2, Err, F1>
+    ExprFFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, N, E2>, L, L, E, E2>
     for &'b mut TraverseEmbedVisitor<F1>
 where
+    L: Clone + 'a,
     N: Clone + 'a,
     F1: FnMut(&E) -> Result<E2, Err>,
 {
@@ -409,50 +399,48 @@ where
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<N, E>,
-    ) -> Result<SubExpr<N, E2>, Self::Error> {
+        subexpr: &'a SubExpr<L, N, E>,
+    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
         Ok(subexpr.rewrap(subexpr.as_ref().visit(&mut **self)?))
     }
     fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> {
         (self.0)(embed)
     }
-    fn visit_label(&mut self, label: &'a Label) -> Result<Label, Self::Error> {
-        Ok(Label::clone(label))
+    fn visit_label(&mut self, label: &'a L) -> Result<L, Self::Error> {
+        Ok(L::clone(label))
     }
 }
 
 pub struct SquashEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, N, E1, E2, F1>
-    ExprFVeryGenericVisitor<'a, SubExpr<N, E2>, SubExpr<N, E1>, Label, E1>
+impl<'a, 'b, L, N, E1, E2, F1>
+    ExprFVeryGenericVisitor<'a, SubExpr<L, N, E2>, SubExpr<L, N, E1>, L, E1>
     for &'b mut SquashEmbedVisitor<F1>
 where
+    L: Clone + 'a,
     N: Clone + 'a,
-    F1: FnMut(&E1) -> SubExpr<N, E2>,
+    F1: FnMut(&E1) -> SubExpr<L, N, E2>,
 {
     type Error = X;
-    type SE2 = SubExpr<N, E2>;
-    type L2 = Label;
+    type SE2 = SubExpr<L, N, E2>;
+    type L2 = L;
     type E2 = E2;
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<N, E1>,
+        subexpr: &'a SubExpr<L, N, E1>,
     ) -> Result<Self::SE2, Self::Error> {
         Ok(subexpr.as_ref().visit(&mut **self)?)
     }
 
-    fn visit_label(
-        &mut self,
-        label: &'a Label,
-    ) -> Result<Self::L2, Self::Error> {
-        Ok(Label::clone(label))
+    fn visit_label(&mut self, label: &'a L) -> Result<Self::L2, Self::Error> {
+        Ok(L::clone(label))
     }
 
     fn visit_binder(
         mut self,
-        label: &'a Label,
-        subexpr: &'a SubExpr<N, E1>,
+        label: &'a L,
+        subexpr: &'a SubExpr<L, N, E1>,
     ) -> Result<(Self::L2, Self::SE2), Self::Error> {
         Ok((self.visit_label(label)?, self.visit_subexpr(subexpr)?))
     }
@@ -460,7 +448,7 @@ where
     fn visit_embed_squash(
         self,
         embed: &'a E1,
-    ) -> Result<SubExpr<N, E2>, Self::Error> {
+    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
         Ok((self.0)(embed))
     }
 
@@ -468,7 +456,7 @@ where
     // Useful to change the result type, and/or avoid some loss of info
     fn visit_resulting_exprf(
         result: ExprF<Self::SE2, Self::L2, Self::E2>,
-    ) -> Result<SubExpr<N, E2>, Self::Error> {
+    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
         // TODO: don't lose note
         Ok(SubExpr::from_expr_no_note(result))
     }
@@ -476,57 +464,69 @@ where
 
 pub struct UnNoteVisitor;
 
-impl<'a, 'b, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<N, E>, SubExpr<X, E>, Label, Label, E, E>
+impl<'a, 'b, L, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, X, E>, L, L, E, E>
     for &'b mut UnNoteVisitor
 where
+    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, E>) -> SubExpr<X, E> {
+    fn visit_subexpr(
+        &mut self,
+        subexpr: &'a SubExpr<L, N, E>,
+    ) -> SubExpr<L, X, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a Label) -> Label {
-        Label::clone(label)
+    fn visit_label(&mut self, label: &'a L) -> L {
+        L::clone(label)
     }
 }
 
 pub struct NoteAbsurdVisitor;
 
-impl<'a, 'b, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<X, E>, SubExpr<N, E>, Label, Label, E, E>
+impl<'a, 'b, L, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<L, X, E>, SubExpr<L, N, E>, L, L, E, E>
     for &'b mut NoteAbsurdVisitor
 where
+    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<X, E>) -> SubExpr<N, E> {
+    fn visit_subexpr(
+        &mut self,
+        subexpr: &'a SubExpr<L, X, E>,
+    ) -> SubExpr<L, N, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a Label) -> Label {
-        Label::clone(label)
+    fn visit_label(&mut self, label: &'a L) -> L {
+        L::clone(label)
     }
 }
 
 pub struct EmbedAbsurdVisitor;
 
-impl<'a, 'b, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<N, X>, SubExpr<N, E>, Label, Label, X, E>
+impl<'a, 'b, L, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<L, N, X>, SubExpr<L, N, E>, L, L, X, E>
     for &'b mut EmbedAbsurdVisitor
 where
+    L: Clone + 'a,
     N: Clone + 'a,
 {
-    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, X>) -> SubExpr<N, E> {
+    fn visit_subexpr(
+        &mut self,
+        subexpr: &'a SubExpr<L, N, X>,
+    ) -> SubExpr<L, N, E> {
         subexpr.rewrap(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a X) -> E {
         match *embed {}
     }
-    fn visit_label(&mut self, label: &'a Label) -> Label {
-        Label::clone(label)
+    fn visit_label(&mut self, label: &'a L) -> L {
+        L::clone(label)
     }
 }
-- 
cgit v1.2.3


From 153cf8dab3b80aba30ac3adfd44e4be251494ea2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 18:37:15 +0200
Subject: Recover arrow type detection

---
 dhall_syntax/src/core.rs    | 15 ++++++++++++-
 dhall_syntax/src/printer.rs | 51 +++++++++++++++++++++++++++++----------------
 2 files changed, 47 insertions(+), 19 deletions(-)

diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index c8a2425..389f037 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,7 +60,7 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Var<Label>(pub Label, pub usize);
+pub struct Var<VarLabel>(pub VarLabel, pub usize);
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -529,6 +529,19 @@ impl<'a> From<&'a Label> for Var<Label> {
     }
 }
 
+/// Trait for things that capture a label used for variables.
+/// Allows normalization to be generic in whether to alpha-normalize or not.
+pub trait VarLabel: std::fmt::Display + Clone {
+    /// Is `self` the default variable (i.e. "_") ?
+    fn is_underscore_var(&self) -> bool;
+}
+
+impl VarLabel for Label {
+    fn is_underscore_var(&self) -> bool {
+        &String::from(self) == "_"
+    }
+}
+
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 9cc1b46..6ebd537 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,8 +3,11 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
-    for ExprF<SE, L, E>
+impl<SE, L, E> Display for ExprF<SE, L, E>
+where
+    SE: Display + Clone,
+    L: VarLabel,
+    E: Display,
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
@@ -15,10 +18,9 @@ impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            // TODO: arrow type
-            // Pi(a, b, c) if &String::from(a) == "_" => {
-            //     write!(f, "{} → {}", b, c)?;
-            // }
+            Pi(a, b, c) if a.is_underscore_var() => {
+                write!(f, "{} → {}", b, c)?;
+            }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -129,23 +131,34 @@ enum PrintPhase {
 #[derive(Clone)]
 struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for PhasedExpr<'a, L, S, A>
+impl<'a, L, S, A> Display for PhasedExpr<'a, L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
-    PhasedExpr<'a, L, S, A>
+impl<'a, L, S, A> PhasedExpr<'a, L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
 {
     fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
+impl<L, S, A> Expr<L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
+{
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -179,12 +192,11 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                // TODO: arrow type
-                // if &String::from(&a) == "_" {
-                //     Pi(a, b.phase(Operator), c)
-                // } else {
+                if a.is_underscore_var() {
+                    Pi(a, b.phase(Operator), c)
+                } else {
                 Pi(a, b, c)
-                // }
+                }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -220,8 +232,11 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for SubExpr<L, S, A>
+impl<L, S, A> Display for SubExpr<L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
-- 
cgit v1.2.3


From 6ad7a2000bf32b96be731cd51da5b841976dae12 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 18:41:21 +0200
Subject: Revert "Recover arrow type detection"

This reverts commit 153cf8dab3b80aba30ac3adfd44e4be251494ea2.
---
 dhall_syntax/src/core.rs    | 15 +------------
 dhall_syntax/src/printer.rs | 51 ++++++++++++++++-----------------------------
 2 files changed, 19 insertions(+), 47 deletions(-)

diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index 389f037..c8a2425 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,7 +60,7 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Var<VarLabel>(pub VarLabel, pub usize);
+pub struct Var<Label>(pub Label, pub usize);
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -529,19 +529,6 @@ impl<'a> From<&'a Label> for Var<Label> {
     }
 }
 
-/// Trait for things that capture a label used for variables.
-/// Allows normalization to be generic in whether to alpha-normalize or not.
-pub trait VarLabel: std::fmt::Display + Clone {
-    /// Is `self` the default variable (i.e. "_") ?
-    fn is_underscore_var(&self) -> bool;
-}
-
-impl VarLabel for Label {
-    fn is_underscore_var(&self) -> bool {
-        &String::from(self) == "_"
-    }
-}
-
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 6ebd537..9cc1b46 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,11 +3,8 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE, L, E> Display for ExprF<SE, L, E>
-where
-    SE: Display + Clone,
-    L: VarLabel,
-    E: Display,
+impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
+    for ExprF<SE, L, E>
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
@@ -18,9 +15,10 @@ where
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            Pi(a, b, c) if a.is_underscore_var() => {
-                write!(f, "{} → {}", b, c)?;
-            }
+            // TODO: arrow type
+            // Pi(a, b, c) if &String::from(a) == "_" => {
+            //     write!(f, "{} → {}", b, c)?;
+            // }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -131,34 +129,23 @@ enum PrintPhase {
 #[derive(Clone)]
 struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
 
-impl<'a, L, S, A> Display for PhasedExpr<'a, L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for PhasedExpr<'a, L, S, A>
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, L, S, A> PhasedExpr<'a, L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
+    PhasedExpr<'a, L, S, A>
 {
     fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<L, S, A> Expr<L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
-{
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -192,11 +179,12 @@ where
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                if a.is_underscore_var() {
-                    Pi(a, b.phase(Operator), c)
-                } else {
+                // TODO: arrow type
+                // if &String::from(&a) == "_" {
+                //     Pi(a, b.phase(Operator), c)
+                // } else {
                 Pi(a, b, c)
-                }
+                // }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -232,11 +220,8 @@ where
     }
 }
 
-impl<L, S, A> Display for SubExpr<L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for SubExpr<L, S, A>
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
-- 
cgit v1.2.3


From ab100be616932dab22a5309df86107b66e93db37 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 18:41:22 +0200
Subject: Revert "Make SubExpr generic in the variable labels type"

This reverts commit 4c159640e5ee77ffa48b85a5bffa56350cf933ef.
---
 dhall/src/binary.rs             |  22 ++---
 dhall/src/expr.rs               |  32 +++----
 dhall/src/normalize.rs          |  48 +++++-----
 dhall/src/serde.rs              |   2 +-
 dhall/src/traits/static_type.rs |  14 +--
 dhall/src/typecheck.rs          |  65 ++++++-------
 dhall/tests/traits.rs           |   4 +-
 dhall_proc_macros/src/quote.rs  |  62 ++++++------
 dhall_syntax/src/core.rs        | 207 +++++++++++++++++++---------------------
 dhall_syntax/src/parser.rs      |  24 ++---
 dhall_syntax/src/printer.rs     |  44 ++++-----
 dhall_syntax/src/visitor.rs     | 130 ++++++++++++-------------
 12 files changed, 303 insertions(+), 351 deletions(-)

diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 0d9f28a..9c31d4c 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -2,7 +2,7 @@ use dhall_syntax::*;
 use itertools::*;
 use serde_cbor::value::value as cbor;
 
-type ParsedExpr = SubExpr<Label, X, Import>;
+type ParsedExpr = SubExpr<X, Import>;
 
 #[derive(Debug)]
 pub enum DecodeError {
@@ -18,32 +18,28 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
 }
 
 fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
-    use cbor::Value::{Array, Bool, Null, Object, String, F64, I64, U64};
+    use cbor::Value::*;
     use dhall_syntax::{BinOp, Builtin, Const};
-    use ExprF::{
-        Annot, App, BoolIf, BoolLit, DoubleLit, Embed, EmptyListLit, Field,
-        IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit, OldOptionalLit, Pi,
-        RecordLit, RecordType, SomeLit, TextLit, UnionLit, UnionType,
-    };
+    use ExprF::*;
     Ok(rc(match data {
         String(s) => match Builtin::parse(s) {
             Some(b) => ExprF::Builtin(b),
             None => match s.as_str() {
                 "True" => BoolLit(true),
                 "False" => BoolLit(false),
-                "Type" => ExprF::Const(Const::Type),
-                "Kind" => ExprF::Const(Const::Kind),
-                "Sort" => ExprF::Const(Const::Sort),
+                "Type" => Const(Const::Type),
+                "Kind" => Const(Const::Kind),
+                "Sort" => Const(Const::Sort),
                 _ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?,
             },
         },
-        U64(n) => ExprF::Var(Var(Label::from("_"), *n as usize)),
+        U64(n) => Var(V(Label::from("_"), *n as usize)),
         F64(x) => DoubleLit((*x).into()),
         Bool(b) => BoolLit(*b),
         Array(vec) => match vec.as_slice() {
             [String(l), U64(n)] => {
                 let l = Label::from(l.as_str());
-                ExprF::Var(Var(l, *n as usize))
+                Var(V(l, *n as usize))
             }
             [U64(0), f, args..] => {
                 let mut f = cbor_value_to_dhall(&f)?;
@@ -96,7 +92,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
                         Err(DecodeError::WrongFormatError("binop".to_owned()))?
                     }
                 };
-                ExprF::BinOp(op, x, y)
+                BinOp(op, x, y)
             }
             [U64(4), t] => {
                 let t = cbor_value_to_dhall(&t)?;
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index efc3928..5bde68f 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -23,17 +23,15 @@ macro_rules! derive_other_traits {
     };
 }
 
-type OutputSubExpr = SubExpr<Label, X, X>;
-
 #[derive(Debug, Clone)]
 pub(crate) struct Parsed(
-    pub(crate) SubExpr<Label, Span, Import>,
+    pub(crate) SubExpr<Span, Import>,
     pub(crate) ImportRoot,
 );
 derive_other_traits!(Parsed);
 
 #[derive(Debug, Clone)]
-pub(crate) struct Resolved(pub(crate) SubExpr<Label, Span, Normalized>);
+pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>);
 derive_other_traits!(Resolved);
 
 pub(crate) use self::typed::TypedInternal;
@@ -59,12 +57,12 @@ impl std::fmt::Display for Normalized {
 }
 
 mod typed {
-    use super::{OutputSubExpr, Type, Typed};
+    use super::{Type, Typed};
     use crate::normalize::{Thunk, Value};
     use crate::typecheck::{
         TypeError, TypeInternal, TypeMessage, TypecheckContext,
     };
-    use dhall_syntax::{Const, Label, Var};
+    use dhall_syntax::{Const, Label, SubExpr, V, X};
     use std::borrow::Cow;
 
     #[derive(Debug, Clone)]
@@ -92,7 +90,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn to_expr(&self) -> OutputSubExpr {
+        pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
             self.to_value().normalize_to_expr()
         }
 
@@ -131,7 +129,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.shift(delta, var),
@@ -141,11 +139,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn subst_shift(
-            &self,
-            var: &Var<Label>,
-            val: &Typed,
-        ) -> Self {
+        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.subst_shift(var, val),
@@ -164,7 +158,7 @@ mod typed {
 ///
 /// For a more general notion of "type", see [Type].
 #[derive(Debug, Clone)]
-pub struct SimpleType(pub(crate) OutputSubExpr);
+pub struct SimpleType(pub(crate) SubExpr<X, X>);
 derive_other_traits!(SimpleType);
 
 pub(crate) use crate::typecheck::TypeInternal;
@@ -184,16 +178,16 @@ impl std::fmt::Display for Type {
 
 // Exposed for the macros
 #[doc(hidden)]
-impl From<SimpleType> for OutputSubExpr {
-    fn from(x: SimpleType) -> OutputSubExpr {
+impl From<SimpleType> for SubExpr<X, X> {
+    fn from(x: SimpleType) -> SubExpr<X, X> {
         x.0
     }
 }
 
 // Exposed for the macros
 #[doc(hidden)]
-impl From<OutputSubExpr> for SimpleType {
-    fn from(x: OutputSubExpr) -> SimpleType {
+impl From<SubExpr<X, X>> for SimpleType {
+    fn from(x: SubExpr<X, X>) -> SimpleType {
         SimpleType(x)
     }
 }
@@ -210,7 +204,7 @@ impl Normalized {
     pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
         Normalized(TypedInternal::from_thunk_and_type(th, t))
     }
-    pub(crate) fn to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
         self.0.to_expr()
     }
     pub(crate) fn to_value(&self) -> Value {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3de12ee..8ae746d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,13 +6,13 @@ use dhall_proc_macros as dhall;
 use dhall_syntax::context::Context;
 use dhall_syntax::{
     rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
-    InterpolatedTextContents, Label, Natural, Span, SubExpr, Var, X,
+    InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X,
 };
 
 use crate::expr::{Normalized, Type, Typed, TypedInternal};
 
-type InputSubExpr = SubExpr<Label, Span, Normalized>;
-type OutputSubExpr = SubExpr<Label, X, X>;
+type InputSubExpr = SubExpr<Span, Normalized>;
+type OutputSubExpr = SubExpr<X, X>;
 
 impl Typed {
     /// Reduce an expression to its normal form, performing beta reduction
@@ -38,11 +38,11 @@ impl Typed {
         Normalized(internal)
     }
 
-    pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Typed(self.0.shift(delta, var))
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         Typed(self.0.subst_shift(var, val))
     }
 
@@ -58,11 +58,11 @@ impl Typed {
 #[derive(Debug, Clone)]
 enum EnvItem {
     Thunk(Thunk),
-    Skip(Var<Label>),
+    Skip(V<Label>),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use EnvItem::*;
         match self {
             Thunk(e) => Thunk(e.shift(delta, var)),
@@ -70,7 +70,7 @@ impl EnvItem {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
             EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -93,8 +93,8 @@ impl NormalizationContext {
                 .insert(x.clone(), EnvItem::Skip(x.into())),
         ))
     }
-    fn lookup(&self, var: &Var<Label>) -> Value {
-        let Var(x, n) = var;
+    fn lookup(&self, var: &V<Label>) -> Value {
+        let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Thunk(t)) => t.to_value(),
             Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
@@ -118,11 +118,11 @@ impl NormalizationContext {
         NormalizationContext(Rc::new(ctx))
     }
 
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
     }
 
-    fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         NormalizationContext(Rc::new(
             self.0.map(|_, e| e.subst_shift(var, val)),
         ))
@@ -144,7 +144,7 @@ pub(crate) enum Value {
     NaturalSuccClosure,
     Pi(Label, TypeThunk, TypeThunk),
 
-    Var(Var<Label>),
+    Var(V<Label>),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -403,7 +403,7 @@ impl Value {
         Value::AppliedBuiltin(b, vec![])
     }
 
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -500,7 +500,7 @@ impl Value {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -616,7 +616,7 @@ mod thunk {
         OutputSubExpr, Value,
     };
     use crate::expr::Typed;
-    use dhall_syntax::{Label, Var};
+    use dhall_syntax::{Label, V};
     use std::cell::{Ref, RefCell};
     use std::rc::Rc;
 
@@ -693,7 +693,7 @@ mod thunk {
             }
         }
 
-        fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+        fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -707,7 +707,7 @@ mod thunk {
             }
         }
 
-        fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+        fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -805,15 +805,11 @@ mod thunk {
             apply_any(self.clone(), th)
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             self.0.borrow().shift(delta, var).into_thunk()
         }
 
-        pub(crate) fn subst_shift(
-            &self,
-            var: &Var<Label>,
-            val: &Typed,
-        ) -> Self {
+        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
             self.0.borrow().subst_shift(var, val).into_thunk()
         }
     }
@@ -859,14 +855,14 @@ impl TypeThunk {
         self.normalize_nf().normalize_to_expr()
     }
 
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
             TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs
index bc76c49..96bc765 100644
--- a/dhall/src/serde.rs
+++ b/dhall/src/serde.rs
@@ -11,7 +11,7 @@ impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T {
     }
 }
 
-struct Deserializer<'a>(Cow<'a, SubExpr<Label, X, X>>);
+struct Deserializer<'a>(Cow<'a, SubExpr<X, X>>);
 
 impl serde::de::Error for Error {
     fn custom<T>(msg: T) -> Self
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index c3f323b..f90b8df 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -32,7 +32,7 @@ pub trait SimpleStaticType {
     fn get_simple_static_type() -> SimpleType;
 }
 
-fn mktype(x: SubExpr<Label, X, X>) -> SimpleType {
+fn mktype(x: SubExpr<X, X>) -> SimpleType {
     x.into()
 }
 
@@ -106,22 +106,22 @@ impl SimpleStaticType for String {
 
 impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) {
     fn get_simple_static_type() -> SimpleType {
-        let ta: SubExpr<_, _, _> = A::get_simple_static_type().into();
-        let tb: SubExpr<_, _, _> = B::get_simple_static_type().into();
+        let ta: SubExpr<_, _> = A::get_simple_static_type().into();
+        let tb: SubExpr<_, _> = B::get_simple_static_type().into();
         mktype(dhall::subexpr!({ _1: ta, _2: tb }))
     }
 }
 
 impl<T: SimpleStaticType> SimpleStaticType for Option<T> {
     fn get_simple_static_type() -> SimpleType {
-        let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
+        let t: SubExpr<_, _> = T::get_simple_static_type().into();
         mktype(dhall::subexpr!(Optional t))
     }
 }
 
 impl<T: SimpleStaticType> SimpleStaticType for Vec<T> {
     fn get_simple_static_type() -> SimpleType {
-        let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
+        let t: SubExpr<_, _> = T::get_simple_static_type().into();
         mktype(dhall::subexpr!(List t))
     }
 }
@@ -142,8 +142,8 @@ impl<T: SimpleStaticType, E: SimpleStaticType> SimpleStaticType
     for std::result::Result<T, E>
 {
     fn get_simple_static_type() -> SimpleType {
-        let tt: SubExpr<_, _, _> = T::get_simple_static_type().into();
-        let te: SubExpr<_, _, _> = E::get_simple_static_type().into();
+        let tt: SubExpr<_, _> = T::get_simple_static_type().into();
+        let te: SubExpr<_, _> = E::get_simple_static_type().into();
         mktype(dhall::subexpr!(< Ok: tt | Err: te>))
     }
 }
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 63041bb..8b7f011 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -14,16 +14,13 @@ use dhall_syntax::*;
 
 use self::TypeMessage::*;
 
-type InputSubExpr = SubExpr<Label, Span, Normalized>;
-type OutputSubExpr = SubExpr<Label, X, X>;
-
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError> {
         type_of(self.0)
     }
     pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
-        let expr = self.0;
-        let ty = ty.to_expr().embed_absurd().note_absurd();
+        let expr: SubExpr<_, _> = self.0;
+        let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd();
         type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
     }
     /// Pretends this expression has been typechecked. Use with care.
@@ -46,7 +43,7 @@ impl Typed {
 }
 
 impl Normalized {
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Normalized(self.0.shift(delta, var))
     }
     pub(crate) fn to_type(self) -> Type {
@@ -58,7 +55,7 @@ impl Type {
     pub(crate) fn to_normalized(&self) -> Normalized {
         self.0.to_normalized()
     }
-    pub(crate) fn to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
         self.0.to_expr()
     }
     pub(crate) fn to_value(&self) -> Value {
@@ -76,10 +73,10 @@ impl Type {
     fn internal_whnf(&self) -> Option<Value> {
         self.0.whnf()
     }
-    pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         Type(self.0.shift(delta, var))
     }
-    pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         Type(self.0.subst_shift(var, val))
     }
 
@@ -127,7 +124,7 @@ impl TypeInternal {
     fn to_normalized(&self) -> Normalized {
         self.to_typed().normalize()
     }
-    fn to_expr(&self) -> OutputSubExpr {
+    fn to_expr(&self) -> SubExpr<X, X> {
         self.to_normalized().to_expr()
     }
     fn to_value(&self) -> Value {
@@ -151,14 +148,14 @@ impl TypeInternal {
             _ => None,
         }
     }
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.shift(delta, var))),
             Const(c) => Const(*c),
         }
     }
-    fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -176,12 +173,12 @@ impl PartialEq for TypeInternal {
 
 #[derive(Debug, Clone)]
 pub(crate) enum EnvItem {
-    Type(Var<Label>, Type),
+    Type(V<Label>, Type),
     Value(Normalized),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use EnvItem::*;
         match self {
             Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
@@ -208,8 +205,8 @@ impl TypecheckContext {
     pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self {
         TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t)))
     }
-    pub(crate) fn lookup(&self, var: &Var<Label>) -> Option<Cow<'_, Type>> {
-        let Var(x, n) = var;
+    pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> {
+        let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)),
             Some(EnvItem::Value(t)) => Some(t.get_type()?),
@@ -241,12 +238,8 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
     }
 }
 
-fn match_vars(
-    vl: &Var<Label>,
-    vr: &Var<Label>,
-    ctx: &[(&Label, &Label)],
-) -> bool {
-    let (Var(xL, mut nL), Var(xR, mut nR)) = (vl, vr);
+fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
+    let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr);
     for &(xL2, xR2) in ctx {
         match (nL, nR) {
             (0, 0) if xL == xL2 && xR == xR2 => return true,
@@ -272,8 +265,8 @@ where
     use dhall_syntax::ExprF::*;
     fn go<'a, S, T>(
         ctx: &mut Vec<(&'a Label, &'a Label)>,
-        el: &'a SubExpr<Label, S, X>,
-        er: &'a SubExpr<Label, T, X>,
+        el: &'a SubExpr<S, X>,
+        er: &'a SubExpr<T, X>,
     ) -> bool
     where
         S: ::std::fmt::Debug,
@@ -357,9 +350,9 @@ fn type_of_const(c: Const) -> Result<Type, TypeError> {
     }
 }
 
-fn type_of_builtin(b: Builtin) -> InputSubExpr {
+fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
     use dhall_syntax::Builtin::*;
-    rc(match b {
+    match b {
         Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
         List | Optional => dhall::expr!(
             Type -> Type
@@ -439,8 +432,7 @@ fn type_of_builtin(b: Builtin) -> InputSubExpr {
         OptionalNone => dhall::expr!(
             forall (A: Type) -> Optional A
         ),
-    })
-    .note_absurd()
+    }
 }
 
 macro_rules! ensure_equal {
@@ -627,7 +619,10 @@ impl TypeIntermediate {
 
 /// Takes an expression that is meant to contain a Type
 /// and turn it into a type, typechecking it along the way.
-fn mktype(ctx: &TypecheckContext, e: InputSubExpr) -> Result<Type, TypeError> {
+fn mktype(
+    ctx: &TypecheckContext,
+    e: SubExpr<Span, Normalized>,
+) -> Result<Type, TypeError> {
     Ok(type_with(ctx, e)?.to_type())
 }
 
@@ -650,7 +645,7 @@ enum Ret {
 /// succeeded, or an error if type-checking failed
 fn type_with(
     ctx: &TypecheckContext,
-    e: InputSubExpr,
+    e: SubExpr<Span, Normalized>,
 ) -> Result<Typed, TypeError> {
     use dhall_syntax::ExprF::{
         Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
@@ -761,7 +756,7 @@ fn type_last_layer(
                 mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
             });
 
-            Ok(RetType(tb.subst_shift(&x.into(), &a)))
+            Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
         }
         Annot(x, t) => {
             let t = t.to_type();
@@ -942,7 +937,9 @@ fn type_last_layer(
             }
         }
         Const(c) => Ok(RetTyped(const_to_typed(c))),
-        Builtin(b) => Ok(RetType(mktype(ctx, type_of_builtin(b))?)),
+        Builtin(b) => {
+            Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?))
+        }
         BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
         IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
@@ -1001,7 +998,7 @@ fn type_last_layer(
 /// `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.
-fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
+fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
     let ctx = TypecheckContext::new();
     let e = type_with(&ctx, e)?;
     // Ensure `e` has a type (i.e. `e` is not `Sort`)
@@ -1012,7 +1009,7 @@ fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
 /// The specific type error
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
-    UnboundVariable(Var<Label>),
+    UnboundVariable(V<Label>),
     InvalidInputType(Normalized),
     InvalidOutputType(Normalized),
     NotAFunction(Typed),
diff --git a/dhall/tests/traits.rs b/dhall/tests/traits.rs
index cf68d7d..6604c06 100644
--- a/dhall/tests/traits.rs
+++ b/dhall/tests/traits.rs
@@ -1,11 +1,11 @@
 #![feature(proc_macro_hygiene)]
 use dhall::de::SimpleStaticType;
 use dhall_proc_macros;
-use dhall_syntax::{Label, SubExpr, X};
+use dhall_syntax::{SubExpr, X};
 
 #[test]
 fn test_static_type() {
-    fn mktype(x: SubExpr<Label, X, X>) -> dhall::expr::SimpleType {
+    fn mktype(x: SubExpr<X, X>) -> dhall::expr::SimpleType {
         x.into()
     }
 
diff --git a/dhall_proc_macros/src/quote.rs b/dhall_proc_macros/src/quote.rs
index d0deaad..eaf4946 100644
--- a/dhall_proc_macros/src/quote.rs
+++ b/dhall_proc_macros/src/quote.rs
@@ -7,7 +7,7 @@ use std::collections::BTreeMap;
 
 pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let input_str = input.to_string();
-    let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote();
+    let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote();
     let no_import =
         |_: &Import| -> X { panic!("Don't use import in dhall::expr!()") };
     let expr = expr.map_embed(no_import);
@@ -17,7 +17,7 @@ pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
 
 pub fn subexpr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let input_str = input.to_string();
-    let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote();
+    let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote();
     let no_import =
         |_: &Import| -> X { panic!("Don't use import in dhall::subexpr!()") };
     let expr = expr.map_embed(no_import);
@@ -31,59 +31,60 @@ pub fn quote_exprf<TS>(expr: ExprF<TS, Label, X>) -> TokenStream
 where
     TS: quote::ToTokens + std::fmt::Debug,
 {
+    use dhall_syntax::ExprF::*;
     match expr {
-        ExprF::Var(_) => unreachable!(),
-        ExprF::Pi(x, t, b) => {
+        Var(_) => unreachable!(),
+        Pi(x, t, b) => {
             let x = quote_label(&x);
             quote! { dhall_syntax::ExprF::Pi(#x, #t, #b) }
         }
-        ExprF::Lam(x, t, b) => {
+        Lam(x, t, b) => {
             let x = quote_label(&x);
             quote! { dhall_syntax::ExprF::Lam(#x, #t, #b) }
         }
-        ExprF::App(f, a) => {
+        App(f, a) => {
             quote! { dhall_syntax::ExprF::App(#f, #a) }
         }
-        ExprF::Annot(x, t) => {
+        Annot(x, t) => {
             quote! { dhall_syntax::ExprF::Annot(#x, #t) }
         }
-        ExprF::Const(c) => {
+        Const(c) => {
             let c = quote_const(c);
             quote! { dhall_syntax::ExprF::Const(#c) }
         }
-        ExprF::Builtin(b) => {
+        Builtin(b) => {
             let b = quote_builtin(b);
             quote! { dhall_syntax::ExprF::Builtin(#b) }
         }
-        ExprF::BinOp(o, a, b) => {
+        BinOp(o, a, b) => {
             let o = quote_binop(o);
             quote! { dhall_syntax::ExprF::BinOp(#o, #a, #b) }
         }
-        ExprF::NaturalLit(n) => {
+        NaturalLit(n) => {
             quote! { dhall_syntax::ExprF::NaturalLit(#n) }
         }
-        ExprF::BoolLit(b) => {
+        BoolLit(b) => {
             quote! { dhall_syntax::ExprF::BoolLit(#b) }
         }
-        ExprF::SomeLit(x) => {
+        SomeLit(x) => {
             quote! { dhall_syntax::ExprF::SomeLit(#x) }
         }
-        ExprF::EmptyListLit(t) => {
+        EmptyListLit(t) => {
             quote! { dhall_syntax::ExprF::EmptyListLit(#t) }
         }
-        ExprF::NEListLit(es) => {
+        NEListLit(es) => {
             let es = quote_vec(es);
             quote! { dhall_syntax::ExprF::NEListLit(#es) }
         }
-        ExprF::RecordType(m) => {
+        RecordType(m) => {
             let m = quote_map(m);
             quote! { dhall_syntax::ExprF::RecordType(#m) }
         }
-        ExprF::RecordLit(m) => {
+        RecordLit(m) => {
             let m = quote_map(m);
             quote! { dhall_syntax::ExprF::RecordLit(#m) }
         }
-        ExprF::UnionType(m) => {
+        UnionType(m) => {
             let m = quote_opt_map(m);
             quote! { dhall_syntax::ExprF::UnionType(#m) }
         }
@@ -94,21 +95,22 @@ where
 // Returns an expression of type SubExpr<_, _>. Expects interpolated variables
 // to be of type SubExpr<_, _>.
 fn quote_subexpr(
-    expr: &SubExpr<Label, X, X>,
+    expr: &SubExpr<X, X>,
     ctx: &Context<Label, ()>,
 ) -> TokenStream {
+    use dhall_syntax::ExprF::*;
     match expr.as_ref().map_ref_with_special_handling_of_binders(
         |e| quote_subexpr(e, ctx),
         |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())),
         |_| unreachable!(),
         Label::clone,
     ) {
-        ExprF::Var(Var(ref s, n)) => {
+        Var(V(ref s, n)) => {
             match ctx.lookup(s, n) {
                 // Non-free variable; interpolates as itself
                 Some(()) => {
                     let s: String = s.into();
-                    let var = quote! { dhall_syntax::Var(#s.into(), #n) };
+                    let var = quote! { dhall_syntax::V(#s.into(), #n) };
                     rc(quote! { dhall_syntax::ExprF::Var(#var) })
                 }
                 // Free variable; interpolates as a rust variable
@@ -117,7 +119,7 @@ fn quote_subexpr(
                     // TODO: insert appropriate shifts ?
                     let v: TokenStream = s.parse().unwrap();
                     quote! { {
-                        let x: dhall_syntax::SubExpr<_, _, _> = #v.clone();
+                        let x: dhall_syntax::SubExpr<_, _> = #v.clone();
                         x
                     } }
                 }
@@ -127,24 +129,22 @@ fn quote_subexpr(
     }
 }
 
-// Returns an expression of type Expr<_, _, _>. Expects interpolated variables
-// to be of type SubExpr<_, _, _>.
-fn quote_expr(
-    expr: &Expr<Label, X, X>,
-    ctx: &Context<Label, ()>,
-) -> TokenStream {
+// Returns an expression of type Expr<_, _>. Expects interpolated variables
+// to be of type SubExpr<_, _>.
+fn quote_expr(expr: &Expr<X, X>, ctx: &Context<Label, ()>) -> TokenStream {
+    use dhall_syntax::ExprF::*;
     match expr.map_ref_with_special_handling_of_binders(
         |e| quote_subexpr(e, ctx),
         |l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())),
         |_| unreachable!(),
         Label::clone,
     ) {
-        ExprF::Var(Var(ref s, n)) => {
+        Var(V(ref s, n)) => {
             match ctx.lookup(s, n) {
                 // Non-free variable; interpolates as itself
                 Some(()) => {
                     let s: String = s.into();
-                    let var = quote! { dhall_syntax::Var(#s.into(), #n) };
+                    let var = quote! { dhall_syntax::V(#s.into(), #n) };
                     quote! { dhall_syntax::ExprF::Var(#var) }
                 }
                 // Free variable; interpolates as a rust variable
@@ -153,7 +153,7 @@ fn quote_expr(
                     // TODO: insert appropriate shifts ?
                     let v: TokenStream = s.parse().unwrap();
                     quote! { {
-                        let x: dhall_syntax::SubExpr<_, _, _> = #v.clone();
+                        let x: dhall_syntax::SubExpr<_, _> = #v.clone();
                         x.unroll()
                     } }
                 }
diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index c8a2425..a186d19 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,7 +60,19 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Var<Label>(pub Label, pub usize);
+pub struct V<Label>(pub Label, pub usize);
+
+// This is only for the specific `Label` type, not generic
+impl From<Label> for V<Label> {
+    fn from(x: Label) -> V<Label> {
+        V(x, 0)
+    }
+}
+impl<'a> From<&'a Label> for V<Label> {
+    fn from(x: &'a Label) -> V<Label> {
+        V(x.clone(), 0)
+    }
+}
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -125,52 +137,44 @@ pub enum Builtin {
     TextShow,
 }
 
-pub type ParsedExpr = SubExpr<Label, X, Import>;
-pub type ResolvedExpr = SubExpr<Label, X, X>;
+pub type ParsedExpr = SubExpr<X, Import>;
+pub type ResolvedExpr = SubExpr<X, X>;
 pub type DhallExpr = ResolvedExpr;
 
 // Each node carries an annotation. In practice it's either X (no annotation) or a Span.
 #[derive(Debug)]
-pub struct SubExpr<VarLabel, Note, Embed>(
-    Rc<(Expr<VarLabel, Note, Embed>, Option<Note>)>,
-);
+pub struct SubExpr<Note, Embed>(Rc<(Expr<Note, Embed>, Option<Note>)>);
 
-impl<VarLabel: PartialEq, Note, Embed: PartialEq> std::cmp::PartialEq
-    for SubExpr<VarLabel, Note, Embed>
-{
+impl<Note, Embed: PartialEq> std::cmp::PartialEq for SubExpr<Note, Embed> {
     fn eq(&self, other: &Self) -> bool {
         self.0.as_ref().0 == other.0.as_ref().0
     }
 }
 
-impl<VarLabel: Eq, Note, Embed: Eq> std::cmp::Eq
-    for SubExpr<VarLabel, Note, Embed>
-{
-}
+impl<Note, Embed: Eq> std::cmp::Eq for SubExpr<Note, Embed> {}
 
-pub type Expr<VarLabel, Note, Embed> =
-    ExprF<SubExpr<VarLabel, Note, Embed>, VarLabel, Embed>;
+pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Embed>;
 
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
 // smart pointers.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ExprF<SubExpr, VarLabel, Embed> {
+pub enum ExprF<SubExpr, Label, Embed> {
     Const(Const),
     ///  `x`
     ///  `x@n`
-    Var(Var<VarLabel>),
+    Var(V<Label>),
     ///  `λ(x : A) -> b`
-    Lam(VarLabel, SubExpr, SubExpr),
+    Lam(Label, SubExpr, SubExpr),
     ///  `A -> B`
     ///  `∀(x : A) -> B`
-    Pi(VarLabel, SubExpr, SubExpr),
+    Pi(Label, SubExpr, SubExpr),
     ///  `f a`
     App(SubExpr, SubExpr),
     ///  `let x     = r in e`
     ///  `let x : t = r in e`
-    Let(VarLabel, Option<SubExpr>, SubExpr, SubExpr),
+    Let(Label, Option<SubExpr>, SubExpr, SubExpr),
     ///  `x : t`
     Annot(SubExpr, SubExpr),
     /// Built-in values
@@ -231,7 +235,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_under_binder: impl FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err> {
+    ) -> Result<ExprF<SE2, L2, E2>, Err>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         self.visit(visitor::TraverseRefWithBindersVisitor {
             visit_subexpr,
             visit_under_binder,
@@ -245,7 +253,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err> {
+    ) -> Result<ExprF<SE2, L2, E2>, Err>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         self.visit(visitor::TraverseRefVisitor {
             visit_subexpr,
             visit_embed,
@@ -259,7 +271,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_under_binder: impl FnMut(&'a L, &'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2> {
+    ) -> ExprF<SE2, L2, E2>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         trivial_result(self.traverse_ref_with_special_handling_of_binders(
             |x| Ok(map_subexpr(x)),
             |l, x| Ok(map_under_binder(l, x)),
@@ -273,7 +289,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2> {
+    ) -> ExprF<SE2, L2, E2>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         trivial_result(self.traverse_ref(
             |x| Ok(map_subexpr(x)),
             |x| Ok(map_embed(x)),
@@ -286,7 +306,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
     ) -> Result<ExprF<SE2, L, E>, Err>
     where
-        L: Clone,
+        L: Ord + Clone,
         E: Clone,
     {
         self.traverse_ref(
@@ -301,31 +321,26 @@ impl<SE, L, E> ExprF<SE, L, E> {
         map_subexpr: impl Fn(&'a SE) -> SE2,
     ) -> ExprF<SE2, L, E>
     where
-        L: Clone,
+        L: Ord + Clone,
         E: Clone,
     {
         self.map_ref(map_subexpr, E::clone, L::clone)
     }
 }
 
-impl<L, N, E> Expr<L, N, E> {
+impl<N, E> Expr<N, E> {
     fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<Expr<L, N, E2>, Err>
+    ) -> Result<Expr<N, E2>, Err>
     where
-        L: Clone,
         N: Clone,
     {
         self.visit(&mut visitor::TraverseEmbedVisitor(visit_embed))
     }
 
-    fn map_embed<E2>(
-        &self,
-        mut map_embed: impl FnMut(&E) -> E2,
-    ) -> Expr<L, N, E2>
+    fn map_embed<E2>(&self, mut map_embed: impl FnMut(&E) -> E2) -> Expr<N, E2>
     where
-        L: Clone,
         N: Clone,
     {
         trivial_result(self.traverse_embed(|x| Ok(map_embed(x))))
@@ -333,52 +348,52 @@ impl<L, N, E> Expr<L, N, E> {
 
     pub fn squash_embed<E2>(
         &self,
-        f: impl FnMut(&E) -> SubExpr<L, N, E2>,
-    ) -> SubExpr<L, N, E2>
+        f: impl FnMut(&E) -> SubExpr<N, E2>,
+    ) -> SubExpr<N, E2>
     where
-        L: Clone,
         N: Clone,
     {
         trivial_result(self.visit(&mut visitor::SquashEmbedVisitor(f)))
     }
 }
 
-impl<L: Clone, E: Clone> Expr<L, X, E> {
-    pub fn note_absurd<N>(&self) -> Expr<L, N, E> {
+impl<E: Clone> Expr<X, E> {
+    pub fn note_absurd<N>(&self) -> Expr<N, E> {
         self.visit(&mut visitor::NoteAbsurdVisitor)
     }
 }
 
-impl<L: Clone, N: Clone> Expr<L, N, X> {
-    pub fn embed_absurd<E>(&self) -> Expr<L, N, E> {
+impl<N: Clone> Expr<N, X> {
+    pub fn embed_absurd<E>(&self) -> Expr<N, E> {
         self.visit(&mut visitor::EmbedAbsurdVisitor)
     }
 }
 
-impl<V, N, E> SubExpr<V, N, E> {
-    pub fn as_ref(&self) -> &Expr<V, N, E> {
+impl<N, E> SubExpr<N, E> {
+    pub fn as_ref(&self) -> &Expr<N, E> {
         &self.0.as_ref().0
     }
 
-    pub fn new(x: Expr<V, N, E>, n: N) -> Self {
+    pub fn new(x: Expr<N, E>, n: N) -> Self {
         SubExpr(Rc::new((x, Some(n))))
     }
 
-    pub fn from_expr_no_note(x: Expr<V, N, E>) -> Self {
+    pub fn from_expr_no_note(x: Expr<N, E>) -> Self {
         SubExpr(Rc::new((x, None)))
     }
 
-    pub fn unnote(&self) -> SubExpr<V, X, E>
+    pub fn unnote(&self) -> SubExpr<X, E>
     where
-        V: Clone,
         E: Clone,
     {
         SubExpr::from_expr_no_note(
             self.as_ref().visit(&mut visitor::UnNoteVisitor),
         )
     }
+}
 
-    pub fn rewrap<E2>(&self, x: Expr<V, N, E2>) -> SubExpr<V, N, E2>
+impl<N: Clone, E> SubExpr<N, E> {
+    pub fn rewrap<E2>(&self, x: Expr<N, E2>) -> SubExpr<N, E2>
     where
         N: Clone,
     {
@@ -388,9 +403,8 @@ impl<V, N, E> SubExpr<V, N, E> {
     pub fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<SubExpr<V, N, E2>, Err>
+    ) -> Result<SubExpr<N, E2>, Err>
     where
-        V: Clone,
         N: Clone,
     {
         Ok(self.rewrap(self.as_ref().traverse_embed(visit_embed)?))
@@ -399,9 +413,8 @@ impl<V, N, E> SubExpr<V, N, E> {
     pub fn map_embed<E2>(
         &self,
         map_embed: impl FnMut(&E) -> E2,
-    ) -> SubExpr<V, N, E2>
+    ) -> SubExpr<N, E2>
     where
-        V: Clone,
         N: Clone,
     {
         self.rewrap(self.as_ref().map_embed(map_embed))
@@ -410,12 +423,8 @@ impl<V, N, E> SubExpr<V, N, E> {
     pub fn map_subexprs_with_special_handling_of_binders<'a>(
         &'a self,
         map_expr: impl FnMut(&'a Self) -> Self,
-        map_under_binder: impl FnMut(&'a V, &'a Self) -> Self,
-    ) -> Self
-    where
-        V: Clone,
-        N: Clone,
-    {
+        map_under_binder: impl FnMut(&'a Label, &'a Self) -> Self,
+    ) -> Self {
         match self.as_ref() {
             ExprF::Embed(_) => SubExpr::clone(self),
             // This calls ExprF::map_ref
@@ -423,7 +432,7 @@ impl<V, N, E> SubExpr<V, N, E> {
                 map_expr,
                 map_under_binder,
                 |_| unreachable!(),
-                V::clone,
+                Label::clone,
             )),
         }
     }
@@ -432,34 +441,26 @@ impl<V, N, E> SubExpr<V, N, E> {
     /// capture by shifting variable indices
     /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
     /// for details
-    pub fn shift(&self, delta: isize, var: &Var<V>) -> Self
-    where
-        V: Clone + PartialEq,
-        N: Clone,
-    {
+    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self.as_ref() {
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.shift(delta, var),
-                |x: &V, e| e.shift(delta, &var.shift(1, &Var::new(x.clone()))),
+                |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
             ),
         }
     }
 
-    pub fn subst_shift(&self, var: &Var<V>, val: &Self) -> Self
-    where
-        V: Clone + PartialEq,
-        N: Clone,
-    {
+    pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
         match self.as_ref() {
             ExprF::Var(v) if v == var => val.clone(),
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.subst_shift(var, val),
-                |x: &V, e| {
+                |x: &Label, e| {
                     e.subst_shift(
-                        &var.shift(1, &Var::new(x.clone())),
-                        &val.shift(1, &Var::new(x.clone())),
+                        &var.shift(1, &x.into()),
+                        &val.shift(1, &x.into()),
                     )
                 },
             ),
@@ -467,26 +468,26 @@ impl<V, N, E> SubExpr<V, N, E> {
     }
 }
 
-impl<L: Clone, N: Clone> SubExpr<L, N, X> {
-    pub fn embed_absurd<T>(&self) -> SubExpr<L, N, T> {
+impl<N: Clone> SubExpr<N, X> {
+    pub fn embed_absurd<T>(&self) -> SubExpr<N, T> {
         self.rewrap(self.as_ref().embed_absurd())
     }
 }
 
-impl<L: Clone, E: Clone> SubExpr<L, X, E> {
-    pub fn note_absurd<N>(&self) -> SubExpr<L, N, E> {
+impl<E: Clone> SubExpr<X, E> {
+    pub fn note_absurd<N>(&self) -> SubExpr<N, E> {
         SubExpr::from_expr_no_note(self.as_ref().note_absurd())
     }
 }
 
-impl<L, N, E> Clone for SubExpr<L, N, E> {
+impl<N, E> Clone for SubExpr<N, E> {
     fn clone(&self) -> Self {
         SubExpr(Rc::clone(&self.0))
     }
 }
 
 // Should probably rename this
-pub fn rc<L, E>(x: Expr<L, X, E>) -> SubExpr<L, X, E> {
+pub fn rc<E>(x: Expr<X, E>) -> SubExpr<X, E> {
     SubExpr::from_expr_no_note(x)
 }
 
@@ -500,35 +501,18 @@ fn add_ui(u: usize, i: isize) -> usize {
     }
 }
 
-impl<L> Var<L> {
-    fn new(x: L) -> Self {
-        Var(x, 0)
-    }
-}
-impl<L: PartialEq + Clone> Var<L> {
-    pub fn shift(&self, delta: isize, var: &Var<L>) -> Self {
-        let Var(x, n) = var;
-        let Var(y, m) = self;
+impl<Label: PartialEq + Clone> V<Label> {
+    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        let V(x, n) = var;
+        let V(y, m) = self;
         if x == y && n <= m {
-            Var(y.clone(), add_ui(*m, delta))
+            V(y.clone(), add_ui(*m, delta))
         } else {
-            Var(y.clone(), *m)
+            V(y.clone(), *m)
         }
     }
 }
 
-// This is only for the specific `Label` type, not generic
-impl From<Label> for Var<Label> {
-    fn from(x: Label) -> Var<Label> {
-        Var(x, 0)
-    }
-}
-impl<'a> From<&'a Label> for Var<Label> {
-    fn from(x: &'a Label) -> Var<Label> {
-        Var(x.clone(), 0)
-    }
-}
-
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
@@ -536,9 +520,9 @@ impl<'a> From<&'a Label> for Var<Label> {
 ///
 pub fn shift<N, E>(
     delta: isize,
-    var: &Var<Label>,
-    in_expr: &SubExpr<Label, N, E>,
-) -> SubExpr<Label, N, E>
+    var: &V<Label>,
+    in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E>
 where
     N: Clone,
 {
@@ -547,8 +531,8 @@ where
 
 pub fn shift0_multiple<N, E>(
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<Label, N, E>,
-) -> SubExpr<Label, N, E>
+    in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E>
 where
     N: Clone,
 {
@@ -558,15 +542,16 @@ where
 fn shift0_multiple_inner<N, E>(
     ctx: &Context<Label, ()>,
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<Label, N, E>,
-) -> SubExpr<Label, N, E>
+    in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E>
 where
     N: Clone,
 {
+    use crate::ExprF::*;
     match in_expr.as_ref() {
-        ExprF::Var(Var(y, m)) if ctx.lookup(y, *m).is_none() => {
+        Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
             let delta = deltas.get(y).unwrap_or(&0);
-            in_expr.rewrap(ExprF::Var(Var(y.clone(), add_ui(*m, *delta))))
+            in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
         }
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| shift0_multiple_inner(ctx, deltas, e),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index bdef553..83ccc1e 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -8,13 +8,7 @@ use std::rc::Rc;
 
 use dhall_generated_parser::{DhallParser, Rule};
 
-use crate::ExprF::{
-    Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit, Embed,
-    EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit,
-    OldOptionalLit, Pi, Projection, RecordLit, RecordType, SomeLit, TextLit,
-    UnionLit, UnionType,
-};
-
+use crate::ExprF::*;
 use crate::*;
 
 // This file consumes the parse tree generated by pest and turns it into
@@ -22,10 +16,10 @@ use crate::*;
 // their own crate because they are quite general and useful. For now they
 // are here and hopefully you can figure out how they work.
 
-type ParsedExpr = Expr<Label, Span, Import>;
-type ParsedSubExpr = SubExpr<Label, Span, Import>;
-type ParsedText = InterpolatedText<ParsedSubExpr>;
-type ParsedTextContents = InterpolatedTextContents<ParsedSubExpr>;
+type ParsedExpr = Expr<Span, Import>;
+type ParsedSubExpr = SubExpr<Span, Import>;
+type ParsedText = InterpolatedText<SubExpr<Span, Import>>;
+type ParsedTextContents = InterpolatedTextContents<SubExpr<Span, Import>>;
 
 pub type ParseError = pest::error::Error<Rule>;
 
@@ -510,17 +504,17 @@ make_parser! {
 
     rule!(identifier<ParsedSubExpr> as expression; span; children!(
         [variable(v)] => {
-            spanned(span, ExprF::Var(v))
+            spanned(span, Var(v))
         },
         [builtin(e)] => e,
     ));
 
-    rule!(variable<Var<Label>>; children!(
+    rule!(variable<V<Label>>; children!(
         [label(l), natural_literal(idx)] => {
-            Var(l, idx)
+            V(l, idx)
         },
         [label(l)] => {
-            Var(l, 0)
+            V(l, 0)
         },
     ));
 
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 9cc1b46..e3b180b 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,9 +3,7 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
-    for ExprF<SE, L, E>
-{
+impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
         match self {
@@ -15,10 +13,9 @@ impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            // TODO: arrow type
-            // Pi(a, b, c) if &String::from(a) == "_" => {
-            //     write!(f, "{} → {}", b, c)?;
-            // }
+            Pi(a, b, c) if &String::from(a) == "_" => {
+                write!(f, "{} → {}", b, c)?;
+            }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -127,25 +124,21 @@ enum PrintPhase {
 // Wraps an Expr with a phase, so that phase selsction can be done
 // separate from the actual printing
 #[derive(Clone)]
-struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
+struct PhasedExpr<'a, S, A>(&'a SubExpr<S, A>, PrintPhase);
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for PhasedExpr<'a, L, S, A>
-{
+impl<'a, S: Clone, A: Display + Clone> Display for PhasedExpr<'a, S, A> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
-    PhasedExpr<'a, L, S, A>
-{
-    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
+impl<'a, S: Clone, A: Display + Clone> PhasedExpr<'a, S, A> {
+    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
+impl<S: Clone, A: Display + Clone> Expr<S, A> {
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -179,12 +172,11 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                // TODO: arrow type
-                // if &String::from(&a) == "_" {
-                //     Pi(a, b.phase(Operator), c)
-                // } else {
-                Pi(a, b, c)
-                // }
+                if &String::from(&a) == "_" {
+                    Pi(a, b.phase(Operator), c)
+                } else {
+                    Pi(a, b, c)
+                }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -220,9 +212,7 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for SubExpr<L, S, A>
-{
+impl<S: Clone, A: Display + Clone> Display for SubExpr<S, A> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
     }
@@ -484,9 +474,9 @@ impl Display for Scheme {
     }
 }
 
-impl<Label: Display> Display for Var<Label> {
+impl<Label: Display> Display for V<Label> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        let Var(x, n) = self;
+        let V(x, n) = self;
         x.fmt(f)?;
         if *n != 0 {
             write!(f, "@{}", n)?;
diff --git a/dhall_syntax/src/visitor.rs b/dhall_syntax/src/visitor.rs
index a8e5a8c..7fdf217 100644
--- a/dhall_syntax/src/visitor.rs
+++ b/dhall_syntax/src/visitor.rs
@@ -48,6 +48,8 @@ pub trait ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>: Sized {
 impl<'a, T, Ret, SE1, L1, E1>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, Result<Ret, T::Error>> for T
 where
+    L1: Ord,
+    T::L2: Ord,
     T: ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> Result<Ret, T::Error> {
@@ -67,27 +69,31 @@ where
             })
         }
         fn btmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<Label, SE>,
+            x: &'a BTreeMap<L, SE>,
             mut v: V,
-        ) -> Result<BTreeMap<Label, V::SE2>, V::Error>
+        ) -> Result<BTreeMap<V::L2, V::SE2>, V::Error>
         where
+            L: Ord,
+            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
-                .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
+                .map(|(k, x)| Ok((v.visit_label(k)?, v.visit_subexpr(x)?)))
                 .collect()
         }
         fn btoptmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<Label, Option<SE>>,
+            x: &'a BTreeMap<L, Option<SE>>,
             mut v: V,
-        ) -> Result<BTreeMap<Label, Option<V::SE2>>, V::Error>
+        ) -> Result<BTreeMap<V::L2, Option<V::SE2>>, V::Error>
         where
+            L: Ord,
+            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
                 .map(|(k, x)| {
                     Ok((
-                        k.clone(),
+                        v.visit_label(k)?,
                         match x {
                             Some(x) => Some(v.visit_subexpr(x)?),
                             None => None,
@@ -98,14 +104,9 @@ where
         }
 
         let mut v = self;
-        use crate::ExprF::{
-            Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit,
-            Embed, EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit,
-            NaturalLit, OldOptionalLit, Pi, Projection, RecordLit, RecordType,
-            SomeLit, TextLit, UnionLit, UnionType,
-        };
+        use crate::ExprF::*;
         T::visit_resulting_exprf(match input {
-            ExprF::Var(Var(l, n)) => ExprF::Var(Var(v.visit_label(l)?, *n)),
+            Var(V(l, n)) => Var(V(v.visit_label(l)?, *n)),
             Lam(l, t, e) => {
                 let t = v.visit_subexpr(t)?;
                 let (l, e) = v.visit_binder(l, e)?;
@@ -149,16 +150,20 @@ where
             RecordType(kts) => RecordType(btmap(kts, v)?),
             RecordLit(kvs) => RecordLit(btmap(kvs, v)?),
             UnionType(kts) => UnionType(btoptmap(kts, v)?),
-            UnionLit(l, x, kts) => {
-                UnionLit(l.clone(), v.visit_subexpr(x)?, btoptmap(kts, v)?)
-            }
+            UnionLit(k, x, kts) => UnionLit(
+                v.visit_label(k)?,
+                v.visit_subexpr(x)?,
+                btoptmap(kts, v)?,
+            ),
             Merge(x, y, t) => Merge(
                 v.visit_subexpr(x)?,
                 v.visit_subexpr(y)?,
                 opt(t, |e| v.visit_subexpr(e))?,
             ),
-            Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
-            Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
+            Field(e, l) => Field(v.visit_subexpr(e)?, v.visit_label(l)?),
+            Projection(e, ls) => {
+                Projection(v.visit_subexpr(e)?, vec(ls, |l| v.visit_label(l))?)
+            }
             Embed(a) => return v.visit_embed_squash(a),
         })
     }
@@ -309,6 +314,8 @@ where
 impl<'a, T, SE1, SE2, L1, L2, E1, E2>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, ExprF<SE2, L2, E2>> for T
 where
+    L1: Ord,
+    L2: Ord,
     T: ExprFInFallibleVisitor<'a, SE1, SE2, L1, L2, E1, E2>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> ExprF<SE2, L2, E2> {
@@ -330,6 +337,8 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
+    L: Ord,
+    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F2: FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
     F4: FnOnce(&'a E) -> Result<E2, Err>,
@@ -368,6 +377,8 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
+    L: Ord,
+    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F3: FnOnce(&'a E) -> Result<E2, Err>,
     F4: FnMut(&'a L) -> Result<L2, Err>,
@@ -387,11 +398,10 @@ where
 
 pub struct TraverseEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, L, N, E, E2, Err, F1>
-    ExprFFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, N, E2>, L, L, E, E2>
+impl<'a, 'b, N, E, E2, Err, F1>
+    ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, Label, Label, E, E2>
     for &'b mut TraverseEmbedVisitor<F1>
 where
-    L: Clone + 'a,
     N: Clone + 'a,
     F1: FnMut(&E) -> Result<E2, Err>,
 {
@@ -399,48 +409,50 @@ where
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<L, N, E>,
-    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
+        subexpr: &'a SubExpr<N, E>,
+    ) -> Result<SubExpr<N, E2>, Self::Error> {
         Ok(subexpr.rewrap(subexpr.as_ref().visit(&mut **self)?))
     }
     fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> {
         (self.0)(embed)
     }
-    fn visit_label(&mut self, label: &'a L) -> Result<L, Self::Error> {
-        Ok(L::clone(label))
+    fn visit_label(&mut self, label: &'a Label) -> Result<Label, Self::Error> {
+        Ok(Label::clone(label))
     }
 }
 
 pub struct SquashEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, L, N, E1, E2, F1>
-    ExprFVeryGenericVisitor<'a, SubExpr<L, N, E2>, SubExpr<L, N, E1>, L, E1>
+impl<'a, 'b, N, E1, E2, F1>
+    ExprFVeryGenericVisitor<'a, SubExpr<N, E2>, SubExpr<N, E1>, Label, E1>
     for &'b mut SquashEmbedVisitor<F1>
 where
-    L: Clone + 'a,
     N: Clone + 'a,
-    F1: FnMut(&E1) -> SubExpr<L, N, E2>,
+    F1: FnMut(&E1) -> SubExpr<N, E2>,
 {
     type Error = X;
-    type SE2 = SubExpr<L, N, E2>;
-    type L2 = L;
+    type SE2 = SubExpr<N, E2>;
+    type L2 = Label;
     type E2 = E2;
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<L, N, E1>,
+        subexpr: &'a SubExpr<N, E1>,
     ) -> Result<Self::SE2, Self::Error> {
         Ok(subexpr.as_ref().visit(&mut **self)?)
     }
 
-    fn visit_label(&mut self, label: &'a L) -> Result<Self::L2, Self::Error> {
-        Ok(L::clone(label))
+    fn visit_label(
+        &mut self,
+        label: &'a Label,
+    ) -> Result<Self::L2, Self::Error> {
+        Ok(Label::clone(label))
     }
 
     fn visit_binder(
         mut self,
-        label: &'a L,
-        subexpr: &'a SubExpr<L, N, E1>,
+        label: &'a Label,
+        subexpr: &'a SubExpr<N, E1>,
     ) -> Result<(Self::L2, Self::SE2), Self::Error> {
         Ok((self.visit_label(label)?, self.visit_subexpr(subexpr)?))
     }
@@ -448,7 +460,7 @@ where
     fn visit_embed_squash(
         self,
         embed: &'a E1,
-    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
+    ) -> Result<SubExpr<N, E2>, Self::Error> {
         Ok((self.0)(embed))
     }
 
@@ -456,7 +468,7 @@ where
     // Useful to change the result type, and/or avoid some loss of info
     fn visit_resulting_exprf(
         result: ExprF<Self::SE2, Self::L2, Self::E2>,
-    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
+    ) -> Result<SubExpr<N, E2>, Self::Error> {
         // TODO: don't lose note
         Ok(SubExpr::from_expr_no_note(result))
     }
@@ -464,69 +476,57 @@ where
 
 pub struct UnNoteVisitor;
 
-impl<'a, 'b, L, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, X, E>, L, L, E, E>
+impl<'a, 'b, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<N, E>, SubExpr<X, E>, Label, Label, E, E>
     for &'b mut UnNoteVisitor
 where
-    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(
-        &mut self,
-        subexpr: &'a SubExpr<L, N, E>,
-    ) -> SubExpr<L, X, E> {
+    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, E>) -> SubExpr<X, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a L) -> L {
-        L::clone(label)
+    fn visit_label(&mut self, label: &'a Label) -> Label {
+        Label::clone(label)
     }
 }
 
 pub struct NoteAbsurdVisitor;
 
-impl<'a, 'b, L, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<L, X, E>, SubExpr<L, N, E>, L, L, E, E>
+impl<'a, 'b, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<X, E>, SubExpr<N, E>, Label, Label, E, E>
     for &'b mut NoteAbsurdVisitor
 where
-    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(
-        &mut self,
-        subexpr: &'a SubExpr<L, X, E>,
-    ) -> SubExpr<L, N, E> {
+    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<X, E>) -> SubExpr<N, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a L) -> L {
-        L::clone(label)
+    fn visit_label(&mut self, label: &'a Label) -> Label {
+        Label::clone(label)
     }
 }
 
 pub struct EmbedAbsurdVisitor;
 
-impl<'a, 'b, L, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<L, N, X>, SubExpr<L, N, E>, L, L, X, E>
+impl<'a, 'b, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<N, X>, SubExpr<N, E>, Label, Label, X, E>
     for &'b mut EmbedAbsurdVisitor
 where
-    L: Clone + 'a,
     N: Clone + 'a,
 {
-    fn visit_subexpr(
-        &mut self,
-        subexpr: &'a SubExpr<L, N, X>,
-    ) -> SubExpr<L, N, E> {
+    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, X>) -> SubExpr<N, E> {
         subexpr.rewrap(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a X) -> E {
         match *embed {}
     }
-    fn visit_label(&mut self, label: &'a L) -> L {
-        L::clone(label)
+    fn visit_label(&mut self, label: &'a Label) -> Label {
+        Label::clone(label)
     }
 }
-- 
cgit v1.2.3


From 6792d3da32d11b5303b00d1cc667f6f946d8bf33 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 19:51:26 +0200
Subject: We actually don't need SubExpr::shift anymore

---
 dhall/src/normalize.rs   |  9 +++---
 dhall_syntax/src/core.rs | 81 ------------------------------------------------
 2 files changed, 5 insertions(+), 85 deletions(-)

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 8ae746d..d84c2d5 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -187,17 +187,18 @@ impl Value {
                 let a = n.normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
-            Value::ListConsClosure(n, None) => {
-                let a = n.normalize_to_expr();
+            Value::ListConsClosure(a, None) => {
                 // Avoid accidental capture of the new `x` variable
                 let a1 = a.shift(1, &Label::from("x").into());
+                let a1 = a1.normalize_to_expr();
+                let a = a.normalize_to_expr();
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
-                let v = v.normalize_to_expr();
-                let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
                 let v = v.shift(1, &Label::from("xs").into());
+                let v = v.normalize_to_expr();
+                let a = n.normalize_to_expr();
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
             }
             Value::NaturalSuccClosure => {
diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index a186d19..7cdda64 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -1,9 +1,7 @@
 #![allow(non_snake_case)]
 use std::collections::BTreeMap;
-use std::collections::HashMap;
 use std::rc::Rc;
 
-use crate::context::Context;
 use crate::visitor;
 use crate::*;
 
@@ -436,36 +434,6 @@ impl<N: Clone, E> SubExpr<N, E> {
             )),
         }
     }
-
-    /// `shift` is used by both normalization and type-checking to avoid variable
-    /// capture by shifting variable indices
-    /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
-    /// for details
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        match self.as_ref() {
-            ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
-            _ => self.map_subexprs_with_special_handling_of_binders(
-                |e| e.shift(delta, var),
-                |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
-            ),
-        }
-    }
-
-    pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
-        match self.as_ref() {
-            ExprF::Var(v) if v == var => val.clone(),
-            ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
-            _ => self.map_subexprs_with_special_handling_of_binders(
-                |e| e.subst_shift(var, val),
-                |x: &Label, e| {
-                    e.subst_shift(
-                        &var.shift(1, &x.into()),
-                        &val.shift(1, &x.into()),
-                    )
-                },
-            ),
-        }
-    }
 }
 
 impl<N: Clone> SubExpr<N, X> {
@@ -512,52 +480,3 @@ impl<Label: PartialEq + Clone> V<Label> {
         }
     }
 }
-
-/// `shift` is used by both normalization and type-checking to avoid variable
-/// capture by shifting variable indices
-/// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
-/// for details
-///
-pub fn shift<N, E>(
-    delta: isize,
-    var: &V<Label>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
-    N: Clone,
-{
-    in_expr.shift(delta, var)
-}
-
-pub fn shift0_multiple<N, E>(
-    deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
-    N: Clone,
-{
-    shift0_multiple_inner(&Context::new(), deltas, in_expr)
-}
-
-fn shift0_multiple_inner<N, E>(
-    ctx: &Context<Label, ()>,
-    deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
-    N: Clone,
-{
-    use crate::ExprF::*;
-    match in_expr.as_ref() {
-        Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
-            let delta = deltas.get(y).unwrap_or(&0);
-            in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
-        }
-        _ => in_expr.map_subexprs_with_special_handling_of_binders(
-            |e| shift0_multiple_inner(ctx, deltas, e),
-            |x: &Label, e| {
-                shift0_multiple_inner(&ctx.insert(x.clone(), ()), deltas, e)
-            },
-        ),
-    }
-}
-- 
cgit v1.2.3


From 3b9dac7fccf5faea61703177cafe476f72518585 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 20:42:05 +0200
Subject: subst_shift now correctly preserves WHNF

---
 dhall/src/normalize.rs | 50 ++++++++++++++++++++++++--------------------------
 1 file changed, 24 insertions(+), 26 deletions(-)

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index d84c2d5..904c0a2 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -25,17 +25,13 @@ impl Typed {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized {
-        let internal = match self.0 {
-            TypedInternal::Sort => TypedInternal::Sort,
-            TypedInternal::Value(thunk, t) => {
-                // TODO: stupid but needed for now
-                let thunk =
-                    Thunk::from_normalized_expr(thunk.normalize_to_expr());
+        match &self.0 {
+            TypedInternal::Sort => {}
+            TypedInternal::Value(thunk, _) => {
                 thunk.normalize_nf();
-                TypedInternal::Value(thunk, t)
             }
-        };
-        Normalized(internal)
+        }
+        Normalized(self.0)
     }
 
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
@@ -503,6 +499,25 @@ impl Value {
 
     pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
         match self {
+            // Retry normalizing since substituting may allow progress
+            Value::AppliedBuiltin(b, args) => apply_builtin(
+                *b,
+                args.iter().map(|v| v.subst_shift(var, val)).collect(),
+            ),
+            // Retry normalizing since substituting may allow progress
+            Value::PartialExpr(e) => {
+                normalize_one_layer(e.map_ref_with_special_handling_of_binders(
+                    |v| v.subst_shift(var, val),
+                    |x, v| {
+                        v.subst_shift(
+                            &var.shift(1, &x.into()),
+                            &val.shift(1, &x.into()),
+                        )
+                    },
+                    X::clone,
+                    Label::clone,
+                ))
+            }
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
                 t.subst_shift(var, val),
@@ -511,10 +526,6 @@ impl Value {
                     &val.shift(1, &x.into()),
                 ),
             ),
-            Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
-                *b,
-                args.iter().map(|v| v.subst_shift(var, val)).collect(),
-            ),
             Value::NaturalSuccClosure => Value::NaturalSuccClosure,
             Value::OptionalSomeClosure(tth) => {
                 Value::OptionalSomeClosure(tth.subst_shift(var, val))
@@ -594,19 +605,6 @@ impl Value {
                     })
                     .collect(),
             ),
-            Value::PartialExpr(e) => {
-                Value::PartialExpr(e.map_ref_with_special_handling_of_binders(
-                    |v| v.subst_shift(var, val),
-                    |x, v| {
-                        v.subst_shift(
-                            &var.shift(1, &x.into()),
-                            &val.shift(1, &x.into()),
-                        )
-                    },
-                    X::clone,
-                    Label::clone,
-                ))
-            }
         }
     }
 }
-- 
cgit v1.2.3


From 0e6bc247d254a60eb1ba234e538864f0e9604efe Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 22:57:56 +0200
Subject: Clarify match_vars implementation

---
 dhall/src/typecheck.rs | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8b7f011..fc9db9f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -239,21 +239,21 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
 }
 
 fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
-    let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr);
+    let mut vl = vl.clone();
+    let mut vr = vr.clone();
     for &(xL2, xR2) in ctx {
-        match (nL, nR) {
-            (0, 0) if xL == xL2 && xR == xR2 => return true,
-            (_, _) => {
-                if xL == xL2 {
-                    nL -= 1;
-                }
-                if xR == xR2 {
-                    nR -= 1;
-                }
-            }
+        let vl2 = xL2.into();
+        let vr2 = xR2.into();
+        if vl == vl2 && vr == vr2 {
+            // Both were bound variables and correspond to the same binder
+            return true;
+        } else {
+            vl = vl.shift(-1, &vl2);
+            vr = vr.shift(-1, &vr2);
         }
     }
-    xL == xR && nL == nR
+    // Both were free variables
+    vl == vr
 }
 
 // Equality up to alpha-equivalence (renaming of bound variables)
-- 
cgit v1.2.3


From e8560d0dcb6c8051e2059f369258ec4bf07879f3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 5 May 2019 00:10:58 +0200
Subject: Implement alpha-normalization

Closes #12
---
 dhall/src/expr.rs      |  20 +++--
 dhall/src/normalize.rs | 214 +++++++++++++++++++++++++++++++++++++------------
 dhall/src/tests.rs     |   9 ++-
 dhall/src/typecheck.rs |  20 ++---
 4 files changed, 194 insertions(+), 69 deletions(-)

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 5bde68f..90efd39 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -58,11 +58,11 @@ impl std::fmt::Display for Normalized {
 
 mod typed {
     use super::{Type, Typed};
-    use crate::normalize::{Thunk, Value};
+    use crate::normalize::{DoubleVar, Thunk, Value};
     use crate::typecheck::{
         TypeError, TypeInternal, TypeMessage, TypecheckContext,
     };
-    use dhall_syntax::{Const, Label, SubExpr, V, X};
+    use dhall_syntax::{Const, SubExpr, X};
     use std::borrow::Cow;
 
     #[derive(Debug, Clone)]
@@ -94,6 +94,10 @@ mod typed {
             self.to_value().normalize_to_expr()
         }
 
+        pub(crate) fn to_expr_alpha(&self) -> SubExpr<X, X> {
+            self.to_value().normalize_to_expr_maybe_alpha(true)
+        }
+
         pub(crate) fn to_thunk(&self) -> Thunk {
             match self {
                 TypedInternal::Value(th, _) => th.clone(),
@@ -129,7 +133,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.shift(delta, var),
@@ -139,7 +143,7 @@ mod typed {
             }
         }
 
-        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+        pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
             match self {
                 TypedInternal::Value(th, t) => TypedInternal::Value(
                     th.subst_shift(var, val),
@@ -207,16 +211,16 @@ impl Normalized {
     pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
         self.0.to_expr()
     }
+    #[allow(dead_code)]
+    pub(crate) fn to_expr_alpha(&self) -> SubExpr<X, X> {
+        self.0.to_expr_alpha()
+    }
     pub(crate) fn to_value(&self) -> Value {
         self.0.to_value()
     }
     pub(crate) fn to_thunk(&self) -> Thunk {
         self.0.to_thunk()
     }
-    #[allow(dead_code)]
-    pub(crate) fn unnote(self) -> Normalized {
-        Normalized(self.0)
-    }
 }
 
 impl Typed {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 904c0a2..3e13350 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -34,11 +34,11 @@ impl Typed {
         Normalized(self.0)
     }
 
-    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         Typed(self.0.shift(delta, var))
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
         Typed(self.0.subst_shift(var, val))
     }
 
@@ -51,14 +51,68 @@ impl Typed {
     }
 }
 
+/// Stores a pair of variables: a normal one and if relevant one
+/// that corresponds to the alpha-normalized version of the first one.
+#[derive(Debug, Clone)]
+pub(crate) struct DoubleVar {
+    normal: V<Label>,
+    alpha: Option<V<()>>,
+}
+
+impl DoubleVar {
+    pub(crate) fn to_var(&self, alpha: bool) -> V<Label> {
+        match (alpha, &self.alpha) {
+            (true, Some(x)) => V("_".into(), x.1),
+            _ => self.normal.clone(),
+        }
+    }
+    pub(crate) fn from_var(normal: V<Label>) -> Self {
+        DoubleVar {
+            normal,
+            alpha: None,
+        }
+    }
+    pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+        DoubleVar {
+            normal: self.normal.shift(delta, &var.normal),
+            alpha: match (&self.alpha, &var.alpha) {
+                (Some(x), Some(v)) => Some(x.shift(delta, v)),
+                _ => None,
+            },
+        }
+    }
+}
+
+impl std::cmp::PartialEq for DoubleVar {
+    fn eq(&self, other: &Self) -> bool {
+        self.normal == other.normal
+    }
+}
+
+impl std::cmp::Eq for DoubleVar {}
+
+impl From<Label> for DoubleVar {
+    fn from(x: Label) -> DoubleVar {
+        DoubleVar {
+            normal: V(x, 0),
+            alpha: Some(V((), 0)),
+        }
+    }
+}
+impl<'a> From<&'a Label> for DoubleVar {
+    fn from(x: &'a Label) -> DoubleVar {
+        x.clone().into()
+    }
+}
+
 #[derive(Debug, Clone)]
 enum EnvItem {
     Thunk(Thunk),
-    Skip(V<Label>),
+    Skip(DoubleVar),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         use EnvItem::*;
         match self {
             Thunk(e) => Thunk(e.shift(delta, var)),
@@ -66,7 +120,7 @@ impl EnvItem {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
             EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -94,7 +148,8 @@ impl NormalizationContext {
         match self.0.lookup(x, *n) {
             Some(EnvItem::Thunk(t)) => t.to_value(),
             Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
-            None => Value::Var(var.clone()),
+            // Free variable
+            None => Value::Var(DoubleVar::from_var(var.clone())),
         }
     }
     pub(crate) fn from_typecheck_ctx(
@@ -114,11 +169,11 @@ impl NormalizationContext {
         NormalizationContext(Rc::new(ctx))
     }
 
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
     }
 
-    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
         NormalizationContext(Rc::new(
             self.0.map(|_, e| e.subst_shift(var, val)),
         ))
@@ -140,7 +195,7 @@ pub(crate) enum Value {
     NaturalSuccClosure,
     Pi(Label, TypeThunk, TypeThunk),
 
-    Var(V<Label>),
+    Var(DoubleVar),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -166,77 +221,99 @@ impl Value {
 
     /// Convert the value to a fully normalized syntactic expression
     pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+        self.normalize_to_expr_maybe_alpha(false)
+    }
+    /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
+    /// if alpha is `true`
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
         match self {
             Value::Lam(x, t, e) => rc(ExprF::Lam(
-                x.clone(),
-                t.normalize_to_expr(),
-                e.normalize_to_expr(),
+                if alpha { "_".into() } else { x.clone() },
+                t.normalize_to_expr_maybe_alpha(alpha),
+                e.normalize_to_expr_maybe_alpha(alpha),
             )),
             Value::AppliedBuiltin(b, args) => {
                 let mut e = rc(ExprF::Builtin(*b));
                 for v in args {
-                    e = rc(ExprF::App(e, v.normalize_to_expr()));
+                    e = rc(ExprF::App(
+                        e,
+                        v.normalize_to_expr_maybe_alpha(alpha),
+                    ));
                 }
                 e
             }
             Value::OptionalSomeClosure(n) => {
-                let a = n.normalize_to_expr();
+                let a = n.normalize_to_expr_maybe_alpha(alpha);
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
             Value::ListConsClosure(a, None) => {
                 // Avoid accidental capture of the new `x` variable
                 let a1 = a.shift(1, &Label::from("x").into());
-                let a1 = a1.normalize_to_expr();
-                let a = a.normalize_to_expr();
+                let a1 = a1.normalize_to_expr_maybe_alpha(alpha);
+                let a = a.normalize_to_expr_maybe_alpha(alpha);
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
                 // Avoid accidental capture of the new `xs` variable
                 let v = v.shift(1, &Label::from("xs").into());
-                let v = v.normalize_to_expr();
-                let a = n.normalize_to_expr();
+                let v = v.normalize_to_expr_maybe_alpha(alpha);
+                let a = n.normalize_to_expr_maybe_alpha(alpha);
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
             }
             Value::NaturalSuccClosure => {
                 dhall::subexpr!(λ(x : Natural) -> x + 1)
             }
             Value::Pi(x, t, e) => rc(ExprF::Pi(
-                x.clone(),
-                t.normalize_to_expr(),
-                e.normalize_to_expr(),
+                if alpha { "_".into() } else { x.clone() },
+                t.normalize_to_expr_maybe_alpha(alpha),
+                e.normalize_to_expr_maybe_alpha(alpha),
             )),
-            Value::Var(v) => rc(ExprF::Var(v.clone())),
+            Value::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
             Value::Const(c) => rc(ExprF::Const(*c)),
             Value::BoolLit(b) => rc(ExprF::BoolLit(*b)),
             Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
             Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
             Value::EmptyOptionalLit(n) => rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.normalize_to_expr(),
+                n.normalize_to_expr_maybe_alpha(alpha),
             )),
             Value::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.normalize_to_expr()))
+                rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
             }
             Value::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.normalize_to_expr()))
+                rc(ExprF::EmptyListLit(n.normalize_to_expr_maybe_alpha(alpha)))
             }
             Value::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.into_iter().map(|n| n.normalize_to_expr()).collect(),
+                elts.into_iter()
+                    .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
+                    .collect(),
             )),
             Value::RecordLit(kvs) => rc(ExprF::RecordLit(
                 kvs.iter()
-                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
+                    .map(|(k, v)| {
+                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+                    })
                     .collect(),
             )),
             Value::RecordType(kts) => rc(ExprF::RecordType(
                 kts.iter()
-                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
+                    .map(|(k, v)| {
+                        (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
+                    })
                     .collect(),
             )),
             Value::UnionType(kts) => rc(ExprF::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
+                        (
+                            k.clone(),
+                            v.as_ref().map(|v| {
+                                v.normalize_to_expr_maybe_alpha(alpha)
+                            }),
+                        )
                     })
                     .collect(),
             )),
@@ -244,23 +321,34 @@ impl Value {
                 let kts = kts
                     .iter()
                     .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
+                        (
+                            k.clone(),
+                            v.as_ref().map(|v| {
+                                v.normalize_to_expr_maybe_alpha(alpha)
+                            }),
+                        )
                     })
                     .collect();
                 rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
             }
             Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
                 l.clone(),
-                v.normalize_to_expr(),
+                v.normalize_to_expr_maybe_alpha(alpha),
                 kts.iter()
                     .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
+                        (
+                            k.clone(),
+                            v.as_ref().map(|v| {
+                                v.normalize_to_expr_maybe_alpha(alpha)
+                            }),
+                        )
                     })
                     .collect(),
             )),
             Value::TextLit(elts) => {
                 fn normalize_textlit(
                     elts: &Vec<InterpolatedTextContents<Thunk>>,
+                    alpha: bool,
                 ) -> InterpolatedText<OutputSubExpr> {
                     elts.iter()
                         .flat_map(|contents| {
@@ -268,12 +356,14 @@ impl Value {
                             let new_interpolated = match contents {
                                 Expr(n) => match &*n.normalize_nf() {
                                     Value::TextLit(elts2) => {
-                                        normalize_textlit(elts2)
+                                        normalize_textlit(elts2, alpha)
                                     }
                                     e => InterpolatedText::from((
                                         String::new(),
                                         vec![(
-                                            e.normalize_to_expr(),
+                                            e.normalize_to_expr_maybe_alpha(
+                                                alpha,
+                                            ),
                                             String::new(),
                                         )],
                                     )),
@@ -285,10 +375,10 @@ impl Value {
                         .collect()
                 }
 
-                rc(ExprF::TextLit(normalize_textlit(elts)))
+                rc(ExprF::TextLit(normalize_textlit(elts, alpha)))
             }
             Value::PartialExpr(e) => {
-                rc(e.map_ref_simple(|v| v.normalize_to_expr()))
+                rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
             }
         }
     }
@@ -400,7 +490,7 @@ impl Value {
         Value::AppliedBuiltin(b, vec![])
     }
 
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -497,7 +587,7 @@ impl Value {
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
         match self {
             // Retry normalizing since substituting may allow progress
             Value::AppliedBuiltin(b, args) => apply_builtin(
@@ -611,11 +701,10 @@ impl Value {
 
 mod thunk {
     use super::{
-        apply_any, normalize_whnf, InputSubExpr, NormalizationContext,
-        OutputSubExpr, Value,
+        apply_any, normalize_whnf, DoubleVar, InputSubExpr,
+        NormalizationContext, OutputSubExpr, Value,
     };
     use crate::expr::Typed;
-    use dhall_syntax::{Label, V};
     use std::cell::{Ref, RefCell};
     use std::rc::Rc;
 
@@ -692,7 +781,7 @@ mod thunk {
             }
         }
 
-        fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -706,7 +795,7 @@ mod thunk {
             }
         }
 
-        fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+        fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -793,7 +882,14 @@ mod thunk {
         }
 
         pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
-            self.normalize_nf().normalize_to_expr()
+            self.normalize_to_expr_maybe_alpha(false)
+        }
+
+        pub(crate) fn normalize_to_expr_maybe_alpha(
+            &self,
+            alpha: bool,
+        ) -> OutputSubExpr {
+            self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
         }
 
         pub(crate) fn app_val(&self, val: Value) -> Value {
@@ -804,11 +900,11 @@ mod thunk {
             apply_any(self.clone(), th)
         }
 
-        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
             self.0.borrow().shift(delta, var).into_thunk()
         }
 
-        pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+        pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
             self.0.borrow().subst_shift(var, val).into_thunk()
         }
     }
@@ -850,18 +946,21 @@ impl TypeThunk {
         }
     }
 
-    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
-        self.normalize_nf().normalize_to_expr()
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
+        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
             TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
         }
     }
 
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
@@ -1117,7 +1216,7 @@ fn apply_any(f: Thunk, a: Thunk) -> Value {
 fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
     match expr.as_ref() {
         ExprF::Embed(e) => return e.to_value(),
-        ExprF::Var(v) => return ctx.lookup(&v),
+        ExprF::Var(v) => return ctx.lookup(v),
         _ => {}
     }
 
@@ -1383,6 +1482,12 @@ mod spec_tests {
         };
     }
 
+    macro_rules! alpha_norm {
+        ($name:ident, $path:expr) => {
+            make_spec_test!(AlphaNormalization, Success, $name, $path);
+        };
+    }
+
     norm!(success_haskell_tutorial_access_0, "haskell-tutorial/access/0");
     norm!(success_haskell_tutorial_access_1, "haskell-tutorial/access/1");
     // norm!(success_haskell_tutorial_combineTypes_0, "haskell-tutorial/combineTypes/0");
@@ -1709,4 +1814,11 @@ mod spec_tests {
     norm!(success_unit_UnionTypeEmpty, "unit/UnionTypeEmpty");
     norm!(success_unit_UnionTypeNormalizeArguments, "unit/UnionTypeNormalizeArguments");
     norm!(success_unit_Variable, "unit/Variable");
+
+    alpha_norm!(alpha_success_unit_FunctionBindingUnderscore, "unit/FunctionBindingUnderscore");
+    alpha_norm!(alpha_success_unit_FunctionBindingX, "unit/FunctionBindingX");
+    alpha_norm!(alpha_success_unit_FunctionNestedBindingX, "unit/FunctionNestedBindingX");
+    alpha_norm!(alpha_success_unit_FunctionTypeBindingUnderscore, "unit/FunctionTypeBindingUnderscore");
+    alpha_norm!(alpha_success_unit_FunctionTypeBindingX, "unit/FunctionTypeBindingX");
+    alpha_norm!(alpha_success_unit_FunctionTypeNestedBindingX, "unit/FunctionTypeNestedBindingX");
 }
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index ce74606..6b2ab60 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -43,6 +43,7 @@ pub enum Feature {
     Parser,
     Import,
     Normalization,
+    AlphaNormalization,
     Typecheck,
     TypeInference,
 }
@@ -83,6 +84,7 @@ pub fn run_test(
         Parser => "parser/",
         Import => "import/",
         Normalization => "normalization/",
+        AlphaNormalization => "alpha-normalization/",
         Typecheck => "typecheck/",
         TypeInference => "type-inference/",
     };
@@ -139,6 +141,11 @@ pub fn run_test(
                     let expr = expr.skip_typecheck().normalize();
                     assert_eq_display!(expr, expected);
                 }
+                AlphaNormalization => {
+                    let expr =
+                        expr.skip_typecheck().normalize().to_expr_alpha();
+                    assert_eq_display!(expr, expected.to_expr());
+                }
             }
         }
         Failure => {
@@ -154,7 +161,7 @@ pub fn run_test(
                 Import => {
                     parse_file_str(&file_path)?.resolve().unwrap_err();
                 }
-                Normalization => unreachable!(),
+                Normalization | AlphaNormalization => unreachable!(),
                 Typecheck | TypeInference => {
                     parse_file_str(&file_path)?
                         .skip_resolve()?
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index fc9db9f..fcf4bd8 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -5,7 +5,9 @@ use std::collections::BTreeMap;
 use std::fmt;
 
 use crate::expr::*;
-use crate::normalize::{NormalizationContext, Thunk, TypeThunk, Value};
+use crate::normalize::{
+    DoubleVar, NormalizationContext, Thunk, TypeThunk, Value,
+};
 use crate::traits::DynamicType;
 use dhall_proc_macros as dhall;
 use dhall_syntax;
@@ -43,7 +45,7 @@ impl Typed {
 }
 
 impl Normalized {
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         Normalized(self.0.shift(delta, var))
     }
     pub(crate) fn to_type(self) -> Type {
@@ -73,10 +75,10 @@ impl Type {
     fn internal_whnf(&self) -> Option<Value> {
         self.0.whnf()
     }
-    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         Type(self.0.shift(delta, var))
     }
-    pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
         Type(self.0.subst_shift(var, val))
     }
 
@@ -148,14 +150,14 @@ impl TypeInternal {
             _ => None,
         }
     }
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.shift(delta, var))),
             Const(c) => Const(*c),
         }
     }
-    fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
         use TypeInternal::*;
         match self {
             Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -173,12 +175,12 @@ impl PartialEq for TypeInternal {
 
 #[derive(Debug, Clone)]
 pub(crate) enum EnvItem {
-    Type(V<Label>, Type),
+    Type(DoubleVar, Type),
     Value(Normalized),
 }
 
 impl EnvItem {
-    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
         use EnvItem::*;
         match self {
             Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
@@ -756,7 +758,7 @@ fn type_last_layer(
                 mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
             });
 
-            Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
+            Ok(RetType(tb.subst_shift(&x.into(), &a)))
         }
         Annot(x, t) => {
             let t = t.to_type();
-- 
cgit v1.2.3


From dadcd9aa595bf3f469514ccb586eace61a9c6b03 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 5 May 2019 00:17:07 +0200
Subject: Use alpha-normalization in equivalence checking

---
 dhall/src/typecheck.rs | 82 ++------------------------------------------------
 1 file changed, 2 insertions(+), 80 deletions(-)

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index fcf4bd8..8137417 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -69,9 +69,6 @@ impl Type {
     fn as_const(&self) -> Option<Const> {
         self.0.as_const()
     }
-    fn internal(&self) -> &TypeInternal {
-        &self.0
-    }
     fn internal_whnf(&self) -> Option<Value> {
         self.0.whnf()
     }
@@ -240,89 +237,14 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
     }
 }
 
-fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
-    let mut vl = vl.clone();
-    let mut vr = vr.clone();
-    for &(xL2, xR2) in ctx {
-        let vl2 = xL2.into();
-        let vr2 = xR2.into();
-        if vl == vl2 && vr == vr2 {
-            // Both were bound variables and correspond to the same binder
-            return true;
-        } else {
-            vl = vl.shift(-1, &vl2);
-            vr = vr.shift(-1, &vr2);
-        }
-    }
-    // Both were free variables
-    vl == vr
-}
-
 // Equality up to alpha-equivalence (renaming of bound variables)
 fn prop_equal<T, U>(eL0: T, eR0: U) -> bool
 where
     T: Borrow<Type>,
     U: Borrow<Type>,
 {
-    use dhall_syntax::ExprF::*;
-    fn go<'a, S, T>(
-        ctx: &mut Vec<(&'a Label, &'a Label)>,
-        el: &'a SubExpr<S, X>,
-        er: &'a SubExpr<T, X>,
-    ) -> bool
-    where
-        S: ::std::fmt::Debug,
-        T: ::std::fmt::Debug,
-    {
-        match (el.as_ref(), er.as_ref()) {
-            (Const(a), Const(b)) => a == b,
-            (Builtin(a), Builtin(b)) => a == b,
-            (Var(vL), Var(vR)) => match_vars(vL, vR, ctx),
-            (Pi(xL, tL, bL), Pi(xR, tR, bR)) => {
-                go(ctx, tL, tR) && {
-                    ctx.push((xL, xR));
-                    let eq2 = go(ctx, bL, bR);
-                    ctx.pop();
-                    eq2
-                }
-            }
-            (App(fL, aL), App(fR, aR)) => go(ctx, fL, fR) && go(ctx, aL, aR),
-            (RecordType(ktsL0), RecordType(ktsR0)) => {
-                ktsL0.len() == ktsR0.len()
-                    && ktsL0
-                        .iter()
-                        .zip(ktsR0.iter())
-                        .all(|((kL, tL), (kR, tR))| kL == kR && go(ctx, tL, tR))
-            }
-            (UnionType(ktsL0), UnionType(ktsR0)) => {
-                ktsL0.len() == ktsR0.len()
-                    && ktsL0.iter().zip(ktsR0.iter()).all(
-                        |((kL, tL), (kR, tR))| {
-                            kL == kR
-                                && match (tL, tR) {
-                                    (None, None) => true,
-                                    (Some(tL), Some(tR)) => go(ctx, tL, tR),
-                                    _ => false,
-                                }
-                        },
-                    )
-            }
-            (_, _) => false,
-        }
-    }
-    match (eL0.borrow().internal(), eR0.borrow().internal()) {
-        // (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
-        // (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
-        _ => {
-            let mut ctx = vec![];
-            go(
-                &mut ctx,
-                &eL0.borrow().to_expr(),
-                &eR0.borrow().to_expr(),
-            )
-        }
-        // _ => false,
-    }
+    eL0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
+        == eR0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
 }
 
 fn const_to_typed(c: Const) -> Typed {
-- 
cgit v1.2.3


From 8e4182f26b20b28f60fb0c21b3e08e19314de9a0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 5 May 2019 00:43:41 +0200
Subject: Make Value equality be alpha-equivalence

Closes #66, #65
---
 dhall/src/expr.rs      | 10 ++++-
 dhall/src/normalize.rs | 99 +++++++++++++++++++++++++++++++++++++++++++-------
 dhall/src/typecheck.rs | 11 ++----
 3 files changed, 99 insertions(+), 21 deletions(-)

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 90efd39..071bb92 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -44,7 +44,7 @@ pub(crate) struct Normalized(pub(crate) TypedInternal);
 
 impl std::cmp::PartialEq for Normalized {
     fn eq(&self, other: &Self) -> bool {
-        self.to_expr() == other.to_expr()
+        self.0 == other.0
     }
 }
 
@@ -153,6 +153,14 @@ mod typed {
             }
         }
     }
+
+    impl std::cmp::PartialEq for TypedInternal {
+        fn eq(&self, other: &Self) -> bool {
+            self.to_value() == other.to_value()
+        }
+    }
+
+    impl std::cmp::Eq for TypedInternal {}
 }
 
 /// A Dhall expression representing a simple type.
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3e13350..c11dd82 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -53,7 +53,7 @@ impl Typed {
 
 /// Stores a pair of variables: a normal one and if relevant one
 /// that corresponds to the alpha-normalized version of the first one.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, Eq)]
 pub(crate) struct DoubleVar {
     normal: V<Label>,
     alpha: Option<V<()>>,
@@ -83,14 +83,17 @@ impl DoubleVar {
     }
 }
 
+/// Equality is up to alpha-equivalence.
 impl std::cmp::PartialEq for DoubleVar {
     fn eq(&self, other: &Self) -> bool {
-        self.normal == other.normal
+        match (&self.alpha, &other.alpha) {
+            (Some(x), Some(y)) => x == y,
+            (None, None) => self.normal == other.normal,
+            _ => false,
+        }
     }
 }
 
-impl std::cmp::Eq for DoubleVar {}
-
 impl From<Label> for DoubleVar {
     fn from(x: Label) -> DoubleVar {
         DoubleVar {
@@ -104,6 +107,52 @@ impl<'a> From<&'a Label> for DoubleVar {
         x.clone().into()
     }
 }
+impl From<AlphaLabel> for DoubleVar {
+    fn from(x: AlphaLabel) -> DoubleVar {
+        let l: Label = x.into();
+        l.into()
+    }
+}
+impl<'a> From<&'a AlphaLabel> for DoubleVar {
+    fn from(x: &'a AlphaLabel) -> DoubleVar {
+        x.clone().into()
+    }
+}
+
+// Exactly like a Label, but equality returns always true.
+// This is so that Value equality is exactly alpha-equivalence.
+#[derive(Debug, Clone, Eq)]
+pub(crate) struct AlphaLabel(Label);
+
+impl AlphaLabel {
+    fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
+        if alpha {
+            "_".into()
+        } else {
+            self.to_label()
+        }
+    }
+    fn to_label(&self) -> Label {
+        self.clone().into()
+    }
+}
+
+impl std::cmp::PartialEq for AlphaLabel {
+    fn eq(&self, _other: &Self) -> bool {
+        true
+    }
+}
+
+impl From<Label> for AlphaLabel {
+    fn from(x: Label) -> AlphaLabel {
+        AlphaLabel(x)
+    }
+}
+impl From<AlphaLabel> for Label {
+    fn from(x: AlphaLabel) -> Label {
+        x.0
+    }
+}
 
 #[derive(Debug, Clone)]
 enum EnvItem {
@@ -181,10 +230,11 @@ impl NormalizationContext {
 }
 
 /// A semantic value.
-#[derive(Debug, Clone)]
+/// Equality is up to alpha-equivalence (renaming of bound variables).
+#[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum Value {
     /// Closures
-    Lam(Label, Thunk, Thunk),
+    Lam(AlphaLabel, Thunk, Thunk),
     AppliedBuiltin(Builtin, Vec<Thunk>),
     /// `λ(x: a) -> Some x`
     OptionalSomeClosure(TypeThunk),
@@ -193,7 +243,7 @@ pub(crate) enum Value {
     ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
-    Pi(Label, TypeThunk, TypeThunk),
+    Pi(AlphaLabel, TypeThunk, TypeThunk),
 
     Var(DoubleVar),
     Const(Const),
@@ -231,7 +281,7 @@ impl Value {
     ) -> OutputSubExpr {
         match self {
             Value::Lam(x, t, e) => rc(ExprF::Lam(
-                if alpha { "_".into() } else { x.clone() },
+                x.to_label_maybe_alpha(alpha),
                 t.normalize_to_expr_maybe_alpha(alpha),
                 e.normalize_to_expr_maybe_alpha(alpha),
             )),
@@ -267,7 +317,7 @@ impl Value {
                 dhall::subexpr!(λ(x : Natural) -> x + 1)
             }
             Value::Pi(x, t, e) => rc(ExprF::Pi(
-                if alpha { "_".into() } else { x.clone() },
+                x.to_label_maybe_alpha(alpha),
                 t.normalize_to_expr_maybe_alpha(alpha),
                 e.normalize_to_expr_maybe_alpha(alpha),
             )),
@@ -908,6 +958,13 @@ mod thunk {
             self.0.borrow().subst_shift(var, val).into_thunk()
         }
     }
+
+    impl std::cmp::PartialEq for Thunk {
+        fn eq(&self, other: &Self) -> bool {
+            &*self.as_value() == &*other.as_value()
+        }
+    }
+    impl std::cmp::Eq for Thunk {}
 }
 
 pub(crate) use thunk::Thunk;
@@ -946,6 +1003,13 @@ impl TypeThunk {
         }
     }
 
+    pub(crate) fn to_value(&self) -> Value {
+        match self {
+            TypeThunk::Thunk(th) => th.to_value(),
+            TypeThunk::Type(t) => t.to_value(),
+        }
+    }
+
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
@@ -968,6 +1032,13 @@ impl TypeThunk {
     }
 }
 
+impl std::cmp::PartialEq for TypeThunk {
+    fn eq(&self, other: &Self) -> bool {
+        self.to_value() == other.to_value()
+    }
+}
+impl std::cmp::Eq for TypeThunk {}
+
 fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
     use dhall_syntax::Builtin::*;
     use Value::*;
@@ -1252,10 +1323,12 @@ fn normalize_one_layer(expr: ExprF<Thunk, Label, X>) -> Value {
         ExprF::Embed(_) => unreachable!(),
         ExprF::Var(_) => unreachable!(),
         ExprF::Annot(x, _) => RetThunk(x),
-        ExprF::Lam(x, t, e) => RetValue(Lam(x, t, e)),
-        ExprF::Pi(x, t, e) => {
-            RetValue(Pi(x, TypeThunk::from_thunk(t), TypeThunk::from_thunk(e)))
-        }
+        ExprF::Lam(x, t, e) => RetValue(Lam(x.into(), t, e)),
+        ExprF::Pi(x, t, e) => RetValue(Pi(
+            x.into(),
+            TypeThunk::from_thunk(t),
+            TypeThunk::from_thunk(e),
+        )),
         ExprF::Let(x, _, v, b) => {
             let v = Typed::from_thunk_untyped(v);
             RetThunk(b.subst_shift(&x.into(), &v))
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8137417..2b87bd2 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -243,8 +243,7 @@ where
     T: Borrow<Type>,
     U: Borrow<Type>,
 {
-    eL0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
-        == eR0.borrow().to_value().normalize_to_expr_maybe_alpha(true)
+    eL0.borrow().to_value() == eR0.borrow().to_value()
 }
 
 fn const_to_typed(c: Const) -> Typed {
@@ -352,9 +351,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
             forall (nothing: optional) ->
             optional
         ),
-        // TODO: alpha-equivalence in type-inference tests
         OptionalNone => dhall::expr!(
-            forall (A: Type) -> Optional A
+            forall (a: Type) -> Optional a
         ),
     }
 }
@@ -436,7 +434,7 @@ impl TypeIntermediate {
 
                 Typed::from_thunk_and_type(
                     Value::Pi(
-                        x.clone(),
+                        x.clone().into(),
                         TypeThunk::from_type(ta.clone()),
                         TypeThunk::from_type(tb.clone()),
                     )
@@ -823,12 +821,11 @@ fn type_last_layer(
                     match &r.internal_whnf() {
                         Some(Value::UnionType(kts)) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
-                            // TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
                             Some(Some(t)) => {
                                 Ok(RetType(
                                     TypeIntermediate::Pi(
                                         ctx.clone(),
-                                        x.clone(),
+                                        "_".into(),
                                         t.to_type(ctx)?,
                                         r.clone(),
                                     )
-- 
cgit v1.2.3