There's an implicit binder around the env

chalk-solve/src/clauses.rs

@@ -949,6 +949,7 @@ fn match_alias_ty<I: Interner>(
     }
 }
 
+#[instrument(level = "debug", skip(db))]
 pub fn program_clauses_for_env<'db, I: Interner>(
     db: &'db dyn RustIrDatabase<I>,
     environment: &Environment<I>,

chalk-solve/src/clauses/builder.rs

@@ -16,6 +16,7 @@ pub struct ClauseBuilder<'me, I: Interner> {
     clauses: &'me mut Vec<ProgramClause<I>>,
     binders: Vec<VariableKind<I>>,
     parameters: Vec<GenericArg<I>>,
+    binder_depth: usize,
 }
 
 impl<'me, I: Interner> ClauseBuilder<'me, I> {
@@ -25,6 +26,7 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
             clauses,
             binders: vec![],
             parameters: vec![],
+            binder_depth: 0,
         }
     }
 
@@ -89,7 +91,7 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
             priority,
         };
 
-        let clause = if self.binders.is_empty() {
+        let clause = if self.binder_depth == 0 {
             // Compensate for the added empty binder
             clause.shifted_in(interner)
         } else {
@@ -148,12 +150,14 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
                 .zip(old_len..)
                 .map(|(pk, i)| (i, pk).to_generic_arg(interner)),
         );
+        self.binder_depth += 1;
         let value = binders.substitute(self.interner(), &self.parameters[old_len..]);
         debug!(?value);
         let res = op(self, value);
 
         self.binders.truncate(old_len);
         self.parameters.truncate(old_len);
+        self.binder_depth -= 1;
         res
     }
 

chalk-solve/src/clauses/env_elaborator.rs

@@ -9,7 +9,7 @@ use crate::Ty;
 use crate::{debug_span, TyKind};
 use chalk_ir::interner::Interner;
 use chalk_ir::visit::{ControlFlow, Visit, Visitor};
-use chalk_ir::{DebruijnIndex, Environment};
+use chalk_ir::{Binders, DebruijnIndex, Environment};
 use rustc_hash::FxHashSet;
 use tracing::instrument;
 
@@ -26,34 +26,29 @@ pub(super) fn elaborate_env_clauses<I: Interner>(
     environment: &Environment<I>,
 ) {
     let mut this_round = vec![];
-    in_clauses.visit_with(
-        &mut EnvElaborator::new(db, &mut this_round, environment),
-        DebruijnIndex::INNERMOST,
+    let mut builder = ClauseBuilder::new(db, &mut this_round);
+    // There's an implicit binders around the environment (from Canonical)
+    builder.push_binders(
+        Binders::empty(db.interner(), chalk_ir::Substitution::empty(db.interner())),
+        |builder, _| {
+            let mut elaborater = EnvElaborator {
+                db,
+                builder,
+                environment,
+            };
+            in_clauses.visit_with(&mut elaborater, DebruijnIndex::INNERMOST);
+        },
     );
     out.extend(this_round);
 }
 
-struct EnvElaborator<'me, I: Interner> {
+struct EnvElaborator<'me, 'builder, I: Interner> {
     db: &'me dyn RustIrDatabase<I>,
-    builder: ClauseBuilder<'me, I>,
+    builder: &'builder mut ClauseBuilder<'me, I>,
     environment: &'me Environment<I>,
 }
 
-impl<'me, I: Interner> EnvElaborator<'me, I> {
-    fn new(
-        db: &'me dyn RustIrDatabase<I>,
-        out: &'me mut Vec<ProgramClause<I>>,
-        environment: &'me Environment<I>,
-    ) -> Self {
-        EnvElaborator {
-            db,
-            builder: ClauseBuilder::new(db, out),
-            environment,
-        }
-    }
-}
-
-impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> {
+impl<'me, 'builder, I: Interner> Visitor<'me, I> for EnvElaborator<'me, 'builder, I> {
     type BreakTy = ();
 
     fn as_dyn(&mut self) -> &mut dyn Visitor<'me, I, BreakTy = Self::BreakTy> {
@@ -66,9 +61,7 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> {
     #[instrument(level = "debug", skip(self, _outer_binder))]
     fn visit_ty(&mut self, ty: &Ty<I>, _outer_binder: DebruijnIndex) -> ControlFlow<()> {
         match ty.kind(self.interner()) {
-            TyKind::Alias(alias_ty) => {
-                match_alias_ty(&mut self.builder, self.environment, alias_ty)
-            }
+            TyKind::Alias(alias_ty) => match_alias_ty(self.builder, self.environment, alias_ty),
             TyKind::Placeholder(_) => {}
 
             // FIXME(#203) -- We haven't fully figured out the implied
@@ -79,7 +72,7 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> {
 
             _ => {
                 // This shouldn't fail because of the above clauses
-                match_ty(&mut self.builder, self.environment, &ty)
+                match_ty(self.builder, self.environment, &ty)
                     .map_err(|_| ())
                     .unwrap()
             }
@@ -98,15 +91,15 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> {
                 FromEnv::Trait(trait_ref) => {
                     let trait_datum = self.db.trait_datum(trait_ref.trait_id);
 
-                    trait_datum.to_program_clauses(&mut self.builder, self.environment);
+                    trait_datum.to_program_clauses(self.builder, self.environment);
 
                     // If we know that `T: Iterator`, then we also know
                     // things about `<T as Iterator>::Item`, so push those
                     // implied bounds too:
                     for &associated_ty_id in &trait_datum.associated_ty_ids {
                         self.db
                             .associated_ty_data(associated_ty_id)
-                            .to_program_clauses(&mut self.builder, self.environment);
+                            .to_program_clauses(self.builder, self.environment);
                     }
                     ControlFlow::CONTINUE
                 }

tests/test/misc.rs

@@ -817,5 +817,14 @@ fn env_bound_vars() {
         } yields {
             "Unique"
         }
+        goal {
+            exists<'a> {
+                if (FromEnv(&'a ())) {
+                    WellFormed(&'a ())
+                }
+            }
+        } yields {
+            "Unique"
+        }
     }
 }