3 files changed, 42 insertions, 33 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 16ea48f..a6ab79e 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -17,27 +17,6 @@ pub(crate) struct TyCtx {
     ctx: Vec<(Binder, CtxItem)>,
 }
 
-impl CtxItem {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(match self {
-            CtxItem::Kept(v, t) => {
-                CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
-            }
-            CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
-        })
-    }
-    fn under_multiple_binders(&self, shift_map: &HashMap<Label, usize>) -> Self
-    where
-        Self: Clone,
-    {
-        let mut v = self.clone();
-        for (x, n) in shift_map {
-            v = v.shift(*n as isize, &x.into()).unwrap();
-        }
-        v
-    }
-}
-
 impl TyCtx {
     pub fn new() -> Self {
         TyCtx { ctx: Vec::new() }
@@ -66,12 +45,16 @@ impl TyCtx {
             let l = b.to_label();
             match var.over_binder(&l) {
                 None => {
-                    let i = i.under_multiple_binders(&shift_map);
                     return Some(match i {
-                        CtxItem::Kept(newvar, t) => {
-                            Value::from_kind_and_type(ValueKind::Var(newvar), t)
+                        CtxItem::Kept(newvar, t) => Value::from_kind_and_type(
+                            ValueKind::Var(
+                                newvar.under_multiple_binders(&shift_map),
+                            ),
+                            t.under_multiple_binders(&shift_map),
+                        ),
+                        CtxItem::Replaced(v) => {
+                            v.under_multiple_binders(&shift_map)
                         }
-                        CtxItem::Replaced(v) => v,
                     });
                 }
                 Some(newvar) => var = newvar,
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index ad03187..049c2a9 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -240,9 +240,7 @@ impl Value {
     }
 
     pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(Value(Rc::new(RefCell::new(
-            self.0.borrow().shift(delta, var)?,
-        ))))
+        Some(self.0.borrow().shift(delta, var)?.into_value())
     }
     pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self>
     where
@@ -257,6 +255,20 @@ impl Value {
         // Can't fail since delta is positive
         self.shift(1, &x.into()).unwrap()
     }
+    pub(crate) fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self
+    where
+        Self: Clone,
+    {
+        let mut v = self.clone();
+        for (x, n) in shift_map {
+            // Can't fail since delta is positive
+            v = v.shift(*n as isize, &x.into()).unwrap();
+        }
+        v
+    }
     pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match &*self.as_kind() {
             // If the var matches, we can just reuse the provided value instead of copying it.
@@ -267,9 +279,7 @@ impl Value {
                 }
                 val.clone()
             }
-            _ => Value(Rc::new(RefCell::new(
-                self.0.borrow().subst_shift(var, val),
-            ))),
+            _ => self.0.borrow().subst_shift(var, val).into_value(),
         }
     }
 }
@@ -434,7 +444,7 @@ impl ValueKind<Value> {
         ValueKind::AppliedBuiltin(b, vec![])
     }
 
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(match self {
             ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
             _ => self.traverse_ref_with_special_handling_of_binders(
@@ -443,7 +453,7 @@ impl ValueKind<Value> {
             )?,
         })
     }
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match self {
             ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
             ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index a110632..7c2c4de 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,3 +1,5 @@
+use std::collections::HashMap;
+
 use crate::syntax::{Label, V};
 
 /// Stores a pair of variables: a normal one and one
@@ -38,6 +40,20 @@ impl AlphaVar {
         // Can't fail since delta is positive
         self.shift(1, &x.into()).unwrap()
     }
+    pub(crate) fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self
+    where
+        Self: Clone,
+    {
+        let mut v = self.clone();
+        for (x, n) in shift_map {
+            // Can't fail since delta is positive
+            v = v.shift(*n as isize, &x.into()).unwrap();
+        }
+        v
+    }
 }
 
 impl Binder {