Don't inherit clause priority in implications

So if we had some implication A => B, if the solution for A had low priority, we
also made B low priority. After some testing, I don't think this is right.

Author: flodiebold

chalk-solve/src/recursive/fulfill.rs

@@ -75,8 +75,6 @@ pub(crate) struct Fulfill<'s, 'db, I: Interner> {
     /// The remaining goals to prove or refute
     obligations: Vec<Obligation<I>>,
 
-    priority: ClausePriority,
-
     /// Lifetime constraints that must be fulfilled for a solution to be fully
     /// validated.
     constraints: HashSet<InEnvironment<Constraint<I>>>,
@@ -91,7 +89,6 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
     pub(crate) fn new<T: Fold<I, I, Result = T> + HasInterner<Interner = I> + Clone>(
         solver: &'s mut Solver<'db, I>,
         ucanonical_goal: &UCanonical<InEnvironment<T>>,
-        priority: ClausePriority,
     ) -> (Self, Substitution<I>, InEnvironment<T::Result>) {
         let (infer, subst, canonical_goal) = InferenceTable::from_canonical(
             solver.program.interner(),
@@ -102,7 +99,6 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
             solver,
             infer,
             obligations: vec![],
-            priority,
             constraints: HashSet::new(),
             cannot_prove: false,
         };
@@ -225,8 +221,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
             quantified,
             universes,
         } = self.infer.u_canonicalize(interner, &quantified);
-        let (result, new_priority) = self.solver.solve_goal(quantified, minimums);
-        self.priority = self.priority & new_priority;
+        let result = self.solver.solve_goal(quantified, minimums);
         Ok(PositiveSolution {
             free_vars,
             universes,
@@ -255,7 +250,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
             .infer
             .u_canonicalize(self.solver.program.interner(), &canonicalized);
         let mut minimums = Minimums::new(); // FIXME -- minimums here seems wrong
-        if let (Ok(solution), _priority) = self.solver.solve_goal(quantified, &mut minimums) {
+        if let Ok(solution) = self.solver.solve_goal(quantified, &mut minimums) {
             if solution.is_unique() {
                 Err(NoSolution)
             } else {
@@ -384,14 +379,14 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
         mut self,
         subst: Substitution<I>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> Fallible<Solution<I>> {
         let outcome = match self.fulfill(minimums) {
             Ok(o) => o,
-            Err(e) => return (Err(e), self.priority),
+            Err(e) => return Err(e),
         };
 
         if self.cannot_prove {
-            return (Ok(Solution::Ambig(Guidance::Unknown)), self.priority);
+            return Ok(Solution::Ambig(Guidance::Unknown));
         }
 
         if outcome.is_complete() {
@@ -403,7 +398,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
                 self.solver.program.interner(),
                 &ConstrainedSubst { subst, constraints },
             );
-            return (Ok(Solution::Unique(constrained.quantified)), self.priority);
+            return Ok(Solution::Unique(constrained.quantified));
         }
 
         // Otherwise, we have (positive or negative) obligations remaining, but
@@ -433,15 +428,12 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
                         let subst = self
                             .infer
                             .canonicalize(self.solver.program.interner(), &subst);
-                        return (
-                            Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))),
-                            self.priority,
-                        );
+                        return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified)));
                     }
                 }
             }
 
-            (Ok(Solution::Ambig(Guidance::Unknown)), self.priority)
+            Ok(Solution::Ambig(Guidance::Unknown))
         } else {
             // While we failed to prove the goal, we still learned that
             // something had to hold. Here's an example where this happens:
@@ -466,10 +458,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
             let subst = self
                 .infer
                 .canonicalize(self.solver.program.interner(), &subst);
-            (
-                Ok(Solution::Ambig(Guidance::Definite(subst.quantified))),
-                self.priority,
-            )
+            Ok(Solution::Ambig(Guidance::Definite(subst.quantified)))
         }
     }
 

chalk-solve/src/recursive/mod.rs

@@ -105,7 +105,7 @@ impl<'me, I: Interner> Solver<'me, I> {
         debug!("solve_root_goal(canonical_goal={:?})", canonical_goal);
         assert!(self.context.stack.is_empty());
         let minimums = &mut Minimums::new();
-        self.solve_goal(canonical_goal.clone(), minimums).0
+        self.solve_goal(canonical_goal.clone(), minimums)
     }
 
     /// Attempt to solve a goal that has been fully broken down into leaf form
@@ -115,13 +115,13 @@ impl<'me, I: Interner> Solver<'me, I> {
         &mut self,
         goal: UCanonicalGoal<I>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> Fallible<Solution<I>> {
         info_heading!("solve_goal({:?})", goal);
 
         // First check the cache.
         if let Some(value) = self.context.cache.get(&goal) {
             debug!("solve_reduced_goal: cache hit, value={:?}", value);
-            return (value.clone(), ClausePriority::High);
+            return value.clone();
         }
 
         // Next, check if the goal is in the search tree already.
@@ -139,13 +139,10 @@ impl<'me, I: Interner> Solver<'me, I> {
                         constraints: vec![],
                     };
                     debug!("applying coinductive semantics");
-                    return (
-                        Ok(Solution::Unique(Canonical {
-                            value,
-                            binders: goal.canonical.binders,
-                        })),
-                        ClausePriority::High,
-                    );
+                    return Ok(Solution::Unique(Canonical {
+                        value,
+                        binders: goal.canonical.binders,
+                    }));
                 }
 
                 self.context.stack[depth].flag_cycle();
@@ -160,7 +157,7 @@ impl<'me, I: Interner> Solver<'me, I> {
                 "solve_goal: cycle detected, previous solution {:?} with prio {:?}",
                 previous_solution, previous_solution_priority
             );
-            (previous_solution, previous_solution_priority)
+            previous_solution
         } else {
             // Otherwise, push the goal onto the stack and create a table.
             // The initial result for this table is error.
@@ -195,7 +192,7 @@ impl<'me, I: Interner> Solver<'me, I> {
             }
 
             info!("solve_goal: solution = {:?} prio {:?}", result, priority);
-            (result, priority)
+            result
         }
     }
 
@@ -345,11 +342,11 @@ impl<'me, I: Interner> Solver<'me, I> {
         minimums: &mut Minimums,
     ) -> (Fallible<Solution<I>>, ClausePriority) {
         debug_heading!("solve_via_simplification({:?})", canonical_goal);
-        let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal, ClausePriority::High);
+        let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal);
         if let Err(e) = fulfill.push_goal(&goal.environment, goal.goal) {
             return (Err(e), ClausePriority::High);
         }
-        fulfill.solve(subst, minimums)
+        (fulfill.solve(subst, minimums), ClausePriority::High)
     }
 
     /// See whether we can solve a goal by implication on any of the given
@@ -434,7 +431,7 @@ impl<'me, I: Interner> Solver<'me, I> {
             clause
         );
         let interner = self.program.interner();
-        let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal, clause.value.priority);
+        let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal);
         let ProgramClauseImplication {
             consequence,
             conditions,
@@ -455,7 +452,7 @@ impl<'me, I: Interner> Solver<'me, I> {
         }
 
         // and then try to solve
-        fulfill.solve(subst, minimums)
+        (fulfill.solve(subst, minimums), clause.value.priority)
     }
 
     fn program_clauses_for_goal(