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 +++++++++++++++++++++--------------------
 6 files changed, 100 insertions(+), 83 deletions(-)

(limited to 'dhall/src')

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),
-- 
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 ++++++++++++++++++++---------------------
 6 files changed, 83 insertions(+), 100 deletions(-)

(limited to 'dhall/src')

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),
-- 
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 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'dhall/src')

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 => {
-- 
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(-)

(limited to 'dhall/src')

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(-)

(limited to 'dhall/src')

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(-)

(limited to 'dhall/src')

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(-)

(limited to 'dhall/src')

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(-)

(limited to 'dhall/src')

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