rework cycle handling

A cycle was previously coinductive if all steps were coinductive.
Change this to instead considerm cycles to be coinductive if they
step through at least one where-bound of an impl of a coinductive
trait goal.

Author: lcnr

compiler/rustc_middle/src/ty/context.rs

@@ -594,6 +594,10 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
         self.trait_is_auto(trait_def_id)
     }
 
+    fn trait_is_coinductive(self, trait_def_id: DefId) -> bool {
+        self.trait_is_coinductive(trait_def_id)
+    }
+
     fn trait_is_alias(self, trait_def_id: DefId) -> bool {
         self.trait_is_alias(trait_def_id)
     }

compiler/rustc_middle/src/ty/predicate.rs

@@ -52,10 +52,6 @@ impl<'tcx> rustc_type_ir::inherent::Predicate<TyCtxt<'tcx>> for Predicate<'tcx>
         self.as_clause()
     }
 
-    fn is_coinductive(self, interner: TyCtxt<'tcx>) -> bool {
-        self.is_coinductive(interner)
-    }
-
     fn allow_normalization(self) -> bool {
         self.allow_normalization()
     }
@@ -120,6 +116,8 @@ impl<'tcx> Predicate<'tcx> {
         Some(tcx.mk_predicate(kind))
     }
 
+    /// Only used by the old solver to decide whether a predicate is accepted
+    /// in a coinductive trait solver cycle.
     #[instrument(level = "debug", skip(tcx), ret)]
     pub fn is_coinductive(self, tcx: TyCtxt<'tcx>) -> bool {
         match self.kind().skip_binder() {

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

@@ -21,7 +21,7 @@ use tracing::{debug, instrument, trace};
 use crate::canonicalizer::Canonicalizer;
 use crate::delegate::SolverDelegate;
 use crate::resolve::EagerResolver;
-use crate::solve::eval_ctxt::NestedGoals;
+use crate::solve::eval_ctxt::{CurrentGoalKind, NestedGoals};
 use crate::solve::{
     CanonicalInput, CanonicalResponse, Certainty, EvalCtxt, ExternalConstraintsData, Goal,
     MaybeCause, NestedNormalizationGoals, NoSolution, PredefinedOpaquesData, QueryInput,
@@ -109,18 +109,22 @@ where
         //
         // As we return all ambiguous nested goals, we can ignore the certainty returned
         // by `try_evaluate_added_goals()`.
-        let (certainty, normalization_nested_goals) = if self.is_normalizes_to_goal {
-            let NestedGoals { normalizes_to_goals, goals } = std::mem::take(&mut self.nested_goals);
-            if cfg!(debug_assertions) {
-                assert!(normalizes_to_goals.is_empty());
-                if goals.is_empty() {
-                    assert!(matches!(goals_certainty, Certainty::Yes));
+        let (certainty, normalization_nested_goals) = match self.current_goal_kind {
+            CurrentGoalKind::NormalizesTo => {
+                let NestedGoals { normalizes_to_goals, goals } =
+                    std::mem::take(&mut self.nested_goals);
+                if cfg!(debug_assertions) {
+                    assert!(normalizes_to_goals.is_empty());
+                    if goals.is_empty() {
+                        assert!(matches!(goals_certainty, Certainty::Yes));
+                    }
                 }
+                (certainty, NestedNormalizationGoals(goals))
+            }
+            CurrentGoalKind::Misc | CurrentGoalKind::CoinductiveTrait => {
+                let certainty = certainty.unify_with(goals_certainty);
+                (certainty, NestedNormalizationGoals::empty())
             }
-            (certainty, NestedNormalizationGoals(goals))
-        } else {
-            let certainty = certainty.unify_with(goals_certainty);
-            (certainty, NestedNormalizationGoals::empty())
         };
 
         if let Certainty::Maybe(cause @ MaybeCause::Overflow { .. }) = certainty {
@@ -163,19 +167,24 @@ where
         // ambiguous alias types which get replaced with fresh inference variables
         // during generalization. This prevents hangs caused by an exponential blowup,
         // see tests/ui/traits/next-solver/coherence-alias-hang.rs.
-        //
-        // We don't do so for `NormalizesTo` goals as we erased the expected term and
-        // bailing with overflow here would prevent us from detecting a type-mismatch,
-        // causing a coherence error in diesel, see #131969. We still bail with overflow
-        // when later returning from the parent AliasRelate goal.
-        if !self.is_normalizes_to_goal {
-            let num_non_region_vars =
-                canonical.variables.iter().filter(|c| !c.is_region() && c.is_existential()).count();
-            if num_non_region_vars > self.cx().recursion_limit() {
-                debug!(?num_non_region_vars, "too many inference variables -> overflow");
-                return Ok(self.make_ambiguous_response_no_constraints(MaybeCause::Overflow {
-                    suggest_increasing_limit: true,
-                }));
+        match self.current_goal_kind {
+            // We don't do so for `NormalizesTo` goals as we erased the expected term and
+            // bailing with overflow here would prevent us from detecting a type-mismatch,
+            // causing a coherence error in diesel, see #131969. We still bail with overflow
+            // when later returning from the parent AliasRelate goal.
+            CurrentGoalKind::NormalizesTo => {}
+            CurrentGoalKind::Misc | CurrentGoalKind::CoinductiveTrait => {
+                let num_non_region_vars = canonical
+                    .variables
+                    .iter()
+                    .filter(|c| !c.is_region() && c.is_existential())
+                    .count();
+                if num_non_region_vars > self.cx().recursion_limit() {
+                    debug!(?num_non_region_vars, "too many inference variables -> overflow");
+                    return Ok(self.make_ambiguous_response_no_constraints(MaybeCause::Overflow {
+                        suggest_increasing_limit: true,
+                    }));
+                }
             }
         }
 

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};
@@ -20,12 +21,51 @@ use crate::solve::inspect::{self, ProofTreeBuilder};
 use crate::solve::search_graph::SearchGraph;
 use crate::solve::{
     CanonicalInput, Certainty, FIXPOINT_STEP_LIMIT, Goal, GoalEvaluationKind, GoalSource,
-    HasChanged, NestedNormalizationGoals, NoSolution, PredefinedOpaquesData, QueryResult,
+    HasChanged, NestedNormalizationGoals, NoSolution, PredefinedOpaquesData, QueryInput,
+    QueryResult,
 };
 
 pub(super) mod canonical;
 mod probe;
 
+/// The kind of goal we're currently proving.
+///
+/// This has effects on cycle handling handling and on how we compute
+/// query responses, see the variant descriptions for more info.
+#[derive(Debug, Copy, Clone)]
+enum CurrentGoalKind {
+    Misc,
+    /// We're proving an trait goal for a coinductive trait, either an auto trait or `Sized`.
+    ///
+    /// These are currently the only goals whose impl where-clauses are considered to be
+    /// productive steps.
+    CoinductiveTrait,
+    /// Unlike other goals, `NormalizesTo` goals act like functions with the expected term
+    /// always being fully unconstrained. This would weaken inference however, as the nested
+    /// goals never get the inference constraints from the actual normalized-to type.
+    ///
+    /// Because of this we return any ambiguous nested goals from `NormalizesTo` to the
+    /// caller when then adds these to its own context. The caller is always an `AliasRelate`
+    /// goal so this never leaks out of the solver.
+    NormalizesTo,
+}
+
+impl CurrentGoalKind {
+    fn from_query_input<I: Interner>(cx: I, input: QueryInput<I, I::Predicate>) -> CurrentGoalKind {
+        match input.goal.predicate.kind().skip_binder() {
+            ty::PredicateKind::Clause(ty::ClauseKind::Trait(pred)) => {
+                if cx.trait_is_coinductive(pred.trait_ref.def_id) {
+                    CurrentGoalKind::CoinductiveTrait
+                } else {
+                    CurrentGoalKind::Misc
+                }
+            }
+            ty::PredicateKind::NormalizesTo(_) => CurrentGoalKind::NormalizesTo,
+            _ => CurrentGoalKind::Misc,
+        }
+    }
+}
+
 pub struct EvalCtxt<'a, D, I = <D as SolverDelegate>::Interner>
 where
     D: SolverDelegate<Interner = I>,
@@ -51,14 +91,10 @@ where
     /// The variable info for the `var_values`, only used to make an ambiguous response
     /// with no constraints.
     variables: I::CanonicalVars,
-    /// Whether we're currently computing a `NormalizesTo` goal. Unlike other goals,
-    /// `NormalizesTo` goals act like functions with the expected term always being
-    /// fully unconstrained. This would weaken inference however, as the nested goals
-    /// never get the inference constraints from the actual normalized-to type. Because
-    /// of this we return any ambiguous nested goals from `NormalizesTo` to the caller
-    /// when then adds these to its own context. The caller is always an `AliasRelate`
-    /// goal so this never leaks out of the solver.
-    is_normalizes_to_goal: bool,
+
+    /// What kind of goal we're currently computing, see the enum definition
+    /// for more info.
+    current_goal_kind: CurrentGoalKind,
     pub(super) var_values: CanonicalVarValues<I>,
 
     predefined_opaques_in_body: I::PredefinedOpaques,
@@ -226,8 +262,11 @@ where
         self.delegate.typing_mode()
     }
 
-    pub(super) fn set_is_normalizes_to_goal(&mut self) {
-        self.is_normalizes_to_goal = true;
+    pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {
+        match (self.current_goal_kind, source) {
+            (CurrentGoalKind::CoinductiveTrait, GoalSource::ImplWhereBound) => PathKind::Coinductive,
+            _ => PathKind::Inductive,
+        }
     }
 
     /// Creates a root evaluation context and search graph. This should only be
@@ -256,7 +295,7 @@ where
             max_input_universe: ty::UniverseIndex::ROOT,
             variables: Default::default(),
             var_values: CanonicalVarValues::dummy(),
-            is_normalizes_to_goal: false,
+            current_goal_kind: CurrentGoalKind::Misc,
             origin_span,
             tainted: Ok(()),
         };
@@ -294,7 +333,7 @@ where
             delegate,
             variables: canonical_input.canonical.variables,
             var_values,
-            is_normalizes_to_goal: false,
+            current_goal_kind: CurrentGoalKind::from_query_input(cx, input),
             predefined_opaques_in_body: input.predefined_opaques_in_body,
             max_input_universe: canonical_input.canonical.max_universe,
             search_graph,
@@ -340,6 +379,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 +392,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 +436,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 +449,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/eval_ctxt/probe.rs

@@ -34,7 +34,7 @@ where
             delegate,
             variables: outer_ecx.variables,
             var_values: outer_ecx.var_values,
-            is_normalizes_to_goal: outer_ecx.is_normalizes_to_goal,
+            current_goal_kind: outer_ecx.current_goal_kind,
             predefined_opaques_in_body: outer_ecx.predefined_opaques_in_body,
             max_input_universe,
             search_graph: outer_ecx.search_graph,

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

@@ -28,7 +28,6 @@ where
         &mut self,
         goal: Goal<I, NormalizesTo<I>>,
     ) -> QueryResult<I> {
-        self.set_is_normalizes_to_goal();
         debug_assert!(self.term_is_fully_unconstrained(goal));
         let cx = self.cx();
         match goal.predicate.alias.kind(cx) {

compiler/rustc_next_trait_solver/src/solve/search_graph.rs

@@ -2,7 +2,6 @@ use std::convert::Infallible;
 use std::marker::PhantomData;
 
 use rustc_type_ir::Interner;
-use rustc_type_ir::inherent::*;
 use rustc_type_ir::search_graph::{self, PathKind};
 use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
 
@@ -94,10 +93,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_type_ir/src/inherent.rs

@@ -462,8 +462,6 @@ pub trait Predicate<I: Interner<Predicate = Self>>:
 {
     fn as_clause(self) -> Option<I::Clause>;
 
-    fn is_coinductive(self, interner: I) -> bool;
-
     // FIXME: Eventually uplift the impl out of rustc and make this defaulted.
     fn allow_normalization(self) -> bool;
 }

compiler/rustc_type_ir/src/interner.rs

@@ -279,6 +279,8 @@ pub trait Interner:
 
     fn trait_is_auto(self, trait_def_id: Self::DefId) -> bool;
 
+    fn trait_is_coinductive(self, trait_def_id: Self::DefId) -> bool;
+
     fn trait_is_alias(self, trait_def_id: Self::DefId) -> bool;
 
     fn trait_is_dyn_compatible(self, trait_def_id: Self::DefId) -> bool;