diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 11eac166711..4a0bbef8319 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -1487,8 +1487,13 @@ impl<'forest, C: Context + 'forest, CO: ContextOps + 'forest> SolveState<'for /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is /// false, since `XXX` is not an auto trait. pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool { + debug_heading!("top_of_stack_is_coinductive_from(depth={:?})", depth); 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 50128308324..8521d005437 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -16,6 +16,7 @@ mod dyn_ty; mod env_elaborator; mod generalize; pub mod program_clauses; +pub mod syntactic_eq; /// For auto-traits, we generate a default rule for every struct, /// unless there is a manual impl for that struct given explicitly. @@ -242,9 +243,15 @@ fn program_clauses_that_could_match( .opaque_ty_data(opaque_ty.opaque_ty_id) .to_program_clauses(builder), }, - DomainGoal::WellFormed(WellFormed::Trait(trait_ref)) - | DomainGoal::LocalImplAllowed(trait_ref) => { - db.trait_datum(trait_ref.trait_id) + DomainGoal::LocalImplAllowed(trait_ref) => db + .trait_datum(trait_ref.trait_id) + .to_program_clauses(builder), + 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); } DomainGoal::ObjectSafe(trait_id) => { diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs index c1a20585e35..7c5408403de 100644 --- a/chalk-solve/src/clauses/builder.rs +++ b/chalk-solve/src/clauses/builder.rs @@ -2,6 +2,7 @@ use std::iter; 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; use chalk_ir::interner::{HasInterner, Interner}; @@ -77,18 +78,17 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> { priority, }; - if self.binders.len() == 0 { - self.clauses - .push(ProgramClauseData::Implies(clause).intern(interner)); + let clause = if self.binders.len() == 0 { + ProgramClauseData::Implies(clause).intern(interner) } else { - self.clauses.push( - ProgramClauseData::ForAll(Binders::new( - VariableKinds::from(interner, self.binders.clone()), - clause, - )) - .intern(interner), - ); - } + ProgramClauseData::ForAll(Binders::new( + VariableKinds::from(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/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index e7349654729..2e042e593cf 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -856,6 +856,7 @@ impl ToProgramClauses for AssociatedTyDatum { // add new type parameter U builder.push_bound_ty(|builder, ty| { + let alias = AliasTy::Projection(projection.clone()); // `Normalize(::Assoc -> U)` let normalize = Normalize { alias: AliasTy::Projection(projection.clone()), @@ -864,8 +865,8 @@ impl ToProgramClauses for AssociatedTyDatum { // `AliasEq(::Assoc = U)` let projection_eq = AliasEq { - alias: AliasTy::Projection(projection), - ty, + alias: alias.clone(), + ty: ty.clone(), }; // Projection equality rule from above. @@ -874,7 +875,7 @@ impl ToProgramClauses for AssociatedTyDatum { // AliasEq(::Assoc = U) :- // Normalize(::Assoc -> U). // } - builder.push_clause(projection_eq, Some(normalize)); + builder.push_clause(projection_eq.clone(), Some(normalize)); }); }); } diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs new file mode 100644 index 00000000000..ec7be31009d --- /dev/null +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -0,0 +1,165 @@ +use std::{iter, mem::replace}; + +use chalk_engine::fallible::Fallible; +use chalk_ir::{ + cast::Cast, + fold::{shift::Shift, Fold, Folder, SuperFold}, + interner::Interner, + AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, Goal, GoalData, Goals, ProgramClause, + ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, VariableKind, + VariableKinds, +}; + +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, + new_params: Vec>, + new_goals: Vec>, + 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 = TyData::BoundVar(bound_var).intern(interner); + match ty.data(interner) { + TyData::Alias(alias @ AliasTy::Projection(_)) => { + self.new_params.push(VariableKind::Ty); + self.new_goals.push( + AliasEq { + alias: alias.clone(), + ty: new_ty.clone(), + } + .cast(interner), + ); + self.binders_len += 1; + ty.super_fold_with(self, outer_binder)?; + Ok(new_ty) + } + TyData::Function(_) => Ok(ty.clone()), + _ => Ok(ty.super_fold_with(self, outer_binder)?), + } + } + + fn fold_program_clause( + &mut self, + clause: &ProgramClause, + outer_binder: DebruijnIndex, + ) -> Fallible> { + let interner = self.interner; + + let ((binders, implication), in_binders) = match clause.data(interner) { + ProgramClauseData::ForAll(for_all) => (for_all.clone().into(), true), + // introduce a dummy binder and shift implication through it + ProgramClauseData::Implies(implication) => ( + ( + VariableKinds::new(interner), + implication.shifted_in(interner), + ), + false, + ), + }; + let mut binders: Vec<_> = binders.as_slice(interner).clone().into(); + + let outer_binder = outer_binder.shifted_in(); + + self.binders_len = binders.len(); + let consequence = implication.consequence.fold_with(self, outer_binder)?; + // Immediately move `new_params` out of of the folder struct so it's safe + // to call `.fold_with` again + let new_params = replace(&mut self.new_params, vec![]); + let new_goals = replace(&mut self.new_goals, vec![]); + + let mut conditions = implication.conditions.fold_with(self, outer_binder)?; + if new_params.is_empty() && !in_binders { + // shift the clause out since we didn't use the dummy binder + return Ok(ProgramClauseData::Implies( + ProgramClauseImplication { + consequence, + conditions, + priority: implication.priority, + } + .shifted_out(interner)?, + ) + .intern(interner)); + } + + binders.extend(new_params.into_iter()); + + conditions = Goals::from( + interner, + conditions.iter(interner).cloned().chain(new_goals), + ); + + Ok(ProgramClauseData::ForAll(Binders::new( + VariableKinds::from(interner, binders), + ProgramClauseImplication { + consequence, + conditions, + priority: implication.priority, + }, + )) + .intern(interner)) + } + + fn fold_goal(&mut self, goal: &Goal, outer_binder: DebruijnIndex) -> Fallible> { + assert!(self.new_params.is_empty(), true); + + let interner = self.interner; + match goal.data(interner) { + GoalData::DomainGoal(_) | GoalData::EqGoal(_) => (), + _ => return goal.super_fold_with(self, outer_binder), + }; + + 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 = replace(&mut self.new_params, vec![]); + let new_goals = replace(&mut self.new_goals, vec![]); + + if new_params.is_empty() { + return Ok(goal.clone()); + } + + let goal = GoalData::All(Goals::from( + interner, + iter::once(syn_goal).into_iter().chain(new_goals), + )) + .intern(interner); + + Ok(GoalData::Quantified( + QuantifierKind::Exists, + Binders::new(VariableKinds::from(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 45bda7b9656..7d62f0b0189 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) { @@ -26,10 +38,33 @@ impl IsCoinductive for Goal { WhereClause::AliasEq(..) => 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 }