Skip to content

Commit 34e91ec

Browse files
Higher ranked goal source, do overflow handling less badly
1 parent 3e03b1b commit 34e91ec

15 files changed

+163
-144
lines changed

compiler/rustc_middle/src/traits/solve.rs

+2
Original file line numberDiff line numberDiff line change
@@ -273,6 +273,8 @@ pub enum GoalSource {
273273
/// they are from an impl where-clause. This is necessary due to
274274
/// backwards compatability, cc trait-system-refactor-initiatitive#70.
275275
ImplWhereBound,
276+
/// Instantiating a higher-ranked goal and re-proving it.
277+
InstantiateHigherRanked,
276278
}
277279

278280
/// Possible ways the given goal can be proven.

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

+1
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
127127
let source = match source {
128128
GoalSource::Misc => "misc",
129129
GoalSource::ImplWhereBound => "impl where-bound",
130+
GoalSource::InstantiateHigherRanked => "higher-ranked goal",
130131
};
131132
writeln!(this.f, "ADDED GOAL ({source}): {goal:?}")?
132133
}

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -454,7 +454,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
454454
} else {
455455
self.infcx.enter_forall(kind, |kind| {
456456
let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
457-
self.add_goal(GoalSource::ImplWhereBound, goal);
457+
self.add_goal(GoalSource::InstantiateHigherRanked, goal);
458458
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
459459
})
460460
}

compiler/rustc_trait_selection/src/solve/fulfill.rs

+76-75
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,10 @@ use rustc_infer::traits::solve::inspect::ProbeKind;
77
use rustc_infer::traits::solve::{CandidateSource, GoalSource, MaybeCause};
88
use rustc_infer::traits::{
99
self, FulfillmentError, FulfillmentErrorCode, MismatchedProjectionTypes, Obligation,
10-
PredicateObligation, SelectionError, TraitEngine,
10+
ObligationCause, PredicateObligation, SelectionError, TraitEngine,
1111
};
12-
use rustc_middle::ty;
1312
use rustc_middle::ty::error::{ExpectedFound, TypeError};
13+
use rustc_middle::ty::{self, TyCtxt};
1414

1515
use super::eval_ctxt::GenerateProofTree;
1616
use super::inspect::{ProofTreeInferCtxtExt, ProofTreeVisitor};
@@ -219,14 +219,14 @@ fn fulfillment_error_for_no_solution<'tcx>(
219219
}
220220
ty::PredicateKind::Subtype(pred) => {
221221
let (a, b) = infcx.enter_forall_and_leak_universe(
222-
root_obligation.predicate.kind().rebind((pred.a, pred.b)),
222+
obligation.predicate.kind().rebind((pred.a, pred.b)),
223223
);
224224
let expected_found = ExpectedFound::new(true, a, b);
225225
FulfillmentErrorCode::SubtypeError(expected_found, TypeError::Sorts(expected_found))
226226
}
227227
ty::PredicateKind::Coerce(pred) => {
228228
let (a, b) = infcx.enter_forall_and_leak_universe(
229-
root_obligation.predicate.kind().rebind((pred.a, pred.b)),
229+
obligation.predicate.kind().rebind((pred.a, pred.b)),
230230
);
231231
let expected_found = ExpectedFound::new(false, a, b);
232232
FulfillmentErrorCode::SubtypeError(expected_found, TypeError::Sorts(expected_found))
@@ -272,17 +272,30 @@ fn fulfillment_error_for_stalled<'tcx>(
272272
}
273273
}
274274

275+
fn find_best_leaf_obligation<'tcx>(
276+
infcx: &InferCtxt<'tcx>,
277+
obligation: &PredicateObligation<'tcx>,
278+
) -> PredicateObligation<'tcx> {
279+
let obligation = infcx.resolve_vars_if_possible(obligation.clone());
280+
infcx
281+
.visit_proof_tree(
282+
obligation.clone().into(),
283+
&mut BestObligation { obligation: obligation.clone() },
284+
)
285+
.break_value()
286+
.unwrap_or(obligation)
287+
}
288+
275289
struct BestObligation<'tcx> {
276290
obligation: PredicateObligation<'tcx>,
277291
}
278292

