-
-
Notifications
You must be signed in to change notification settings - Fork 15.2k
trait solver: Capture binder region constraints while relating #157984
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
Dnreikronos
wants to merge
9
commits into
rust-lang:main
Choose a base branch
from
Dnreikronos:trait_solver/binder_region_constraints
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
9 commits
Select commit
Hold shift + click to select a range
bda8867
Capture binder region constraints while relating
Dnreikronos 4d4128b
Register solver region constraints while relating
Dnreikronos df359c7
Reproduce direct solver region registration failures
Dnreikronos d045016
Handle reflexive solver region constraints
Dnreikronos 8e08637
Normalize equated region vars in solver constraints
Dnreikronos 9fdde3f
Normalize transitive equated region variables
Dnreikronos 4bc4324
Move region constraint tests into test module
Dnreikronos c274696
Adapt region constraints to upstream APIs
Dnreikronos 70b9601
Clarify region constraint branch terminology
Dnreikronos File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| use super::compute_equated_region_var_replacements_from; | ||
|
|
||
| #[test] | ||
| fn equated_region_var_replacements_follow_transitive_region_var_chains() { | ||
| const REVAR_1: u8 = 1; | ||
| const REVAR_2: u8 = 2; | ||
| const PLACEHOLDER: u8 = 3; | ||
|
|
||
| let region_outlives = | ||
| [(REVAR_1, REVAR_2), (REVAR_2, REVAR_1), (REVAR_2, PLACEHOLDER), (PLACEHOLDER, REVAR_2)]; | ||
|
|
||
| let replacements = compute_equated_region_var_replacements_from( | ||
| ®ion_outlives, | ||
| |r| matches!(r, REVAR_1 | REVAR_2), | ||
| |r| matches!(r, REVAR_1 | REVAR_2), | ||
| ); | ||
|
|
||
| assert_eq!(replacements, vec![(REVAR_1, PLACEHOLDER), (REVAR_2, PLACEHOLDER)]); | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
19 changes: 19 additions & 0 deletions
19
tests/ui/assumptions_on_binders/principal-upcast-region-eq-issue-157859.rs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| //@compile-flags: -Zassumptions-on-binders -Znext-solver=globally | ||
| //@ dont-require-annotations: ERROR | ||
|
|
||
| trait Super<U> { | ||
| fn a(&self) { | ||
| let a: &dyn Sub = &(); | ||
| let b: &dyn Super<for<'a> fn(&'a ())> = a; | ||
| } | ||
| } | ||
|
|
||
| impl<T> Super<T> for () {} | ||
|
|
||
| trait Sub: Super<fn(&'static ())> {} | ||
|
|
||
| impl Sub for () {} | ||
|
|
||
| fn main() { | ||
| let a: &dyn Sub = &(); | ||
| } |
13 changes: 13 additions & 0 deletions
13
tests/ui/assumptions_on_binders/principal-upcast-region-eq-issue-157859.stderr
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| error[E0277]: the trait bound `&dyn Sub: CoerceUnsized<&dyn Super<for<'a> fn(&'a ())>>` is not satisfied | ||
| --> $DIR/principal-upcast-region-eq-issue-157859.rs:7:49 | ||
| | | ||
| LL | let b: &dyn Super<for<'a> fn(&'a ())> = a; | ||
| | ^ the nightly-only, unstable trait `Unsize<dyn Super<for<'a> fn(&'a ())>>` is not implemented for `dyn Sub` | ||
| | | ||
| = note: all implementations of `Unsize` are provided automatically by the compiler, see <https://doc.rust-lang.org/stable/std/marker/trait.Unsize.html> for more information | ||
| = note: required for `&dyn Sub` to implement `CoerceUnsized<&dyn Super<for<'a> fn(&'a ())>>` | ||
| = note: required for the cast from `&dyn Sub` to `&dyn Super<for<'a> fn(&'a ())>` | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
||
| For more information about this error, try `rustc --explain E0277`. |
23 changes: 23 additions & 0 deletions
23
tests/ui/assumptions_on_binders/trait-upcast-projection-region-eq.rs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| //@ compile-flags: -Zassumptions-on-binders -Znext-solver=globally | ||
|
|
||
| trait Super { | ||
| type Assoc; | ||
|
|
||
| fn a(&self) { | ||
| let a: &dyn Sub = &(); | ||
| let b: &dyn Super<Assoc = for<'a> fn(&'a ())> = a; | ||
| //~^ ERROR the trait bound `&dyn Sub: CoerceUnsized<&dyn Super<Assoc = for<'a> fn(&'a ())>>` is not satisfied | ||
| } | ||
| } | ||
|
|
||
| impl Super for () { | ||
| type Assoc = fn(&'static ()); | ||
| } | ||
|
|
||
| trait Sub: Super<Assoc = fn(&'static ())> {} | ||
|
|
||
| impl Sub for () {} | ||
|
|
||
| fn main() { | ||
| let a: &dyn Sub = &(); | ||
| } |
13 changes: 13 additions & 0 deletions
13
tests/ui/assumptions_on_binders/trait-upcast-projection-region-eq.stderr
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| error[E0277]: the trait bound `&dyn Sub: CoerceUnsized<&dyn Super<Assoc = for<'a> fn(&'a ())>>` is not satisfied | ||
| --> $DIR/trait-upcast-projection-region-eq.rs:8:57 | ||
| | | ||
| LL | let b: &dyn Super<Assoc = for<'a> fn(&'a ())> = a; | ||
| | ^ the nightly-only, unstable trait `Unsize<dyn Super<Assoc = for<'a> fn(&'a ())>>` is not implemented for `dyn Sub` | ||
| | | ||
| = note: all implementations of `Unsize` are provided automatically by the compiler, see <https://doc.rust-lang.org/stable/std/marker/trait.Unsize.html> for more information | ||
| = note: required for `&dyn Sub` to implement `CoerceUnsized<&dyn Super<Assoc = for<'a> fn(&'a ())>>` | ||
| = note: required for the cast from `&dyn Sub` to `&dyn Super<Assoc = for<'a> fn(&'a ())>` | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
||
| For more information about this error, try `rustc --explain E0277`. |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
im having a hard time understanding what motivated this change 🤔 can you give an example with:
View changes since the review
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
fyi I checked this with a local trace on
tests/ui/assumptions_on_binders/alias_outlives.rs, and I think I have a better handle on what is happening now.The passing case has this env assumption:
To prove
T::Assoc: for<'a> Trait<'a>, we enter the binder and proveT::Assoc: Trait<'!a_u1>. Selecting the blanket impl introduces an impl lifetime var,'?0in my trace.Before this normalization, the relevant constraint was:
So the alias being matched is
<T as AliasHaver>::Assoc, but its outlives target is'?0, not the placeholder directly.After normalization, the same constraint becomes:
Then matching against
<T as AliasHaver>::Assoc: 'staticgives:For the failing case, where the env only has
<T as AliasHaver>::Assoc: 'a, it gives:and that stays unsatisfied, which is what we want.
Without this normalization, the trace keeps the alias target as
'?0, andREGIONCK_ENV_PASSfails with:My read is that alias/env matching gets here before the later region closure pass. We already know
'?0 == '!a_u1in the sameAndbranch, but unless we make that visible first, the alias outlives path sees a current-universe var instead of the placeholder shape it needs.idk if this is the nicest layer for it, but the trace made the motivation a lot clearer to me. ltm if you want the raw trace bits and I can paste them too.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What actually goes wrong when we have these constraints:
im having a hard time understanding how we go from that to an
Ambiguitysomewhere. I'm assuming that this is happening inalias_outlives_candidates_from_assumptionswhen trying to rewriteAliasTyOutlivesViaEnv? I would expect that we get back aRegionOutlives('static, '?0)constraint from that, i don't understand why that would go on to cause problems :3Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yeah, your expectation would be right if
<T as AliasHaver>::Assoc: 'staticwas in the assumptions available here. fyi i traced this again and that's the bit i was missing.while handling
U1, i found thatget_placeholder_assumptions(U1)hastype_outlives: []. the'staticassumption comes from the root param env, soalias_outlives_candidates_from_assumptionsgivesOr([])here instead ofRegionOutlives('static, '?0).the rewrite then tries to move
AliasTyOutlivesViaEnv(...: '?0)out ofU1, butPlaceholderReplaceronly replaces placeholders, not revars.'?0stays inU1, themax_universe(candidate) < ucheck fails, and that addsAmbiguity. btw, there are still candidates that could work once this gets back to the root, butevaluate_solver_constraintsees the ambiguous branch and nothing that's already true inU1, so the wholeOrbecomes ambiguous before any of them get there.normalization changes
'?0to the placeholder it's equated with first.PlaceholderReplacercan bind that, which lets the alias-outlives candidate escapeU1. once it gets back to the root, the full env is there and the'staticassumption can be matched.so imo your reasoning is right. if
RegionOutlives('static, '?0)existed here, the later closure should handle it. that edge just never gets produced at this point because the root assumption isn't available yet.idk if normalization is the nicest layer for this tbh, it does feel a little blunt to me. imo doing it before the rewrite still makes sense though, since that's where the equality and the type-outlives constraint are together in the same
And. ltm if you want the raw trace bits :)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what do you mean by this? can you link me to the place that adds the ambiguity? as far as I'm aware we only add ambiguity when we have
Noneassumptions for a binder (or when handling AliasTyOutlivesViaEnv during coherence)this also seems problematic to me 😅 I don't think that evaluating
OR(ambig, 'a: 'b)should result inambigthat feels wrong 🤔 I would probably expect us to just keep that as is. I guess this isn't technically wrong but it does make us wildly conservative wrt considering things to be ambiguous when they might still be fine...I would probably like us to fix this too 🤔
I think this is something we should "just" fix 🤔 we should be rewriting
<T as Trait>::Assoc: '?x_u1tofor<'a> <T as Trait>::Assoc: 'awhen rewriting things inu1. Or more generally, we should never be rewriting type outlives constraints to different type outlives in the same universe. The max_universe should either be lowered or they should now be region outlives constraintsas a fix this is slightly conservative 🤔 which is unfortunate, but I would need to spend a lot more time thinking about this before adding some form of "resolving regions" (or normalization as you've called it).
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
thx for your comment by the way it's cleared up a lot to me about things here (so much stuff is scuffed from my original impl of -Zassumptions-on-binders! lol!)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yeah, this is the
AmbiguityI meant in my previous comment: it's added here.PlaceholderReplacerdoesn't touch'?0_u1, so the candidate is still inu1, the< ucheck fails, and thatelsepushesAmbiguity. fyi I wasn't sayingalias_outlives_candidates_from_assumptionsitself adds it, my wording there was a bit imprecise.and yeah, I think you're right about the evaluator too. The rewrite also produces an
AliasTyOutlivesViaEnv(...: 'static)candidate, which could work once it reaches the root and the full env is available. Butevaluate_solver_constraintturnsOr(Ambiguity, remaining_candidate)intoAmbiguitybefore that happens. imo that's too eager, keeping the mixedOraround makes more sense so the other candidate still gets a chance at the root.btw I agree that handling the current-universe revar in
PlaceholderReplacersounds cleaner than the normalization I added. tbh I like that quite a bit more since it directly rewrites<T as Trait>::Assoc: '?x_u1intofor<'a> <T as Trait>::Assoc: 'aand keeps the universe-escaping logic local. The normalization works for this case, but idk, walking the wholeAndand replacing equated vars feels a bit too broad.would you prefer if I drop the normalization and make
PlaceholderReplacerrewrite current-universe revars to fresh bound regions instead? also, should the mixedOrevaluation be fixed in this PR, or would you rather keep that as a follow-up? ltm what you think :)