Rollup merge of #136824 - lcnr:yeet, r=compiler-errors

solver cycles are coinductive once they have one coinductive step

Implements the new cycle semantics in the new solver, dealing with the fallout from rust-lang/trait-system-refactor-initiative#10.

The first commit has been extensively fuzzed via https://github.com/lcnr/search_graph_fuzz.

A trait solver cycle is now coinductive if it has at least one *coinductive step*. A step is only considered coinductive if it's a where-clause of an impl of a coinductive trait. The only coinductive traits are `Sized` and auto traits.

This differs from the current stable because where a cycle had to consist of exclusively coinductive goals. This is overly limiting and wasn't properly enforced as it (mostly) ignored all non-trait goals.

A more in-depth explanation of my reasoning can be found in this separate doc: https://gist.github.com/lcnr/c49d887bbd34f5d05c36d1cf7a1bf5a5. A summary:
- imagine using dictionary passing style: map where-bounds to additional "dictonary" fn arguments instead of monomorphization
- impls are the only source of truth and introduce a *constructor* of the dictionary type
- a trait goal holds if mapping its proof tree to dictionary passing style results in a valid corecursive function
- a corecursive function is valid if it is guarded: matching on it should result in a constructor in a finite amount of time. This property should recursively hold for all fields of the constructor
    - a function is guarded if the recursive call is *behind* a constructor
    - **and** this constructor is not *moved out of*, e.g. by accessing a field of the dictionary
- the "not moved out of" condition is difficult to guarantee in general, e.g. for item bounds of associated types. However, there is no way to *move out* of an auto trait as there is no information you can get from *the inside of* an auto trait bound in the trait system
- if we encounter a cycle/recursive call which involves an auto trait, we can always convert the proof tree into a non-recursive function which calls a corecursive function whose first step is the construction of the auto trait dict and which only recursively depends on itself (by inlining the original function until they reach the uses of the auto trait)

**we can therefore make any cycle during which we step into an auto trait (or `Sized`) impl coinductive**

----

To fix rust-lang/trait-system-refactor-initiative#10 we could go with a more restrictive version which tries to restrict cycles to only allow code already supported on stable, potentially forcing cycles to be ambiguous if they step through an impl-where clause of a non-coinductive trait.

`PathKind` should be a strictly ordered set to allow merging paths without worry. We could therefore add another variant `PathKind::ForceUnknown` which is greater than `PathKind::Coinductive`. We already have to add such a third `PathKind` in #137314 anyways.

I am not doing this here due to multiple reasons:
- I cannot think of a principled reason why cycles using an impl to normalize differ in any way from simply using that impl to prove a trait bound. It feels unnecessary and like it makes it more difficult to reason about our cycle semantics :<
- This PR does not affect stable as coherence doesn't care about whether a goal holds or is ambiguous. So we don't yet have to make a final decision

r? `@compiler-errors` `@nikomatsakis`

Author: jieyouxu

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

@@ -4,7 +4,6 @@ use rustc_data_structures::intern::Interned;
 use rustc_hir::def_id::DefId;
 use rustc_macros::{HashStable, extension};
 use rustc_type_ir as ir;
-use tracing::instrument;
 
 use crate::ty::{
     self, DebruijnIndex, EarlyBinder, PredicatePolarity, Ty, TyCtxt, TypeFlags, Upcast, UpcastFrom,
@@ -51,10 +50,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()
     }
@@ -119,17 +114,6 @@ impl<'tcx> Predicate<'tcx> {
         Some(tcx.mk_predicate(kind))
     }
 
-    #[instrument(level = "debug", skip(tcx), ret)]
-    pub fn is_coinductive(self, tcx: TyCtxt<'tcx>) -> bool {
-        match self.kind().skip_binder() {
-            ty::PredicateKind::Clause(ty::ClauseKind::Trait(data)) => {
-                tcx.trait_is_coinductive(data.def_id())
-            }
-            ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(_)) => true,
-            _ => false,
-        }
-    }
-
     /// Whether this projection can be soundly normalized.
     ///
     /// Wf predicates must not be normalized, as normalization

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,22 @@ where
         self.delegate.typing_mode()
     }
 
-    pub(super) fn set_is_normalizes_to_goal(&mut self) {
-        self.is_normalizes_to_goal = true;
+    /// Computes the `PathKind` for the step from the current goal to the
+    /// nested goal required due to `source`.
+    ///
+    /// See #136824 for a more detailed reasoning for this behavior. We
+    /// consider cycles to be coinductive if they 'step into' a where-clause
+    /// of a coinductive trait. We will likely extend this function in the future
+    /// 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
+            }
+            _ => PathKind::Inductive,
+        }
     }
 
     /// Creates a root evaluation context and search graph. This should only be
