change proven_via probe to be coinductive

Author: lcnr

Diff for: compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs

@@ -60,6 +60,12 @@ where
     /// 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,
+
+    /// Whether the current `probe` should be treated as a coinductive step when encountering
+    /// trait solver cycles. This changes the step kind of all nested goals computed in that
+    /// probe to be coinductive.
+    is_coinductive_probe: bool,
+
     pub(super) var_values: CanonicalVarValues<I>,
 
     predefined_opaques_in_body: I::PredefinedOpaques,
@@ -232,6 +238,10 @@ where
     }
 
     pub(super) fn step_kind_for_source(&self, source: GoalSource) -> PathKind {
+        if self.is_coinductive_probe {
+            return PathKind::Coinductive;
+        }
+
         match source {
             GoalSource::ImplWhereBound => PathKind::Coinductive,
             _ => PathKind::Inductive,
@@ -265,6 +275,7 @@ where
             variables: Default::default(),
             var_values: CanonicalVarValues::dummy(),
             is_normalizes_to_goal: false,
+            is_coinductive_probe: false,
             origin_span,
             tainted: Ok(()),
         };
@@ -303,6 +314,7 @@ where
             variables: canonical_input.canonical.variables,
             var_values,
             is_normalizes_to_goal: false,
+            is_coinductive_probe: false,
             predefined_opaques_in_body: input.predefined_opaques_in_body,
             max_input_universe: canonical_input.canonical.max_universe,
             search_graph,

Diff for: compiler/rustc_next_trait_solver/src/solve/eval_ctxt/probe.rs

@@ -35,6 +35,42 @@ where
             variables: outer_ecx.variables,
             var_values: outer_ecx.var_values,
             is_normalizes_to_goal: outer_ecx.is_normalizes_to_goal,
+            is_coinductive_probe: outer_ecx.is_coinductive_probe,
+            predefined_opaques_in_body: outer_ecx.predefined_opaques_in_body,
+            max_input_universe,
+            search_graph: outer_ecx.search_graph,
+            nested_goals: outer_ecx.nested_goals.clone(),
+            origin_span: outer_ecx.origin_span,
+            tainted: outer_ecx.tainted,
+            inspect: outer_ecx.inspect.take_and_enter_probe(),
+        };
+        let r = nested_ecx.delegate.probe(|| {
+            let r = f(&mut nested_ecx);
+            nested_ecx.inspect.probe_final_state(delegate, max_input_universe);
+            r
+        });
+        if !nested_ecx.inspect.is_noop() {
+            let probe_kind = probe_kind(&r);
+            nested_ecx.inspect.probe_kind(probe_kind);
+            outer_ecx.inspect = nested_ecx.inspect.finish_probe();
+        }
+        r
+    }
+
+    pub(in crate::solve) fn enter_coinductively(
+        self,
+        f: impl FnOnce(&mut EvalCtxt<'_, D>) -> T,
+    ) -> T {
+        let ProbeCtxt { ecx: outer_ecx, probe_kind, _result } = self;
+
+        let delegate = outer_ecx.delegate;
+        let max_input_universe = outer_ecx.max_input_universe;
+        let mut nested_ecx = EvalCtxt {
+            delegate,
+            variables: outer_ecx.variables,
+            var_values: outer_ecx.var_values,
+            is_normalizes_to_goal: outer_ecx.is_normalizes_to_goal,
+            is_coinductive_probe: true,
             predefined_opaques_in_body: outer_ecx.predefined_opaques_in_body,
             max_input_universe,
             search_graph: outer_ecx.search_graph,

Diff for: compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs

@@ -93,7 +93,7 @@ where
             ty::AliasTermKind::ProjectionTy | ty::AliasTermKind::ProjectionConst => {
                 let candidates = self.assemble_and_evaluate_candidates(goal);
                 let (_, proven_via) =
-                    self.probe(|_| ProbeKind::ShadowedEnvProbing).enter(|ecx| {
+                    self.probe(|_| ProbeKind::ShadowedEnvProbing).enter_coinductively(|ecx| {
                         let trait_goal: Goal<I, ty::TraitPredicate<I>> =
                             goal.with(cx, goal.predicate.alias.trait_ref(cx));
                         ecx.compute_trait_goal(trait_goal)