rework search graph cycle handling

Author: lcnr

compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs

@@ -180,7 +180,7 @@ where
         span: I::Span,
     ) -> (Result<(HasChanged, Certainty), NoSolution>, Option<inspect::GoalEvaluation<I>>) {
         EvalCtxt::enter_root(self, self.cx().recursion_limit(), generate_proof_tree, span, |ecx| {
-            ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
+            ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Root, goal)
         })
     }
 
@@ -191,7 +191,7 @@ where
     ) -> bool {
         self.probe(|| {
             EvalCtxt::enter_root(self, root_depth, GenerateProofTree::No, I::Span::dummy(), |ecx| {
-                ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Misc, goal)
+                ecx.evaluate_goal(GoalEvaluationKind::Root, GoalSource::Root, goal)
             })
             .0
         })
@@ -212,7 +212,7 @@ where
             self.cx().recursion_limit(),
             generate_proof_tree,
             I::Span::dummy(),
-            |ecx| ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Misc, goal),
+            |ecx| ecx.evaluate_goal_raw(GoalEvaluationKind::Root, GoalSource::Root, goal),
         )
     }
 }
@@ -340,6 +340,7 @@ where
         cx: I,
         search_graph: &'a mut SearchGraph<D>,
         canonical_input: CanonicalInput<I>,
+        source: GoalSource,
         goal_evaluation: &mut ProofTreeBuilder<D>,
     ) -> QueryResult<I> {
         let mut canonical_goal_evaluation =
@@ -352,6 +353,7 @@ where
             search_graph.with_new_goal(
                 cx,
                 canonical_input,
+                source,
                 &mut canonical_goal_evaluation,
                 |search_graph, canonical_goal_evaluation| {
                     EvalCtxt::enter_canonical(
@@ -395,12 +397,10 @@ where
     /// `NormalizesTo` is only used by `AliasRelate`, all other callsites
     /// should use [`EvalCtxt::evaluate_goal`] which discards that empty
     /// storage.
-    // FIXME(-Znext-solver=coinduction): `_source` is currently unused but will
-    // be necessary once we implement the new coinduction approach.
     pub(super) fn evaluate_goal_raw(
         &mut self,
         goal_evaluation_kind: GoalEvaluationKind,
-        _source: GoalSource,
+        source: GoalSource,
         goal: Goal<I, I::Predicate>,
     ) -> Result<(NestedNormalizationGoals<I>, HasChanged, Certainty), NoSolution> {
         let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
@@ -410,6 +410,7 @@ where
             self.cx(),
             self.search_graph,
             canonical_goal,
+            source,
             &mut goal_evaluation,
         );
         let response = match canonical_response {

compiler/rustc_next_trait_solver/src/solve/search_graph.rs

@@ -94,10 +94,6 @@ where
         let certainty = from_result.unwrap().value.certainty;
         response_no_constraints(cx, for_input, certainty)
     }
-
-    fn step_is_coinductive(cx: I, input: CanonicalInput<I>) -> bool {
-        input.canonical.value.goal.predicate.is_coinductive(cx)
-    }
 }
 
 fn response_no_constraints<I: Interner>(

compiler/rustc_trait_selection/src/solve/fulfill/derive_errors.rs

@@ -354,6 +354,7 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
 
             let obligation;
             match (child_mode, nested_goal.source()) {
+                (_, GoalSource::Root) => unreachable!(),
                 (ChildMode::Trait(_) | ChildMode::Host(_), GoalSource::Misc) => {
                     continue;
                 }

compiler/rustc_trait_selection/src/solve/inspect/analyse.rs

@@ -446,6 +446,6 @@ impl<'tcx> InferCtxt<'tcx> {
             visitor.span(),
         );
         let proof_tree = proof_tree.unwrap();
-        visitor.visit_goal(&InspectGoal::new(self, depth, proof_tree, None, GoalSource::Misc))
+        visitor.visit_goal(&InspectGoal::new(self, depth, proof_tree, None, GoalSource::Root))
     }
 }