extend SLG solver with a similar optimization

Author: nikomatsakis

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-solve/src/solve.rs

@@ -103,10 +103,9 @@ impl<I: Interner> Solution<I> {
 
     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,
         }
     }

tests/test/misc.rs

@@ -812,9 +812,7 @@ fn env_bound_vars() {
                     WellFormed(&'a ())
                 }
             }
-        } yields[SolverChoice::slg_default()] {
-            expect![["Ambiguous; definite substitution for<?U0> { [?0 := '^0.0] }"]]
-        } yields[SolverChoice::recursive_default()] {
+        } yields {
             expect![[r#"Unique; for<?U0> { substitution [?0 := '^0.0] }"#]]
         }
         goal {