-Znext-solver : Abort on the first overflowed obligation in fulfillment - #162223
Conversation
|
Some changes occurred to the core trait solver cc @rust-lang/initiative-trait-system-refactor |
rustbot
added
S-waiting-on-review
| // We limit the total count of inference progress to avoid hang so we don't | ||
| // try to recover from this. | ||
| // It's more complicated to collect all overflows so we stopped doing that. | ||
| // This is consistent with the old solver's behavior. |
There was a problem hiding this comment.
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?
|
couldn't not look at this 😅 @ShoyuVanilla please still look at this PR as it's useful, but r? lcnr |
|
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. |
|
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. |
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 |
lcnr
added
the
I-types-nominated
a6c578a to
85c8774
Compare
This comment has been minimized.
This comment has been minimized.
lcnr
removed
the
I-types-nominated
|
r=me after rebase :3 |
85c8774 to
3dab168
Compare
|
This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
|
@bors r=lcnr |
rust-bors
Bot
added
S-waiting-on-bors
|
Forgot to commit auto formatting :/ |
rust-bors
Bot
added
S-waiting-on-author
|
This pull request was unapproved. |
3dab168 to
96536dd
Compare
|
@bors r=lcnr |
rust-bors
Bot
added
S-waiting-on-bors
Rollup merge of #162223 - adwinwhite:abort-on-fulfillment-overflow, r=lcnr `-Znext-solver` : Abort on the first overflowed obligation in fulfillment 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
5 participants
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