Freshen normalizes-to hack goal RHS in the evaluate loop

Author: compiler-errors

compiler/rustc_trait_selection/src/solve/eval_ctxt.rs

@@ -48,7 +48,20 @@ pub(super) enum IsNormalizesToHack {
 
 #[derive(Debug, Clone)]
 pub(super) struct NestedGoals<'tcx> {
+    /// This normalizes-to goal that is treated specially during the evaluation
+    /// loop. In each iteration we take the RHS of the projection, replace it with
+    /// a fresh inference variable, and only after evaluating that goal do we
+    /// equate the fresh inference variable with the actual RHS of the predicate.
+    ///
+    /// This is both to improve caching, and to avoid using the RHS of the
+    /// projection predicate to influence the normalizes-to candidate we select.
+    ///
+    /// This is not a 'real' nested goal. We must not forget to replace the RHS
+    /// with a fresh inference variable when we evaluate this goal. That can result
+    /// in a trait solver cycle. This would currently result in overflow but can be
+    /// can be unsound with more powerful coinduction in the future.
     pub(super) normalizes_to_hack_goal: Option<Goal<'tcx, ty::ProjectionPredicate<'tcx>>>,
+    /// The rest of the goals which have not yet processed or remain ambiguous.
     pub(super) goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 }
 
@@ -163,6 +176,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             canonical_response,
         )?;
 
+        if !has_changed && !nested_goals.is_empty() {
+            bug!("an unchanged goal shouldn't have any side-effects on instantiation");
+        }
+
         // Check that rerunning this query with its inference constraints applied
         // doesn't result in new inference constraints and has the same result.
         //
@@ -180,9 +197,17 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             let canonical_response =
                 EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
             if !canonical_response.value.var_values.is_identity() {
-                bug!("unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}");
+                bug!(
+                    "unstable result: re-canonicalized goal={canonical_goal:#?} \
+                     response={canonical_response:#?}"
+                );
+            }
+            if certainty != canonical_response.value.certainty {
+                bug!(
+                    "unstable certainty: {certainty:#?} re-canonicalized goal={canonical_goal:#?} \
+                     response={canonical_response:#?}"
+                );
             }
-            assert_eq!(certainty, canonical_response.value.certainty);
         }
 
         Ok((has_changed, certainty, nested_goals))
