diff --git a/chalk-derive/src/lib.rs b/chalk-derive/src/lib.rs
index 55daf0510f2..fcf7b3890f8 100644
--- a/chalk-derive/src/lib.rs
+++ b/chalk-derive/src/lib.rs
@@ -33,7 +33,7 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
                 fn fold_with<'i>(
                     &self,
                     folder: &mut dyn Folder < 'i, #arg, #arg >,
-                    binders: usize,
+                    outer_binder: DebruijnIndex,
                 ) -> ::chalk_engine::fallible::Fallible<Self::Result> {
                     #body
                 }
@@ -97,7 +97,7 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
                 fn fold_with<'i>(
                     &self,
                     folder: &mut dyn Folder < 'i, _I, _TI >,
-                    binders: usize,
+                    outer_binder: DebruijnIndex,
                 ) -> ::chalk_engine::fallible::Fallible<Self::Result>
                 where
                     _I: 'i,
@@ -136,7 +136,7 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
                 fn fold_with<'i>(
                     &self,
                     folder: &mut dyn Folder < 'i, #i, _TI >,
-                    binders: usize,
+                    outer_binder: DebruijnIndex,
                 ) -> ::chalk_engine::fallible::Fallible<Self::Result>
                 where
                     #i: 'i,
@@ -157,7 +157,7 @@ fn derive_fold_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream {
         Data::Struct(s) => {
             let fields = s.fields.into_iter().map(|f| {
                 let name = f.ident.as_ref().expect("Unnamed field in Foldable struct");
-                quote! { #name: self.#name.fold_with(folder, binders)? }
+                quote! { #name: self.#name.fold_with(folder, outer_binder)? }
             });
             quote! {
                 Ok(#type_name {
@@ -187,7 +187,7 @@ fn derive_fold_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream {
                             .collect();
                         quote! {
                             #type_name::#variant( #(ref #names),* ) => {
-                                Ok(#type_name::#variant( #(#names.fold_with(folder, binders)?),* ))
+                                Ok(#type_name::#variant( #(#names.fold_with(folder, outer_binder)?),* ))
                             }
                         }
                     }
diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
index 47dd8662729..6042ab89cd9 100644
--- a/chalk-integration/src/lowering.rs
+++ b/chalk-integration/src/lowering.rs
@@ -1,6 +1,6 @@
 use chalk_ir::cast::{Cast, Caster};
 use chalk_ir::interner::ChalkIr;
-use chalk_ir::{self, AssocTypeId, ImplId, StructId, TraitId};
+use chalk_ir::{self, AssocTypeId, BoundVar, DebruijnIndex, ImplId, StructId, TraitId};
 use chalk_parse::ast::*;
 use chalk_rust_ir as rust_ir;
 use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, ToParameter};
@@ -19,7 +19,7 @@ type TraitKinds = BTreeMap<chalk_ir::TraitId<ChalkIr>, TypeKind>;
 type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedTyLookup>;
 type AssociatedTyValueIds =
     BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedTyValueId<ChalkIr>>;
-type ParameterMap = BTreeMap<chalk_ir::ParameterKind<Ident>, usize>;
+type ParameterMap = BTreeMap<chalk_ir::ParameterKind<Ident>, BoundVar>;
 
 pub type LowerResult<T> = Result<T, RustIrError>;
 
@@ -62,11 +62,11 @@ struct AssociatedTyLookup {
 
 enum TypeLookup {
     Struct(chalk_ir::StructId<ChalkIr>),
-    Parameter(usize),
+    Parameter(BoundVar),
 }
 
 enum LifetimeLookup {
-    Parameter(usize),
+    Parameter(BoundVar),
 }
 
 const SELF: &str = "Self";
@@ -138,12 +138,15 @@ impl<'k> Env<'k> {
         I: IntoIterator<Item = chalk_ir::ParameterKind<Ident>>,
         I::IntoIter: ExactSizeIterator,
     {
-        let binders = binders.into_iter().enumerate().map(|(i, k)| (k, i));
+        let binders = binders
+            .into_iter()
+            .enumerate()
+            .map(|(i, k)| (k, BoundVar::new(DebruijnIndex::INNERMOST, i)));
         let len = binders.len();
         let parameter_map: ParameterMap = self
             .parameter_map
             .iter()
-            .map(|(&k, &v)| (k, v + len))
+            .map(|(&k, &v)| (k, v.shifted_in()))
             .chain(binders)
             .collect();
         if parameter_map.len() != self.parameter_map.len() + len {
@@ -395,6 +398,16 @@ trait LowerParameterMap {
             .chain(self.synthetic_parameters()) // (*) see below
             .collect()
          */
+
+        // (*) It is important that the declared parameters come
+        // before the synthetic parameters in the ordering. This is
+        // because of traits, when used as types, only have the first
+        // N parameters in their kind (that is, they do not have Self).
+        //
+        // Note that if `Self` appears in the where-clauses etc, the
+        // trait is not object-safe, and hence not supposed to be used
+        // as an object. Actually the handling of object types is
+        // probably just kind of messed up right now. That's ok.
     }
 
     fn parameter_refs(&self) -> Vec<chalk_ir::Parameter<ChalkIr>> {
@@ -407,16 +420,10 @@ trait LowerParameterMap {
     }
 
     fn parameter_map(&self) -> ParameterMap {
-        // (*) It is important that the declared parameters come
-        // before the subtle parameters in the ordering. This is
-        // because of traits, when used as types, only have the first
-        // N parameters in their kind (that is, they do not have Self).
-        //
-        // Note that if `Self` appears in the where-clauses etc, the
-        // trait is not object-safe, and hence not supposed to be used
-        // as an object. Actually the handling of object types is
-        // probably just kind of messed up right now. That's ok.
-        self.all_parameters().into_iter().zip(0..).collect()
+        self.all_parameters()
+            .into_iter()
+            .zip((0..).map(|i| BoundVar::new(DebruijnIndex::INNERMOST, i)))
+            .collect()
     }
 
     fn interner(&self) -> &ChalkIr {
@@ -997,7 +1004,11 @@ impl LowerTy for Ty {
                             .flat_map(|qil| {
                                 qil.into_where_clauses(
                                     interner,
-                                    chalk_ir::TyData::BoundVar(0).intern(interner),
+                                    chalk_ir::TyData::BoundVar(BoundVar::new(
+                                        DebruijnIndex::INNERMOST,
+                                        0,
+                                    ))
+                                    .intern(interner),
                                 )
                             })
                             .collect())
@@ -1187,11 +1198,7 @@ impl LowerClause for Clause {
             .into_iter()
             .map(
                 |implication: chalk_ir::Binders<chalk_ir::ProgramClauseImplication<ChalkIr>>| {
-                    if implication.binders.is_empty() {
-                        chalk_ir::ProgramClause::Implies(implication.value)
-                    } else {
-                        chalk_ir::ProgramClause::ForAll(implication)
-                    }
+                    chalk_ir::ProgramClause::ForAll(implication)
                 },
             )
             .collect();
@@ -1236,12 +1243,16 @@ impl LowerTrait for TraitDefn {
             .map(|defn| env.associated_ty_lookups[&(trait_id, defn.name.str)].id)
             .collect();
 
-        Ok(rust_ir::TraitDatum {
+        let trait_datum = rust_ir::TraitDatum {
             id: trait_id,
             binders: binders,
             flags: self.flags.lower(),
             associated_ty_ids,
-        })
+        };
+
+        debug!("trait_datum={:?}", trait_datum);
+
+        Ok(trait_datum)
     }
 }
 
diff --git a/chalk-ir/src/cast.rs b/chalk-ir/src/cast.rs
index b7077e23492..6d47a071d3f 100644
--- a/chalk-ir/src/cast.rs
+++ b/chalk-ir/src/cast.rs
@@ -138,15 +138,11 @@ impl<I: Interner> CastTo<Goal<I>> for EqGoal<I> {
 
 impl<T: CastTo<Goal<I>>, I: Interner> CastTo<Goal<I>> for Binders<T> {
     fn cast_to(self, interner: &I) -> Goal<I> {
-        if self.binders.is_empty() {
-            self.value.cast(interner)
-        } else {
-            GoalData::Quantified(
-                QuantifierKind::ForAll,
-                self.map(|bound| bound.cast(interner)),
-            )
-            .intern(interner)
-        }
+        GoalData::Quantified(
+            QuantifierKind::ForAll,
+            self.map(|bound| bound.cast(interner)),
+        )
+        .intern(interner)
     }
 }
 
@@ -199,14 +195,10 @@ where
     I: Interner,
 {
     fn cast_to(self, interner: &I) -> ProgramClause<I> {
-        if self.binders.is_empty() {
-            self.value.cast::<ProgramClause<I>>(interner)
-        } else {
-            ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
-                consequence: bound.cast(interner),
-                conditions: Goals::new(interner),
-            }))
-        }
+        ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
+            consequence: bound.cast(interner),
+            conditions: Goals::new(interner),
+        }))
     }
 }
 
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 666406323f6..76cda36b1d7 100644
--- a/chalk-ir/src/debug.rs
+++ b/chalk-ir/src/debug.rs
@@ -123,7 +123,7 @@ impl<I: Interner> Debug for TypeName<I> {
 impl<I: Interner> Debug for TyData<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         match self {
-            TyData::BoundVar(depth) => write!(fmt, "^{}", depth),
+            TyData::BoundVar(db) => write!(fmt, "{:?}", db),
             TyData::Dyn(clauses) => write!(fmt, "{:?}", clauses),
             TyData::InferenceVar(var) => write!(fmt, "{:?}", var),
             TyData::Apply(apply) => write!(fmt, "{:?}", apply),
@@ -134,6 +134,20 @@ impl<I: Interner> Debug for TyData<I> {
     }
 }
 
+impl Debug for BoundVar {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        let BoundVar { debruijn, index } = self;
+        write!(fmt, "{:?}.{:?}", debruijn, index)
+    }
+}
+
+impl Debug for DebruijnIndex {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        let DebruijnIndex { depth } = self;
+        write!(fmt, "^{}", depth)
+    }
+}
+
 impl<I: Interner> Debug for DynTy<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         let DynTy { bounds } = self;
@@ -161,7 +175,7 @@ impl<I: Interner> Debug for Fn<I> {
 impl<I: Interner> Debug for LifetimeData<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         match self {
-            LifetimeData::BoundVar(depth) => write!(fmt, "'^{}", depth),
+            LifetimeData::BoundVar(db) => write!(fmt, "'{:?}", db),
             LifetimeData::InferenceVar(var) => write!(fmt, "'{:?}", var),
             LifetimeData::Placeholder(index) => write!(fmt, "'{:?}", index),
             LifetimeData::Phantom(..) => unreachable!(),
@@ -294,19 +308,24 @@ impl<T: Debug> Debug for Binders<T> {
             ref binders,
             ref value,
         } = *self;
-        if !binders.is_empty() {
-            write!(fmt, "for<")?;
-            for (index, binder) in binders.iter().enumerate() {
-                if index > 0 {
-                    write!(fmt, ", ")?;
-                }
-                match *binder {
-                    ParameterKind::Ty(()) => write!(fmt, "type")?,
-                    ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
-                }
+
+        // NB: We always print the `for<>`, even if it is empty,
+        // because it may affect the debruijn indices of things
+        // contained within. For example, `for<> { ^1.0 }` is very
+        // different from `^1.0` in terms of what variable is being
+        // referenced.
+
+        write!(fmt, "for<")?;
+        for (index, binder) in binders.iter().enumerate() {
+            if index > 0 {
+                write!(fmt, ", ")?;
+            }
+            match *binder {
+                ParameterKind::Ty(()) => write!(fmt, "type")?,
+                ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
             }
-            write!(fmt, "> ")?;
         }
+        write!(fmt, "> ")?;
         Debug::fmt(value, fmt)
     }
 }
@@ -331,6 +350,12 @@ impl<T: Display> Display for Canonical<T> {
         let Canonical { binders, value } = self;
 
         if binders.is_empty() {
+            // Ordinarily, we try to print all binder levels, if they
+            // are empty, but we can skip in this *particular* case
+            // because we know that `Canonical` terms are never
+            // supposed to contain free variables.  In other words,
+            // all "bound variables" that appear inside the canonical
+            // value must reference values that appear in `binders`.
             write!(f, "{}", value)?;
         } else {
             write!(f, "for<")?;
diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs
index 93b7651f058..5bc642e5b9e 100644
--- a/chalk-ir/src/fold.rs
+++ b/chalk-ir/src/fold.rs
@@ -80,30 +80,34 @@ where
     /// encountered when folding. By default, invokes
     /// `super_fold_with`, which will in turn invoke the more
     /// specialized folding methods below, like `fold_free_var_ty`.
-    fn fold_ty(&mut self, ty: &Ty<I>, binders: usize) -> Fallible<Ty<TI>> {
-        ty.super_fold_with(self.as_dyn(), binders)
+    fn fold_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> Fallible<Ty<TI>> {
+        ty.super_fold_with(self.as_dyn(), outer_binder)
     }
 
     /// Top-level callback: invoked for each `Lifetime<I>` that is
     /// encountered when folding. By default, invokes
     /// `super_fold_with`, which will in turn invoke the more
     /// specialized folding methods below, like `fold_free_lifetime_ty`.
-    fn fold_lifetime(&mut self, lifetime: &Lifetime<I>, binders: usize) -> Fallible<Lifetime<TI>> {
-        lifetime.super_fold_with(self.as_dyn(), binders)
+    fn fold_lifetime(
+        &mut self,
+        lifetime: &Lifetime<I>,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Lifetime<TI>> {
+        lifetime.super_fold_with(self.as_dyn(), outer_binder)
     }
 
     /// Invoked for every program clause. By default, recursively folds the goals contents.
     fn fold_program_clause(
         &mut self,
         clause: &ProgramClause<I>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<ProgramClause<TI>> {
-        clause.super_fold_with(self.as_dyn(), binders)
+        clause.super_fold_with(self.as_dyn(), outer_binder)
     }
 
     /// Invoked for every goal. By default, recursively folds the goals contents.
-    fn fold_goal(&mut self, goal: &Goal<I>, binders: usize) -> Fallible<Goal<TI>> {
-        goal.super_fold_with(self.as_dyn(), binders)
+    fn fold_goal(&mut self, goal: &Goal<I>, outer_binder: DebruijnIndex) -> Fallible<Goal<TI>> {
+        goal.super_fold_with(self.as_dyn(), outer_binder)
     }
 
     /// If overridden to return true, then folding will panic if a
@@ -122,20 +126,36 @@ where
     ///
     /// This should return a type suitable for a context with
     /// `binders` in scope.
-    fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible<Ty<TI>> {
+    fn fold_free_var_ty(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<TI>> {
         if self.forbid_free_vars() {
-            panic!("unexpected free variable with depth `{:?}`", depth)
+            panic!(
+                "unexpected free variable with depth `{:?}` with outer binder {:?}",
+                bound_var, outer_binder
+            )
         } else {
-            Ok(TyData::<TI>::BoundVar(depth + binders).intern(self.target_interner()))
+            let bound_var = bound_var.shifted_in_from(outer_binder);
+            Ok(TyData::<TI>::BoundVar(bound_var).intern(self.target_interner()))
         }
     }
 
     /// As `fold_free_var_ty`, but for lifetimes.
-    fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible<Lifetime<TI>> {
+    fn fold_free_var_lifetime(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Lifetime<TI>> {
         if self.forbid_free_vars() {
-            panic!("unexpected free variable with depth `{:?}`", depth)
+            panic!(
+                "unexpected free variable with depth `{:?}` with outer binder {:?}",
+                bound_var, outer_binder
+            )
         } else {
-            Ok(LifetimeData::<TI>::BoundVar(depth + binders).intern(self.target_interner()))
+            let bound_var = bound_var.shifted_in_from(outer_binder);
+            Ok(LifetimeData::<TI>::BoundVar(bound_var).intern(self.target_interner()))
         }
     }
 
@@ -152,10 +172,11 @@ where
     ///
     /// - `universe` is the universe of the `TypeName::ForAll` that was found
     /// - `binders` is the number of binders in scope
+    #[allow(unused_variables)]
     fn fold_free_placeholder_ty(
         &mut self,
         universe: PlaceholderIndex,
-        _binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<TI>> {
         if self.forbid_free_placeholders() {
             panic!("unexpected placeholder type `{:?}`", universe)
@@ -165,10 +186,11 @@ where
     }
 
     /// As with `fold_free_placeholder_ty`, but for lifetimes.
+    #[allow(unused_variables)]
     fn fold_free_placeholder_lifetime(
         &mut self,
         universe: PlaceholderIndex,
-        _binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<TI>> {
         if self.forbid_free_placeholders() {
             panic!("unexpected placeholder lifetime `{:?}`", universe)
@@ -191,7 +213,12 @@ where
     ///
     /// - `universe` is the universe of the `TypeName::ForAll` that was found
     /// - `binders` is the number of binders in scope
-    fn fold_inference_ty(&mut self, var: InferenceVar, _binders: usize) -> Fallible<Ty<TI>> {
+    #[allow(unused_variables)]
+    fn fold_inference_ty(
+        &mut self,
+        var: InferenceVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<TI>> {
         if self.forbid_inference_vars() {
             panic!("unexpected inference type `{:?}`", var)
         } else {
@@ -200,10 +227,11 @@ where
     }
 
     /// As with `fold_free_inference_ty`, but for lifetimes.
+    #[allow(unused_variables)]
     fn fold_inference_lifetime(
         &mut self,
         var: InferenceVar,
-        _binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<TI>> {
         if self.forbid_inference_vars() {
             panic!("unexpected inference lifetime `'{:?}`", var)
@@ -248,7 +276,7 @@ pub trait Fold<I: Interner, TI: TargetInterner<I> = I>: Debug {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -262,7 +290,7 @@ pub trait SuperFold<I: Interner, TI: TargetInterner<I> = I>: Fold<I, TI> {
     fn super_fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -278,13 +306,13 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Ty<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        folder.fold_ty(self, binders)
+        folder.fold_ty(self, outer_binder)
     }
 }
 
@@ -297,37 +325,38 @@ where
     fn super_fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<TI>>
     where
         I: 'i,
         TI: 'i,
     {
-        match self.data(folder.interner()) {
-            TyData::BoundVar(depth) => {
-                if *depth >= binders {
-                    folder.fold_free_var_ty(*depth - binders, binders)
+        let interner = folder.interner();
+        match self.data(interner) {
+            TyData::BoundVar(bound_var) => {
+                if let Some(bound_var1) = bound_var.shifted_out_to(outer_binder) {
+                    // This variable was bound outside of the binders
+                    // that we have traversed during folding;
+                    // therefore, it is free. Let the folder have a
+                    // crack at it.
+                    folder.fold_free_var_ty(bound_var1, outer_binder)
                 } else {
-                    Ok(TyData::<TI>::BoundVar(*depth).intern(folder.target_interner()))
+                    // This variable was bound within the binders that
+                    // we folded over, so just return a bound
+                    // variable.
+                    Ok(TyData::<TI>::BoundVar(*bound_var).intern(folder.target_interner()))
                 }
             }
-            TyData::Dyn(clauses) => {
-                Ok(TyData::Dyn(clauses.fold_with(folder, binders)?)
-                    .intern(folder.target_interner()))
-            }
-            TyData::InferenceVar(var) => folder.fold_inference_ty(*var, binders),
-            TyData::Apply(apply) => {
-                Ok(TyData::Apply(apply.fold_with(folder, binders)?)
-                    .intern(folder.target_interner()))
-            }
-            TyData::Placeholder(ui) => Ok(folder.fold_free_placeholder_ty(*ui, binders)?),
-            TyData::Alias(proj) => Ok(
-                TyData::Alias(proj.fold_with(folder, binders)?).intern(folder.target_interner())
-            ),
-            TyData::Function(fun) => {
-                Ok(TyData::Function(fun.fold_with(folder, binders)?)
-                    .intern(folder.target_interner()))
-            }
+            TyData::Dyn(clauses) => Ok(TyData::Dyn(clauses.fold_with(folder, outer_binder)?)
+                .intern(folder.target_interner())),
+            TyData::InferenceVar(var) => folder.fold_inference_ty(*var, outer_binder),
+            TyData::Apply(apply) => Ok(TyData::Apply(apply.fold_with(folder, outer_binder)?)
+                .intern(folder.target_interner())),
+            TyData::Placeholder(ui) => Ok(folder.fold_free_placeholder_ty(*ui, outer_binder)?),
+            TyData::Alias(proj) => Ok(TyData::Alias(proj.fold_with(folder, outer_binder)?)
+                .intern(folder.target_interner())),
+            TyData::Function(fun) => Ok(TyData::Function(fun.fold_with(folder, outer_binder)?)
+                .intern(folder.target_interner())),
         }
     }
 }
@@ -341,13 +370,13 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Lifetime<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        folder.fold_lifetime(self, binders)
+        folder.fold_lifetime(self, outer_binder)
     }
 }
 
@@ -359,25 +388,31 @@ where
     fn super_fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<TI>>
     where
         I: 'i,
         TI: 'i,
     {
         let interner = folder.interner();
-        let target_interner = folder.target_interner();
         match self.data(interner) {
-            LifetimeData::BoundVar(depth) => {
-                if *depth >= binders {
-                    folder.fold_free_var_lifetime(depth - binders, binders)
+            LifetimeData::BoundVar(bound_var) => {
+                if let Some(bound_var1) = bound_var.shifted_out_to(outer_binder) {
+                    // This variable was bound outside of the binders
+                    // that we have traversed during folding;
+                    // therefore, it is free. Let the folder have a
+                    // crack at it.
+                    folder.fold_free_var_lifetime(bound_var1, outer_binder)
                 } else {
-                    Ok(LifetimeData::<TI>::BoundVar(*depth).intern(target_interner))
+                    // This variable was bound within the binders that
+                    // we folded over, so just return a bound
+                    // variable.
+                    Ok(LifetimeData::<TI>::BoundVar(*bound_var).intern(folder.target_interner()))
                 }
             }
-            LifetimeData::InferenceVar(var) => folder.fold_inference_lifetime(*var, binders),
+            LifetimeData::InferenceVar(var) => folder.fold_inference_lifetime(*var, outer_binder),
             LifetimeData::Placeholder(universe) => {
-                folder.fold_free_placeholder_lifetime(*universe, binders)
+                folder.fold_free_placeholder_lifetime(*universe, outer_binder)
             }
             LifetimeData::Phantom(..) => unreachable!(),
         }
@@ -392,13 +427,13 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goal<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        folder.fold_goal(self, binders)
+        folder.fold_goal(self, outer_binder)
     }
 }
 
@@ -407,7 +442,7 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for Goal<I> {
     fn super_fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -417,7 +452,7 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for Goal<I> {
         let target_interner = folder.target_interner();
         Ok(Goal::new(
             target_interner,
-            self.data(interner).fold_with(folder, binders)?,
+            self.data(interner).fold_with(folder, outer_binder)?,
         ))
     }
 }
@@ -431,12 +466,12 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ProgramClause<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        folder.fold_program_clause(self, binders)
+        folder.fold_program_clause(self, outer_binder)
     }
 }
diff --git a/chalk-ir/src/fold/binder_impls.rs b/chalk-ir/src/fold/binder_impls.rs
index 7599adcaae3..b811ab2e245 100644
--- a/chalk-ir/src/fold/binder_impls.rs
+++ b/chalk-ir/src/fold/binder_impls.rs
@@ -11,7 +11,7 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Fn<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -19,11 +19,11 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Fn<I> {
     {
         let Fn {
             num_binders,
-            ref parameters,
-        } = *self;
+            parameters,
+        } = self;
         Ok(Fn {
-            num_binders,
-            parameters: parameters.fold_with(folder, binders + num_binders)?,
+            num_binders: *num_binders,
+            parameters: parameters.fold_with(folder, outer_binder.shifted_in())?,
         })
     }
 }
@@ -37,17 +37,17 @@ where
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
         let Binders {
-            binders: ref self_binders,
-            value: ref self_value,
-        } = *self;
-        let value = self_value.fold_with(folder, binders + self_binders.len())?;
+            binders: self_binders,
+            value: self_value,
+        } = self;
+        let value = self_value.fold_with(folder, outer_binder.shifted_in())?;
         Ok(Binders {
             binders: self_binders.clone(),
             value: value,
@@ -65,17 +65,17 @@ where
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
         let Canonical {
-            binders: ref self_binders,
-            value: ref self_value,
-        } = *self;
-        let value = self_value.fold_with(folder, binders + self_binders.len())?;
+            binders: self_binders,
+            value: self_value,
+        } = self;
+        let value = self_value.fold_with(folder, outer_binder.shifted_in())?;
         Ok(Canonical {
             binders: self_binders.clone(),
             value: value,
diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs
index efef4c114fb..88a27d13219 100644
--- a/chalk-ir/src/fold/boring_impls.rs
+++ b/chalk-ir/src/fold/boring_impls.rs
@@ -16,13 +16,13 @@ impl<'a, T: Fold<I, TI>, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for &'a
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        (**self).fold_with(folder, binders)
+        (**self).fold_with(folder, outer_binder)
     }
 }
 
@@ -31,13 +31,15 @@ impl<T: Fold<I, TI>, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Vec<T>
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        self.iter().map(|e| e.fold_with(folder, binders)).collect()
+        self.iter()
+            .map(|e| e.fold_with(folder, outer_binder))
+            .collect()
     }
 }
 
@@ -46,13 +48,13 @@ impl<T: Fold<I, TI>, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Box<T>
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        Ok(Box::new((**self).fold_with(folder, binders)?))
+        Ok(Box::new((**self).fold_with(folder, outer_binder)?))
     }
 }
 
@@ -61,13 +63,13 @@ impl<T: Fold<I, TI>, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Arc<T>
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
-        Ok(Arc::new((**self).fold_with(folder, binders)?))
+        Ok(Arc::new((**self).fold_with(folder, outer_binder)?))
     }
 }
 
@@ -75,14 +77,14 @@ macro_rules! tuple_fold {
     ($($n:ident),*) => {
         impl<$($n: Fold<I, TI>,)* I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ($($n,)*) {
             type Result = ($($n::Result,)*);
-            fn fold_with<'i>(&self, folder: &mut dyn Folder<'i, I, TI>, binders: usize) -> Fallible<Self::Result>
+            fn fold_with<'i>(&self, folder: &mut dyn Folder<'i, I, TI>, outer_binder: DebruijnIndex) -> Fallible<Self::Result>
             where
                 I: 'i,
                 TI: 'i,
             {
                 #[allow(non_snake_case)]
                 let &($(ref $n),*) = self;
-                Ok(($($n.fold_with(folder, binders)?,)*))
+                Ok(($($n.fold_with(folder, outer_binder)?,)*))
             }
         }
     }
@@ -98,7 +100,7 @@ impl<T: Fold<I, TI>, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Option<
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -106,7 +108,7 @@ impl<T: Fold<I, TI>, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Option<
     {
         match self {
             None => Ok(None),
-            Some(e) => Ok(Some(e.fold_with(folder, binders)?)),
+            Some(e) => Ok(Some(e.fold_with(folder, outer_binder)?)),
         }
     }
 }
@@ -116,7 +118,7 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Parameter<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -125,7 +127,7 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Parameter<I> {
         let interner = folder.interner();
         let target_interner = folder.target_interner();
 
-        let data = self.data(interner).fold_with(folder, binders)?;
+        let data = self.data(interner).fold_with(folder, outer_binder)?;
         Ok(Parameter::new(target_interner, data))
     }
 }
@@ -135,7 +137,7 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Substitution<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -143,7 +145,9 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Substitution<I> {
     {
         let interner = folder.interner();
         let target_interner = folder.target_interner();
-        let folded = self.iter(interner).map(|p| p.fold_with(folder, binders));
+        let folded = self
+            .iter(interner)
+            .map(|p| p.fold_with(folder, outer_binder));
         Ok(Substitution::from_fallible(target_interner, folded)?)
     }
 }
@@ -153,7 +157,7 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -161,7 +165,9 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
     {
         let interner = folder.interner();
         let target_interner = folder.target_interner();
-        let folded = self.iter(interner).map(|p| p.fold_with(folder, binders));
+        let folded = self
+            .iter(interner)
+            .map(|p| p.fold_with(folder, outer_binder));
         Ok(Goals::from_fallible(target_interner, folded)?)
     }
 }
@@ -174,7 +180,7 @@ macro_rules! copy_fold {
             fn fold_with<'i>(
                 &self,
                 _folder: &mut dyn ($crate::fold::Folder<'i, I, TI>),
-                _binders: usize,
+                _outer_binder: DebruijnIndex,
             ) -> ::chalk_engine::fallible::Fallible<Self::Result>
             where
                 I: 'i,
@@ -190,6 +196,7 @@ copy_fold!(UniverseIndex);
 copy_fold!(usize);
 copy_fold!(PlaceholderIndex);
 copy_fold!(QuantifierKind);
+copy_fold!(DebruijnIndex);
 copy_fold!(chalk_engine::TableIndex);
 copy_fold!(chalk_engine::TimeStamp);
 copy_fold!(());
@@ -202,7 +209,7 @@ macro_rules! id_fold {
             fn fold_with<'i>(
                 &self,
                 _folder: &mut dyn ($crate::fold::Folder<'i, I, TI>),
-                _binders: usize,
+                _outer_binder: DebruijnIndex,
             ) -> ::chalk_engine::fallible::Fallible<Self::Result>
             where
                 I: 'i,
@@ -225,7 +232,7 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
     fn super_fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> ::chalk_engine::fallible::Fallible<Self::Result>
     where
         I: 'i,
@@ -233,10 +240,10 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
     {
         match self {
             ProgramClause::Implies(pci) => {
-                Ok(ProgramClause::Implies(pci.fold_with(folder, binders)?))
+                Ok(ProgramClause::Implies(pci.fold_with(folder, outer_binder)?))
             }
             ProgramClause::ForAll(pci) => {
-                Ok(ProgramClause::ForAll(pci.fold_with(folder, binders)?))
+                Ok(ProgramClause::ForAll(pci.fold_with(folder, outer_binder)?))
             }
         }
     }
@@ -248,7 +255,7 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for PhantomData<I> {
     fn fold_with<'i>(
         &self,
         _folder: &mut dyn Folder<'i, I, TI>,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> ::chalk_engine::fallible::Fallible<Self::Result>
     where
         I: 'i,
@@ -268,16 +275,16 @@ where
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
         match self {
-            ParameterKind::Ty(a) => Ok(ParameterKind::Ty(a.fold_with(folder, binders)?)),
+            ParameterKind::Ty(a) => Ok(ParameterKind::Ty(a.fold_with(folder, outer_binder)?)),
             ParameterKind::Lifetime(a) => {
-                Ok(ParameterKind::Lifetime(a.fold_with(folder, binders)?))
+                Ok(ParameterKind::Lifetime(a.fold_with(folder, outer_binder)?))
             }
         }
     }
@@ -296,7 +303,7 @@ where
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -312,13 +319,13 @@ where
             floundered_subgoals,
         } = self;
         Ok(ExClause {
-            subst: subst.fold_with(folder, binders)?,
+            subst: subst.fold_with(folder, outer_binder)?,
             ambiguous: *ambiguous,
-            constraints: constraints.fold_with(folder, binders)?,
-            subgoals: subgoals.fold_with(folder, binders)?,
-            delayed_subgoals: delayed_subgoals.fold_with(folder, binders)?,
-            answer_time: answer_time.fold_with(folder, binders)?,
-            floundered_subgoals: floundered_subgoals.fold_with(folder, binders)?,
+            constraints: constraints.fold_with(folder, outer_binder)?,
+            subgoals: subgoals.fold_with(folder, outer_binder)?,
+            delayed_subgoals: delayed_subgoals.fold_with(folder, outer_binder)?,
+            answer_time: answer_time.fold_with(folder, outer_binder)?,
+            floundered_subgoals: floundered_subgoals.fold_with(folder, outer_binder)?,
         })
     }
 }
@@ -336,7 +343,7 @@ where
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
@@ -347,8 +354,8 @@ where
             floundered_time,
         } = self;
         Ok(FlounderedSubgoal {
-            floundered_literal: floundered_literal.fold_with(folder, binders)?,
-            floundered_time: floundered_time.fold_with(folder, binders)?,
+            floundered_literal: floundered_literal.fold_with(folder, outer_binder)?,
+            floundered_time: floundered_time.fold_with(folder, outer_binder)?,
         })
     }
 }
@@ -363,15 +370,15 @@ where
     fn fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Self::Result>
     where
         I: 'i,
         TI: 'i,
     {
         match self {
-            Literal::Positive(goal) => Ok(Literal::Positive(goal.fold_with(folder, binders)?)),
-            Literal::Negative(goal) => Ok(Literal::Negative(goal.fold_with(folder, binders)?)),
+            Literal::Positive(goal) => Ok(Literal::Positive(goal.fold_with(folder, outer_binder)?)),
+            Literal::Negative(goal) => Ok(Literal::Negative(goal.fold_with(folder, outer_binder)?)),
         }
     }
 }
diff --git a/chalk-ir/src/fold/shift.rs b/chalk-ir/src/fold/shift.rs
index 83c1225c585..eba8d91f716 100644
--- a/chalk-ir/src/fold/shift.rs
+++ b/chalk-ir/src/fold/shift.rs
@@ -4,88 +4,57 @@ use crate::*;
 /// Methods for converting debruijn indices to move values into or out
 /// of binders.
 pub trait Shift<I: Interner>: Fold<I, I> {
-    /// Shifts debruijn indices in `self` **up**, which is used when a
-    /// value is being placed under additional levels of binders.
-    ///
-    /// For example, if we had some goal
-    /// like:
-    ///
-    /// ```notrust
-    /// T: Trait<?X>
-    /// ```
-    ///
-    /// where `?X` refers to some inference variable (and hence has depth 3),
-    /// we might use `up_shift` when constructing a goal like:
-    ///
-    /// ```notrust
-    /// exists<U> { T = U, T: Trait<?X> }
-    /// ```
-    ///
-    /// This is because, internally, the inference variable `?X` (as
-    /// well as the new quantified variable `U`) are going to be
-    /// represented by debruijn indices. So if the index of `X` is
-    /// zero, then while originally we might have had `T: Trait<?0>`,
-    /// inside the `exists` we want to represent `X` with `?1`, to
-    /// account for the binder:
-    ///
-    /// ```notrust
-    ///     exists { T = ?0, T: Trait<?1> }
-    ///                  ^^           ^^ refers to `?X`
-    ///                  refers to `U`
-    /// ```
-    fn shifted_in(&self, interner: &I, adjustment: usize) -> Self::Result;
-
-    /// Shifts debruijn indices in `self` **down**, hence **removing**
-    /// a value from binders. This will fail with `Err(NoSolution)` in
-    /// the case that the value refers to something from one of those
-    /// binders.
-    ///
-    /// Consider the final example from `up_shift`:
-    ///
-    /// ```notrust
-    ///     exists { T = ?0, T: Trait<?1> }
-    ///                  ^^           ^^ refers to `?X`
-    ///                  refers to `U`
-    /// ```
-    ///
-    /// If we `down_shift` the `T: Trait<?1>` goal by 1,
-    /// we will get `T: Trait<?0>`, which is what we started with.
-    /// In other words, we will have extracted it from the `exists`
-    /// binder.
-    ///
-    /// But if we try to `down_shift` the `T = ?0` goal by 1, we will
-    /// get `Err`, because it refers to the type bound by the
-    /// `exists`.
-    fn shifted_out(&self, interner: &I, adjustment: usize) -> Fallible<Self::Result>;
+    /// Shifts this term in one level of binders.
+    fn shifted_in(&self, interner: &I) -> Self::Result;
+
+    /// Shifts a term valid at `outer_binder` so that it is
+    /// valid at the innermost binder. See [`DebruijnIndex::shifted_in_from`]
+    /// for a detailed explanation.
+    fn shifted_in_from(&self, interner: &I, source_binder: DebruijnIndex) -> Self::Result;
+
+    /// Shifts this term out one level of binders.
+    fn shifted_out(&self, interner: &I) -> Fallible<Self::Result>;
+
+    /// Shifts a term valid at the innermost binder so that it is
+    /// valid at `outer_binder`. See [`DebruijnIndex::shifted_out_to`]
+    /// for a detailed explanation.
+    fn shifted_out_to(&self, interner: &I, target_binder: DebruijnIndex) -> Fallible<Self::Result>;
 }
 
 impl<T: Fold<I, I> + Eq, I: Interner> Shift<I> for T {
-    fn shifted_in(&self, interner: &I, adjustment: usize) -> T::Result {
+    fn shifted_in(&self, interner: &I) -> Self::Result {
+        self.shifted_in_from(interner, DebruijnIndex::ONE)
+    }
+
+    fn shifted_in_from(&self, interner: &I, source_binder: DebruijnIndex) -> T::Result {
         self.fold_with(
             &mut Shifter {
-                adjustment,
+                source_binder,
                 interner,
             },
-            0,
+            DebruijnIndex::INNERMOST,
         )
         .unwrap()
     }
 
-    fn shifted_out(&self, interner: &I, adjustment: usize) -> Fallible<T::Result> {
+    fn shifted_out_to(&self, interner: &I, target_binder: DebruijnIndex) -> Fallible<T::Result> {
         self.fold_with(
             &mut DownShifter {
-                adjustment,
+                target_binder,
                 interner,
             },
-            0,
+            DebruijnIndex::INNERMOST,
         )
     }
+
+    fn shifted_out(&self, interner: &I) -> Fallible<Self::Result> {
+        self.shifted_out_to(interner, DebruijnIndex::ONE)
+    }
 }
 
 /// A folder that adjusts debruijn indices by a certain amount.
-///
 struct Shifter<'i, I> {
-    adjustment: usize,
+    source_binder: DebruijnIndex,
     interner: &'i I,
 }
 
@@ -93,8 +62,10 @@ impl<I> Shifter<'_, I> {
     /// Given a free variable at `depth`, shifts that depth to `depth
     /// + self.adjustment`, and then wraps *that* within the internal
     /// set `binders`.
-    fn adjust(&self, depth: usize, binders: usize) -> usize {
-        depth + self.adjustment + binders
+    fn adjust(&self, bound_var: BoundVar, outer_binder: DebruijnIndex) -> BoundVar {
+        bound_var
+            .shifted_in_from(self.source_binder)
+            .shifted_in_from(outer_binder)
     }
 }
 
@@ -103,12 +74,23 @@ impl<'i, I: Interner> Folder<'i, I> for Shifter<'i, I> {
         self
     }
 
-    fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible<Ty<I>> {
-        Ok(TyData::<I>::BoundVar(self.adjust(depth, binders)).intern(self.interner()))
+    fn fold_free_var_ty(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<I>> {
+        Ok(TyData::<I>::BoundVar(self.adjust(bound_var, outer_binder)).intern(self.interner()))
     }
 
-    fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible<Lifetime<I>> {
-        Ok(LifetimeData::<I>::BoundVar(self.adjust(depth, binders)).intern(self.interner()))
+    fn fold_free_var_lifetime(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Lifetime<I>> {
+        Ok(
+            LifetimeData::<I>::BoundVar(self.adjust(bound_var, outer_binder))
+                .intern(self.interner()),
+        )
     }
 
     fn interner(&self) -> &'i I {
@@ -126,7 +108,7 @@ impl<'i, I: Interner> Folder<'i, I> for Shifter<'i, I> {
 /// *out* from binders. Consider this example:
 ///
 struct DownShifter<'i, I> {
-    adjustment: usize,
+    target_binder: DebruijnIndex,
     interner: &'i I,
 }
 
@@ -139,9 +121,9 @@ impl<I> DownShifter<'_, I> {
     /// those internal binders (i.e., `depth < self.adjustment`) the
     /// this will fail with `Err`. Otherwise, returns the variable at
     /// this new depth (but adjusted to appear within `binders`).
-    fn adjust(&self, depth: usize, binders: usize) -> Fallible<usize> {
-        match depth.checked_sub(self.adjustment) {
-            Some(new_depth) => Ok(new_depth + binders),
+    fn adjust(&self, bound_var: BoundVar, outer_binder: DebruijnIndex) -> Fallible<BoundVar> {
+        match bound_var.shifted_out_to(self.target_binder) {
+            Some(bound_var1) => Ok(bound_var1.shifted_in_from(outer_binder)),
             None => Err(NoSolution),
         }
     }
@@ -152,12 +134,23 @@ impl<'i, I: Interner> Folder<'i, I> for DownShifter<'i, I> {
         self
     }
 
-    fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible<Ty<I>> {
-        Ok(TyData::<I>::BoundVar(self.adjust(depth, binders)?).intern(self.interner()))
+    fn fold_free_var_ty(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<I>> {
+        Ok(TyData::<I>::BoundVar(self.adjust(bound_var, outer_binder)?).intern(self.interner()))
     }
 
-    fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible<Lifetime<I>> {
-        Ok(LifetimeData::<I>::BoundVar(self.adjust(depth, binders)?).intern(self.interner()))
+    fn fold_free_var_lifetime(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Lifetime<I>> {
+        Ok(
+            LifetimeData::<I>::BoundVar(self.adjust(bound_var, outer_binder)?)
+                .intern(self.interner()),
+        )
     }
 
     fn interner(&self) -> &'i I {
diff --git a/chalk-ir/src/fold/subst.rs b/chalk-ir/src/fold/subst.rs
index 50fec40d8d1..f2a775cd609 100644
--- a/chalk-ir/src/fold/subst.rs
+++ b/chalk-ir/src/fold/subst.rs
@@ -3,8 +3,8 @@ use crate::fold::shift::Shift;
 
 pub struct Subst<'s, 'i, I: Interner> {
     /// Values to substitute. A reference to a free variable with
-    /// index `i` will be mapped to `parameters[i]` -- if `i >
-    /// parameters.len()`, then we will leave the variable untouched.
+    /// index `i` will be mapped to `parameter_lists[i]` -- if `i >
+    /// parameter_lists.len()`, then we will leave the variable untouched.
     parameters: &'s [Parameter<I>],
     interner: &'i I,
 }
@@ -17,7 +17,7 @@ impl<I: Interner> Subst<'_, '_, I> {
                     parameters,
                     interner,
                 },
-                0,
+                DebruijnIndex::INNERMOST,
             )
             .unwrap()
     }
@@ -28,30 +28,62 @@ impl<'i, I: Interner> Folder<'i, I> for Subst<'_, 'i, I> {
         self
     }
 
-    fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible<Ty<I>> {
-        let interner = self.interner();
-        if depth >= self.parameters.len() {
-            Ok(TyData::<I>::BoundVar(depth - self.parameters.len() + binders).intern(interner))
-        } else {
-            match self.parameters[depth].data(interner) {
-                ParameterKind::Ty(t) => Ok(t.shifted_in(interner, binders)),
+    fn fold_free_var_ty(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<I>> {
+        // We are eliminating one binder, but binders outside of that get preserved.
+        //
+        // So e.g. consider this:
+        //
+        // ```
+        // for<A, B> { for<C> { [A, C] } }
+        // //          ^ the binder we are substituing with `[u32]`
+        // ```
+        //
+        // Here, `A` would be `^1.0` and `C` would be `^0.0`. We will replace `^0.0` with the
+        // 0th index from the list (`u32`). We will convert `^1.0` (A) to `^0.0` -- i.e., shift
+        // it **out** of one level of binder (the `for<C>` binder we are eliminating).
+        //
+        // This gives us as a result:
+        //
+        // ```
+        // for<A, B> { [A, u32] }
+        //              ^ represented as `^0.0`
+        // ```
+        if let Some(index) = bound_var.index_if_innermost() {
+            match self.parameters[index].data(self.interner()) {
+                ParameterKind::Ty(t) => Ok(t.shifted_in_from(self.interner(), outer_binder)),
                 _ => panic!("mismatched kinds in substitution"),
             }
+        } else {
+            Ok(bound_var
+                .shifted_out()
+                .expect("cannot fail because this is not the innermost")
+                .shifted_in_from(outer_binder)
+                .to_ty(self.interner()))
         }
     }
 
-    fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible<Lifetime<I>> {
-        let interner = self.interner();
-        if depth >= self.parameters.len() {
-            Ok(
-                LifetimeData::<I>::BoundVar(depth - self.parameters.len() + binders)
-                    .intern(interner),
-            )
-        } else {
-            match self.parameters[depth].data(interner) {
-                ParameterKind::Lifetime(l) => Ok(l.shifted_in(interner, binders)),
+    fn fold_free_var_lifetime(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Lifetime<I>> {
+        // see comment in `fold_free_var_ty`
+
+        if let Some(index) = bound_var.index_if_innermost() {
+            match self.parameters[index].data(self.interner()) {
+                ParameterKind::Lifetime(l) => Ok(l.shifted_in_from(self.interner(), outer_binder)),
                 _ => panic!("mismatched kinds in substitution"),
             }
+        } else {
+            Ok(bound_var
+                .shifted_out()
+                .unwrap()
+                .shifted_in_from(outer_binder)
+                .to_lifetime(self.interner()))
         }
     }
 
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
index ca633c87be4..54c2b3b0d94 100644
--- a/chalk-ir/src/lib.rs
+++ b/chalk-ir/src/lib.rs
@@ -183,9 +183,9 @@ impl<I: Interner> Ty<I> {
     }
 
     /// If this is a `TyData::BoundVar(d)`, returns `Some(d)` else `None`.
-    pub fn bound(&self, interner: &I) -> Option<usize> {
-        if let TyData::BoundVar(depth) = self.data(interner) {
-            Some(*depth)
+    pub fn bound(&self, interner: &I) -> Option<BoundVar> {
+        if let TyData::BoundVar(bv) = self.data(interner) {
+            Some(*bv)
         } else {
             None
         }
@@ -212,7 +212,7 @@ impl<I: Interner> Ty<I> {
     /// check, intended only for debug assertions, because I am lazy.
     pub fn needs_shift(&self, interner: &I) -> bool {
         let ty = self.clone();
-        ty != ty.shifted_in(interner, 1)
+        ty != ty.shifted_in(interner)
     }
 }
 
@@ -252,14 +252,8 @@ pub enum TyData<I: Interner> {
     Function(Fn<I>),
 
     /// References the binding at the given depth. The index is a [de
-    /// Bruijn index], so it counts back through the in-scope binders,
-    /// with 0 being the innermost binder. This is used in impls and
-    /// the like. For example, if we had a rule like `for<T> { (T:
-    /// Clone) :- (T: Copy) }`, then `T` would be represented as a
-    /// `BoundVar(0)` (as the `for` is the innermost binder).
-    ///
-    /// [de Bruijn index]: https://en.wikipedia.org/wiki/De_Bruijn_index
-    BoundVar(usize),
+    /// Bruijn index], so it counts back through the in-scope binders.
+    BoundVar(BoundVar),
 
     /// Inference variable defined in the current inference context.
     InferenceVar(InferenceVar),
@@ -271,6 +265,237 @@ impl<I: Interner> TyData<I> {
     }
 }
 
+/// Identifies a particular bound variable within a binder.
+/// Variables are identified by the combination of a [`DebruijnIndex`],
+/// which identifies the *binder*, and an index within that binder.
+///
+/// Consider this case:
+///
+/// ```ignore
+/// forall<'a, 'b> { forall<'c, 'd> { ... } }
+/// ```
+///
+/// Within the `...` term:
+///
+/// * the variable `'a` have a debruijn index of 1 and index 0
+/// * the variable `'b` have a debruijn index of 1 and index 1
+/// * the variable `'c` have a debruijn index of 0 and index 0
+/// * the variable `'d` have a debruijn index of 0 and index 1
+///
+/// The variables `'a` and `'b` both have debruijn index of 1 because,
+/// counting out, they are the 2nd binder enclosing `...`. The indices
+/// identify the location *within* that binder.
+///
+/// The variables `'c` and `'d` both have debruijn index of 0 because
+/// they appear in the *innermost* binder enclosing the `...`. The
+/// indices identify the location *within* that binder.
+#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
+pub struct BoundVar {
+    pub debruijn: DebruijnIndex,
+    pub index: usize,
+}
+
+impl BoundVar {
+    pub fn new(debruijn: DebruijnIndex, index: usize) -> Self {
+        Self { debruijn, index }
+    }
+
+    pub fn to_ty<I: Interner>(self, interner: &I) -> Ty<I> {
+        TyData::<I>::BoundVar(self).intern(interner)
+    }
+
+    pub fn to_lifetime<I: Interner>(self, interner: &I) -> Lifetime<I> {
+        LifetimeData::<I>::BoundVar(self).intern(interner)
+    }
+
+    /// True if this variable is bound within the `amount` innermost binders.
+    pub fn bound_within(self, outer_binder: DebruijnIndex) -> bool {
+        self.debruijn.within(outer_binder)
+    }
+
+    /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]).
+    #[must_use]
+    pub fn shifted_in(self) -> Self {
+        BoundVar::new(self.debruijn.shifted_in(), self.index)
+    }
+
+    /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]).
+    #[must_use]
+    pub fn shifted_in_from(self, outer_binder: DebruijnIndex) -> Self {
+        BoundVar::new(self.debruijn.shifted_in_from(outer_binder), self.index)
+    }
+
+    /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]).
+    #[must_use]
+    pub fn shifted_out(self) -> Option<Self> {
+        self.debruijn
+            .shifted_out()
+            .map(|db| BoundVar::new(db, self.index))
+    }
+
+    /// Adjusts the debruijn index (see [`DebruijnIndex::shifted_in`]).
+    #[must_use]
+    pub fn shifted_out_to(self, outer_binder: DebruijnIndex) -> Option<Self> {
+        self.debruijn
+            .shifted_out_to(outer_binder)
+            .map(|db| BoundVar::new(db, self.index))
+    }
+
+    /// Return the index of the bound variable, but only if it is bound
+    /// at the innermost binder. Otherwise, returns `None`.
+    pub fn index_if_innermost(self) -> Option<usize> {
+        self.index_if_bound_at(DebruijnIndex::INNERMOST)
+    }
+
+    /// Return the index of the bound variable, but only if it is bound
+    /// at the innermost binder. Otherwise, returns `None`.
+    pub fn index_if_bound_at(self, debruijn: DebruijnIndex) -> Option<usize> {
+        if self.debruijn == debruijn {
+            Some(self.index)
+        } else {
+            None
+        }
+    }
+}
+
+/// References the binder at the given depth. The index is a [de
+/// Bruijn index], so it counts back through the in-scope binders,
+/// with 0 being the innermost binder. This is used in impls and
+/// the like. For example, if we had a rule like `for<T> { (T:
+/// Clone) :- (T: Copy) }`, then `T` would be represented as a
+/// `BoundVar(0)` (as the `for` is the innermost binder).
+///
+/// [de Bruijn index]: https://en.wikipedia.org/wiki/De_Bruijn_index
+#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
+pub struct DebruijnIndex {
+    depth: u32,
+}
+
+impl DebruijnIndex {
+    pub const INNERMOST: DebruijnIndex = DebruijnIndex { depth: 0 };
+    pub const ONE: DebruijnIndex = DebruijnIndex { depth: 1 };
+
+    pub fn new(depth: u32) -> Self {
+        DebruijnIndex { depth }
+    }
+
+    pub fn depth(self) -> u32 {
+        self.depth
+    }
+
+    /// True if the binder identified by this index is within the
+    /// binder identified by the index `outer_binder`.
+    ///
+    /// # Example
+    ///
+    /// Imagine you have the following binders in scope
+    ///
+    /// ```ignore
+    /// forall<a> forall<b> forall<c>
+    /// ```
+    ///
+    /// then the Debruijn index for `c` would be `0`, the index for
+    /// `b` would be 1, and so on. Now consider the following calls:
+    ///
+    /// * `c.within(a) = true`
+    /// * `b.within(a) = true`
+    /// * `a.within(a) = false`
+    /// * `a.within(c) = false`
+    pub fn within(self, outer_binder: DebruijnIndex) -> bool {
+        self < outer_binder
+    }
+
+    /// Returns the resulting index when this value is moved into
+    /// through one binder.
+    #[must_use]
+    pub fn shifted_in(self) -> DebruijnIndex {
+        self.shifted_in_from(DebruijnIndex::ONE)
+    }
+
+    /// Update this index in place by shifting it "in" through
+    /// `amount` number of binders.
+    pub fn shift_in(&mut self) {
+        *self = self.shifted_in();
+    }
+
+    /// Adds `outer_binder` levels to the `self` index. Intuitively, this
+    /// shifts the `self` index, which was valid at the outer binder,
+    /// so that it is valid at the innermost binder.
+    ///
+    /// Example: Assume that the following binders are in scope:
+    ///
+    /// ```ignore
+    /// for<A> for<B> for<C> for<D>
+    ///            ^ outer binder
+    /// ```
+    ///
+    /// Assume further that the `outer_binder` argument is 2,
+    /// which means that it is referring to the `for<B>` binder
+    /// (since `D` would be the innermost binder).
+    ///
+    /// This means that `self` is relative to the binder `B` -- so
+    /// if `self` is 0 (`INNERMOST`), then it refers to `B`,
+    /// and if `self` is 1, then it refers to `A`.
+    ///
+    /// We will return as follows:
+    ///
+    /// * `0.shifted_in_from(2) = 2` -- i.e., `B`, when shifted in to the binding level `D`, has index 2
+    /// * `1.shifted_in_from(2) = 3` -- i.e., `A`, when shifted in to the binding level `D`, has index 3
+    /// * `2.shifted_in_from(1) = 3` -- here, we changed the `outer_binder`  to refer to `C`.
+    ///   Therefore `2` (relative to `C`) refers to `A`, so the result is still 3 (since `A`, relative to the
+    ///   innermost binder, has index 3).
+    #[must_use]
+    pub fn shifted_in_from(self, outer_binder: DebruijnIndex) -> DebruijnIndex {
+        DebruijnIndex::new(self.depth() + outer_binder.depth())
+    }
+
+    /// Returns the resulting index when this value is moved out from
+    /// `amount` number of new binders.
+    #[must_use]
+    pub fn shifted_out(self) -> Option<DebruijnIndex> {
+        self.shifted_out_to(DebruijnIndex::ONE)
+    }
+
+    /// Update in place by shifting out from `amount` binders.
+    pub fn shift_out(&mut self) {
+        *self = self.shifted_out().unwrap();
+    }
+
+    /// Subtracts `outer_binder` levels from the `self` index. Intuitively, this
+    /// shifts the `self` index, which was valid at the innermost
+    /// binder, to one that is valid at the binder `outer_binder`.
+    ///
+    /// This will return `None` if the `self` index is internal to the
+    /// outer binder (i.e., if `self < outer_binder`).
+    ///
+    /// Example: Assume that the following binders are in scope:
+    ///
+    /// ```ignore
+    /// for<A> for<B> for<C> for<D>
+    ///            ^ outer binder
+    /// ```
+    ///
+    /// Assume further that the `outer_binder` argument is 2,
+    /// which means that it is referring to the `for<B>` binder
+    /// (since `D` would be the innermost binder).
+    ///
+    /// This means that the result is relative to the binder `B` -- so
+    /// if `self` is 0 (`INNERMOST`), then it refers to `B`,
+    /// and if `self` is 1, then it refers to `A`.
+    ///
+    /// We will return as follows:
+    ///
+    /// * `1.shifted_out_to(2) = None` -- i.e., the binder for `C` can't be named from the binding level `B`
+    /// * `3.shifted_out_to(2) = Some(1)` -- i.e., `A`, when shifted out to the binding level `B`, has index 1
+    pub fn shifted_out_to(self, outer_binder: DebruijnIndex) -> Option<DebruijnIndex> {
+        if self.within(outer_binder) {
+            None
+        } else {
+            Some(DebruijnIndex::new(self.depth() - outer_binder.depth()))
+        }
+    }
+}
+
 /// A "DynTy" could be either a `dyn Trait` or an (opaque) `impl
 /// Trait`. Both of them are conceptually very related to a
 /// "existential type" of the form `exists<T> { T: Trait }`. The
@@ -372,7 +597,7 @@ impl<I: Interner> Lifetime<I> {
 #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
 pub enum LifetimeData<I: Interner> {
     /// See TyData::Var(_).
-    BoundVar(usize),
+    BoundVar(BoundVar),
     InferenceVar(InferenceVar),
     Placeholder(PlaceholderIndex),
     Phantom(Void, PhantomData<I>),
@@ -858,26 +1083,22 @@ impl<T> Binders<T> {
         }
     }
 
-    /// Introduces a fresh type variable at the start of the binders and returns new Binders with
-    /// the result of the operator function applied.
+    /// Creates a fresh binders that contains a single type
+    /// variable. The result of the closure will be embedded in this
+    /// binder. Note that you should be careful with what you return
+    /// from the closure to account for the binder that will be added.
     ///
-    /// forall<?0, ?1> will become forall<?0, ?1, ?2> where ?0 is the fresh variable
-    pub fn with_fresh_type_var<U, I>(
-        self,
-        interner: &I,
-        op: impl FnOnce(<T as Fold<I, I>>::Result, Ty<I>) -> U,
-    ) -> Binders<U>
+    /// XXX FIXME -- this is potentially a pretty footgun-y function.
+    pub fn with_fresh_type_var<I>(interner: &I, op: impl FnOnce(Ty<I>) -> T) -> Binders<T>
     where
         I: Interner,
-        T: Shift<I>,
     {
         // The new variable is at the front and everything afterwards is shifted up by 1
-        let new_var = TyData::<I>::BoundVar(0).intern(interner);
-        let value = op(self.value.shifted_in(interner, 1), new_var);
+        let new_var =
+            TyData::<I>::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(interner);
+        let value = op(new_var);
         Binders {
-            binders: iter::once(ParameterKind::Ty(()))
-                .chain(self.binders.iter().cloned())
-                .collect(),
+            binders: iter::once(ParameterKind::Ty(())).collect(),
             value,
         }
     }
@@ -966,20 +1187,28 @@ pub enum ProgramClause<I: Interner> {
     ForAll(Binders<ProgramClauseImplication<I>>),
 }
 
+impl<I: Interner> ProgramClauseImplication<I> {
+    pub fn into_from_env_clause(self, interner: &I) -> ProgramClauseImplication<I> {
+        if self.conditions.is_empty(interner) {
+            ProgramClauseImplication {
+                consequence: self.consequence.into_from_env_goal(interner),
+                conditions: self.conditions.clone(),
+            }
+        } else {
+            self
+        }
+    }
+}
+
 impl<I: Interner> ProgramClause<I> {
     pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
         match self {
             ProgramClause::Implies(implication) => {
-                if implication.conditions.is_empty(interner) {
-                    ProgramClause::Implies(ProgramClauseImplication {
-                        consequence: implication.consequence.into_from_env_goal(interner),
-                        conditions: Goals::new(interner),
-                    })
-                } else {
-                    ProgramClause::Implies(implication)
-                }
+                ProgramClause::Implies(implication.into_from_env_clause(interner))
+            }
+            ProgramClause::ForAll(binders_implication) => {
+                ProgramClause::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
             }
-            clause => clause,
         }
     }
 }
@@ -1113,23 +1342,19 @@ impl<I: Interner> Goal<I> {
         GoalData::Not(self).intern(interner)
     }
 
-    /// Takes a goal `G` and turns it into `compatible { G }`
+    /// Takes a goal `G` and turns it into `compatible { G }`.
     pub fn compatible(self, interner: &I) -> Self {
         // compatible { G } desugars into: forall<T> { if (Compatible, DownstreamType(T)) { G } }
         // This activates the compatible modality rules and introduces an anonymous downstream type
         GoalData::Quantified(
             QuantifierKind::ForAll,
-            Binders {
-                value: self,
-                binders: Vec::new(),
-            }
-            .with_fresh_type_var(interner, |goal, ty| {
+            Binders::with_fresh_type_var(interner, |ty| {
                 GoalData::Implies(
                     vec![
                         DomainGoal::Compatible(()).cast(interner),
                         DomainGoal::DownstreamType(ty).cast(interner),
                     ],
-                    goal,
+                    self.shifted_in(interner),
                 )
                 .intern(interner)
             }),
@@ -1306,18 +1531,19 @@ impl<I: Interner> Substitution<I> {
     /// Basically, each value is mapped to a type or lifetime with its
     /// same index.
     pub fn is_identity_subst(&self, interner: &I) -> bool {
-        self.iter(interner)
-            .zip(0..)
-            .all(|(parameter, index)| match parameter.data(interner) {
+        self.iter(interner).zip(0..).all(|(parameter, index)| {
+            let index_db = BoundVar::new(DebruijnIndex::INNERMOST, index);
+            match parameter.data(interner) {
                 ParameterKind::Ty(ty) => match ty.data(interner) {
-                    TyData::BoundVar(depth) => index == *depth,
+                    TyData::BoundVar(depth) => index_db == *depth,
                     _ => false,
                 },
                 ParameterKind::Lifetime(lifetime) => match lifetime.data(interner) {
-                    LifetimeData::BoundVar(depth) => index == *depth,
+                    LifetimeData::BoundVar(depth) => index_db == *depth,
                     _ => false,
                 },
-            })
+            }
+        })
     }
 
     pub fn apply<T>(&self, value: &T, interner: &I) -> T::Result
@@ -1330,7 +1556,7 @@ impl<I: Interner> Substitution<I> {
                     interner,
                     subst: self,
                 },
-                0,
+                DebruijnIndex::INNERMOST,
             )
             .unwrap()
     }
@@ -1392,18 +1618,26 @@ impl<'i, I: Interner> Folder<'i, I> for &SubstFolder<'i, I> {
         self
     }
 
-    fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible<Ty<I>> {
-        let interner = self.interner();
-        let ty = self.at(depth);
-        let ty = ty.assert_ty_ref(interner);
-        Ok(ty.shifted_in(interner, binders))
-    }
-
-    fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible<Lifetime<I>> {
-        let interner = self.interner();
-        let l = self.at(depth);
-        let l = l.assert_lifetime_ref(interner);
-        Ok(l.shifted_in(interner, binders))
+    fn fold_free_var_ty(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<I>> {
+        assert_eq!(bound_var.debruijn, DebruijnIndex::INNERMOST);
+        let ty = self.at(bound_var.index);
+        let ty = ty.assert_ty_ref(self.interner());
+        Ok(ty.shifted_in_from(self.interner(), outer_binder))
+    }
+
+    fn fold_free_var_lifetime(
+        &mut self,
+        bound_var: BoundVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Lifetime<I>> {
+        assert_eq!(bound_var.debruijn, DebruijnIndex::INNERMOST);
+        let l = self.at(bound_var.index);
+        let l = l.assert_lifetime_ref(self.interner());
+        Ok(l.shifted_in_from(self.interner(), outer_binder))
     }
 
     fn interner(&self) -> &'i I {
diff --git a/chalk-ir/src/macros.rs b/chalk-ir/src/macros.rs
index e4ff4e3a6ad..4c315ae9acc 100644
--- a/chalk-ir/src/macros.rs
+++ b/chalk-ir/src/macros.rs
@@ -34,8 +34,12 @@ macro_rules! ty {
         $crate::TyData::InferenceVar($crate::InferenceVar::from($b)).intern(&chalk_ir::interner::ChalkIr)
     };
 
+    (bound $d:tt $b:tt) => {
+        $crate::TyData::BoundVar($crate::BoundVar::new($crate::DebruijnIndex::new($d), $b)).intern(&chalk_ir::interner::ChalkIr)
+    };
+
     (bound $b:expr) => {
-        $crate::TyData::BoundVar($b).intern(&chalk_ir::interner::ChalkIr)
+        $crate::TyData::BoundVar($crate::BoundVar::new($crate::DebruijnIndex::INNERMOST, $b)).intern(&chalk_ir::interner::ChalkIr)
     };
 
     (expr $b:expr) => {
@@ -70,8 +74,12 @@ macro_rules! lifetime {
         $crate::LifetimeData::InferenceVar($crate::InferenceVar::from($b)).intern(&chalk_ir::interner::ChalkIr)
     };
 
+    (bound $d:tt $b:tt) => {
+        $crate::LifetimeData::BoundVar($crate::BoundVar::new($crate::DebruijnIndex::new($d), $b)).intern(&chalk_ir::interner::ChalkIr)
+    };
+
     (bound $b:expr) => {
-        $crate::LifetimeData::BoundVar($b).intern(&chalk_ir::interner::ChalkIr)
+        $crate::LifetimeData::BoundVar($crate::BoundVar::new($crate::DebruijnIndex::INNERMOST, $b)).intern(&chalk_ir::interner::ChalkIr)
     };
 
     (placeholder $b:expr) => {
diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs
index 77f4eda6c04..a6e7524b6e8 100644
--- a/chalk-rust-ir/src/lib.rs
+++ b/chalk-rust-ir/src/lib.rs
@@ -7,9 +7,9 @@ use chalk_ir::cast::Cast;
 use chalk_ir::fold::{shift::Shift, Fold, Folder};
 use chalk_ir::interner::{HasInterner, Interner, TargetInterner};
 use chalk_ir::{
-    AliasEq, AliasTy, AssocTypeId, Binders, ImplId, LifetimeData, Parameter, ParameterKind,
-    QuantifiedWhereClause, StructId, Substitution, TraitId, TraitRef, Ty, TyData, TypeName,
-    WhereClause,
+    AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData,
+    Parameter, ParameterKind, QuantifiedWhereClause, StructId, Substitution, TraitId, TraitRef, Ty,
+    TyData, TypeName, WhereClause,
 };
 use std::iter;
 
@@ -172,7 +172,7 @@ impl<I: Interner> IntoWhereClauses<I> for QuantifiedInlineBound<I> {
     type Output = QuantifiedWhereClause<I>;
 
     fn into_where_clauses(&self, interner: &I, self_ty: Ty<I>) -> Vec<QuantifiedWhereClause<I>> {
-        let self_ty = self_ty.shifted_in(interner, self.binders.len());
+        let self_ty = self_ty.shifted_in(interner);
         self.value
             .into_where_clauses(interner, self_ty)
             .into_iter()
@@ -265,17 +265,30 @@ pub trait ToParameter {
     /// the indices, and invoke `to_parameter()` on the `(binder,
     /// index)` pair. The result will be a reference to a bound
     /// variable of appropriate kind at the corresponding index.
-    fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I>;
+    fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
+        self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST)
+    }
+
+    fn to_parameter_at_depth<I: Interner>(
+        &self,
+        interner: &I,
+        debruijn: DebruijnIndex,
+    ) -> Parameter<I>;
 }
 
 impl<'a> ToParameter for (&'a ParameterKind<()>, usize) {
-    fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
+    fn to_parameter_at_depth<I: Interner>(
+        &self,
+        interner: &I,
+        debruijn: DebruijnIndex,
+    ) -> Parameter<I> {
         let &(binder, index) = self;
+        let bound_var = BoundVar::new(debruijn, index);
         match *binder {
-            ParameterKind::Lifetime(_) => LifetimeData::BoundVar(index)
+            ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var)
                 .intern(interner)
                 .cast(interner),
-            ParameterKind::Ty(_) => TyData::BoundVar(index).intern(interner).cast(interner),
+            ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner),
         }
     }
 }
diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs
index 42c08b54534..871f8d45bc5 100644
--- a/chalk-solve/src/clauses/builder.rs
+++ b/chalk-solve/src/clauses/builder.rs
@@ -85,19 +85,23 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
     pub fn push_binders<V>(&mut self, binders: &Binders<V>, op: impl FnOnce(&mut Self, V::Result))
     where
         V: Fold<I> + HasInterner<Interner = I>,
+        V::Result: std::fmt::Debug,
     {
-        let interner = self.interner();
+        debug_heading!("push_binders({:?})", binders);
+
         let old_len = self.binders.len();
+        let interner = self.interner();
         self.binders.extend(binders.binders.clone());
-        let params: Vec<_> = binders
-            .binders
-            .iter()
-            .zip(old_len..)
-            .map(|p| p.to_parameter(interner))
-            .collect();
-        self.parameters.extend(params);
+        self.parameters.extend(
+            binders
+                .binders
+                .iter()
+                .zip(old_len..)
+                .map(|p| p.to_parameter(interner)),
+        );
 
-        let value = binders.substitute(interner, &self.parameters[old_len..]);
+        let value = binders.substitute(self.interner(), &self.parameters[old_len..]);
+        debug!("push_binders: value={:?}", value);
         op(self, value);
 
         self.binders.truncate(old_len);
diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs
index 0e3a5ba6f1d..b99658e7133 100644
--- a/chalk-solve/src/clauses/env_elaborator.rs
+++ b/chalk-solve/src/clauses/env_elaborator.rs
@@ -44,12 +44,14 @@ impl<'me, I: Interner> EnvElaborator<'me, I> {
     }
 
     fn visit_alias_ty(&mut self, alias_ty: &AliasTy<I>) {
+        debug!("EnvElaborator::visit_alias_ty(alias_ty={:?})", alias_ty);
         self.db
             .associated_ty_data(alias_ty.associated_ty_id)
             .to_program_clauses(&mut self.builder);
     }
 
     fn visit_ty(&mut self, ty: &Ty<I>) {
+        debug!("EnvElaborator::visit_ty(ty={:?})", ty);
         let interner = self.db.interner();
         match ty.data(interner) {
             TyData::Apply(application_ty) => {
@@ -70,6 +72,7 @@ impl<'me, I: Interner> EnvElaborator<'me, I> {
     }
 
     fn visit_from_env(&mut self, from_env: &FromEnv<I>) {
+        debug!("EnvElaborator::visit_from_env(from_env={:?})", from_env);
         match from_env {
             FromEnv::Trait(trait_ref) => {
                 let trait_datum = self.db.trait_datum(trait_ref.trait_id);
@@ -90,6 +93,10 @@ impl<'me, I: Interner> EnvElaborator<'me, I> {
     }
 
     fn visit_domain_goal(&mut self, domain_goal: &DomainGoal<I>) {
+        debug!(
+            "EnvElaborator::visit_domain_goal(domain_goal={:?})",
+            domain_goal
+        );
         match domain_goal {
             DomainGoal::FromEnv(from_env) => self.visit_from_env(from_env),
             _ => {}
@@ -97,6 +104,7 @@ impl<'me, I: Interner> EnvElaborator<'me, I> {
     }
 
     fn visit_program_clause(&mut self, clause: &ProgramClause<I>) {
+        debug!("visit_program_clause(clause={:?})", clause);
         match clause {
             ProgramClause::Implies(clause) => self.visit_domain_goal(&clause.consequence),
             ProgramClause::ForAll(clause) => self.visit_domain_goal(&clause.value.consequence),
diff --git a/chalk-solve/src/coherence/solve.rs b/chalk-solve/src/coherence/solve.rs
index fc6dc3acd24..993009c6a18 100644
--- a/chalk-solve/src/coherence/solve.rs
+++ b/chalk-solve/src/coherence/solve.rs
@@ -63,38 +63,33 @@ impl<I: Interner> CoherenceSolver<'_, I> {
     // Examples:
     //
     //  Impls:
-    //      impl<T> Foo for T { }
-    //      impl Foo for i32 { }
+    //      impl<T> Foo for T { }   // rhs
+    //      impl Foo for i32 { }    // lhs
     //  Generates:
-    //      not { compatible { exists<T> { T = i32 } } }
+    //      not { compatible { exists<T> { exists<> { T = i32 } } } }
     //
     //  Impls:
-    //      impl<T1, U> Foo<T1> for Vec<U> { }
-    //      impl<T2> Foo<T2> for Vec<i32> { }
+    //      impl<T1, U> Foo<T1> for Vec<U> { }  // rhs
+    //      impl<T2> Foo<T2> for Vec<i32> { }   // lhs
     //  Generates:
-    //      not { compatible { exists<T1, U, T2> { Vec<U> = Vec<i32>, T1 = T2 } } }
+    //      not { compatible { exists<T1, U> { exists<T2> { Vec<U> = Vec<i32>, T1 = T2 } } } }
     //
     //  Impls:
     //      impl<T> Foo for Vec<T> where T: Bar { }
     //      impl<U> Foo for Vec<U> where U: Baz { }
     //  Generates:
-    //      not { compatible { exists<T, U> { Vec<T> = Vec<U>, T: Bar, U: Baz } } }
+    //      not { compatible { exists<T> { exists<U> { Vec<T> = Vec<U>, T: Bar, U: Baz } } } }
     //
     fn disjoint(&self, lhs: &ImplDatum<I>, rhs: &ImplDatum<I>) -> bool {
         debug_heading!("overlaps(lhs={:#?}, rhs={:#?})", lhs, rhs);
 
         let interner = self.db.interner();
-        let lhs_len = lhs.binders.len();
-
-        // Join the two impls' binders together
-        let mut binders = lhs.binders.binders.clone();
-        binders.extend(rhs.binders.binders.clone());
 
         // Upshift the rhs variables in params to account for the joined binders
         let lhs_params = params(interner, lhs).iter().cloned();
         let rhs_params = params(interner, rhs)
             .iter()
-            .map(|param| param.shifted_in(interner, lhs_len));
+            .map(|param| param.shifted_in(interner));
 
         // Create an equality goal for every input type the trait, attempting
         // to unify the inputs to both impls with one another
@@ -109,7 +104,7 @@ impl<I: Interner> CoherenceSolver<'_, I> {
             .value
             .where_clauses
             .iter()
-            .map(|wc| wc.shifted_in(interner, lhs_len));
+            .map(|wc| wc.shifted_in(interner));
 
         // Create a goal for each clause in both where clauses
         let wc_goals = lhs_where_clauses
@@ -119,7 +114,16 @@ impl<I: Interner> CoherenceSolver<'_, I> {
         // Join all the goals we've created together with And, then quantify them
         // over the joined binders. This is our query.
         let goal = Box::new(Goal::all(interner, params_goals.chain(wc_goals)))
-            .quantify(interner, QuantifierKind::Exists, binders)
+            .quantify(
+                interner,
+                QuantifierKind::Exists,
+                lhs.binders.binders.clone(),
+            )
+            .quantify(
+                interner,
+                QuantifierKind::Exists,
+                rhs.binders.binders.clone(),
+            )
             .compatible(interner)
             .negate(interner);
 
@@ -171,34 +175,49 @@ impl<I: Interner> CoherenceSolver<'_, I> {
             return false;
         }
 
-        let more_len = more_special.binders.len();
-
-        // Create parameter equality goals.
-        let more_special_params = params(interner, more_special).iter().cloned();
-        let less_special_params = params(interner, less_special)
+        // Create parameter equality goals. Note that parameters from
+        // the "more special" goal have to be "shifted in" across the
+        // binder for the "less special" impl.
+        let more_special_params = params(interner, more_special)
             .iter()
-            .map(|p| p.shifted_in(interner, more_len));
+            .map(|p| p.shifted_in(interner));
+        let less_special_params = params(interner, less_special).iter().cloned();
         let params_goals = more_special_params
             .zip(less_special_params)
             .map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
 
-        // Create the where clause goals.
-        let more_special_wc = more_special
+        // Create less special where clause goals. These reference the parameters
+        // from the "less special" impl, which are at the same debruijn depth here.
+        let less_special_wc = less_special
             .binders
             .value
             .where_clauses
             .iter()
             .cloned()
-            .casted(interner)
-            .collect();
-        let less_special_wc = less_special
+            .casted(interner);
+
+        // Create the "more special" where clause goals. These will be
+        // added as an implication without the "less special" goals in
+        // scope, no shift required.
+        let more_special_wc = more_special
             .binders
             .value
             .where_clauses
             .iter()
-            .map(|wc| wc.shifted_in(interner, more_len).cast(interner));
+            .cloned()
+            .casted(interner)
+            .collect();
 
-        // Join all of the goals together.
+        // Join all of the goals together:
+        //
+        // forall<..more special..> {
+        //   if (<more special wc>) {
+        //     exists<..less special..> {
+        //       ..less special goals..
+        //       ..equality goals..
+        //     }
+        //   }
+        // }
         let goal = Box::new(Goal::all(interner, params_goals.chain(less_special_wc)))
             .quantify(
                 interner,
diff --git a/chalk-solve/src/infer/canonicalize.rs b/chalk-solve/src/infer/canonicalize.rs
index ab86adbfa30..8fe71537ac7 100644
--- a/chalk-solve/src/infer/canonicalize.rs
+++ b/chalk-solve/src/infer/canonicalize.rs
@@ -38,7 +38,7 @@ impl<I: Interner> InferenceTable<I> {
             max_universe: UniverseIndex::root(),
             interner,
         };
-        let value = value.fold_with(&mut q, 0).unwrap();
+        let value = value.fold_with(&mut q, DebruijnIndex::INNERMOST).unwrap();
         let free_vars = q.free_vars.clone();
         let max_universe = q.max_universe;
 
@@ -107,7 +107,7 @@ where
     fn fold_free_placeholder_ty(
         &mut self,
         universe: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<I>> {
         let interner = self.interner;
         self.max_universe = max(self.max_universe, universe.ui);
@@ -117,7 +117,7 @@ where
     fn fold_free_placeholder_lifetime(
         &mut self,
         universe: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         let interner = self.interner;
         self.max_universe = max(self.max_universe, universe.ui);
@@ -128,14 +128,24 @@ where
         true
     }
 
-    fn fold_inference_ty(&mut self, var: InferenceVar, binders: usize) -> Fallible<Ty<I>> {
-        debug_heading!("fold_inference_ty(depth={:?}, binders={:?})", var, binders);
+    fn fold_inference_ty(
+        &mut self,
+        var: InferenceVar,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<I>> {
+        debug_heading!(
+            "fold_inference_ty(depth={:?}, binders={:?})",
+            var,
+            outer_binder
+        );
         let interner = self.interner;
         let var = EnaVariable::from(var);
         match self.table.probe_ty_var(interner, var) {
             Some(ty) => {
                 debug!("bound to {:?}", ty);
-                Ok(ty.fold_with(self, 0)?.shifted_in(interner, binders))
+                Ok(ty
+                    .fold_with(self, DebruijnIndex::INNERMOST)?
+                    .shifted_in_from(interner, outer_binder))
             }
             None => {
                 // If this variable is not yet bound, find its
@@ -143,9 +153,9 @@ where
                 // and then map `root_var` to a fresh index that is
                 // unique to this quantification.
                 let free_var = ParameterKind::Ty(self.table.unify.find(var));
-                let position = self.add(free_var);
-                debug!("not yet unified: position={:?}", position);
-                Ok(TyData::BoundVar(position + binders).intern(interner))
+                let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.add(free_var));
+                debug!("not yet unified: position={:?}", bound_var);
+                Ok(TyData::BoundVar(bound_var.shifted_in_from(outer_binder)).intern(interner))
             }
         }
     }
@@ -153,25 +163,29 @@ where
     fn fold_inference_lifetime(
         &mut self,
         var: InferenceVar,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         debug_heading!(
-            "fold_inference_lifetime(depth={:?}, binders={:?})",
+            "fold_inference_lifetime(depth={:?}, outer_binder={:?})",
             var,
-            binders
+            outer_binder
         );
         let interner = self.interner;
         let var = EnaVariable::from(var);
         match self.table.probe_lifetime_var(interner, var) {
             Some(l) => {
                 debug!("bound to {:?}", l);
-                Ok(l.fold_with(self, 0)?.shifted_in(interner, binders))
+                Ok(l.fold_with(self, DebruijnIndex::INNERMOST)?
+                    .shifted_in_from(interner, outer_binder))
             }
             None => {
                 let free_var = ParameterKind::Lifetime(self.table.unify.find(var));
-                let position = self.add(free_var);
-                debug!("not yet unified: position={:?}", position);
-                Ok(LifetimeData::BoundVar(position + binders).intern(interner))
+                let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.add(free_var));
+                debug!("not yet unified: position={:?}", bound_var);
+                Ok(
+                    LifetimeData::BoundVar(bound_var.shifted_in_from(outer_binder))
+                        .intern(interner),
+                )
             }
         }
     }
diff --git a/chalk-solve/src/infer/invert.rs b/chalk-solve/src/infer/invert.rs
index 2fbbae6b713..35ebe0a185d 100644
--- a/chalk-solve/src/infer/invert.rs
+++ b/chalk-solve/src/infer/invert.rs
@@ -91,7 +91,7 @@ impl<I: Interner> InferenceTable<I> {
         assert!(quantified.binders.is_empty());
         let inverted = quantified
             .value
-            .fold_with(&mut Inverter::new(interner, self), 0)
+            .fold_with(&mut Inverter::new(interner, self), DebruijnIndex::INNERMOST)
             .unwrap();
         Some(inverted)
     }
@@ -126,7 +126,7 @@ where
     fn fold_free_placeholder_ty(
         &mut self,
         universe: PlaceholderIndex,
-        binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<I>> {
         let table = &mut self.table;
         Ok(self
@@ -134,13 +134,13 @@ where
             .entry(universe)
             .or_insert_with(|| table.new_variable(universe.ui))
             .to_ty(self.interner())
-            .shifted_in(self.interner(), binders))
+            .shifted_in(self.interner()))
     }
 
     fn fold_free_placeholder_lifetime(
         &mut self,
         universe: PlaceholderIndex,
-        binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         let table = &mut self.table;
         Ok(self
@@ -148,7 +148,7 @@ where
             .entry(universe)
             .or_insert_with(|| table.new_variable(universe.ui))
             .to_lifetime(self.interner())
-            .shifted_in(self.interner(), binders))
+            .shifted_in(self.interner()))
     }
 
     fn forbid_free_vars(&self) -> bool {
diff --git a/chalk-solve/src/infer/normalize_deep.rs b/chalk-solve/src/infer/normalize_deep.rs
index 19dcf9cbf58..ae6aecf6d5c 100644
--- a/chalk-solve/src/infer/normalize_deep.rs
+++ b/chalk-solve/src/infer/normalize_deep.rs
@@ -25,7 +25,7 @@ impl<I: Interner> InferenceTable<I> {
                     interner,
                     table: self,
                 },
-                0,
+                DebruijnIndex::INNERMOST,
             )
             .unwrap()
     }
@@ -44,11 +44,17 @@ where
         self
     }
 
-    fn fold_inference_ty(&mut self, var: InferenceVar, binders: usize) -> Fallible<Ty<I>> {
+    fn fold_inference_ty(
+        &mut self,
+        var: InferenceVar,
+        _outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<I>> {
         let interner = self.interner;
         let var = EnaVariable::from(var);
         match self.table.probe_ty_var(interner, var) {
-            Some(ty) => Ok(ty.fold_with(self, 0)?.shifted_in(interner, binders)), // FIXME shift
+            Some(ty) => Ok(ty
+                .fold_with(self, DebruijnIndex::INNERMOST)?
+                .shifted_in(interner)), // FIXME shift
             None => Ok(var.to_ty(interner)),
         }
     }
@@ -56,12 +62,14 @@ where
     fn fold_inference_lifetime(
         &mut self,
         var: InferenceVar,
-        binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         let interner = self.interner;
         let var = EnaVariable::from(var);
         match self.table.probe_lifetime_var(interner, var) {
-            Some(l) => Ok(l.fold_with(self, 0)?.shifted_in(interner, binders)),
+            Some(l) => Ok(l
+                .fold_with(self, DebruijnIndex::INNERMOST)?
+                .shifted_in(interner)),
             None => Ok(var.to_lifetime(interner)), // FIXME shift
         }
     }
diff --git a/chalk-solve/src/infer/test.rs b/chalk-solve/src/infer/test.rs
index 8583abd23e6..4db887456ac 100644
--- a/chalk-solve/src/infer/test.rs
+++ b/chalk-solve/src/infer/test.rs
@@ -259,7 +259,7 @@ fn quantify_ty_under_binder() {
             )
             .quantified,
         Canonical {
-            value: ty!(function 3 (apply (item 0) (bound 1) (bound 3) (bound 3) (lifetime (bound 4)))),
+            value: ty!(function 3 (apply (item 0) (bound 1) (bound 1 0) (bound 1 0) (lifetime (bound 1 1)))),
             binders: vec![ParameterKind::Ty(U0), ParameterKind::Lifetime(U0)],
         }
     );
diff --git a/chalk-solve/src/infer/ucanonicalize.rs b/chalk-solve/src/infer/ucanonicalize.rs
index bcb17f9d542..385bd08c956 100644
--- a/chalk-solve/src/infer/ucanonicalize.rs
+++ b/chalk-solve/src/infer/ucanonicalize.rs
@@ -22,7 +22,7 @@ impl<I: Interner> InferenceTable<I> {
                     universes: &mut universes,
                     interner,
                 },
-                0,
+                DebruijnIndex::INNERMOST,
             )
             .unwrap();
 
@@ -36,7 +36,7 @@ impl<I: Interner> InferenceTable<I> {
                     universes: &universes,
                     interner,
                 },
-                0,
+                DebruijnIndex::INNERMOST,
             )
             .unwrap();
         let binders = value0
@@ -226,7 +226,7 @@ impl UniverseMap {
                     interner,
                     universes: self,
                 },
-                0,
+                DebruijnIndex::INNERMOST,
             )
             .unwrap()
     }
@@ -250,7 +250,7 @@ where
     fn fold_free_placeholder_ty(
         &mut self,
         universe: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<I>> {
         self.universes.add(universe.ui);
         Ok(universe.to_ty::<I>(self.interner()))
@@ -259,7 +259,7 @@ where
     fn fold_free_placeholder_lifetime(
         &mut self,
         universe: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         self.universes.add(universe.ui);
         Ok(universe.to_lifetime(self.interner()))
@@ -298,7 +298,7 @@ where
     fn fold_free_placeholder_ty(
         &mut self,
         universe0: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<I>> {
         let ui = self.universes.map_universe_to_canonical(universe0.ui);
         Ok(PlaceholderIndex {
@@ -311,7 +311,7 @@ where
     fn fold_free_placeholder_lifetime(
         &mut self,
         universe0: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         let universe = self.universes.map_universe_to_canonical(universe0.ui);
         Ok(PlaceholderIndex {
@@ -346,7 +346,7 @@ where
     fn fold_free_placeholder_ty(
         &mut self,
         universe0: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<I>> {
         let ui = self.universes.map_universe_from_canonical(universe0.ui);
         Ok(PlaceholderIndex {
@@ -359,7 +359,7 @@ where
     fn fold_free_placeholder_lifetime(
         &mut self,
         universe0: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         let universe = self.universes.map_universe_from_canonical(universe0.ui);
         Ok(PlaceholderIndex {
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
index 34fbabe124a..2bf1f00600e 100644
--- a/chalk-solve/src/infer/unify.rs
+++ b/chalk-solve/src/infer/unify.rs
@@ -255,7 +255,10 @@ impl<'t, I: Interner> Unifier<'t, I> {
         // as the variable is unified.
         let universe_index = self.table.universe_of_unbound_var(var);
 
-        let ty1 = ty.fold_with(&mut OccursCheck::new(self, var, universe_index), 0)?;
+        let ty1 = ty.fold_with(
+            &mut OccursCheck::new(self, var, universe_index),
+            DebruijnIndex::INNERMOST,
+        )?;
 
         self.table
             .unify
@@ -401,7 +404,7 @@ where
     fn fold_free_placeholder_ty(
         &mut self,
         universe: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<I>> {
         let interner = self.interner();
         if self.universe_index < universe.ui {
@@ -414,7 +417,7 @@ where
     fn fold_free_placeholder_lifetime(
         &mut self,
         ui: PlaceholderIndex,
-        _binders: usize,
+        _outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         let interner = self.interner();
         if self.universe_index < ui.ui {
@@ -444,14 +447,18 @@ where
         }
     }
 
-    fn fold_inference_ty(&mut self, var: InferenceVar, _binders: usize) -> Fallible<Ty<I>> {
+    fn fold_inference_ty(
+        &mut self,
+        var: InferenceVar,
+        _outer_binder: DebruijnIndex,
+    ) -> Fallible<Ty<I>> {
         let interner = self.interner();
         let var = EnaVariable::from(var);
         match self.unifier.table.unify.probe_value(var) {
             // If this variable already has a value, fold over that value instead.
             InferenceValue::Bound(normalized_ty) => {
                 let normalized_ty = normalized_ty.ty(interner).unwrap();
-                let normalized_ty = normalized_ty.fold_with(self, 0)?;
+                let normalized_ty = normalized_ty.fold_with(self, DebruijnIndex::INNERMOST)?;
                 assert!(!normalized_ty.needs_shift(interner));
                 Ok(normalized_ty)
             }
@@ -486,7 +493,7 @@ where
     fn fold_inference_lifetime(
         &mut self,
         var: InferenceVar,
-        binders: usize,
+        outer_binder: DebruijnIndex,
     ) -> Fallible<Lifetime<I>> {
         // a free existentially bound region; find the
         // inference variable it corresponds to
@@ -512,7 +519,7 @@ where
 
             InferenceValue::Bound(l) => {
                 let l = l.lifetime(interner).unwrap();
-                let l = l.fold_with(self, binders)?;
+                let l = l.fold_with(self, outer_binder)?;
                 assert!(!l.needs_shift(interner));
                 Ok(l.clone())
             }
diff --git a/chalk-solve/src/solve/slg/aggregate.rs b/chalk-solve/src/solve/slg/aggregate.rs
index 0763c1a46dd..bdd4068adcb 100644
--- a/chalk-solve/src/solve/slg/aggregate.rs
+++ b/chalk-solve/src/solve/slg/aggregate.rs
@@ -189,7 +189,13 @@ fn is_trivial<I: Interner>(interner: &I, subst: &Canonical<Substitution<I>>) ->
             // variables.
             ParameterKind::Ty(t) => match t.bound(interner) {
                 None => false,
-                Some(depth) => depth == index,
+                Some(bound_var) => {
+                    if let Some(index1) = bound_var.index_if_innermost() {
+                        index == index1
+                    } else {
+                        false
+                    }
+                }
             },
 
             // And no lifetime mappings. (This is too strict, but we never
diff --git a/chalk-solve/src/solve/slg/resolvent.rs b/chalk-solve/src/solve/slg/resolvent.rs
index e0cbd1c7218..b4967ba762a 100644
--- a/chalk-solve/src/solve/slg/resolvent.rs
+++ b/chalk-solve/src/solve/slg/resolvent.rs
@@ -269,8 +269,20 @@ struct AnswerSubstitutor<'t, I: Interner> {
     table: &'t mut InferenceTable<I>,
     environment: &'t Environment<I>,
     answer_subst: &'t Substitution<I>,
-    answer_binders: usize,
-    pending_binders: usize,
+
+    /// Tracks the debrujn index of the first binder that is outside
+    /// the term we are traversing. This starts as `DebruijnIndex::INNERMOST`,
+    /// since we have not yet traversed *any* binders, but when we visit
+    /// the inside of a binder, it would be incremented.
+    ///
+    /// Example: If we are visiting `(for<type> A, B, C, for<type> for<type> D)`,
+    /// then this would be:
+    ///
+    /// * `1`, when visiting `A`,
+    /// * `0`, when visiting `B` and `C`,
+    /// * `2`, when visiting `D`.
+    outer_binder: DebruijnIndex,
+
     ex_clause: &'t mut ExClause<SlgContext<I>>,
     interner: &'t I,
 }
@@ -291,8 +303,7 @@ impl<I: Interner> AnswerSubstitutor<'_, I> {
             environment,
             answer_subst,
             ex_clause,
-            answer_binders: 0,
-            pending_binders: 0,
+            outer_binder: DebruijnIndex::INNERMOST,
         };
         Zip::zip_with(&mut this, answer, pending)?;
         Ok(())
@@ -301,21 +312,21 @@ impl<I: Interner> AnswerSubstitutor<'_, I> {
     fn unify_free_answer_var(
         &mut self,
         interner: &I,
-        answer_depth: usize,
+        answer_var: BoundVar,
         pending: ParameterKind<&Ty<I>, &Lifetime<I>>,
     ) -> Fallible<bool> {
-        // This variable is bound in the answer, not free, so it
-        // doesn't represent a reference into the answer substitution.
-        if answer_depth < self.answer_binders {
-            return Ok(false);
-        }
+        let answer_index = match answer_var.index_if_bound_at(self.outer_binder) {
+            Some(index) => index,
+
+            // This variable is bound in the answer, not free, so it
+            // doesn't represent a reference into the answer substitution.
+            None => return Ok(false),
+        };
 
-        let answer_param = self
-            .answer_subst
-            .at(interner, answer_depth - self.answer_binders);
+        let answer_param = self.answer_subst.at(interner, answer_index);
 
         let pending_shifted = pending
-            .shifted_out(interner, self.pending_binders)
+            .shifted_out_to(interner, self.outer_binder)
             .unwrap_or_else(|_| {
                 panic!(
                     "truncate extracted a pending value that references internal binder: {:?}",
@@ -343,13 +354,29 @@ impl<I: Interner> AnswerSubstitutor<'_, I> {
     /// that case, there should be a corresponding bound variable in
     /// the pending goal. This bit of code just checks that latter
     /// case.
-    fn assert_matching_vars(&mut self, answer_depth: usize, pending_depth: usize) -> Fallible<()> {
-        assert!(answer_depth < self.answer_binders);
-        assert!(pending_depth < self.pending_binders);
-        assert_eq!(
-            self.answer_binders - answer_depth,
-            self.pending_binders - pending_depth
-        );
+    fn assert_matching_vars(
+        &mut self,
+        answer_var: BoundVar,
+        pending_var: BoundVar,
+    ) -> Fallible<()> {
+        let BoundVar {
+            debruijn: answer_depth,
+            index: answer_index,
+        } = answer_var;
+        let BoundVar {
+            debruijn: pending_depth,
+            index: pending_index,
+        } = pending_var;
+
+        // Both bound variables are bound within the term we are matching
+        assert!(answer_depth.within(self.outer_binder));
+
+        // They are bound at the same (relative) depth
+        assert_eq!(answer_depth, pending_depth);
+
+        // They are bound at the same index within the binder
+        assert_eq!(answer_index, pending_index,);
+
         Ok(())
     }
 }
@@ -390,11 +417,9 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
             }
 
             (TyData::Function(answer), TyData::Function(pending)) => {
-                self.answer_binders += answer.num_binders;
-                self.pending_binders += pending.num_binders;
+                self.outer_binder.shift_in();
                 Zip::zip_with(self, &answer.parameters, &pending.parameters)?;
-                self.answer_binders -= answer.num_binders;
-                self.pending_binders -= pending.num_binders;
+                self.outer_binder.shift_out();
                 Ok(())
             }
 
@@ -459,11 +484,9 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
     where
         T: Zip<I> + Fold<I, Result = T>,
     {
-        self.answer_binders += answer.binders.len();
-        self.pending_binders += pending.binders.len();
+        self.outer_binder.shift_in();
         Zip::zip_with(self, &answer.value, &pending.value)?;
-        self.answer_binders -= answer.binders.len();
-        self.pending_binders -= pending.binders.len();
+        self.outer_binder.shift_out();
         Ok(())
     }
 
diff --git a/chalk-solve/src/solve/truncate.rs b/chalk-solve/src/solve/truncate.rs
index 5809b435e43..966c1923bee 100644
--- a/chalk-solve/src/solve/truncate.rs
+++ b/chalk-solve/src/solve/truncate.rs
@@ -23,7 +23,7 @@ where
 
     let mut truncater = Truncater::new(interner, infer, max_size);
     let value = value
-        .fold_with(&mut truncater, 0)
+        .fold_with(&mut truncater, DebruijnIndex::INNERMOST)
         .expect("Truncater is infallible");
     debug!(
         "truncate: overflow={} value={:?}",
@@ -81,15 +81,15 @@ where
         self
     }
 
-    fn fold_ty(&mut self, ty: &Ty<I>, binders: usize) -> Fallible<Ty<I>> {
+    fn fold_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> Fallible<Ty<I>> {
         if let Some(normalized_ty) = self.infer.normalize_shallow(self.interner, ty) {
-            return self.fold_ty(&normalized_ty, binders);
+            return self.fold_ty(&normalized_ty, outer_binder);
         }
 
         let pre_size = self.current_size;
         self.current_size += 1;
 
-        let result = ty.super_fold_with(self, binders)?;
+        let result = ty.super_fold_with(self, outer_binder)?;
 
         // We wish to maintain the invariant that:
         //
@@ -102,7 +102,8 @@ where
         // a fresh existential variable (in the innermost universe).
         let post_size = self.current_size;
         let result = if pre_size < self.max_size && post_size > self.max_size {
-            self.overflow(pre_size).shifted_in(self.interner(), binders)
+            self.overflow(pre_size)
+                .shifted_in_from(self.interner(), outer_binder)
         } else {
             result
         };
@@ -116,8 +117,12 @@ where
         Ok(result)
     }
 
-    fn fold_lifetime(&mut self, lifetime: &Lifetime<I>, binders: usize) -> Fallible<Lifetime<I>> {
-        lifetime.super_fold_with(self, binders)
+    fn fold_lifetime(
+        &mut self,
+        lifetime: &Lifetime<I>,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Lifetime<I>> {
+        lifetime.super_fold_with(self, outer_binder)
     }
 
     fn interner(&self) -> &'i I {
diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs
index d4a76cb4880..c28641f6c14 100644
--- a/chalk-solve/src/wf.rs
+++ b/chalk-solve/src/wf.rs
@@ -5,6 +5,7 @@ use crate::solve::SolverChoice;
 use crate::split::Split;
 use crate::RustIrDatabase;
 use chalk_ir::cast::*;
+use chalk_ir::fold::shift::Shift;
 use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::*;
 use chalk_rust_ir::*;
@@ -40,6 +41,8 @@ pub struct WfSolver<'db, I: Interner> {
 }
 
 /// A trait for retrieving all types appearing in some Chalk construction.
+///
+/// FIXME: why is this not a `Folder`?
 trait FoldInputTypes: HasInterner {
     fn fold(&self, interner: &Self::Interner, accumulator: &mut Vec<Ty<Self::Interner>>);
 }
@@ -139,7 +142,18 @@ impl<I: Interner> FoldInputTypes for WhereClause<I> {
 
 impl<T: FoldInputTypes> FoldInputTypes for Binders<T> {
     fn fold(&self, interner: &T::Interner, accumulator: &mut Vec<Ty<T::Interner>>) {
-        self.value.fold(interner, accumulator);
+        // FIXME: This aspect of how we've formulated implied bounds
+        // seems to have an "eager normalization" problem, what about
+        // where clauses like `for<T> { <Self as Foo<T>>::Bar }`?
+        //
+        // For now, the unwrap will panic.
+        let mut types = vec![];
+        self.value.fold(interner, &mut types);
+        accumulator.extend(
+            types
+                .into_iter()
+                .map(|ty| ty.shifted_out(interner).unwrap()),
+        );
     }
 }
 
@@ -262,6 +276,7 @@ where
         // Things to prove well-formed: input types of the where-clauses, projection types
         // appearing in the header, associated type values, and of course the trait ref.
         let trait_ref_wf = DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()));
+        debug!("verify_trait_impl: input_types={:?}", input_types);
         let goals = input_types
             .into_iter()
             .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)).cast(interner))
@@ -269,6 +284,7 @@ where
             .chain(Some(trait_ref_wf).cast(interner));
 
         let goal = Goal::all(interner, goals);
+        debug!("verify_trait_impl: goal={:?}", goal);
 
         // Assumptions: types appearing in the header which are not projection types are
         // assumed to be well-formed, and where clauses declared on the impl are assumed
@@ -347,20 +363,28 @@ where
         let interner = self.db.interner();
         let assoc_ty = &self.db.associated_ty_value(assoc_ty_id);
 
-        // The substitutions for the binders on this associated type
-        // value. These would be placeholders like `'!a` and `!T`, in
-        // our example above.
-        //
-        // We begin with the associated type binders, as that `forall`
-        // is innermost, and then chain in the binders from the impl
-        // (which are generated by the caller).
-        let all_parameters: Vec<_> = assoc_ty
-            .value
-            .binders
-            .iter()
-            .zip(0..)
-            .map(|p| p.to_parameter(interner))
-            .collect();
+        // Split the binders on the assoc. ty value into those
+        // from the *impl* (in our example, `T`) and those from
+        // the associated type (in our example, `'a`).
+        let (impl_binders, value_binders) = self
+            .db
+            .split_associated_ty_value_parameters(&assoc_ty.value.binders, assoc_ty);
+
+        // In our final goal, the binders from the impl will be
+        // something like `^1.N` -- i.e., a debruijn index of 1 --
+        // and the binders from the associted type value will be `^0.N`.
+        let all_parameters: Vec<_> = {
+            let value_parameters = value_binders
+                .iter()
+                .zip(0..)
+                .map(|p| p.to_parameter(interner));
+            let impl_debruin = DebruijnIndex::INNERMOST.shifted_in();
+            let impl_parameters = impl_binders
+                .iter()
+                .zip(0..)
+                .map(|p| p.to_parameter_at_depth(interner, impl_debruin));
+            value_parameters.chain(impl_parameters).collect()
+        };
 
         // Get the projection for this associated type:
         //
@@ -435,13 +459,11 @@ where
 
         let goal = GoalData::Implies(hypotheses, goal).intern(interner);
 
+        debug!("compute_assoc_ty_goal: goal={:?}", goal);
+
         // Create a composed goal that is universally quantified over
         // the parameters from the associated type value (e.g.,
         // `forall<'a> { .. }` in our example).
-        let (_, value_binders) = self
-            .db
-            .split_associated_ty_value_parameters(&assoc_ty.value.binders, assoc_ty);
-
         Some(goal.quantify(interner, QuantifierKind::ForAll, value_binders.to_vec()))
     }
 }
diff --git a/tests/lowering/mod.rs b/tests/lowering/mod.rs
index 2a794dc2a9a..cac5bf492d1 100644
--- a/tests/lowering/mod.rs
+++ b/tests/lowering/mod.rs
@@ -162,7 +162,7 @@ fn goal_quantifiers() {
     db.with_program(|_| {
         assert_eq!(
             format!("{:?}", goal),
-            "ForAll<type> { Exists<type> { ForAll<type> { Implemented(^0: Foo<^1, ^2>) } } }"
+            "ForAll<type> { Exists<type> { ForAll<type> { Implemented(^0.0: Foo<^1.0, ^2.0>) } } }"
         );
     });
 }
@@ -197,7 +197,7 @@ fn atc_accounting() {
     impl_id: ImplId(#2),
     associated_ty_id: (Iterable::Iter),
     value: for<lifetime, type> AssociatedTyValueBound {
-        ty: Iter<'^0, ^1>
+        ty: Iter<'^0.0, ^0.1>
     },
 }"#
             .replace(",\n", "\n"),
@@ -215,8 +215,8 @@ fn atc_accounting() {
             "ForAll<type> { \
              ForAll<lifetime> { \
              ForAll<type> { \
-             all(AliasEq(<^2 as Iterable>::Iter<'^1> = ^0), \
-             Implemented(^2: Iterable)) \
+             all(AliasEq(<^2.0 as Iterable>::Iter<'^1.0> = ^0.0), \
+             Implemented(^2.0: Iterable)) \
              } \
              } \
              }"
diff --git a/tests/test/coinduction.rs b/tests/test/coinduction.rs
index 0bbb139b4e6..16026996476 100644
--- a/tests/test/coinduction.rs
+++ b/tests/test/coinduction.rs
@@ -165,7 +165,7 @@ fn coinductive_trivial_variant3() {
         goal {
             exists<T, U> { T: C1<U> }
         } yields {
-            r"Unique; for<?U0,?U0> { substitution [?0 := ^0, ?1 := ^1], lifetime constraints [] }"
+            r"Unique; for<?U0,?U0> { substitution [?0 := ^0.0, ?1 := ^0.1], lifetime constraints [] }"
         }
     }
 }
diff --git a/tests/test/impls.rs b/tests/test/impls.rs
index aeeae99f1e6..7c9cd168f61 100644
--- a/tests/test/impls.rs
+++ b/tests/test/impls.rs
@@ -350,7 +350,7 @@ fn definite_guidance() {
                 T: Debug
             }
         } yields {
-            "Ambiguous; definite substitution for<?U0> { [?0 := Foo<^0>] }"
+            "Ambiguous; definite substitution for<?U0> { [?0 := Foo<^0.0>] }"
         }
     }
 }
diff --git a/tests/test/misc.rs b/tests/test/misc.rs
index 9e35ed79bf9..a3d76bf00f7 100644
--- a/tests/test/misc.rs
+++ b/tests/test/misc.rs
@@ -154,7 +154,7 @@ fn only_draw_so_many_blow_up() {
         goal {
             exists<T> { T: Foo }
         } yields[SolverChoice::slg(10, Some(2))] {
-            "Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0>] }"
+            "Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"
         }
     }
 }
diff --git a/tests/test/projection.rs b/tests/test/projection.rs
index b52b417b1ae..bd8eb56e638 100644
--- a/tests/test/projection.rs
+++ b/tests/test/projection.rs
@@ -492,8 +492,8 @@ fn normalize_under_binder() {
             }
         } yields {
             "Unique; for<?U0> { \
-             substitution [?0 := Ref<'^0, I32>], \
-             lifetime constraints [InEnvironment { environment: Env([]), goal: '^0 == '!1_0 }] \
+             substitution [?0 := Ref<'^0.0, I32>], \
+             lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
              }"
         }
     }
@@ -523,7 +523,7 @@ fn normalize_under_binder_multi() {
             }
         } yields_all {
             "substitution [?0 := I32], lifetime constraints []",
-            "for<?U0,?U0> { substitution [?0 := (Deref::Item)<Ref<'^0, I32>, '^1>], lifetime constraints [InEnvironment { environment: Env([]), goal: '^0 == '!1_0 }, InEnvironment { environment: Env([]), goal: '^1 == '!1_0 }] }"
+            "for<?U0,?U0> { substitution [?0 := (Deref::Item)<Ref<'^0.0, I32>, '^0.1>], lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }, InEnvironment { environment: Env([]), goal: '^0.1 == '!1_0 }] }"
         }
 
         goal {
diff --git a/tests/test/unify.rs b/tests/test/unify.rs
index a060b89c8f5..2988fd9ef6f 100644
--- a/tests/test/unify.rs
+++ b/tests/test/unify.rs
@@ -82,7 +82,7 @@ fn unify_quantified_lifetimes() {
         program {
         }
 
-        // Check that `'a` (here, `'^0`) is not unified
+        // Check that `'a` (here, `'^0.0`) is not unified
         // with `'!1_0`, because they belong to incompatible
         // universes.
         goal {
@@ -93,8 +93,8 @@ fn unify_quantified_lifetimes() {
             }
         } yields {
             "Unique; for<?U0> { \
-             substitution [?0 := '^0], \
-             lifetime constraints [InEnvironment { environment: Env([]), goal: '^0 == '!1_0 }] \
+             substitution [?0 := '^0.0], \
+             lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
              }"
         }
 
@@ -110,8 +110,8 @@ fn unify_quantified_lifetimes() {
             }
         } yields {
             "Unique; for<?U0> { \
-             substitution [?0 := '^0, ?1 := '!1_0], \
-             lifetime constraints [InEnvironment { environment: Env([]), goal: '^0 == '!1_0 }] \
+             substitution [?0 := '^0.0, ?1 := '!1_0], \
+             lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
              }"
         }
     }
@@ -135,8 +135,8 @@ fn equality_binder() {
             }
         } yields {
             "Unique; for<?U1> { \
-                 substitution [?0 := '^0], \
-                 lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '^0 }] \
+                 substitution [?0 := '^0.0], \
+                 lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '^0.0 }] \
              }"
         }
     }
@@ -180,7 +180,7 @@ fn mixed_indices_unify() {
             }
         } yields {
             "Unique; for<?U0,?U0> { \
-                 substitution [?0 := '^0, ?1 := ^1, ?2 := ^1], \
+                 substitution [?0 := '^0.0, ?1 := ^0.1, ?2 := ^0.1], \
                  lifetime constraints []\
              }"
         }
@@ -207,7 +207,7 @@ fn mixed_indices_match_program() {
             }
         } yields {
             "Unique; for<?U0> { \
-                 substitution [?0 := '^0, ?1 := S, ?2 := S], \
+                 substitution [?0 := '^0.0, ?1 := S, ?2 := S], \
                  lifetime constraints [] \
              }"
         }
@@ -237,7 +237,7 @@ fn mixed_indices_normalize_application() {
                 }
             }
         } yields {
-            "Unique; for<?U0,?U0> { substitution [?0 := '^0, ?1 := ^1, ?2 := ^1], "
+            "Unique; for<?U0,?U0> { substitution [?0 := '^0.0, ?1 := ^0.1, ?2 := ^0.1], "
         }
     }
 }
@@ -265,7 +265,7 @@ fn mixed_indices_normalize_gat_application() {
             // Our GAT parameter <X> is mapped to ?0; all others appear left to right
             // in our Normalize(...) goal.
             "Unique; for<?U0,?U0,?U0> { \
-                substitution [?0 := ^0, ?1 := '^1, ?2 := ^2, ?3 := ^0, ?4 := ^2], "
+                substitution [?0 := ^0.0, ?1 := '^0.1, ?2 := ^0.2, ?3 := ^0.0, ?4 := ^0.2], "
         }
     }
 }