@@ -256,7 +306,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 +344,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 +390,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 +403,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 +447,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 +460,7 @@ where
             self.cx(),
             self.search_graph,
             canonical_goal,
+            self.step_kind_for_source(source),
             &mut goal_evaluation,
         );
         let response = match canonical_response {
@@ -630,16 +681,19 @@ where
 
     #[instrument(level = "trace", skip(self))]
     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, goal.param_env));
+        goal.predicate = goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(
+            self,
+            GoalSource::Misc,
+            goal.param_env,
+        ));
         self.inspect.add_normalizes_to_goal(self.delegate, self.max_input_universe, goal);
         self.nested_goals.normalizes_to_goals.push(goal);
     }
 
     #[instrument(level = "debug", skip(self))]
     pub(super) fn add_goal(&mut self, source: GoalSource, mut goal: Goal<I, I::Predicate>) {
         goal.predicate =
-            goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(self, goal.param_env));
+            goal.predicate.fold_with(&mut ReplaceAliasWithInfer::new(self, source, goal.param_env));
         self.inspect.add_goal(self.delegate, self.max_input_universe, source, goal);
         self.nested_goals.goals.push((source, goal));
     }
@@ -1053,13 +1107,21 @@ where
 ///
 /// This is a performance optimization to more eagerly detect cycles during trait
 /// solving. See tests/ui/traits/next-solver/cycles/cycle-modulo-ambig-aliases.rs.
+///
+/// The emitted goals get evaluated in the context of the parent goal; by
+/// replacing aliases in nested goals we essentially pull the normalization out of
+/// the nested goal. We want to treat the goal as if the normalization still happens
+/// inside of the nested goal by inheriting the `step_kind` of the nested goal and
+/// storing it in the `GoalSource` of the emitted `AliasRelate` goals.
+/// This is necessary for tests/ui/sized/coinductive-1.rs to compile.
 struct ReplaceAliasWithInfer<'me, 'a, D, I>
 where
     D: SolverDelegate<Interner = I>,
     I: Interner,
 {
     ecx: &'me mut EvalCtxt<'a, D>,
     param_env: I::ParamEnv,
+    normalization_goal_source: GoalSource,
     cache: HashMap<I::Ty, I::Ty>,
 }
 
@@ -1068,8 +1130,18 @@ where
     D: SolverDelegate<Interner = I>,
     I: Interner,
 {
-    fn new(ecx: &'me mut EvalCtxt<'a, D>, param_env: I::ParamEnv) -> Self {
-        ReplaceAliasWithInfer { ecx, param_env, cache: Default::default() }
+    fn new(
+        ecx: &'me mut EvalCtxt<'a, D>,
+        for_goal_source: GoalSource,
+        param_env: I::ParamEnv,
+    ) -> Self {
+        let step_kind = ecx.step_kind_for_source(for_goal_source);
+        ReplaceAliasWithInfer {
+            ecx,
+            param_env,
+            normalization_goal_source: GoalSource::NormalizeGoal(step_kind),
+            cache: Default::default(),
+        }
     }
 }
 
@@ -1092,7 +1164,7 @@ where
                     ty::AliasRelationDirection::Equate,
                 );
                 self.ecx.add_goal(
-                    GoalSource::Misc,
+                    self.normalization_goal_source,
                     Goal::new(self.cx(), self.param_env, normalizes_to),
                 );
                 infer_ty
@@ -1121,7 +1193,7 @@ where
                     ty::AliasRelationDirection::Equate,
                 );
                 self.ecx.add_goal(
-                    GoalSource::Misc,
+                    self.normalization_goal_source,
                     Goal::new(self.cx(), self.param_env, normalizes_to),
                 );
                 infer_ct

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/inherent.rs

@@ -39,7 +39,7 @@ where
         //
         // FIXME(-Znext-solver=coinductive): I think this should be split
         // and we tag the impl bounds with `GoalSource::ImplWhereBound`?
-        // Right not this includes both the impl and the assoc item where bounds,
+        // Right now this includes both the impl and the assoc item where bounds,
         // and I don't think the assoc item where-bounds are allowed to be coinductive.
         self.add_goals(
             GoalSource::Misc,

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) {