From f979cd1c6a2447a8c9df413eb5a3d94e1506a1a1 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 10 Mar 2022 16:35:11 -0500 Subject: [PATCH 1/6] start of a fix for rust-lang/chalk#727 --- chalk-recursive/src/combine.rs | 7 +- chalk-recursive/src/solve.rs | 7 +- chalk-solve/src/solve.rs | 57 +++++++++---- tests/test/ambiguity_issue_727.rs | 133 ++++++++++++++++++++++++++++++ tests/test/mod.rs | 1 + 5 files changed, 181 insertions(+), 24 deletions(-) create mode 100644 tests/test/ambiguity_issue_727.rs diff --git a/chalk-recursive/src/combine.rs b/chalk-recursive/src/combine.rs index a1bcde72b94..682af6d3bef 100644 --- a/chalk-recursive/src/combine.rs +++ b/chalk-recursive/src/combine.rs @@ -4,6 +4,7 @@ use tracing::debug; use chalk_ir::interner::Interner; use chalk_ir::{ClausePriority, DomainGoal, GenericArg}; +#[tracing::instrument(level = "Debug", skip(interner))] pub(super) fn with_priorities( interner: I, domain_goal: &DomainGoal, @@ -12,7 +13,7 @@ pub(super) fn with_priorities( b: Solution, prio_b: ClausePriority, ) -> (Solution, ClausePriority) { - match (prio_a, prio_b, a, b) { + let result = match (prio_a, prio_b, a, b) { (ClausePriority::High, ClausePriority::Low, higher, lower) | (ClausePriority::Low, ClausePriority::High, lower, higher) => { // if we have a high-priority solution and a low-priority solution, @@ -34,7 +35,9 @@ pub(super) fn with_priorities( } } (_, _, a, b) => (a.combine(b, interner), prio_a), - } + }; + debug!(?result, "combined result"); + result } fn calculate_inputs( diff --git a/chalk-recursive/src/solve.rs b/chalk-recursive/src/solve.rs index c5c4adbb070..a3212bafb09 100644 --- a/chalk-recursive/src/solve.rs +++ b/chalk-recursive/src/solve.rs @@ -154,11 +154,6 @@ trait SolveIterationHelpers: SolveDatabase { for program_clause in clauses { debug_span!("solve_from_clauses", clause = ?program_clause); - // If we have a completely ambiguous answer, it's not going to get better, so stop - if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) { - return Ok(Solution::Ambig(Guidance::Unknown)); - } - let ProgramClauseData(implication) = program_clause.data(self.interner()); let infer = infer.clone(); let subst = subst.clone(); @@ -187,8 +182,10 @@ trait SolveIterationHelpers: SolveDatabase { } if let Some((s, _)) = cur_solution { + debug!("solve_from_clauses: result = {:?}", s); Ok(s) } else { + debug!("solve_from_clauses: error"); Err(NoSolution) } } diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 96ef7ce51af..19389188650 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -44,23 +44,23 @@ impl Solution { /// There are multiple candidate solutions, which may or may not agree on /// the values for existential variables; attempt to combine them. This /// operation does not depend on the order of its arguments. - // - // This actually isn't as precise as it could be, in two ways: - // - // a. It might be that while there are multiple distinct candidates, they - // all agree about *some things*. To be maximally precise, we would - // compute the intersection of what they agree on. It's not clear though - // that this is actually what we want Rust's inference to do, and it's - // certainly not what it does today. - // - // b. There might also be an ambiguous candidate and a successful candidate, - // both with the same refined-goal. In that case, we could probably claim - // success, since if the conditions of the ambiguous candidate were met, - // we know the success would apply. Example: `?0: Clone` yields ambiguous - // candidate `Option: Clone` and successful candidate `Option: - // Clone`. - // - // But you get the idea. + /// + /// This actually isn't as precise as it could be, in two ways: + /// + /// a. It might be that while there are multiple distinct candidates, they + /// all agree about *some things*. To be maximally precise, we would + /// compute the intersection of what they agree on. It's not clear though + /// that this is actually what we want Rust's inference to do, and it's + /// certainly not what it does today. + /// + /// b. There might also be an ambiguous candidate and a successful candidate, + /// both with the same refined-goal. In that case, we could probably claim + /// success, since if the conditions of the ambiguous candidate were met, + /// we know the success would apply. Example: `?0: Clone` yields ambiguous + /// candidate `Option: Clone` and successful candidate `Option: + /// Clone`. + /// + /// But you get the idea. pub fn combine(self, other: Solution, interner: I) -> Solution { use self::Guidance::*; @@ -68,6 +68,19 @@ impl Solution { return self; } + // Special case hack: if one solution is "true" without any constraints, + // that is always the combined result. + // + // This is not as general as it could be: ideally, if we had one solution + // that is Unique with a simpler substitution than the other one, or region constraints + // which are a subset, we'd combine them. + if self.is_trivial_and_always_true(interner) { + return self; + } + if other.is_trivial_and_always_true(interner) { + return other; + } + debug!( "combine {} with {}", self.display(interner), @@ -88,6 +101,16 @@ impl Solution { Solution::Ambig(guidance) } + fn is_trivial_and_always_true(&self, interner: I) -> bool { + match self { + Solution::Unique(constrained_subst) => { + constrained_subst.value.subst.is_identity_subst(interner) + && constrained_subst.value.constraints.is_empty(interner) + } + Solution::Ambig(_) => false, + } + } + /// View this solution purely in terms of type inference guidance pub fn into_guidance(self) -> Guidance { match self { diff --git a/tests/test/ambiguity_issue_727.rs b/tests/test/ambiguity_issue_727.rs new file mode 100644 index 00000000000..64fbcbb2d8f --- /dev/null +++ b/tests/test/ambiguity_issue_727.rs @@ -0,0 +1,133 @@ +use super::*; + +#[test] +fn issue_727_1() { + test!( + program { + #[upstream] #[non_enumerable] #[lang(sized)] + trait Sized {} + + #[non_enumerable] #[object_safe] + trait Database {} + + #[non_enumerable] + trait QueryGroup + where + Self: Sized, + { + type DynDb: Database + HasQueryGroup; + } + + #[non_enumerable] #[object_safe] + trait HasQueryGroup + where + Self: Database, + G: QueryGroup, + G: Sized, + { } + + #[non_enumerable] #[object_safe] + trait HelloWorld + where + Self: HasQueryGroup, + { } + + struct HelloWorldStorage {} + + impl QueryGroup for HelloWorldStorage { + type DynDb = dyn HelloWorld + 'static; + } + impl HelloWorld for DB + where + DB: Database, + DB: HasQueryGroup, + DB: Sized, + { } + } + + goal { + forall { + if (FromEnv(T: Database); FromEnv(T: HasQueryGroup); FromEnv(T: Sized)) { + T: HelloWorld + } + } + } yields[SolverChoice::slg_default()] { // ok + expect![["Unique"]] + } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance" + expect![["Unique"]] + } + ); +} + +#[test] +fn issue_727_2() { + test!( + program { + #[non_enumerable] #[object_safe] + trait Database {} + + #[non_enumerable] + trait QueryGroup + { + type DynDb: Database + HasQueryGroup; + } + + #[non_enumerable] #[object_safe] + trait HasQueryGroup + where + Self: Database, + G: QueryGroup, + { } + + struct HelloWorldStorage {} + + impl QueryGroup for HelloWorldStorage { + type DynDb = dyn HasQueryGroup + 'static; + } + } + + goal { + forall { + if (FromEnv(T: HasQueryGroup)) { + T: Database + } + } + } yields[SolverChoice::slg_default()] { + expect![["Unique"]] + } yields[SolverChoice::recursive_default()] { + expect![["Unique"]] + } + ); +} + +#[test] +fn issue_727_3() { + test!( + program { + #[non_enumerable] + trait Database {} + + #[non_enumerable] + trait HasQueryGroup + where + Self: Database, + { } + + struct HelloWorldStorage {} + + impl Database for HelloWorldStorage { } + } + + goal { + forall { + if (FromEnv(HelloWorldStorage: HasQueryGroup); FromEnv(HelloWorldStorage: HasQueryGroup)) { + HelloWorldStorage: Database + } + } + } yields[SolverChoice::slg_default()] { + expect![["Unique"]] + } yields[SolverChoice::recursive_default()] { + expect![["Unique"]] + } + ); +} diff --git a/tests/test/mod.rs b/tests/test/mod.rs index 824b00cd598..6ce285eb979 100644 --- a/tests/test/mod.rs +++ b/tests/test/mod.rs @@ -404,6 +404,7 @@ fn solve_aggregated( expected.assert_eq(head); } +mod ambiguity_issue_727; mod arrays; mod auto_traits; mod closures; From d55a9a238443eb443c838fa533e0fe6d90a2beb4 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 10 Mar 2022 16:36:00 -0500 Subject: [PATCH 2/6] mark the failing test as "WIP" --- tests/test/ambiguity_issue_727.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test/ambiguity_issue_727.rs b/tests/test/ambiguity_issue_727.rs index 64fbcbb2d8f..6c8981fac38 100644 --- a/tests/test/ambiguity_issue_727.rs +++ b/tests/test/ambiguity_issue_727.rs @@ -95,7 +95,7 @@ fn issue_727_2() { } yields[SolverChoice::slg_default()] { expect![["Unique"]] } yields[SolverChoice::recursive_default()] { - expect![["Unique"]] + expect![[r#"Ambiguous; no inference guidance"#]] // FIXME rust-lang/chalk#727 } ); } From 2e759c19c6fda25e0bb62bd21e18df727cc63f7c Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 15 Mar 2022 20:03:52 -0400 Subject: [PATCH 3/6] fix tests I inspected the results, seems good --- tests/test/misc.rs | 8 +++++--- tests/test/mod.rs | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/tests/test/misc.rs b/tests/test/misc.rs index 198c3c437ee..e96e5ef1191 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -749,7 +749,7 @@ fn empty_definite_guidance() { } yields[SolverChoice::slg_default()] { expect![["Unique"]] } yields[SolverChoice::recursive_default()] { - expect![["Ambiguous; suggested substitution []"]] + expect![[r#"Unique"#]] } } } @@ -812,8 +812,10 @@ fn env_bound_vars() { WellFormed(&'a ()) } } - } yields { + } yields[SolverChoice::slg_default()] { expect![["Ambiguous; definite substitution for { [?0 := '^0.0] }"]] + } yields[SolverChoice::recursive_default()] { + expect![[r#"Unique; for { substitution [?0 := '^0.0] }"#]] } goal { exists<'a> { @@ -841,7 +843,7 @@ fn recursive_hang() { } yields[SolverChoice::slg_default()] { expect![["Ambiguous; definite substitution for { [?0 := ^0.0, ?1 := '^0.1] }"]] } yields[SolverChoice::recursive_default()] { - expect![["Ambiguous; suggested substitution for { [?0 := ^0.0, ?1 := '^0.1] }"]] + expect![[r#"Ambiguous; no inference guidance"#]] } } } diff --git a/tests/test/mod.rs b/tests/test/mod.rs index 6ce285eb979..423e7e954e1 100644 --- a/tests/test/mod.rs +++ b/tests/test/mod.rs @@ -394,11 +394,11 @@ fn solve_aggregated( .expect("Test requires at least one solver"); for (i, other) in tail.iter().enumerate() { println!( - "\ncomparing solvers:\n\tleft: {:?}\n\tright: {:?}\n", + "\ncomparing solvers:\n\texpected: {:?}\n\tactual: {:?}\n", &choices[0], &choices[i + 1] ); - assert_same(head, other); + assert_same(other, head); } expected.assert_eq(head); From a5083eb43e4916b8dcce877041fea630f4d1b2e2 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 15 Mar 2022 20:14:18 -0400 Subject: [PATCH 4/6] add a fast path --- chalk-recursive/src/solve.rs | 6 ++++++ chalk-solve/src/solve.rs | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/chalk-recursive/src/solve.rs b/chalk-recursive/src/solve.rs index a3212bafb09..47db7080ab3 100644 --- a/chalk-recursive/src/solve.rs +++ b/chalk-recursive/src/solve.rs @@ -179,6 +179,12 @@ trait SolveIterationHelpers: SolveDatabase { } else { debug!("Error"); } + + if let Some((cur_solution, _)) = &cur_solution { + if cur_solution.is_trivial_and_always_true(self.interner()) { + break; + } + } } if let Some((s, _)) = cur_solution { diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 19389188650..0734fc53ea3 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -101,7 +101,7 @@ impl Solution { Solution::Ambig(guidance) } - fn is_trivial_and_always_true(&self, interner: I) -> bool { + pub fn is_trivial_and_always_true(&self, interner: I) -> bool { match self { Solution::Unique(constrained_subst) => { constrained_subst.value.subst.is_identity_subst(interner) From 502d989b0442540ca542c830af5ca6dfc0fe9f8d Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 18 Mar 2022 16:29:12 -0400 Subject: [PATCH 5/6] extend SLG solver with a similar optimization --- chalk-engine/src/slg/aggregate.rs | 23 ++++++++++++++++++++++- chalk-ir/src/lib.rs | 9 +++++++++ chalk-solve/src/solve.rs | 7 +++---- tests/test/misc.rs | 4 +--- 4 files changed, 35 insertions(+), 8 deletions(-) diff --git a/chalk-engine/src/slg/aggregate.rs b/chalk-engine/src/slg/aggregate.rs index cce4e14dd61..b15b9f21c28 100644 --- a/chalk-engine/src/slg/aggregate.rs +++ b/chalk-engine/src/slg/aggregate.rs @@ -46,8 +46,16 @@ impl AggregateOps for SlgContextOps<'_, I> { } }; + // If the answer is trivially true and thus subsumes all others, then that's a unique-enough answer for us :) + if subst.value.is_identity_subst_with_no_constraints(interner) { + return Some(Solution::Unique(subst)); + } + + tracing::debug!("subst = {:?}", subst); + // Exactly 1 unconditional answer? let next_answer = answers.peek_answer(&should_continue); + tracing::debug!("next_answer = {:?}", next_answer); if next_answer.is_quantum_exceeded() { if subst.value.subst.is_identity_subst(interner) { return Some(Solution::Ambig(Guidance::Unknown)); @@ -83,9 +91,11 @@ impl AggregateOps for SlgContextOps<'_, I> { break Guidance::Unknown; } + // FIXME: This may cause us to miss some "trivially true" answers maybe? Haven't investigated very deeply. if !answers .any_future_answer(|ref mut new_subst| new_subst.may_invalidate(interner, &subst)) { + tracing::debug!("any_future_answer: false"); break Guidance::Definite(subst); } @@ -96,7 +106,17 @@ impl AggregateOps for SlgContextOps<'_, I> { } let new_subst = match answers.next_answer(&should_continue) { - AnswerResult::Answer(answer1) => answer1.subst, + AnswerResult::Answer(answer1) => { + if answer1 + .subst + .value + .is_identity_subst_with_no_constraints(interner) + { + // If the answer is trivially true and thus subsumes all others, then that's a unique-enough answer for us :) + return Some(Solution::Unique(answer1.subst)); + } + answer1.subst + } AnswerResult::Floundered => { // FIXME: this doesn't trigger for any current tests self.identity_constrained_subst(root_goal) @@ -108,6 +128,7 @@ impl AggregateOps for SlgContextOps<'_, I> { break Guidance::Suggested(subst); } }; + tracing::debug!("new_subst = {:?}", new_subst); subst = merge_into_guidance(interner, &root_goal.canonical, subst, &new_subst); num_answers += 1; }; diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 9376a6563b0..96351648e13 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -3048,6 +3048,15 @@ pub struct ConstrainedSubst { pub constraints: Constraints, } +impl ConstrainedSubst { + /// True if this is an identity subst (it maps variable 0 to variable 0 etc) + /// and has no constraints. This represents an "unconditionally true" answer which + /// is a convenient thing to recognize. + pub fn is_identity_subst_with_no_constraints(&self, interner: I) -> bool { + self.subst.is_identity_subst(interner) && self.constraints.is_empty(interner) + } +} + /// The resulting substitution after solving a goal. #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub struct AnswerSubst { diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 0734fc53ea3..7e6bcb0226f 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -103,10 +103,9 @@ impl Solution { pub fn is_trivial_and_always_true(&self, interner: I) -> bool { match self { - Solution::Unique(constrained_subst) => { - constrained_subst.value.subst.is_identity_subst(interner) - && constrained_subst.value.constraints.is_empty(interner) - } + Solution::Unique(constrained_subst) => constrained_subst + .value + .is_identity_subst_with_no_constraints(interner), Solution::Ambig(_) => false, } } diff --git a/tests/test/misc.rs b/tests/test/misc.rs index e96e5ef1191..b75ba3387e1 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -812,9 +812,7 @@ fn env_bound_vars() { WellFormed(&'a ()) } } - } yields[SolverChoice::slg_default()] { - expect![["Ambiguous; definite substitution for { [?0 := '^0.0] }"]] - } yields[SolverChoice::recursive_default()] { + } yields { expect![[r#"Unique; for { substitution [?0 := '^0.0] }"#]] } goal { From 70b2fdbd7a172c07e0dabaa7c275f4ab94e033a1 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 12 Apr 2022 11:24:03 -0400 Subject: [PATCH 6/6] Revert "extend SLG solver with a similar optimization" This reverts commit 502d989b0442540ca542c830af5ca6dfc0fe9f8d. --- chalk-engine/src/slg/aggregate.rs | 23 +---------------------- chalk-ir/src/lib.rs | 9 --------- chalk-solve/src/solve.rs | 7 ++++--- tests/test/misc.rs | 4 +++- 4 files changed, 8 insertions(+), 35 deletions(-) diff --git a/chalk-engine/src/slg/aggregate.rs b/chalk-engine/src/slg/aggregate.rs index b15b9f21c28..cce4e14dd61 100644 --- a/chalk-engine/src/slg/aggregate.rs +++ b/chalk-engine/src/slg/aggregate.rs @@ -46,16 +46,8 @@ impl AggregateOps for SlgContextOps<'_, I> { } }; - // If the answer is trivially true and thus subsumes all others, then that's a unique-enough answer for us :) - if subst.value.is_identity_subst_with_no_constraints(interner) { - return Some(Solution::Unique(subst)); - } - - tracing::debug!("subst = {:?}", subst); - // Exactly 1 unconditional answer? let next_answer = answers.peek_answer(&should_continue); - tracing::debug!("next_answer = {:?}", next_answer); if next_answer.is_quantum_exceeded() { if subst.value.subst.is_identity_subst(interner) { return Some(Solution::Ambig(Guidance::Unknown)); @@ -91,11 +83,9 @@ impl AggregateOps for SlgContextOps<'_, I> { break Guidance::Unknown; } - // FIXME: This may cause us to miss some "trivially true" answers maybe? Haven't investigated very deeply. if !answers .any_future_answer(|ref mut new_subst| new_subst.may_invalidate(interner, &subst)) { - tracing::debug!("any_future_answer: false"); break Guidance::Definite(subst); } @@ -106,17 +96,7 @@ impl AggregateOps for SlgContextOps<'_, I> { } let new_subst = match answers.next_answer(&should_continue) { - AnswerResult::Answer(answer1) => { - if answer1 - .subst - .value - .is_identity_subst_with_no_constraints(interner) - { - // If the answer is trivially true and thus subsumes all others, then that's a unique-enough answer for us :) - return Some(Solution::Unique(answer1.subst)); - } - answer1.subst - } + AnswerResult::Answer(answer1) => answer1.subst, AnswerResult::Floundered => { // FIXME: this doesn't trigger for any current tests self.identity_constrained_subst(root_goal) @@ -128,7 +108,6 @@ impl AggregateOps for SlgContextOps<'_, I> { break Guidance::Suggested(subst); } }; - tracing::debug!("new_subst = {:?}", new_subst); subst = merge_into_guidance(interner, &root_goal.canonical, subst, &new_subst); num_answers += 1; }; diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 96351648e13..9376a6563b0 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -3048,15 +3048,6 @@ pub struct ConstrainedSubst { pub constraints: Constraints, } -impl ConstrainedSubst { - /// True if this is an identity subst (it maps variable 0 to variable 0 etc) - /// and has no constraints. This represents an "unconditionally true" answer which - /// is a convenient thing to recognize. - pub fn is_identity_subst_with_no_constraints(&self, interner: I) -> bool { - self.subst.is_identity_subst(interner) && self.constraints.is_empty(interner) - } -} - /// The resulting substitution after solving a goal. #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub struct AnswerSubst { diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 7e6bcb0226f..0734fc53ea3 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -103,9 +103,10 @@ impl Solution { pub fn is_trivial_and_always_true(&self, interner: I) -> bool { match self { - Solution::Unique(constrained_subst) => constrained_subst - .value - .is_identity_subst_with_no_constraints(interner), + Solution::Unique(constrained_subst) => { + constrained_subst.value.subst.is_identity_subst(interner) + && constrained_subst.value.constraints.is_empty(interner) + } Solution::Ambig(_) => false, } } diff --git a/tests/test/misc.rs b/tests/test/misc.rs index b75ba3387e1..e96e5ef1191 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -812,7 +812,9 @@ fn env_bound_vars() { WellFormed(&'a ()) } } - } yields { + } yields[SolverChoice::slg_default()] { + expect![["Ambiguous; definite substitution for { [?0 := '^0.0] }"]] + } yields[SolverChoice::recursive_default()] { expect![[r#"Unique; for { substitution [?0 := '^0.0] }"#]] } goal {