Count binders, not variables

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)?),* ))
                             }
                         }
                     }

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

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),
+        }))
     }
 }
 

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<")?;