Higher ranked goal source, do overflow handling less badly

compiler/rustc_middle/src/traits/solve.rs

@@ -273,6 +273,8 @@ pub enum GoalSource {
  /// they are from an impl where-clause. This is necessary due to
  /// backwards compatability, cc trait-system-refactor-initiatitive#70.
  ImplWhereBound,
+ /// Instantiating a higher-ranked goal and re-proving it.
+ InstantiateHigherRanked,
 }
 
 /// Possible ways the given goal can be proven.

compiler/rustc_middle/src/traits/solve/inspect/format.rs

@@ -127,6 +127,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
  let source = match source {
  GoalSource::Misc => "misc",
  GoalSource::ImplWhereBound => "impl where-bound",
+ GoalSource::InstantiateHigherRanked => "higher-ranked goal",
  };
  writeln!(this.f, "ADDED GOAL ({source}): {goal:?}")?
  }

compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs

@@ -453,7 +453,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
  } else {
  self.infcx.enter_forall(kind, |kind| {
  let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
- self.add_goal(GoalSource::ImplWhereBound, goal);
+ self.add_goal(GoalSource::InstantiateHigherRanked, goal);
  self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
  })
  }

compiler/rustc_trait_selection/src/solve/fulfill.rs

@@ -7,10 +7,10 @@ use rustc_infer::traits::solve::inspect::ProbeKind;
 use rustc_infer::traits::solve::{CandidateSource, GoalSource, MaybeCause};
 use rustc_infer::traits::{
  self, FulfillmentError, FulfillmentErrorCode, MismatchedProjectionTypes, Obligation,
- PredicateObligation, SelectionError, TraitEngine,
+ ObligationCause, PredicateObligation, SelectionError, TraitEngine,
 };
-use rustc_middle::ty;
 use rustc_middle::ty::error::{ExpectedFound, TypeError};
+use rustc_middle::ty::{self, TyCtxt};
 
 use super::eval_ctxt::GenerateProofTree;
 use super::inspect::{ProofTreeInferCtxtExt, ProofTreeVisitor};
@@ -219,14 +219,14 @@ fn fulfillment_error_for_no_solution<'tcx>(
  }
  ty::PredicateKind::Subtype(pred) => {
  let (a, b) = infcx.enter_forall_and_leak_universe(
- root_obligation.predicate.kind().rebind((pred.a, pred.b)),
+ obligation.predicate.kind().rebind((pred.a, pred.b)),
  );
  let expected_found = ExpectedFound::new(true, a, b);
  FulfillmentErrorCode::SubtypeError(expected_found, TypeError::Sorts(expected_found))
  }
  ty::PredicateKind::Coerce(pred) => {
  let (a, b) = infcx.enter_forall_and_leak_universe(
- root_obligation.predicate.kind().rebind((pred.a, pred.b)),
+ obligation.predicate.kind().rebind((pred.a, pred.b)),
  );
  let expected_found = ExpectedFound::new(false, a, b);
  FulfillmentErrorCode::SubtypeError(expected_found, TypeError::Sorts(expected_found))
@@ -272,17 +272,30 @@ fn fulfillment_error_for_stalled<'tcx>(
  }
 }
 
