remove priority from the search graph

It turns out we only use this when we are comparing multiple program clauses.

Author: nikomatsakis

chalk-recursive/src/recursive.rs

@@ -149,7 +149,7 @@ impl<'me, I: Interner> Solver<'me, I> {
         // so this function will eventually be constant and the loop terminates.
         loop {
             let minimums = &mut Minimums::new();
-            let (current_answer, current_prio) = self.solve_iteration(&canonical_goal, minimums);
+            let current_answer = self.solve_iteration(&canonical_goal, minimums);
 
             debug!(
                 "solve_new_subgoal: loop iteration result = {:?} with minimums {:?}",
@@ -160,7 +160,6 @@ impl<'me, I: Interner> Solver<'me, I> {
                 // None of our subgoals depended on us directly.
                 // We can return.
                 self.context.search_graph[dfn].solution = current_answer;
-                self.context.search_graph[dfn].solution_priority = current_prio;
                 return *minimums;
             }
 
@@ -177,7 +176,6 @@ impl<'me, I: Interner> Solver<'me, I> {
             };
 
             self.context.search_graph[dfn].solution = current_answer;
-            self.context.search_graph[dfn].solution_priority = current_prio;
 
             // Subtle: if our current answer is ambiguous, we can just stop, and
             // in fact we *must* -- otherwise, we sometimes fail to reach a
@@ -231,10 +229,9 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
 
             // Return the solution from the table.
             let previous_solution = self.context.search_graph[dfn].solution.clone();
-            let previous_solution_priority = self.context.search_graph[dfn].solution_priority;
             info!(
-                "solve_goal: cycle detected, previous solution {:?} with prio {:?}",
-                previous_solution, previous_solution_priority
+                "solve_goal: cycle detected, previous solution {:?}",
+                previous_solution,
             );
             previous_solution
         } else {
@@ -265,7 +262,6 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
 
             // Read final result from table.
             let result = self.context.search_graph[dfn].solution.clone();
-            let priority = self.context.search_graph[dfn].solution_priority;
 
             // If processing this subgoal did not involve anything
             // outside of its subtree, then we can promote it to the
@@ -283,7 +279,7 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
                 }
             }
 
-            info!("solve_goal: solution = {:?} prio {:?}", result, priority);
+            info!("solve_goal: solution = {:?}", result);
             result
         }
     }

chalk-recursive/src/search_graph.rs

@@ -1,6 +1,5 @@
 use super::stack::StackDepth;
 use crate::{Cache, Minimums};
-use chalk_ir::ClausePriority;
 use rustc_hash::FxHashMap;
 use std::fmt::Debug;
 use std::hash::Hash;
@@ -30,7 +29,6 @@ pub(super) struct Node<K, V> {
     pub(crate) goal: K,
 
     pub(crate) solution: V,
-    pub(crate) solution_priority: ClausePriority,
 
     /// This is `Some(X)` if we are actively exploring this node, or
     /// `None` otherwise.
@@ -78,7 +76,6 @@ where
         let node = Node {
             goal: goal.clone(),
             solution,
-            solution_priority: ClausePriority::High,
             stack_depth: Some(stack_depth),
             links: Minimums { positive: dfn },
         };

chalk-recursive/src/solve.rs

@@ -39,7 +39,7 @@ pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> {
         &mut self,
         canonical_goal: &UCanonicalGoal<I>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> Fallible<Solution<I>> {
         let UCanonical {
             universes,
             canonical:
@@ -68,14 +68,14 @@ pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> {
                 // or from the lowered program, which includes fallback
                 // clauses. We try each approach in turn:
 
-                let (prog_solution, prog_prio) = {
+                let prog_solution = {
                     debug_span!("prog_clauses");
 
                     self.solve_from_clauses(&canonical_goal, minimums)
                 };
                 debug!(?prog_solution);
 
-                (prog_solution, prog_prio)
+                prog_solution
             }
 
             _ => {
@@ -107,11 +107,11 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         &mut self,
         canonical_goal: &UCanonicalGoal<I>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> Fallible<Solution<I>> {
         let (infer, subst, goal) = self.new_inference_table(canonical_goal);
         match Fulfill::new_with_simplification(self, infer, subst, goal) {
-            Ok(fulfill) => (fulfill.solve(minimums), ClausePriority::High),
-            Err(e) => (Err(e), ClausePriority::High),
+            Ok(fulfill) => fulfill.solve(minimums),
+            Err(e) => Err(e),
         }
     }
 
@@ -122,7 +122,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         &mut self,
         canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> Fallible<Solution<I>> {
         let mut clauses = vec![];
 
         let db = self.db();
@@ -137,7 +137,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         match program_clauses_that_could_match(db, canonical_goal) {
             Ok(goal_clauses) => clauses.extend(goal_clauses.into_iter().filter(could_match)),
             Err(Floundered) => {
-                return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
+                return Ok(Solution::Ambig(Guidance::Unknown));
             }
         }
 
@@ -155,7 +155,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
 
             // 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)), ClausePriority::High);
+                return Ok(Solution::Ambig(Guidance::Unknown));
             }
 
             let ProgramClauseData(implication) = program_clause.data(self.interner());
@@ -184,7 +184,12 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
                 debug!("Error");
             }
         }
-        cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p)| (Ok(s), p))
+
+        if let Some((s, _)) = cur_solution {
+            Ok(s)
+        } else {
+            Err(NoSolution)
+        }
     }
 
     fn new_inference_table<T: Fold<I, Result = T> + HasInterner<Interner = I> + Clone>(