diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index ea6851338e2..a4c4493504b 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -949,6 +949,7 @@ fn match_alias_ty( } } +#[instrument(level = "debug", skip(db))] pub fn program_clauses_for_env<'db, I: Interner>( db: &'db dyn RustIrDatabase, environment: &Environment, diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs index ae244927d3e..fb63fed1a2e 100644 --- a/chalk-solve/src/clauses/builder.rs +++ b/chalk-solve/src/clauses/builder.rs @@ -16,6 +16,7 @@ pub struct ClauseBuilder<'me, I: Interner> { clauses: &'me mut Vec>, binders: Vec>, parameters: Vec>, + 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 } diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs index de65c106ede..7182766ab4f 100644 --- a/chalk-solve/src/clauses/env_elaborator.rs +++ b/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( environment: &Environment, ) { 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, - builder: ClauseBuilder<'me, I>, + builder: &'builder mut ClauseBuilder<'me, I>, environment: &'me Environment, } -impl<'me, I: Interner> EnvElaborator<'me, I> { - fn new( - db: &'me dyn RustIrDatabase, - out: &'me mut Vec>, - environment: &'me Environment, - ) -> 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, _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,7 +91,7 @@ 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 `::Item`, so push those @@ -106,7 +99,7 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> { 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 } diff --git a/tests/test/misc.rs b/tests/test/misc.rs index b5dccc6af86..478eafc69c2 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -817,5 +817,14 @@ fn env_bound_vars() { } yields { "Unique" } + goal { + exists<'a> { + if (FromEnv(&'a ())) { + WellFormed(&'a ()) + } + } + } yields { + "Unique" + } } }