Merge branch 'alpha-normalization'

4 files changed, 312 insertions, 188 deletions

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 5bde68f..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
     }
 }
 
@@ -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),
@@ -149,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.
@@ -207,16 +219,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 8ae746d..c11dd82 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -25,24 +25,20 @@ 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 {
+    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))
     }
 
@@ -55,14 +51,117 @@ 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, Eq)]
+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,
+            },
+        }
+    }
+}
+
+/// Equality is up to alpha-equivalence.
+impl std::cmp::PartialEq for DoubleVar {
+    fn eq(&self, other: &Self) -> bool {
+        match (&self.alpha, &other.alpha) {
+            (Some(x), Some(y)) => x == y,
+            (None, None) => self.normal == other.normal,
+            _ => false,
+        }
+    }
+}
+
+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()
+    }
+}
+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 {
     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)),
@@ -70,7 +169,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()),
@@ -98,7 +197,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(
@@ -118,11 +218,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)),
         ))
@@ -130,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),
@@ -142,9 +243,9 @@ pub(crate) enum Value {
     ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
-    Pi(Label, TypeThunk, TypeThunk),
+    Pi(AlphaLabel, TypeThunk, TypeThunk),
 
-    Var(V<Label>),
+    Var(DoubleVar),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -170,76 +271,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(),
+                x.to_label_maybe_alpha(alpha),
+                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(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_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)) => {
-                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_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(),
+                x.to_label_maybe_alpha(alpha),
+                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(),
             )),
@@ -247,23 +371,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| {
@@ -271,12 +406,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(),
                                         )],
                                     )),
@@ -288,10 +425,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)))
             }
         }
     }
@@ -403,7 +540,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(),
@@ -500,8 +637,27 @@ 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(
+                *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),
@@ -510,10 +666,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))
@@ -593,30 +745,16 @@ 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,
-                ))
-            }
         }
     }
 }
 
 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;
 
@@ -693,7 +831,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(
@@ -707,7 +845,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(
@@ -794,7 +932,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 {
@@ -805,14 +950,21 @@ 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()
         }
     }
+
+    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;
@@ -851,18 +1003,28 @@ impl TypeThunk {
         }
     }
 
-    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
-        self.normalize_nf().normalize_to_expr()
+    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,
+    ) -> 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)),
@@ -870,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::*;
@@ -1118,7 +1287,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),
         _ => {}
     }
 
@@ -1154,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))
@@ -1384,6 +1555,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");
@@ -1710,4 +1887,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 8b7f011..2b87bd2 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 {
@@ -67,16 +69,13 @@ 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()
     }
-    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 +147,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 +172,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)),
@@ -238,89 +237,13 @@ 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);
-    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;
-                }
-            }
-        }
-    }
-    xL == xR && nL == nR
-}
-
 // 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() == eR0.borrow().to_value()
 }
 
 fn const_to_typed(c: Const) -> Typed {
@@ -428,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
         ),
     }
 }
@@ -512,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()),
                     )
@@ -756,7 +678,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();
@@ -899,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(),
                                     )