Revert "extend SLG solver with a similar optimization"

This reverts commit 502d989.

Author: nikomatsakis

chalk-engine/src/slg/aggregate.rs

@@ -46,16 +46,8 @@ 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));
@@ -91,11 +83,9 @@ 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);
             }
 
@@ -106,17 +96,7 @@ impl<I: Interner> AggregateOps<I> 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<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,15 +3048,6 @@ 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,9 +103,10 @@ 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
-                .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,
         }
     }

tests/test/misc.rs

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