always introduce binders, even if they are empty

If we are counting binding levels, then this is important to keep the
debruijn indices from getting out of whack. In other words, `for ^1.0`
is very different from `^1.0`.

Author: nikomatsakis

chalk-integration/src/lowering.rs

@@ -1196,11 +1196,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();

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

@@ -308,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)
     }
 }
@@ -345,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<")?;

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,13 +93,18 @@ 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),
             _ => {}
         }
     }
 
     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),