279293
impl<'tcx> BestObligation<'tcx> {
280294
fn with_derived_obligation(
281295
&mut self,
282-
derive_obligation: impl FnOnce(&mut Self) -> PredicateObligation<'tcx>,
296+
derived_obligation: PredicateObligation<'tcx>,
283297
and_then: impl FnOnce(&mut Self) -> <Self as ProofTreeVisitor<'tcx>>::Result,
284298
) -> <Self as ProofTreeVisitor<'tcx>>::Result {
285-
let derived_obligation = derive_obligation(self);
286299
let old_obligation = std::mem::replace(&mut self.obligation, derived_obligation);
287300
let res = and_then(self);
288301
self.obligation = old_obligation;
@@ -298,13 +311,10 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
298311
}
299312

300313
fn visit_goal(&mut self, goal: &super::inspect::InspectGoal<'_, 'tcx>) -> Self::Result {
314+
// FIXME: Throw out candidates that have no failing WC and >0 failing misc goal.
315+
// This most likely means that the goal just didn't unify at all, e.g. a param
316+
// candidate with an alias in it.
301317
let candidates = goal.candidates();
302-
// FIXME: Throw out candidates that have no failing WC and >1 failing misc goal.
303-
304-
// HACK:
305-
if self.obligation.recursion_depth > 3 {
306-
return ControlFlow::Break(self.obligation.clone());
307-
}
308318

309319
let [candidate] = candidates.as_slice() else {
310320
return ControlFlow::Break(self.obligation.clone());
@@ -320,80 +330,71 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
320330
let tcx = goal.infcx().tcx;
321331
let mut impl_where_bound_count = 0;
322332
for nested_goal in candidate.instantiate_nested_goals(self.span()) {
323-
if matches!(nested_goal.source(), GoalSource::ImplWhereBound) {
324-
impl_where_bound_count += 1;
325-
} else {
326-
continue;
333+
let obligation;
334+
match nested_goal.source() {
335+
GoalSource::Misc => {
336+
continue;
337+
}
338+
GoalSource::ImplWhereBound => {
339+
obligation = Obligation {
340+
cause: derive_cause(
341+
tcx,
342+
candidate.kind(),
343+
self.obligation.cause.clone(),
344+
impl_where_bound_count,
345+
parent_trait_pred,
346+
),
347+
param_env: nested_goal.goal().param_env,
348+
predicate: nested_goal.goal().predicate,
349+
recursion_depth: self.obligation.recursion_depth + 1,
350+
};
351+
impl_where_bound_count += 1;
352+
}
353+
GoalSource::InstantiateHigherRanked => {
354+
obligation = self.obligation.clone();
355+
}
327356
}
328357

329358
// Skip nested goals that hold.
359+
//FIXME: We should change the max allowed certainty based on if we're
360+
// visiting an ambiguity or error obligation.
330361
if matches!(nested_goal.result(), Ok(Certainty::Yes)) {
331362
continue;
332363
}
333364

334-
self.with_derived_obligation(
335-
|self_| {
336-
let mut cause = self_.obligation.cause.clone();
337-
cause = match candidate.kind() {
338-
ProbeKind::TraitCandidate {
339-
source: CandidateSource::Impl(impl_def_id),
340-
result: _,
341-
} => {
342-
let idx = impl_where_bound_count - 1;
343-
if let Some((_, span)) = tcx
344-
.predicates_of(impl_def_id)
345-
.instantiate_identity(tcx)
346-
.iter()
347-
.nth(idx)
348-
{
349-
cause.derived_cause(parent_trait_pred, |derived| {
350-
traits::ImplDerivedObligation(Box::new(
351-
traits::ImplDerivedObligationCause {
352-
derived,
353-
impl_or_alias_def_id: impl_def_id,
354-
impl_def_predicate_index: Some(idx),
355-
span,
356-
},
357-
))
358-
})
359-
} else {
360-
cause
361-
}
362-
}
363-
ProbeKind::TraitCandidate {
364-
source: CandidateSource::BuiltinImpl(..),
365-
result: _,
366-
} => {
367-
cause.derived_cause(parent_trait_pred, traits::BuiltinDerivedObligation)
368-
}
369-
_ => cause,
370-
};
371-
372-
Obligation {
373-
cause,
374-
param_env: nested_goal.goal().param_env,
375-
predicate: nested_goal.goal().predicate,
376-
recursion_depth: self_.obligation.recursion_depth + 1,
377-
}
378-
},
379-
|self_| self_.visit_goal(&nested_goal),
380-
)?;
365+
self.with_derived_obligation(obligation, |this| nested_goal.visit_with(this))?;
381366
}
382367

383368
ControlFlow::Break(self.obligation.clone())
384369
}
385370
}
386371

387-
fn find_best_leaf_obligation<'tcx>(
388-
infcx: &InferCtxt<'tcx>,
389-
obligation: &PredicateObligation<'tcx>,
390-
) -> PredicateObligation<'tcx> {
391-
let obligation = infcx.resolve_vars_if_possible(obligation.clone());
392-
infcx
393-
.visit_proof_tree(
394-
obligation.clone().into(),
395-
&mut BestObligation { obligation: obligation.clone() },
396-
)
397-
.break_value()
398-
.unwrap_or(obligation)
372+
fn derive_cause<'tcx>(
373+
tcx: TyCtxt<'tcx>,
374+
candidate_kind: ProbeKind<'tcx>,
375+
mut cause: ObligationCause<'tcx>,
376+
idx: usize,
377+
parent_trait_pred: ty::PolyTraitPredicate<'tcx>,
378+
) -> ObligationCause<'tcx> {
379+
match candidate_kind {
380+
ProbeKind::TraitCandidate { source: CandidateSource::Impl(impl_def_id), result: _ } => {
381+
if let Some((_, span)) =
382+
tcx.predicates_of(impl_def_id).instantiate_identity(tcx).iter().nth(idx)
383+
{
384+
cause = cause.derived_cause(parent_trait_pred, |derived| {
385+
traits::ImplDerivedObligation(Box::new(traits::ImplDerivedObligationCause {
386+
derived,
387+
impl_or_alias_def_id: impl_def_id,
388+
impl_def_predicate_index: Some(idx),
389+
span,
390+
}))
391+
})
392+
}
393+
}
394+
ProbeKind::TraitCandidate { source: CandidateSource::BuiltinImpl(..), result: _ } => {
395+
cause = cause.derived_cause(parent_trait_pred, traits::BuiltinDerivedObligation);
396+
}
397+
_ => {}
398+
};
399+
cause
399400
}

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