+fn find_best_leaf_obligation<'tcx>(
+ infcx: &InferCtxt<'tcx>,
+ obligation: &PredicateObligation<'tcx>,
+) -> PredicateObligation<'tcx> {
+ let obligation = infcx.resolve_vars_if_possible(obligation.clone());
+ infcx
+ .visit_proof_tree(
+ obligation.clone().into(),
+ &mut BestObligation { obligation: obligation.clone() },
+ )
+ .break_value()
+ .unwrap_or(obligation)
+}
+
 struct BestObligation<'tcx> {
  obligation: PredicateObligation<'tcx>,
 }
 
 impl<'tcx> BestObligation<'tcx> {
  fn with_derived_obligation(
  &mut self,
- derive_obligation: impl FnOnce(&mut Self) -> PredicateObligation<'tcx>,
+ derived_obligation: PredicateObligation<'tcx>,
  and_then: impl FnOnce(&mut Self) -> <Self as ProofTreeVisitor<'tcx>>::Result,
  ) -> <Self as ProofTreeVisitor<'tcx>>::Result {
- let derived_obligation = derive_obligation(self);
  let old_obligation = std::mem::replace(&mut self.obligation, derived_obligation);
  let res = and_then(self);
  self.obligation = old_obligation;
@@ -298,13 +311,8 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
  }
 
  fn visit_goal(&mut self, goal: &super::inspect::InspectGoal<'_, 'tcx>) -> Self::Result {
- let candidates = goal.candidates();
  // FIXME: Throw out candidates that have no failing WC and >1 failing misc goal.
-
- // HACK:
- if self.obligation.recursion_depth > 3 {
- return ControlFlow::Break(self.obligation.clone());
- }
+ let candidates = goal.candidates();
 
  let [candidate] = candidates.as_slice() else {
  return ControlFlow::Break(self.obligation.clone());
@@ -320,80 +328,71 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
  let tcx = goal.infcx().tcx;
  let mut impl_where_bound_count = 0;
  for nested_goal in candidate.instantiate_nested_goals(self.span()) {
- if matches!(nested_goal.source(), GoalSource::ImplWhereBound) {
- impl_where_bound_count += 1;
- } else {
- continue;
+ let obligation;
+ match nested_goal.source() {
+ GoalSource::Misc => {
+ continue;
+ }
+ GoalSource::ImplWhereBound => {
+ obligation = Obligation {
+ cause: derive_cause(
+ tcx,
+ candidate.kind(),
+ self.obligation.cause.clone(),
+ impl_where_bound_count,
+ parent_trait_pred,
+ ),
+ param_env: nested_goal.goal().param_env,
+ predicate: nested_goal.goal().predicate,
+ recursion_depth: self.obligation.recursion_depth + 1,
+ };
+ impl_where_bound_count += 1;
+ }
+ GoalSource::InstantiateHigherRanked => {
+ obligation = self.obligation.clone();
+ }
  }
 
  // Skip nested goals that hold.
+ //FIXME: We should change the max allowed certainty based on if we're
+ // visiting an ambiguity or error obligation.
  if matches!(nested_goal.result(), Ok(Certainty::Yes)) {
  continue;
  }
 
- self.with_derived_obligation(
- |self_| {
- let mut cause = self_.obligation.cause.clone();
- cause = match candidate.kind() {
- ProbeKind::TraitCandidate {
- source: CandidateSource::Impl(impl_def_id),
- result: _,
- } => {
- let idx = impl_where_bound_count - 1;
- if let Some((_, span)) = tcx
- .predicates_of(impl_def_id)
- .instantiate_identity(tcx)
- .iter()
- .nth(idx)
- {
- cause.derived_cause(parent_trait_pred, |derived| {
- traits::ImplDerivedObligation(Box::new(
- traits::ImplDerivedObligationCause {
- derived,
- impl_or_alias_def_id: impl_def_id,
- impl_def_predicate_index: Some(idx),
- span,
- },
- ))
- })
- } else {
- cause
- }
- }
- ProbeKind::TraitCandidate {
- source: CandidateSource::BuiltinImpl(..),
- result: _,
- } => {
- cause.derived_cause(parent_trait_pred, traits::BuiltinDerivedObligation)
- }
- _ => cause,
- };
-
- Obligation {
- cause,
- param_env: nested_goal.goal().param_env,
- predicate: nested_goal.goal().predicate,
- recursion_depth: self_.obligation.recursion_depth + 1,
- }
- },
- |self_| self_.visit_goal(&nested_goal),
- )?;
+ self.with_derived_obligation(obligation, |self_| nested_goal.visit_with(self_))?;
  }
 
  ControlFlow::Break(self.obligation.clone())
  }
 }
 
-fn find_best_leaf_obligation<'tcx>(
- infcx: &InferCtxt<'tcx>,
- obligation: &PredicateObligation<'tcx>,
-) -> PredicateObligation<'tcx> {
- let obligation = infcx.resolve_vars_if_possible(obligation.clone());
- infcx
- .visit_proof_tree(
- obligation.clone().into(),
- &mut BestObligation { obligation: obligation.clone() },
- )
- .break_value()
- .unwrap_or(obligation)
+fn derive_cause<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ candidate_kind: ProbeKind<'tcx>,
+ mut cause: ObligationCause<'tcx>,
+ idx: usize,
+ parent_trait_pred: ty::PolyTraitPredicate<'tcx>,
+) -> ObligationCause<'tcx> {
+ match candidate_kind {
+ ProbeKind::TraitCandidate { source: CandidateSource::Impl(impl_def_id), result: _ } => {
+ if let Some((_, span)) =
+ tcx.predicates_of(impl_def_id).instantiate_identity(tcx).iter().nth(idx)
+ {
+ cause = cause.derived_cause(parent_trait_pred, |derived| {
+ traits::ImplDerivedObligation(Box::new(traits::ImplDerivedObligationCause {
+ derived,
+ impl_or_alias_def_id: impl_def_id,
+ impl_def_predicate_index: Some(idx),
+ span,
+ }))
+ })
+ }
+ }
+ ProbeKind::TraitCandidate { source: CandidateSource::BuiltinImpl(..), result: _ } => {
+ cause = cause.derived_cause(parent_trait_pred, traits::BuiltinDerivedObligation);
+ }
+ _ => {}
+ };
+ cause
 }

