rework search graph cycle handling

Author: lcnr

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

@@ -9,6 +9,7 @@ use rustc_type_ir::fold::{TypeFoldable, TypeFolder, TypeSuperFoldable};
 use rustc_type_ir::inherent::*;
 use rustc_type_ir::relate::Relate;
 use rustc_type_ir::relate::solver_relating::RelateExt;
+use rustc_type_ir::search_graph::PathKind;
 use rustc_type_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitableExt, TypeVisitor};
 use rustc_type_ir::{self as ty, CanonicalVarValues, InferCtxtLike, Interner, TypingMode};
 use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
@@ -230,6 +231,13 @@ where
         self.is_normalizes_to_goal = true;
     }
 
+    pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {
+        match source {
+            GoalSource::ImplWhereBound => PathKind::Coinductive,
+            _ => PathKind::Inductive,
+        }
+    }
+
     /// Creates a root evaluation context and search graph. This should only be
     /// used from outside of any evaluation, and other methods should be preferred
     /// over using this manually (such as [`SolverDelegateEvalExt::evaluate_root_goal`]).
@@ -340,6 +348,7 @@ where
         cx: I,
         search_graph: &'a mut SearchGraph<D>,
         canonical_input: CanonicalInput<I>,
+        step_kind_from_parent: PathKind,
         goal_evaluation: &mut ProofTreeBuilder<D>,
     ) -> QueryResult<I> {
         let mut canonical_goal_evaluation =
@@ -352,6 +361,7 @@ where
             search_graph.with_new_goal(
                 cx,
                 canonical_input,
+                step_kind_from_parent,
                 &mut canonical_goal_evaluation,
                 |search_graph, canonical_goal_evaluation| {
                     EvalCtxt::enter_canonical(
@@ -395,12 +405,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 +418,7 @@ where
             self.cx(),
             self.search_graph,
             canonical_goal,
+            self.step_kind_for_source(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>(