+10-4
Original file line numberDiff line numberDiff line change
@@ -128,10 +128,8 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
128128
/// back their inference constraints. This function modifies
129129
/// the state of the `infcx`.
130130
pub fn visit_nested_no_probe<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
131-
if self.goal.depth < visitor.config().max_depth {
132-
for goal in self.instantiate_nested_goals(visitor.span()) {
133-
try_visit!(visitor.visit_goal(&goal));
134-
}
131+
for goal in self.instantiate_nested_goals(visitor.span()) {
132+
try_visit!(goal.visit_with(visitor));
135133
}
136134

137135
V::Result::output()
@@ -360,6 +358,14 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
360358
source,
361359
}
362360
}
361+
362+
pub(crate) fn visit_with<V: ProofTreeVisitor<'tcx>>(&self, visitor: &mut V) -> V::Result {
363+
if self.depth < visitor.config().max_depth {
364+
try_visit!(visitor.visit_goal(self));
365+
}
366+
367+
V::Result::output()
368+
}
363369
}
364370

365371
/// The public API to interact with proof trees.

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ LL | impl<T: ?Sized + TwoW> Trait for W<T> {}
66
LL | impl<T: ?Sized + TwoW> Trait for T {}
77
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 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<_>>>>>>>>>>>>>>>>>>>>>>`
88
|
9-
= note: overflow evaluating the requirement `W<W<W<W<W<W<W<W<W<W<W<W<W<W<_>>>>>>>>>>>>>>: TwoW`
9+
= note: overflow evaluating the requirement `W<W<W<W<_>>>>: TwoW`
1010
= help: consider increasing the recursion limit by adding a `#![recursion_limit = "20"]` attribute to your crate (`coherence_fulfill_overflow`)
1111

1212
error: aborting due to 1 previous error

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