compiler/rustc_trait_selection/src/solve/inspect/analyse.rs

@@ -360,6 +360,14 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
  source,
  }
  }
+
+ pub(crate) fn visit_with<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
+ if self.depth < visitor.config().max_depth {
+ try_visit!(visitor.visit_goal(self));
+ }
+
+ V::Result::output()
+ }
 }
 
 /// The public API to interact with proof trees.

tests/ui/traits/next-solver/coherence/coherence-fulfill-overflow.stderr

@@ -6,7 +6,7 @@ LL | impl<T: ?Sized + TwoW> Trait for W<T> {}
 LL | impl<T: ?Sized + TwoW> Trait for T {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<W<_>>>>>>>>>>>>>>>>>>>>>>`
  |
- = note: overflow evaluating the requirement `W<W<W<W<W<W<W<W<W<W<W<W<W<W<_>>>>>>>>>>>>>>: TwoW`
+ = note: overflow evaluating the requirement `W<W<W<W<_>>>>: TwoW`
  = help: consider increasing the recursion limit by adding a `#![recursion_limit = "20"]` attribute to your crate (`coherence_fulfill_overflow`)
 
 error: aborting due to 1 previous error

tests/ui/traits/next-solver/cycles/double-cycle-inductive-coinductive.stderr

@@ -1,52 +1,52 @@
-error[E0275]: overflow evaluating the requirement `(): Trait`
+error[E0275]: overflow evaluating the requirement `(): Inductive`
  --> $DIR/double-cycle-inductive-coinductive.rs:32:19
  |
 LL | impls_trait::<()>();
  | ^^
  |
-note: required for `()` to implement `Inductive`
- --> $DIR/double-cycle-inductive-coinductive.rs:12:16
- |
-LL | impl<T: Trait> Inductive for T {}
- | ----- ^^^^^^^^^ ^
- | |
- | unsatisfied trait bound introduced here
 note: required for `()` to implement `Trait`
  --> $DIR/double-cycle-inductive-coinductive.rs:9:34
  |
 LL | impl<T: Inductive + Coinductive> Trait for T {}
  | --------- ^^^^^ ^
  | |
  | unsatisfied trait bound introduced here
- = note: 2 redundant requirements hidden
+note: required for `()` to implement `Inductive`
+ --> $DIR/double-cycle-inductive-coinductive.rs:12:16
+ |
+LL | impl<T: Trait> Inductive for T {}
+ | ----- ^^^^^^^^^ ^
+ | |
+ | unsatisfied trait bound introduced here
+ = note: 7 redundant requirements hidden
  = note: required for `()` to implement `Trait`
 note: required by a bound in `impls_trait`
  --> $DIR/double-cycle-inductive-coinductive.rs:17:19
  |
 LL | fn impls_trait<T: Trait>() {}
  | ^^^^^ required by this bound in `impls_trait`
 
-error[E0275]: overflow evaluating the requirement `(): TraitRev`
+error[E0275]: overflow evaluating the requirement `(): CoinductiveRev`
  --> $DIR/double-cycle-inductive-coinductive.rs:35:23
  |
 LL | impls_trait_rev::<()>();
  | ^^
  |
-note: required for `()` to implement `CoinductiveRev`
- --> $DIR/double-cycle-inductive-coinductive.rs:27:19
- |
-LL | impl<T: TraitRev> CoinductiveRev for T {}
- | -------- ^^^^^^^^^^^^^^ ^
- | |
- | unsatisfied trait bound introduced here
 note: required for `()` to implement `TraitRev`
  --> $DIR/double-cycle-inductive-coinductive.rs:21:40
  |
 LL | impl<T: CoinductiveRev + InductiveRev> TraitRev for T {}
  | -------------- ^^^^^^^^ ^
  | |
  | unsatisfied trait bound introduced here
- = note: 2 redundant requirements hidden
+note: required for `()` to implement `CoinductiveRev`
+ --> $DIR/double-cycle-inductive-coinductive.rs:27:19
+ |
+LL | impl<T: TraitRev> CoinductiveRev for T {}
+ | -------- ^^^^^^^^^^^^^^ ^
+ | |
+ | unsatisfied trait bound introduced here
+ = note: 7 redundant requirements hidden
  = note: required for `()` to implement `TraitRev`
 note: required by a bound in `impls_trait_rev`
  --> $DIR/double-cycle-inductive-coinductive.rs:29:23

tests/ui/traits/next-solver/cycles/inductive-fixpoint-hang.stderr

@@ -1,19 +1,19 @@
-error[E0275]: overflow evaluating the requirement `W<_>: Trait`
+error[E0275]: overflow evaluating the requirement `W<W<_>>: Trait`
  --> $DIR/inductive-fixpoint-hang.rs:31:19
  |
 LL | impls_trait::<W<_>>();
  | ^^^^
  |
-note: required for `W<W<_>>` to implement `Trait`
+note: required for `W<W<W<_>>>` to implement `Trait`
  --> $DIR/inductive-fixpoint-hang.rs:22:17
  |
 LL | impl<T: ?Sized> Trait for W<W<T>>
  | ^^^^^ ^^^^^^^
 LL | where
 LL | W<T>: Trait,
  | ----- unsatisfied trait bound introduced here
- = note: 3 redundant requirements hidden
- = note: required for `W<W<W<W<W<_>>>>>` to implement `Trait`
+ = note: 8 redundant requirements hidden
+ = note: required for `W<W<W<W<W<W<W<W<W<W<W<_>>>>>>>>>>>` to implement `Trait`
 note: required by a bound in `impls_trait`
  --> $DIR/inductive-fixpoint-hang.rs:28:19
  |

tests/ui/traits/next-solver/cycles/inductive-not-on-stack.rs

@@ -39,8 +39,8 @@ fn impls_ar<T: AR>() {}
 
 fn main() {
  impls_a::<()>();
- //~^ ERROR overflow evaluating the requirement `(): A`
+ //~^ ERROR overflow evaluating the requirement `(): B`
 
  impls_ar::<()>();
- //~^ ERROR overflow evaluating the requirement `(): CR`
+ //~^ ERROR overflow evaluating the requirement `(): AR`
 }