we only need to prove things one way

chalk-engine/src/slg/aggregate.rs

@@ -46,8 +46,16 @@ impl<I: Interner> AggregateOps<I> 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<I: Interner> AggregateOps<I> 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<I: Interner> AggregateOps<I> 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<I: Interner> AggregateOps<I> 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;
         };

chalk-ir/src/lib.rs

@@ -3048,6 +3048,15 @@ pub struct ConstrainedSubst<I: Interner> {
     pub constraints: Constraints<I>,
 }
 
+impl<I: Interner> ConstrainedSubst<I> {
+    /// 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<I: Interner> {

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<I: Interner>(
     interner: I,
     domain_goal: &DomainGoal<I>,
@@ -12,7 +13,7 @@ pub(super) fn with_priorities<I: Interner>(
     b: Solution<I>,
     prio_b: ClausePriority,
 ) -> (Solution<I>, 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<I: Interner>(
             }
         }
         (_, _, a, b) => (a.combine(b, interner), prio_a),
-    }
+    };
+    debug!(?result, "combined result");
+    result
 }
 
 fn calculate_inputs<I: Interner>(

chalk-recursive/src/solve.rs

@@ -154,11 +154,6 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         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();
@@ -184,11 +179,19 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
             } 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 {
+            debug!("solve_from_clauses: result = {:?}", s);
             Ok(s)
         } else {
+            debug!("solve_from_clauses: error");
             Err(NoSolution)
         }
     }

chalk-solve/src/solve.rs

@@ -44,30 +44,43 @@ impl<I: Interner> Solution<I> {
     /// 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<?0>: Clone` and successful candidate `Option<?0>:
-    //    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<?0>: Clone` and successful candidate `Option<?0>:
+    ///    Clone`.
+    ///
+    /// But you get the idea.
     pub fn combine(self, other: Solution<I>, interner: I) -> Solution<I> {
         use self::Guidance::*;
 
         if self == other {
             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,15 @@ impl<I: Interner> Solution<I> {
         Solution::Ambig(guidance)
     }
 
+    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::Ambig(_) => false,
+        }
+    }
+
     /// View this solution purely in terms of type inference guidance
     pub fn into_guidance(self) -> Guidance<I> {
         match self {

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<Self>;
+            }
+
+            #[non_enumerable] #[object_safe]
+            trait HasQueryGroup<G>
+            where
+                Self: Database,
+                G: QueryGroup,
+                G: Sized,
+            { }
+
+            #[non_enumerable] #[object_safe]
+            trait HelloWorld
+            where
+                Self: HasQueryGroup<HelloWorldStorage>,
+            { }
+
+            struct HelloWorldStorage {}
+
+            impl QueryGroup for HelloWorldStorage {
+                type DynDb = dyn HelloWorld + 'static;
+            }
+            impl<DB> HelloWorld for DB
+            where
+                DB: Database,
+                DB: HasQueryGroup<HelloWorldStorage>,
+                DB: Sized,
+            { }
+        }
+
+        goal {
+            forall<T> {
+                if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); 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<Self>;
+            }
+
+            #[non_enumerable] #[object_safe]
+            trait HasQueryGroup<G>
+            where
+                Self: Database,
+                G: QueryGroup,
+            { }
+
+            struct HelloWorldStorage {}
+
+            impl QueryGroup for HelloWorldStorage {
+                type DynDb = dyn HasQueryGroup<HelloWorldStorage> + 'static;
+            }
+        }
+
+        goal {
+            forall<T> {
+                if (FromEnv(T: HasQueryGroup<HelloWorldStorage>)) {
+                    T: Database
+                }
+            }
+        } yields[SolverChoice::slg_default()] {
+            expect![["Unique"]]
+        } yields[SolverChoice::recursive_default()] {
+            expect![[r#"Ambiguous; no inference guidance"#]] // FIXME rust-lang/chalk#727
+        }
+    );
+}
+
+#[test]
+fn issue_727_3() {
+    test!(
+        program {
+            #[non_enumerable]
+            trait Database {}
+
+            #[non_enumerable]
+            trait HasQueryGroup<G>
+            where
+                Self: Database,
+            { }
+
+            struct HelloWorldStorage {}
+
+            impl Database for HelloWorldStorage { }
+        }
+
+        goal {
+            forall<T, S> {
+                if (FromEnv(HelloWorldStorage: HasQueryGroup<T>); FromEnv(HelloWorldStorage: HasQueryGroup<S>)) {
+                    HelloWorldStorage: Database
+                }
+            }
+        } yields[SolverChoice::slg_default()] {
+            expect![["Unique"]]
+        } yields[SolverChoice::recursive_default()] {
+            expect![["Unique"]]
+        }
+    );
+}

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"#]]
         }
     }
 }
@@ -813,7 +813,7 @@ fn env_bound_vars() {
                 }
             }
         } yields {
-            expect![["Ambiguous; definite substitution for<?U0> { [?0 := '^0.0] }"]]
+            expect![[r#"Unique; for<?U0> { substitution [?0 := '^0.0] }"#]]
         }
         goal {
             exists<'a> {
@@ -841,7 +841,7 @@ fn recursive_hang() {
         } yields[SolverChoice::slg_default()] {
             expect![["Ambiguous; definite substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
         } yields[SolverChoice::recursive_default()] {
-            expect![["Ambiguous; suggested substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
+            expect![[r#"Ambiguous; no inference guidance"#]]
         }
     }
 }

tests/test/mod.rs

@@ -394,16 +394,17 @@ 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);
 }
 
+mod ambiguity_issue_727;
 mod arrays;
 mod auto_traits;
 mod closures;