diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 1e7b25b4a44..ad4ddb14709 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -1571,9 +1571,14 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// would be true, since `Send` is an auto trait, which yields a /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is /// false, since `XXX` is not an auto trait. + #[instrument(level = "debug", skip(self))] pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool { StackIndex::iterate_range(self.stack.top_of_stack_from(depth)).all(|d| { let table = self.stack[d].table; + debug!( + "d = {:?}, table = {:?}", + d, self.forest.tables[table].table_goal + ); self.forest.tables[table].coinductive_goal }) } diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index ad2b7586095..d38fca2e4ca 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -18,6 +18,7 @@ mod dyn_ty; mod env_elaborator; mod generalize; pub mod program_clauses; +pub mod syntactic_eq; // yields the types "contained" in `app_ty` fn constituent_types(db: &dyn RustIrDatabase, ty: &TyKind) -> Vec> { @@ -526,11 +527,19 @@ fn program_clauses_that_could_match( }) }); } - DomainGoal::WellFormed(WellFormed::Trait(trait_ref)) - | DomainGoal::LocalImplAllowed(trait_ref) => { + DomainGoal::LocalImplAllowed(trait_ref) => { db.trait_datum(trait_ref.trait_id) .to_program_clauses(builder, environment); } + + DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => { + let self_ty = trait_predicate.self_type_parameter(interner); + if self_ty.bound_var(interner).is_some() || self_ty.inference_var(interner).is_some() { + return Err(Floundered); + } + db.trait_datum(trait_predicate.trait_id) + .to_program_clauses(builder, environment); + } DomainGoal::ObjectSafe(trait_id) => { if builder.db.is_object_safe(*trait_id) { builder.push_fact(DomainGoal::ObjectSafe(*trait_id)); diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs index 6fc3ad8b1e9..98a9f9a9f78 100644 --- a/chalk-solve/src/clauses/builder.rs +++ b/chalk-solve/src/clauses/builder.rs @@ -1,6 +1,7 @@ use std::marker::PhantomData; use crate::cast::{Cast, CastTo}; +use crate::clauses::syntactic_eq::syn_eq_lower; use crate::RustIrDatabase; use chalk_ir::fold::{Fold, Shift}; use chalk_ir::interner::{HasInterner, Interner}; @@ -95,14 +96,13 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> { } else { clause }; + let clause = ProgramClauseData(Binders::new( + VariableKinds::from_iter(interner, self.binders.clone()), + clause, + )) + .intern(interner); - self.clauses.push( - ProgramClauseData(Binders::new( - VariableKinds::from_iter(interner, self.binders.clone()), - clause, - )) - .intern(interner), - ); + self.clauses.push(syn_eq_lower(interner, &clause)); debug!("pushed clause {:?}", self.clauses.last()); } diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs new file mode 100644 index 00000000000..3ec369f47ac --- /dev/null +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -0,0 +1,202 @@ +use std::{iter, mem::take}; + +use chalk_ir::{ + cast::Cast, + fold::{shift::Shift, Fold, Folder, SuperFold}, + interner::Interner, + AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals, + ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyKind, + TyVariableKind, VariableKind, VariableKinds, +}; + +/// Converts a set of clauses to require only syntactic equality. +/// This is done by introducing new parameters and subgoals in cases +/// where semantic equality may diverge, for instance in unnormalized projections. +pub fn syn_eq_lower>(interner: &I, clause: &T) -> >::Result { + let mut folder = SynEqFolder { + interner, + new_params: vec![], + new_goals: vec![], + binders_len: 0, + }; + + clause + .fold_with(&mut folder, DebruijnIndex::INNERMOST) + .unwrap() +} + +struct SynEqFolder<'i, I: Interner> { + interner: &'i I, + /// Stores the kinds of new parameters introduced during folding. + /// The new parameters will either be added to an enclosing `exists` binder (when lowering a goal) + /// or to an enclosing `forall` binder (when lowering a program clause). + new_params: Vec>, + /// For each new parameter `X`, a new goal is introduced to define it, e.g. `EqGoal(::Item, X) + new_goals: Vec>, + + /// Stores the current number of variables in the binder we are adding parameters to. + /// Incremented for each new variable added. + binders_len: usize, +} + +impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { + fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> { + self + } + + fn fold_ty(&mut self, ty: &Ty, outer_binder: DebruijnIndex) -> Fallible> { + let interner = self.interner; + let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.binders_len); + + let new_ty = TyKind::BoundVar(bound_var).intern(interner); + match ty.kind(interner) { + TyKind::Alias(AliasTy::Projection(_)) | TyKind::Function(_) => { + self.new_params + .push(VariableKind::Ty(TyVariableKind::General)); + self.new_goals.push( + EqGoal { + a: new_ty.clone().cast(interner), + b: ty.clone().cast(interner), + } + .cast(interner), + ); + self.binders_len += 1; + Ok(new_ty) + } + _ => ty.super_fold_with(self, outer_binder), + } + } + + /// Convert a program clause to rem + /// + /// Consider this (nonsense) example: + /// + /// ```notrust + /// forall { + /// Implemented(::Item>: Debug) :- + /// Implemented(X: Debug) + /// } + /// ``` + /// + /// we would lower this into: + /// + /// ```notrust + /// forall { + /// Implemented(Y: Debug) :- + /// EqGoal(::Item>, Y), + /// Implemented(X: Debug) + /// } + /// ``` + fn fold_program_clause( + &mut self, + clause: &ProgramClause, + outer_binder: DebruijnIndex, + ) -> Fallible> { + let interner = self.interner; + assert!(self.new_params.is_empty()); + assert!(self.new_goals.is_empty()); + + let ProgramClauseData(binders) = clause.data(interner); + + let implication = binders.skip_binders(); + let mut binders: Vec<_> = binders.binders.as_slice(interner).into(); + + // Adjust the outer binder to account for the binder in the program clause + let outer_binder = outer_binder.shifted_in(); + + // Set binders_len to binders.len() since new parameters will be added into the existing forall<...> binder on the program clause. + self.binders_len = binders.len(); + + // First lower the "consequence" -- in our example that is + // + // ``` + // Implemented(::Item: Debug) + // ``` + // + // then save out the `new_params` and `new_goals` vectors to store any new variables created as a result. + // In this case, that would be the `Y` parameter and `EqGoal(::Item, Y)` goals. + // + // Note that these new parameters will have indices that come after the existing parameters, + // so any references to existing parameters like `X` in the "conditions" are still valid even if we insert new parameters. + let consequence = implication.consequence.fold_with(self, outer_binder)?; + + let mut new_params = take(&mut self.new_params); + let mut new_goals = take(&mut self.new_goals); + + // Now fold the conditions (in our example, Implemented(X: Debug). + // The resulting list might be expanded to include new EqGoal goals. + let mut conditions = implication.conditions.fold_with(self, outer_binder)?; + + new_params.extend(take(&mut self.new_params)); + new_goals.extend(take(&mut self.new_goals)); + + let constraints = implication.constraints.fold_with(self, outer_binder)?; + + new_params.extend(take(&mut self.new_params)); + new_goals.extend(take(&mut self.new_goals)); + + binders.extend(new_params.into_iter()); + + conditions = Goals::from_iter( + interner, + conditions.iter(interner).cloned().chain(new_goals), + ); + + Ok(ProgramClauseData(Binders::new( + VariableKinds::from_iter(interner, binders), + ProgramClauseImplication { + consequence, + conditions, + constraints, + priority: implication.priority, + }, + )) + .intern(interner)) + } + + fn fold_goal(&mut self, goal: &Goal, outer_binder: DebruijnIndex) -> Fallible> { + assert!(self.new_params.is_empty()); + assert!(self.new_goals.is_empty()); + + let interner = self.interner; + match goal.data(interner) { + GoalData::DomainGoal(_) | GoalData::EqGoal(_) => (), + _ => return goal.super_fold_with(self, outer_binder), + }; + + // Set binders_len to zero as in the exists<..> binder we will create, there are no existing variables. + self.binders_len = 0; + + // shifted in because we introduce a new binder + let outer_binder = outer_binder.shifted_in(); + let syn_goal = goal + .shifted_in(interner) + .super_fold_with(self, outer_binder)?; + let new_params = take(&mut self.new_params); + let new_goals = take(&mut self.new_goals); + + if new_params.is_empty() { + return Ok(goal.clone()); + } + + let goal = GoalData::All(Goals::from_iter( + interner, + iter::once(syn_goal).into_iter().chain(new_goals), + )) + .intern(interner); + + Ok(GoalData::Quantified( + QuantifierKind::Exists, + Binders::new(VariableKinds::from_iter(interner, new_params), goal), + ) + .intern(interner)) + } + + fn interner(&self) -> &'i I { + self.interner + } + + fn target_interner(&self) -> &'i I { + self.interner + } +} diff --git a/chalk-solve/src/coinductive_goal.rs b/chalk-solve/src/coinductive_goal.rs index cdb5cca108d..7d6eb0f49a7 100644 --- a/chalk-solve/src/coinductive_goal.rs +++ b/chalk-solve/src/coinductive_goal.rs @@ -15,6 +15,18 @@ pub trait IsCoinductive { } impl IsCoinductive for Goal { + /// A "coinductive" goal `G` is a goal where `G :- G` should be considered + /// true. When we are doing trait solving, if we encounter a cycle of goals + /// where solving `G1` requires `G2..Gn` and solving `Gn` requires `G1`, + /// then our behavior depends on whether each goal `Gi` in that cycle is + /// coinductive. + /// + /// If all the goals are coinductive, then `G1` is considered provable, + /// presuming that all the other subgoals for `G2..Gn` within can be fully + /// proven. + /// + /// If any goal `Gi` in the cycle is inductive, however, then the cycle is + /// considered unprovable. fn is_coinductive(&self, db: &dyn RustIrDatabase) -> bool { let interner = db.interner(); match self.data(interner) { @@ -28,10 +40,33 @@ impl IsCoinductive for Goal { WhereClause::TypeOutlives(..) => false, }, GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true, - GoalData::Quantified(QuantifierKind::ForAll, goal) => { - goal.skip_binders().is_coinductive(db) - } - _ => false, + GoalData::DomainGoal(_) => false, + + // Goals like `forall<..> { G }` or `... => G` we will consider to + // be coinductive if G is coinductive, although in practice I think + // it would be ok to simply consider them coinductive all the time. + GoalData::Quantified(_, goal) => goal.skip_binders().is_coinductive(db), + GoalData::Implies(_, goal) => goal.is_coinductive(db), + + // The "All(...)" quantifier is considered coinductive. This could + // be somewhat surprising as you might have `All(Gc, Gi)` where `Gc` + // is coinductive and `Gi` is inductive. This however is really no + // different than defining a fresh coinductive goal like + // + // ```notrust + // Gx :- Gc, Gi + // ``` + // + // and requiring `Gx` in place of `All(Gc, Gi)`, and that would be + // perfectly reasonable. + GoalData::All(..) => true, + + // For simplicity, just assume these remaining types of goals must + // be inductive, since there is no pressing reason to consider them + // coinductive. + GoalData::Not(_) => false, + GoalData::EqGoal(_) => false, + GoalData::CannotProve => false, } } } diff --git a/chalk-solve/src/ext.rs b/chalk-solve/src/ext.rs index 9d15d8c6c9b..462066763c0 100644 --- a/chalk-solve/src/ext.rs +++ b/chalk-solve/src/ext.rs @@ -1,3 +1,4 @@ +use crate::clauses::syntactic_eq::syn_eq_lower; use crate::infer::InferenceTable; use chalk_ir::fold::Fold; use chalk_ir::interner::{HasInterner, Interner}; @@ -89,7 +90,9 @@ impl GoalExt for Goal { } } }; - let canonical = infer.canonicalize(interner, &peeled_goal).quantified; + let canonical = infer + .canonicalize(interner, &syn_eq_lower(interner, &peeled_goal)) + .quantified; infer.u_canonicalize(interner, &canonical).quantified } @@ -104,7 +107,8 @@ impl GoalExt for Goal { /// Will panic if this goal does in fact contain free variables. fn into_closed_goal(self, interner: &I) -> UCanonical>> { let mut infer = InferenceTable::new(); - let env_goal = InEnvironment::new(&Environment::new(interner), self); + let lowered_goal = syn_eq_lower(interner, &self); + let env_goal = InEnvironment::new(&Environment::new(interner), &lowered_goal); let canonical_goal = infer.canonicalize(interner, &env_goal).quantified; infer.u_canonicalize(interner, &canonical_goal).quantified } diff --git a/tests/test/projection.rs b/tests/test/projection.rs index 25172b4a3cf..f1ce0111eb0 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -968,19 +968,6 @@ fn rust_analyzer_regression() { } } - //fn try_reduce_with(pi: PI, reduce_op: R) -> Option - // where - // PI: ParallelIterator, - // R: FnOnce(T::Ok) -> T, - // T: Try, - // { - // pi.drive_unindexed() - // } - // - // where `drive_unindexed` is a method in `ParallelIterator`: - // - // fn drive_unindexed(self) -> (); - goal { forall { if ( @@ -991,8 +978,8 @@ fn rust_analyzer_regression() { PI: ParallelIterator } } - } yields_first[SolverChoice::slg(4, None)] { - "Floundered" + } yields { + "Unique; substitution [], lifetime constraints []" } } }