Never truncate goal

Author: jackh726

chalk-engine/src/logic.rs

@@ -7,7 +7,6 @@ use crate::table::AnswerIndex;
 use crate::{
     Answer, CompleteAnswer, ExClause, FlounderedSubgoal, Literal, Minimums, TableIndex, TimeStamp,
 };
-use std::mem;
 
 type RootSearchResult<T> = Result<T, RootSearchFail>;
 
@@ -282,7 +281,7 @@ impl<C: Context> Forest<C> {
                 ) {
                     Ok(()) => {
                         let Strand {
-                            infer,
+                            infer: _,
                             ex_clause,
                             selected_subgoal: _,
                             last_pursued_time: _,
@@ -1177,7 +1176,7 @@ impl<C: Context> Forest<C> {
 
         // Subgoal abstraction:
         let (ucanonical_subgoal, universe_map) = match subgoal {
-            Literal::Positive(subgoal) => self.abstract_positive_literal(infer, subgoal),
+            Literal::Positive(subgoal) => self.abstract_positive_literal(infer, subgoal)?,
             Literal::Negative(subgoal) => self.abstract_negative_literal(infer, subgoal)?,
         };
 
@@ -1317,7 +1316,7 @@ impl<C: Context> Forest<C> {
         &mut self,
         infer: &mut dyn InferenceTable<C>,
         subgoal: &C::GoalInEnvironment,
-    ) -> (C::UCanonicalGoalInEnvironment, C::UniverseMap) {
+    ) -> Option<(C::UCanonicalGoalInEnvironment, C::UniverseMap)> {
         // Subgoal abstraction: Rather than looking up the table for
         // `selected_goal` directly, first apply the truncation
         // function. This may introduce fresh variables, making the
@@ -1341,13 +1340,12 @@ impl<C: Context> Forest<C> {
         // irrelevant answers (e.g., `Vec<Vec<u32>>: Sized`), they
         // will fail to unify with our selected goal, producing no
         // resolvent.
-        match infer.truncate_goal(subgoal) {
-            None => infer.fully_canonicalize_goal(subgoal),
-            Some(truncated_subgoal) => {
-                debug!("truncated={:?}", truncated_subgoal);
-                infer.fully_canonicalize_goal(&truncated_subgoal)
-            }
+
+        if infer.truncate_goal(subgoal).is_some() {
+            return None;
         }
+
+        return Some(infer.fully_canonicalize_goal(subgoal));
     }
 
     /// Given a selected negative subgoal, the subgoal is "inverted"
@@ -1452,10 +1450,12 @@ impl<C: Context> Forest<C> {
         // variables that have been inverted, as discussed in the
         // prior paragraph above.) I just didn't feel like dealing
         // with it yet.
-        match infer.truncate_goal(&inverted_subgoal) {
-            Some(_) => None,
-            None => Some(infer.fully_canonicalize_goal(&inverted_subgoal)),
+
+        if infer.truncate_goal(&inverted_subgoal).is_some() {
+            return None;
         }
+
+        return Some(infer.fully_canonicalize_goal(&inverted_subgoal));
     }
 
     /// Removes the subgoal at `subgoal_index` from the strand's

tests/test/cycle.rs

@@ -164,7 +164,7 @@ fn overflow() {
         goal {
             S<Z>: Q
         } yields {
-            "No possible solution"
+            "Ambiguous; no inference guidance"
         }
     }
 }

tests/test/misc.rs

@@ -72,7 +72,8 @@ fn subgoal_abstraction() {
 
         goal {
             exists<T> { T: Foo }
-        } yields_all[SolverChoice::slg(50, None)] {
+        } yields_first[SolverChoice::slg(50, None)] {
+            "Floundered"
         }
     }
 }
@@ -169,25 +170,25 @@ fn subgoal_cycle_uninhabited() {
             impl<T> Foo for Box<T> where Box<Vec<T>>: Foo { }
         }
 
-        // There is no solution here with a finite proof, so we get
-        // back: 0 answer(s) found.
+        // Infinite recursion -> we flounder
         goal {
             exists<T> { T: Foo }
-        } yields_all[SolverChoice::slg(2, None)] {
+        } yields_first[SolverChoice::slg(2, None)] {
+            "Floundered"
         }
 
-        // Unsurprisingly, applying negation succeeds then.
+        // Unsurprisingly, applying negation also flounders.
         goal {
             not { exists<T> { T: Foo } }
-        } yields_all[SolverChoice::slg(2, None)] {
-            "substitution [], lifetime constraints []"
+        } yields_first[SolverChoice::slg(2, None)] {
+            "Floundered"
         }
 
         // Equivalent to the previous.
         goal {
             forall<T> { not { T: Foo } }
-        } yields_all[SolverChoice::slg(2, None)] {
-            "substitution [], lifetime constraints []"
+        } yields_first[SolverChoice::slg(2, None)] {
+            "Floundered"
         }
 
         // However, if we come across a negative goal that exceeds our
@@ -208,8 +209,9 @@ fn subgoal_cycle_uninhabited() {
         // Here, due to the hypothesis, there does indeed exist a suitable T, `U`.
         goal {
             forall<U> { if (U: Foo) { exists<T> { T: Foo } } }
-        } yields_all[SolverChoice::slg(2, None)] {
-            "substitution [?0 := !1_0], lifetime constraints []"
+        } yields_first[SolverChoice::slg(2, None)] {
+            "substitution [?0 := !1_0], lifetime constraints []",
+            "Floundered"
         }
     }
 }
@@ -226,10 +228,12 @@ fn subgoal_cycle_inhabited() {
             impl Foo for u32 { }
         }
 
+        // Exceeds size threshold -> flounder
         goal {
             exists<T> { T: Foo }
-        } yields_all[SolverChoice::slg(3, None)] {
-            "substitution [?0 := u32], lifetime constraints []"
+        } yields_first[SolverChoice::slg(3, None)] {
+            "substitution [?0 := u32], lifetime constraints []",
+            "Floundered"
         }
     }
 }