+18-18
Original file line numberDiff line numberDiff line change
@@ -1,52 +1,52 @@
1-
error[E0275]: overflow evaluating the requirement `(): Trait`
1+
error[E0275]: overflow evaluating the requirement `(): Inductive`
22
--> $DIR/double-cycle-inductive-coinductive.rs:32:19
33
|
44
LL | impls_trait::<()>();
55
| ^^
66
|
7-
note: required for `()` to implement `Inductive`
8-
--> $DIR/double-cycle-inductive-coinductive.rs:12:16
9-
|
10-
LL | impl<T: Trait> Inductive for T {}
11-
| ----- ^^^^^^^^^ ^
12-
| |
13-
| unsatisfied trait bound introduced here
147
note: required for `()` to implement `Trait`
158
--> $DIR/double-cycle-inductive-coinductive.rs:9:34
169
|
1710
LL | impl<T: Inductive + Coinductive> Trait for T {}
1811
| --------- ^^^^^ ^
1912
| |
2013
| unsatisfied trait bound introduced here
21-
= note: 2 redundant requirements hidden
14+
note: required for `()` to implement `Inductive`
15+
--> $DIR/double-cycle-inductive-coinductive.rs:12:16
16+
|
17+
LL | impl<T: Trait> Inductive for T {}
18+
| ----- ^^^^^^^^^ ^
19+
| |
20+
| unsatisfied trait bound introduced here
21+
= note: 7 redundant requirements hidden
2222
= note: required for `()` to implement `Trait`
2323
note: required by a bound in `impls_trait`
2424
--> $DIR/double-cycle-inductive-coinductive.rs:17:19
2525
|
2626
LL | fn impls_trait<T: Trait>() {}
2727
| ^^^^^ required by this bound in `impls_trait`
2828

29-
error[E0275]: overflow evaluating the requirement `(): TraitRev`
29+
error[E0275]: overflow evaluating the requirement `(): CoinductiveRev`
3030
--> $DIR/double-cycle-inductive-coinductive.rs:35:23
3131
|
3232
LL | impls_trait_rev::<()>();
3333
| ^^
3434
|
35-
note: required for `()` to implement `CoinductiveRev`
36-
--> $DIR/double-cycle-inductive-coinductive.rs:27:19
37-
|
38-
LL | impl<T: TraitRev> CoinductiveRev for T {}
39-
| -------- ^^^^^^^^^^^^^^ ^
40-
| |
41-
| unsatisfied trait bound introduced here
4235
note: required for `()` to implement `TraitRev`
4336
--> $DIR/double-cycle-inductive-coinductive.rs:21:40
4437
|
4538
LL | impl<T: CoinductiveRev + InductiveRev> TraitRev for T {}
4639
| -------------- ^^^^^^^^ ^
4740
| |
4841
| unsatisfied trait bound introduced here
49-
= note: 2 redundant requirements hidden
42+
note: required for `()` to implement `CoinductiveRev`
43+
--> $DIR/double-cycle-inductive-coinductive.rs:27:19
44+
|
45+
LL | impl<T: TraitRev> CoinductiveRev for T {}
46+
| -------- ^^^^^^^^^^^^^^ ^
47+
| |
48+
| unsatisfied trait bound introduced here
49+
= note: 7 redundant requirements hidden
5050
= note: required for `()` to implement `TraitRev`
5151
note: required by a bound in `impls_trait_rev`
5252
--> $DIR/double-cycle-inductive-coinductive.rs:29:23

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

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
1-
error[E0275]: overflow evaluating the requirement `W<_>: Trait`
1+
error[E0275]: overflow evaluating the requirement `W<W<_>>: Trait`
22
--> $DIR/inductive-fixpoint-hang.rs:31:19
33
|
44
LL | impls_trait::<W<_>>();
55
| ^^^^
66
|
7-
note: required for `W<W<_>>` to implement `Trait`
7+
note: required for `W<W<W<_>>>` to implement `Trait`
88
--> $DIR/inductive-fixpoint-hang.rs:22:17
99
|
1010
LL | impl<T: ?Sized> Trait for W<W<T>>
1111
| ^^^^^ ^^^^^^^
1212
LL | where
1313
LL | W<T>: Trait,
1414
| ----- unsatisfied trait bound introduced here
15-
= note: 3 redundant requirements hidden
16-
= note: required for `W<W<W<W<W<_>>>>>` to implement `Trait`
15+
= note: 8 redundant requirements hidden
16+
= note: required for `W<W<W<W<W<W<W<W<W<W<W<_>>>>>>>>>>>` to implement `Trait`
1717
note: required by a bound in `impls_trait`
1818
--> $DIR/inductive-fixpoint-hang.rs:28:19
1919
|

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@ fn impls_ar<T: AR>() {}
3939

4040
fn main() {
4141
impls_a::<()>();
42-
//~^ ERROR overflow evaluating the requirement `(): A`
42+
//~^ ERROR overflow evaluating the requirement `(): B`
4343

4444
impls_ar::<()>();
45-
//~^ ERROR overflow evaluating the requirement `(): CR`
45+
//~^ ERROR overflow evaluating the requirement `(): AR`
4646
}

0 commit comments

Comments
 (0)