From 031768f95d3f07c3e068d41f4fb54aaa7ca91b55 Mon Sep 17 00:00:00 2001 From: Mikhail Babenko Date: Thu, 16 Apr 2020 19:47:07 +0300 Subject: [PATCH 01/11] alias eq mvp --- chalk-solve/src/clauses.rs | 1 + chalk-solve/src/clauses/builder.rs | 14 +- chalk-solve/src/clauses/program_clauses.rs | 7 +- chalk-solve/src/clauses/syntactic_eq.rs | 160 +++++++++++++++++++++ chalk-solve/src/ext.rs | 8 +- 5 files changed, 178 insertions(+), 12 deletions(-) create mode 100644 chalk-solve/src/clauses/syntactic_eq.rs diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index ad2b7586095..200597c9cac 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> { 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/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index fc3026889a9..e3a2a07a994 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -869,6 +869,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()), @@ -877,8 +878,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. @@ -887,7 +888,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..f472af47ba1 --- /dev/null +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -0,0 +1,160 @@ +use std::{iter, mem::replace}; + +use chalk_ir::{ + cast::Cast, + fold::{shift::Shift, Fold, Folder, SuperFold}, + interner::Interner, + AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, Fallible, Goal, GoalData, Goals, + ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, TyKind, + 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(TyKind::General)); + 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 ProgramClauseData(binders) = clause.data(interner); + + let implication = binders.skip_binders(); + let mut binders: Vec<_> = binders.binders.as_slice(interner).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)?; + let constraints = implication.constraints.fold_with(self, outer_binder)?; + if new_params.is_empty() { + // shift the clause out since we didn't use the dummy binder + return Ok(ProgramClauseData(Binders::empty( + interner, + ProgramClauseImplication { + consequence, + conditions, + constraints, + priority: implication.priority, + } + .shifted_out(interner)?, + )) + .intern(interner)); + } + + 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(), 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_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/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 } From 0b021353786b158400004f0fd11b72ce5ac1d4b8 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Mon, 4 May 2020 21:12:21 +0000 Subject: [PATCH 02/11] expand coinductive reasoning --- chalk-engine/src/logic.rs | 5 ++++ chalk-solve/src/clauses.rs | 12 ++++++-- chalk-solve/src/coinductive_goal.rs | 43 ++++++++++++++++++++++++++--- 3 files changed, 54 insertions(+), 6 deletions(-) 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 200597c9cac..d38fca2e4ca 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -527,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/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, } } } From cdd88524d81c1bc9dabd32ed4d179b79954569d8 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Sat, 25 Jul 2020 13:10:36 -0400 Subject: [PATCH 03/11] Fixup program clause folding --- chalk-solve/src/clauses/syntactic_eq.rs | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs index f472af47ba1..b31e6910c5b 100644 --- a/chalk-solve/src/clauses/syntactic_eq.rs +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -81,20 +81,6 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { let mut conditions = implication.conditions.fold_with(self, outer_binder)?; let constraints = implication.constraints.fold_with(self, outer_binder)?; - if new_params.is_empty() { - // shift the clause out since we didn't use the dummy binder - return Ok(ProgramClauseData(Binders::empty( - interner, - ProgramClauseImplication { - consequence, - conditions, - constraints, - priority: implication.priority, - } - .shifted_out(interner)?, - )) - .intern(interner)); - } binders.extend(new_params.into_iter()); From 656146d15e2358fe57a498d5e1bf9fe43c8045ce Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Sat, 25 Jul 2020 13:21:54 -0400 Subject: [PATCH 04/11] Address review comments --- chalk-solve/src/clauses/syntactic_eq.rs | 51 ++++++++++++++++++++++--- 1 file changed, 46 insertions(+), 5 deletions(-) diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs index b31e6910c5b..f4766e154f1 100644 --- a/chalk-solve/src/clauses/syntactic_eq.rs +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -58,28 +58,68 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { } } + /// 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) :- + /// AliasEq(::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(); + // 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 `AliasEq(::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. 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 new_params = replace(&mut self.new_params, vec![]); + let mut new_goals = replace(&mut self.new_goals, vec![]); + + // Now fold the conditions (in our example, Implemented(X: Debug). + // The resulting list might be expanded to include new AliasEq goals. let mut conditions = implication.conditions.fold_with(self, outer_binder)?; + + new_params.extend(replace(&mut self.new_params, vec![])); + new_goals.extend(replace(&mut self.new_goals, vec![])); + let constraints = implication.constraints.fold_with(self, outer_binder)?; binders.extend(new_params.into_iter()); @@ -102,7 +142,8 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { } fn fold_goal(&mut self, goal: &Goal, outer_binder: DebruijnIndex) -> Fallible> { - assert!(self.new_params.is_empty(), true); + assert!(self.new_params.is_empty()); + assert!(self.new_goals.is_empty()); let interner = self.interner; match goal.data(interner) { From 9ac4195f7165805aea28c6995fda0493cc3b44e6 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Tue, 28 Jul 2020 18:32:50 -0400 Subject: [PATCH 05/11] Elaborate AliasEq goals --- chalk-solve/src/clauses/env_elaborator.rs | 39 ++++++++++++++--------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs index da7c9481e7e..b77d0954e63 100644 --- a/chalk-solve/src/clauses/env_elaborator.rs +++ b/chalk-solve/src/clauses/env_elaborator.rs @@ -1,12 +1,14 @@ use super::program_clauses::ToProgramClauses; use crate::clauses::builder::ClauseBuilder; use crate::clauses::{match_alias_ty, match_ty}; +use crate::AliasEq; use crate::DomainGoal; use crate::FromEnv; use crate::ProgramClause; use crate::RustIrDatabase; use crate::Ty; -use crate::{debug_span, TyKind}; +use crate::WhereClause; +use crate::{debug_span, TyData}; use chalk_ir::interner::Interner; use chalk_ir::visit::{Visit, Visitor}; use chalk_ir::{DebruijnIndex, Environment}; @@ -87,25 +89,32 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> { } fn visit_domain_goal(&mut self, domain_goal: &DomainGoal, outer_binder: DebruijnIndex) { - if let DomainGoal::FromEnv(from_env) = domain_goal { - debug_span!("visit_domain_goal", ?from_env); - match from_env { - FromEnv::Trait(trait_ref) => { - let trait_datum = self.db.trait_datum(trait_ref.trait_id); + match domain_goal { + DomainGoal::FromEnv(from_env) => { + debug_span!("visit_domain_goal", ?from_env); + match from_env { + 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(&mut self.builder, self.environment); - // If we know that `T: Iterator`, then we also know - // things about `::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); + // If we know that `T: Iterator`, then we also know + // things about `::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); + } } + FromEnv::Ty(ty) => ty.visit_with(self, outer_binder), } - FromEnv::Ty(ty) => ty.visit_with(self, outer_binder), } + DomainGoal::Holds(WhereClause::AliasEq(AliasEq { alias, ty })) => { + match_alias_ty(&mut self.builder, self.environment, alias); + ty.visit_with(self, outer_binder); + } + _ => {} } } } From 29da34503841798a4f03b4467eaeba6356d02269 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Tue, 28 Jul 2020 18:34:46 -0400 Subject: [PATCH 06/11] Update test --- tests/test/projection.rs | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) 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 []" } } } From 21804d87aed30e242ffa1ca047a6b55a4df0c829 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Sun, 2 Aug 2020 16:19:57 -0400 Subject: [PATCH 07/11] Cleanup/add comments --- chalk-solve/src/clauses/program_clauses.rs | 7 ++-- chalk-solve/src/clauses/syntactic_eq.rs | 37 +++++++++++++++------- 2 files changed, 29 insertions(+), 15 deletions(-) diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index e3a2a07a994..fc3026889a9 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -869,7 +869,6 @@ 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()), @@ -878,8 +877,8 @@ impl ToProgramClauses for AssociatedTyDatum { // `AliasEq(::Assoc = U)` let projection_eq = AliasEq { - alias: alias.clone(), - ty: ty.clone(), + alias: AliasTy::Projection(projection), + ty, }; // Projection equality rule from above. @@ -888,7 +887,7 @@ impl ToProgramClauses for AssociatedTyDatum { // AliasEq(::Assoc = U) :- // Normalize(::Assoc -> U). // } - builder.push_clause(projection_eq.clone(), Some(normalize)); + builder.push_clause(projection_eq, Some(normalize)); }); }); } diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs index f4766e154f1..608d5addb4d 100644 --- a/chalk-solve/src/clauses/syntactic_eq.rs +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -1,4 +1,4 @@ -use std::{iter, mem::replace}; +use std::{iter, mem::take}; use chalk_ir::{ cast::Cast, @@ -9,6 +9,9 @@ use chalk_ir::{ 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, @@ -24,8 +27,15 @@ pub fn syn_eq_lower>(interner: &I, clause: &T) -> { 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. `AliasEq(::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, } @@ -50,7 +60,6 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { .cast(interner), ); self.binders_len += 1; - ty.super_fold_with(self, outer_binder)?; Ok(new_ty) } TyData::Function(_) => Ok(ty.clone()), @@ -95,6 +104,9 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { // 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 // // ``` @@ -106,22 +118,23 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { // // 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. - self.binders_len = binders.len(); - let consequence = implication.consequence.fold_with(self, outer_binder)?; - let mut new_params = replace(&mut self.new_params, vec![]); - let mut new_goals = replace(&mut self.new_goals, vec![]); + + 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 AliasEq goals. - let mut conditions = implication.conditions.fold_with(self, outer_binder)?; - new_params.extend(replace(&mut self.new_params, vec![])); - new_goals.extend(replace(&mut self.new_goals, vec![])); + 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( @@ -151,14 +164,16 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { _ => 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 = replace(&mut self.new_params, vec![]); - let new_goals = replace(&mut self.new_goals, vec![]); + 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()); From a1e2c366bc459093069d9e32abf09d8bf3e69e8c Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Mon, 17 Aug 2020 00:46:55 -0400 Subject: [PATCH 08/11] Lower function types --- chalk-solve/src/clauses/syntactic_eq.rs | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs index 608d5addb4d..039a7e401fd 100644 --- a/chalk-solve/src/clauses/syntactic_eq.rs +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -4,7 +4,7 @@ use chalk_ir::{ cast::Cast, fold::{shift::Shift, Fold, Folder, SuperFold}, interner::Interner, - AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, Fallible, Goal, GoalData, Goals, + AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals, ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, TyKind, VariableKind, VariableKinds, }; @@ -62,8 +62,19 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { self.binders_len += 1; Ok(new_ty) } - TyData::Function(_) => Ok(ty.clone()), - _ => Ok(ty.super_fold_with(self, outer_binder)?), + TyData::Function(_) => { + self.new_params.push(VariableKind::Ty(TyKind::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), } } From 63484d5b1ba46b356ae1c19407e4eb4bffc62976 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Wed, 19 Aug 2020 13:56:06 -0400 Subject: [PATCH 09/11] Emit `EqGoal`s for projections / simplify --- chalk-solve/src/clauses/env_elaborator.rs | 37 +++++++++-------------- chalk-solve/src/clauses/syntactic_eq.rs | 16 ++-------- 2 files changed, 16 insertions(+), 37 deletions(-) diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs index b77d0954e63..30dfdc58308 100644 --- a/chalk-solve/src/clauses/env_elaborator.rs +++ b/chalk-solve/src/clauses/env_elaborator.rs @@ -1,13 +1,11 @@ use super::program_clauses::ToProgramClauses; use crate::clauses::builder::ClauseBuilder; use crate::clauses::{match_alias_ty, match_ty}; -use crate::AliasEq; use crate::DomainGoal; use crate::FromEnv; use crate::ProgramClause; use crate::RustIrDatabase; use crate::Ty; -use crate::WhereClause; use crate::{debug_span, TyData}; use chalk_ir::interner::Interner; use chalk_ir::visit::{Visit, Visitor}; @@ -89,32 +87,25 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> { } fn visit_domain_goal(&mut self, domain_goal: &DomainGoal, outer_binder: DebruijnIndex) { - match domain_goal { - DomainGoal::FromEnv(from_env) => { - debug_span!("visit_domain_goal", ?from_env); - match from_env { - FromEnv::Trait(trait_ref) => { - let trait_datum = self.db.trait_datum(trait_ref.trait_id); + if let DomainGoal::FromEnv(from_env) = domain_goal { + debug_span!("visit_domain_goal", ?from_env); + match from_env { + 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(&mut self.builder, self.environment); - // If we know that `T: Iterator`, then we also know - // things about `::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); - } + // If we know that `T: Iterator`, then we also know + // things about `::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); } - FromEnv::Ty(ty) => ty.visit_with(self, outer_binder), } + FromEnv::Ty(ty) => ty.visit_with(self, outer_binder), } - DomainGoal::Holds(WhereClause::AliasEq(AliasEq { alias, ty })) => { - match_alias_ty(&mut self.builder, self.environment, alias); - ty.visit_with(self, outer_binder); - } - _ => {} } } } diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs index 039a7e401fd..b96ee6aef5f 100644 --- a/chalk-solve/src/clauses/syntactic_eq.rs +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -4,7 +4,7 @@ use chalk_ir::{ cast::Cast, fold::{shift::Shift, Fold, Folder, SuperFold}, interner::Interner, - AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals, + AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals, ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, TyKind, VariableKind, VariableKinds, }; @@ -50,19 +50,7 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { let new_ty = TyData::BoundVar(bound_var).intern(interner); match ty.data(interner) { - TyData::Alias(alias @ AliasTy::Projection(_)) => { - self.new_params.push(VariableKind::Ty(TyKind::General)); - self.new_goals.push( - AliasEq { - alias: alias.clone(), - ty: new_ty.clone(), - } - .cast(interner), - ); - self.binders_len += 1; - Ok(new_ty) - } - TyData::Function(_) => { + TyData::Alias(AliasTy::Projection(_)) | TyData::Function(_) => { self.new_params.push(VariableKind::Ty(TyKind::General)); self.new_goals.push( EqGoal { From 25031cb1ab0238fc7fa7c20454cd584c19d68d5c Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Tue, 27 Oct 2020 11:55:17 -0400 Subject: [PATCH 10/11] Fixup --- chalk-solve/src/clauses/env_elaborator.rs | 2 +- chalk-solve/src/clauses/syntactic_eq.rs | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs index 30dfdc58308..da7c9481e7e 100644 --- a/chalk-solve/src/clauses/env_elaborator.rs +++ b/chalk-solve/src/clauses/env_elaborator.rs @@ -6,7 +6,7 @@ use crate::FromEnv; use crate::ProgramClause; use crate::RustIrDatabase; use crate::Ty; -use crate::{debug_span, TyData}; +use crate::{debug_span, TyKind}; use chalk_ir::interner::Interner; use chalk_ir::visit::{Visit, Visitor}; use chalk_ir::{DebruijnIndex, Environment}; diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs index b96ee6aef5f..07d72dbd3e8 100644 --- a/chalk-solve/src/clauses/syntactic_eq.rs +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -5,8 +5,8 @@ use chalk_ir::{ fold::{shift::Shift, Fold, Folder, SuperFold}, interner::Interner, AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals, - ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, TyKind, - VariableKind, VariableKinds, + ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyKind, + TyVariableKind, VariableKind, VariableKinds, }; /// Converts a set of clauses to require only syntactic equality. @@ -48,10 +48,11 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { 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(AliasTy::Projection(_)) | TyData::Function(_) => { - self.new_params.push(VariableKind::Ty(TyKind::General)); + 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), From 04f0e4de21ec08ba4824124b9c653ed84eae8c4a Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Tue, 27 Oct 2020 11:56:15 -0400 Subject: [PATCH 11/11] Fix comments --- chalk-solve/src/clauses/syntactic_eq.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/chalk-solve/src/clauses/syntactic_eq.rs b/chalk-solve/src/clauses/syntactic_eq.rs index 07d72dbd3e8..3ec369f47ac 100644 --- a/chalk-solve/src/clauses/syntactic_eq.rs +++ b/chalk-solve/src/clauses/syntactic_eq.rs @@ -31,7 +31,7 @@ struct SynEqFolder<'i, I: Interner> { /// 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. `AliasEq(::Item, X) + /// 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. @@ -83,7 +83,7 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { /// ```notrust /// forall { /// Implemented(Y: Debug) :- - /// AliasEq(::Item>, Y), + /// EqGoal(::Item>, Y), /// Implemented(X: Debug) /// } /// ``` @@ -114,7 +114,7 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { // ``` // // 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 `AliasEq(::Item, Y)` goals. + // 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. @@ -124,7 +124,7 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> { 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 AliasEq goals. + // 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));