-Znext-solver : Abort on the first overflowed obligation in fulfillment

[adwinwhite]

Fixes rust-lang/trait-system-refactor-initiative#294 cc https://rust-lang.zulipchat.com/#narrow/channel/618216-t-types.2Fcall-for-participation/topic/handling.20overflow.20in.20fulfill/with/621040305

We used to drop all subsequent obligations when one obligation overflows in fulfillment. It means that we don't really prove all obligations even if fulfillment has no pending obligations and returns no error. We now eagerly abort on the first overflowed obligation.

r? @ShoyuVanilla
cc @lcnr

[rustbot]

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

[lcnr]

please also note how it's incredibly rare to actually encounter fulfillment overflow as a single goal would have to result in different inference progress a recursion_depth number of times. This mostly happens in bugs or with Subtype obligations because we no longer use the sub_unification_table in generalize 🤔 also, style question

we currently check depth after incrementing it, which seems odd. Should we flip it around and instead check depth before incrementing it in the else branch?

View changes since the review

[lcnr]

couldn't not look at this 😅

@ShoyuVanilla please still look at this PR as it's useful, but

r? lcnr
r=me after nits

[ShoyuVanilla]

Makes sense to me as well 😄

View changes since this review

[theemathas]

Is this code path reachable from coherence in stable rust?

[adwinwhite]

Is this code path reachable from coherence in stable rust?

One possibility is that one impl specializes another and their overlapping computing has overflowed obligations in fulfillment. I am having trouble constructing a test for this though.

[adwinwhite]

Thinking about specialization a little more. I guess we can assume that if one impl specializes another, they can't have overflowed obligations in fulfillment when computing impossible intersection. The feeling is that the parent's predicates must be provable in the child's param env, so their fresh clauses probably wouldn't progress each other alternatively when put in the same fulfillment.

[lcnr]

Is this code path reachable from coherence in stable rust?

yes, though given the difficulty of actually triggering fulfillment overflow without uses of opaque types, I don't think this is practically observable, I guess a quick types nomination

[rust-bors]

☔ The latest upstream changes (presumably #162406) made this pull request unmergeable. Please resolve the merge conflicts by rebasing.