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