change definitely non-productive cycles to error

5 files changed, 53 insertions, 19 deletions

diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
index b0bbec48947..e48ee71c858 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
@@ -271,12 +271,39 @@ where
     /// and will need to clearly document it in the rustc-dev-guide before
     /// stabilization.
     pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {
-        match (self.current_goal_kind, source) {
-            (_, GoalSource::NormalizeGoal(step_kind)) => step_kind,
-            (CurrentGoalKind::CoinductiveTrait, GoalSource::ImplWhereBound) => {
-                PathKind::Coinductive
+        match source {
+            // We treat these goals as unknown for now. It is likely that most miscellaneous
+            // nested goals will be converted to an inductive variant in the future.
+            //
+            // Having unknown cycles is always the safer option, as changing that to either
+            // succeed or hard error is backwards compatible. If we incorrectly treat a cycle
+            // as inductive even though it should not be, it may be unsound during coherence and
+            // fixing it may cause inference breakage or introduce ambiguity.
+            GoalSource::Misc => PathKind::Unknown,
+            GoalSource::NormalizeGoal(path_kind) => path_kind,
+            GoalSource::ImplWhereBound => {
+                // We currently only consider a cycle coinductive if it steps
+                // into a where-clause of a coinductive trait.
+                //
+                // We probably want to make all traits coinductive in the future,
+                // so we treat cycles involving their where-clauses as ambiguous.
+                if let CurrentGoalKind::CoinductiveTrait = self.current_goal_kind {
+                    PathKind::Coinductive
+                } else {
+                    PathKind::Unknown
+                }
             }
-            _ => PathKind::Inductive,
+            // Relating types is always unproductive. If we were to map proof trees to
+            // corecursive functions as explained in #136824, relating types never
+            // introduces a constructor which could cause the recursion to be guarded.
+            GoalSource::TypeRelating => PathKind::Inductive,
+            // Instantiating a higher ranked goal can never cause the recursion to be
+            // guarded and is therefore unproductive.
+            GoalSource::InstantiateHigherRanked => PathKind::Inductive,
+            // These goal sources are likely unproductive and can be changed to
+            // `PathKind::Inductive`. Keeping them as unknown until we're confident
+            // about this and have an example where it is necessary.
+            GoalSource::AliasBoundConstCondition | GoalSource::AliasWellFormed => PathKind::Unknown,
         }
     }
 
@@ -606,7 +633,7 @@ where
 
             let (NestedNormalizationGoals(nested_goals), _, certainty) = self.evaluate_goal_raw(
                 GoalEvaluationKind::Nested,
-                GoalSource::Misc,
+                GoalSource::TypeRelating,
                 unconstrained_goal,
             )?;
             // Add the nested goals from normalization to our own nested goals.
@@ -683,7 +710,7 @@ where
     pub(super) fn add_normalizes_to_goal(&mut self, mut goal: Goal<I, ty::NormalizesTo<I>>) {
         goal.predicate = goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(
             self,
-            GoalSource::Misc,
+            GoalSource::TypeRelating,
             goal.param_env,
         ));
         self.inspect.add_normalizes_to_goal(self.delegate, self.max_input_universe, goal);
@@ -939,7 +966,15 @@ where
         rhs: T,
     ) -> Result<(), NoSolution> {
         let goals = self.delegate.relate(param_env, lhs, variance, rhs, self.origin_span)?;
-        self.add_goals(GoalSource::Misc, goals);
+        if cfg!(debug_assertions) {
+            for g in goals.iter() {
+                match g.predicate.kind().skip_binder() {
+                    ty::PredicateKind::Subtype { .. } | ty::PredicateKind::AliasRelate(..) => {}
+                    p => unreachable!("unexpected nested goal in `relate`: {p:?}"),
+                }
+            }
+        }
+        self.add_goals(GoalSource::TypeRelating, goals);
         Ok(())
     }
 
diff --git a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
index 1607fbb1b6a..6a8e0790f7c 100644
--- a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
@@ -421,7 +421,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
         self.add_goal(
             delegate,
             max_input_universe,
-            GoalSource::Misc,
+            GoalSource::TypeRelating,
             goal.with(delegate.cx(), goal.predicate),
         );
     }
diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs
index 1fa35b60304..199f0c7512e 100644
--- a/compiler/rustc_next_trait_solver/src/solve/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/mod.rs
@@ -313,7 +313,9 @@ where
                     ty::AliasRelationDirection::Equate,
                 ),
             );
-            self.add_goal(GoalSource::Misc, alias_relate_goal);
+            // We normalize the self type to be able to relate it with
+            // types from candidates.
+            self.add_goal(GoalSource::TypeRelating, alias_relate_goal);
             self.try_evaluate_added_goals()?;
             Ok(self.resolve_vars_if_possible(normalized_term))
         } else {
diff --git a/compiler/rustc_next_trait_solver/src/solve/project_goals.rs b/compiler/rustc_next_trait_solver/src/solve/project_goals.rs
index d9452880071..944d5f0e042 100644
--- a/compiler/rustc_next_trait_solver/src/solve/project_goals.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/project_goals.rs
@@ -24,7 +24,8 @@ where
                 ty::AliasRelationDirection::Equate,
             ),
         );
-        self.add_goal(GoalSource::Misc, goal);
+        // A projection goal holds if the alias is equal to the expected term.
+        self.add_goal(GoalSource::TypeRelating, goal);
         self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
     }
 }
diff --git a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
index 67eb442d2cc..aa1206cd6b7 100644
--- a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
@@ -3,7 +3,7 @@ use std::marker::PhantomData;
 
 use rustc_type_ir::Interner;
 use rustc_type_ir::search_graph::{self, PathKind};
-use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
+use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult};
 
 use super::inspect::ProofTreeBuilder;
 use super::{FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
@@ -47,7 +47,8 @@ where
     ) -> QueryResult<I> {
         match kind {
             PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
-            PathKind::Inductive => response_no_constraints(cx, input, Certainty::overflow(false)),
+            PathKind::Unknown => response_no_constraints(cx, input, Certainty::overflow(false)),
+            PathKind::Inductive => Err(NoSolution),
         }
     }
 
@@ -57,12 +58,7 @@ where
         input: CanonicalInput<I>,
         result: QueryResult<I>,
     ) -> bool {
-        match kind {
-            PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes) == result,
-            PathKind::Inductive => {
-                response_no_constraints(cx, input, Certainty::overflow(false)) == result
-            }
-        }
+        Self::initial_provisional_result(cx, kind, input) == result
     }
 
     fn on_stack_overflow(