@@ -262,15 +287,44 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                 let mut has_changed = Err(Certainty::Yes);
 
                 if let Some(goal) = goals.normalizes_to_hack_goal.take() {
-                    let (_, certainty, nested_goals) = match this.evaluate_goal(
-                        IsNormalizesToHack::Yes,
-                        goal.with(this.tcx(), ty::Binder::dummy(goal.predicate)),
+                    // Replace the goal with an unconstrained infer var, so the
+                    // RHS does not affect projection candidate assembly.
+                    let unconstrained_rhs = this.next_term_infer_of_kind(goal.predicate.term);
+                    let unconstrained_goal = goal.with(
+                        this.tcx(),
+                        ty::Binder::dummy(ty::ProjectionPredicate {
+                            projection_ty: goal.predicate.projection_ty,
+                            term: unconstrained_rhs,
+                        }),
+                    );
+
+                    let (_, certainty, instantiate_goals) =
+                        match this.evaluate_goal(IsNormalizesToHack::Yes, unconstrained_goal) {
+                            Ok(r) => r,
+                            Err(NoSolution) => return Some(Err(NoSolution)),
+                        };
+                    new_goals.goals.extend(instantiate_goals);
+
+                    // Finally, equate the goal's RHS with the unconstrained var.
+                    // We put the nested goals from this into goals instead of
+                    // next_goals to avoid needing to process the loop one extra
+                    // time if this goal returns something -- I don't think this
+                    // matters in practice, though.
+                    match this.eq_and_get_goals(
+                        goal.param_env,
+                        goal.predicate.term,
+                        unconstrained_rhs,
                     ) {
-                        Ok(r) => r,
+                        Ok(eq_goals) => {
+                            goals.goals.extend(eq_goals);
+                        }
                         Err(NoSolution) => return Some(Err(NoSolution)),
                     };
-                    new_goals.goals.extend(nested_goals);
 
+                    // We only look at the `projection_ty` part here rather than
+                    // looking at the "has changed" return from evaluate_goal,
+                    // because we expect the `unconstrained_rhs` part of the predicate
+                    // to have changed -- that means we actually normalized successfully!
                     if goal.predicate.projection_ty
                         != this.resolve_vars_if_possible(goal.predicate.projection_ty)
                     {
@@ -280,40 +334,22 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                     match certainty {
                         Certainty::Yes => {}
                         Certainty::Maybe(_) => {
-                            let goal = this.resolve_vars_if_possible(goal);
-
-                            // The rhs of this `normalizes-to` must always be an unconstrained infer var as it is
-                            // the hack used by `normalizes-to` to ensure that every `normalizes-to` behaves the same
-                            // regardless of the rhs.
-                            //
-                            // However it is important not to unconditionally replace the rhs with a new infer var
-                            // as otherwise we may replace the original unconstrained infer var with a new infer var
-                            // and never propagate any constraints on the new var back to the original var.
-                            let term = this
-                                .term_is_fully_unconstrained(goal)
-                                .then_some(goal.predicate.term)
-                                .unwrap_or_else(|| {
-                                    this.next_term_infer_of_kind(goal.predicate.term)
-                                });
-                            let projection_pred = ty::ProjectionPredicate {
-                                term,
-                                projection_ty: goal.predicate.projection_ty,
-                            };
+                            // We need to resolve vars here so that we correctly
+                            // deal with `has_changed` in the next iteration.
                             new_goals.normalizes_to_hack_goal =
-                                Some(goal.with(this.tcx(), projection_pred));
-
+                                Some(this.resolve_vars_if_possible(goal));
                             has_changed = has_changed.map_err(|c| c.unify_and(certainty));
                         }
                     }
                 }
 
-                for nested_goal in goals.goals.drain(..) {
-                    let (changed, certainty, nested_goals) =
-                        match this.evaluate_goal(IsNormalizesToHack::No, nested_goal) {
+                for goal in goals.goals.drain(..) {
+                    let (changed, certainty, instantiate_goals) =
+                        match this.evaluate_goal(IsNormalizesToHack::No, goal) {
                             Ok(result) => result,
                             Err(NoSolution) => return Some(Err(NoSolution)),
                         };
-                    new_goals.goals.extend(nested_goals);
+                    new_goals.goals.extend(instantiate_goals);
 
                     if changed {
                         has_changed = Ok(());
@@ -322,7 +358,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
                     match certainty {
                         Certainty::Yes => {}
                         Certainty::Maybe(_) => {
-                            new_goals.goals.push(nested_goal);
+                            new_goals.goals.push(goal);
                             has_changed = has_changed.map_err(|c| c.unify_and(certainty));
                         }
                     }

compiler/rustc_trait_selection/src/solve/project_goals.rs

@@ -35,16 +35,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
             let candidates = self.assemble_and_evaluate_candidates(goal);
             self.merge_candidates(candidates)
         } else {
-            let predicate = goal.predicate;
-            let unconstrained_rhs = self.next_term_infer_of_kind(predicate.term);
-            let unconstrained_predicate = ProjectionPredicate {
-                projection_ty: goal.predicate.projection_ty,
-                term: unconstrained_rhs,
-            };
-
-            self.set_normalizes_to_hack_goal(goal.with(self.tcx(), unconstrained_predicate));
-            self.try_evaluate_added_goals()?;
-            self.eq(goal.param_env, unconstrained_rhs, predicate.term)?;
+            self.set_normalizes_to_hack_goal(goal);
             self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
         }
     }