trait solver: Handle reflexive region constraints - #161988
Conversation
rustbot
added
S-waiting-on-review
|
r? @JohnTitor rustbot has assigned @JohnTitor. Use Why was this reviewer chosen?The reviewer was selected based on:
|
rustbot
added
S-waiting-on-author
|
Sup @BoxyUwU and @adwinwhite o/ The first check handles When I followed that path, some information was missing from the assumptions used at the root. The implied There's a similar problem while leaving a binder. If the binder's own assumptions already prove At the root, a I added tests for direct and transitive assumptions, type outlives assumptions, and the root case. The full My take is that #161963 is a good small fix for #161733, while this PR now deals with the wider path behind #19. I would keep the extra work here, but I'm not sure where you want the PR boundary. Would you rather keep it this way or move the extra changes to a follow-up on #161963? |
rustbot
added
S-waiting-on-review
| // matters as constraints are also destructured in the root, where reflexive candidates | ||
| // are the whole reason an OR is satisfiable. E.g. `!T: 'a` with a `!T: 'a` assumption | ||
| // ends up as `Or([.., RegionOutlives('a, 'a)])`. | ||
| RegionOutlives(r1, r2, _) if r1 == r2 => RegionConstraint::new_true(), |
There was a problem hiding this comment.
Do one of your tests cover needing this? It's not clear to me why we need this special case of exactly 'a: 'a in evaluate when we also have the more general fix in pull_region_outlives_constraints
There was a problem hiding this comment.
Yep, there is a test for this now. I replaced the old syn case since that also needed the assumption work moved to #162238.
The new test is a small root case with T: 'a + 'b and a T: 'b constraint. Root destructuring makes an OR with an unrelated 'a: 'b candidate and the reflexive 'b: 'b candidate. The general check in pull_region_outlives_constraints_out_of_universe never gets a chance to handle this because the root does not leave a universe. Regionck also still flattens that OR like an AND, so evaluate has to notice 'b: 'b and make the OR true before that happens.
I removed the evaluator branch once to check the test, and it fails with the lifetime bound error. So I kept this bit, but rewrote the test and comment around the root case. In my opinion it still fits here: same reflexive constraint bug, just a path that does not call the general helper.
6e44229 to
4439c22
Compare
This comment has been minimized.
This comment has been minimized.
| // Root constraints never go through `pull_region_outlives_constraints_out_of_universe`. | ||
| // A reflexive leaf may be the candidate which makes a root OR true, so discharge it here | ||
| // instead of requiring the remaining candidates to hold. | ||
| RegionOutlives(r1, r2, _) if r1 == r2 => {} |
There was a problem hiding this comment.
Want to instead move this into construction of And, i.e. filter out any leaf constraints of the form 'a: 'a 🤔 Then you can drop all of the changes to this function
Feels more appropriately placed than handling region outlives in the type outlives handling function. And I do think in general we probably just don't want to be having 'a: 'a constraints littered all over the place since they're kind useless
There was a problem hiding this comment.
Yep, done. And::new drops any 'a: 'a leaf now, and all the changes to destructure_type_outlives_constraints_in_root are gone, it's back to what it was.
I did have to add one more thing for that to actually work. Or::new returns true as soon as it sees an empty And. Without it the root test still fails, because the reflexive candidate becomes And([]) and you end up with Or([And([]), And([X])]), which isn't is_true(). Regionck still flattens ORs like ANDs, so it would go and ask for X anyway. Seems like the right canonical form regardless, an empty AND is true so the OR is true.
I also pointed Or::new_leaf and RegionConstraint::new_leaf at And::new/Or::new. They were building the boxes by hand, so a reflexive leaf could slip past the filter there.
I like this better than what I had. The special casing in the root function never really felt like it belonged in the type outlives arm, and having one rule about what an AND is allowed to contain is easier to keep in my head.
There's one small side effect. test-infra-fails-properly was using 'c: 'c as the deliberately wrong candidate in its expect clause, and that canonicalizes to true now, so the error changed shape. I swapped it for 'b: 'c so the test still shows a mismatched candidate instead of true vs false. If you'd rather just bless the new output and leave the test alone, say so and I'll flip it.
A reflexive `'a: 'a` leaf is always satisfied, so filter it out in `And::new` instead of pattern matching for it in the places which happen to build such a constraint. An AND which ends up empty is trivially true, which makes the OR containing it true. This is how a reflexive candidate discharges a root type outlives constraint, so `destructure_type_outlives_constraints_in_root` no longer has to look at region outlives leaves at all.
6709071 to
ca6e6f0
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. |
| /// An OR of AND of LEAF constraints. Always in "canonical form" meaning: | ||
| /// - No two ANDs are equivalent | ||
| /// - All ANDs are in canonical form | ||
| /// - If any AND is empty, i.e. trivially true, it is the only AND |
There was a problem hiding this comment.
Can you add a FIXME(-Zassumptions-on-binders) that we should consider doing something more general and dropping ands which are supersets of other ands. E.g. OR(AND('a: 'b), AND('a: 'b, 'b: 'c)) really ought to just drop the second AND
There was a problem hiding this comment.
Added, right under the canonical form list.
I wrote it so the empty AND rule reads as the small case of the same idea. An empty AND is a subset of everything, so a general superset check gives you the "if any AND is empty it is the only AND" line for free. Felt odd listing them as two separate rules once I noticed that.
Agree on the general point though. Keeping AND('a: 'b, 'b: 'c) around next to AND('a: 'b) is just more for regionck to walk through for nothing.
| let mut new_ands: Vec<And<I, S>> = Vec::new(); | ||
|
|
||
| for and in ands { | ||
| // An empty AND is trivially true, which makes the whole OR true no matter what the |
There was a problem hiding this comment.
same here :3
There was a problem hiding this comment.
Added, on the dedup check since that's the code you'd actually touch to do it.
Funny thing I ran into while writing it: the subset check is already half of is_and_equivalent_to. That does containment both ways, so "is a superset of" is just dropping one of the two all calls. So it's not a cost thing.
The reason I didn't just do it is that it isn't only a filter. Right now I skip an AND if it matches one I already pushed. For the general rule I'd also have to go back and drop ANDs I already pushed when a smaller one turns up later, since iteration order decides which one you see first. That's a real change to the loop and I'd rather not sneak it into a PR about reflexive constraints.
There was a problem hiding this comment.
Yeah good to do as a separate PR. cc rust-lang/project-assumptions-on-binders#47
|
@rustbot author |
rustbot
added
S-waiting-on-author
|
Reminder, once the PR becomes ready for a review, use |
|
@rustbot ready |
rustbot
added
S-waiting-on-review
|
sick, I'll r+ this once CI is green. |
…utlives_assumptions, r=BoxyUwU trait solver: Include implied outlives assumptions Part of rust-lang/project-assumptions-on-binders#19 Split out of rust-lang#161988 after @BoxyUwU pointed out that these are about which assumptions we keep, not really about reflexive region constraints. I went back through where each piece comes from and found two gaps. Inside a binder we kept `Ty: 'a`, but the region relation only knew about explicit region clauses. That means something like `&'b T: 'a` did not also give us `'b: 'a`. At the root it was a slightly different version of the same problem: `known_type_outlives` has the explicit where clauses, while implied bounds from things like `&'b self` live in `region_bound_pairs`, so constraint destructuring never saw them. `Assumptions::new` now pulls the free region components out of type outlives clauses and adds those edges to the region relation. I think doing it there is the cleanest spot. All callers get the same view of an assumption, and the original type clauses stay around for placeholder and alias cases. Regions bound inside the type are ignored because they do not name anything we can use outside that binder. The root path now adds its implied type bounds to the same assumption set before destructuring. The regression uses an implied `I: 'b` from a receiver and a separate `'b: 'a` relation, so it covers this without leaning on the reflexive fix from rust-lang#161988. There are also binder checks for a reference and a higher-ranked function type. Those caught an easy testing trap here: a green direct constraint could have depended on the other PR, so the checks look at the lifted candidates instead. Personally, I think splitting this was the right call. It is really a change to how assumption data is built, and that is easier to reason about on its own than under the reflexive constraint fix. cc @BoxyUwU, this is the pair of changes you asked me to pull out.
…utlives_assumptions, r=BoxyUwU trait solver: Include implied outlives assumptions Part of rust-lang/project-assumptions-on-binders#19 Split out of rust-lang#161988 after @BoxyUwU pointed out that these are about which assumptions we keep, not really about reflexive region constraints. I went back through where each piece comes from and found two gaps. Inside a binder we kept `Ty: 'a`, but the region relation only knew about explicit region clauses. That means something like `&'b T: 'a` did not also give us `'b: 'a`. At the root it was a slightly different version of the same problem: `known_type_outlives` has the explicit where clauses, while implied bounds from things like `&'b self` live in `region_bound_pairs`, so constraint destructuring never saw them. `Assumptions::new` now pulls the free region components out of type outlives clauses and adds those edges to the region relation. I think doing it there is the cleanest spot. All callers get the same view of an assumption, and the original type clauses stay around for placeholder and alias cases. Regions bound inside the type are ignored because they do not name anything we can use outside that binder. The root path now adds its implied type bounds to the same assumption set before destructuring. The regression uses an implied `I: 'b` from a receiver and a separate `'b: 'a` relation, so it covers this without leaning on the reflexive fix from rust-lang#161988. There are also binder checks for a reference and a higher-ranked function type. Those caught an easy testing trap here: a green direct constraint could have depended on the other PR, so the checks look at the lifted candidates instead. Personally, I think splitting this was the right call. It is really a change to how assumption data is built, and that is easier to reason about on its own than under the reflexive constraint fix. cc @BoxyUwU, this is the pair of changes you asked me to pull out.
Rollup merge of #162238 - Dnreikronos:trait_solver/implied_outlives_assumptions, r=BoxyUwU trait solver: Include implied outlives assumptions Part of rust-lang/project-assumptions-on-binders#19 Split out of #161988 after @BoxyUwU pointed out that these are about which assumptions we keep, not really about reflexive region constraints. I went back through where each piece comes from and found two gaps. Inside a binder we kept `Ty: 'a`, but the region relation only knew about explicit region clauses. That means something like `&'b T: 'a` did not also give us `'b: 'a`. At the root it was a slightly different version of the same problem: `known_type_outlives` has the explicit where clauses, while implied bounds from things like `&'b self` live in `region_bound_pairs`, so constraint destructuring never saw them. `Assumptions::new` now pulls the free region components out of type outlives clauses and adds those edges to the region relation. I think doing it there is the cleanest spot. All callers get the same view of an assumption, and the original type clauses stay around for placeholder and alias cases. Regions bound inside the type are ignored because they do not name anything we can use outside that binder. The root path now adds its implied type bounds to the same assumption set before destructuring. The regression uses an implied `I: 'b` from a receiver and a separate `'b: 'a` relation, so it covers this without leaning on the reflexive fix from #161988. There are also binder checks for a reference and a higher-ranked function type. Those caught an easy testing trap here: a green direct constraint could have depended on the other PR, so the checks look at the lifted candidates instead. Personally, I think splitting this was the right call. It is really a change to how assumption data is built, and that is easier to reason about on its own than under the reflexive constraint fix. cc @BoxyUwU, this is the pair of changes you asked me to pull out.
4 participants
View all comments
Fixes rust-lang/project-assumptions-on-binders#19
A reflexive placeholder constraint like
'a: 'acan show up after we compute transitive region constraints. We then try to pull it out of the current universe by looking for lower-universe candidates. With none to choose from it becomes false, even though'a: 'awas true the whole time.I first had this buried in the binder region work, which made a green test pretty meaningless because too much else was changing around it. Split out on its own, the fix is just to accept equal regions before doing the universe rewrite. I think that is the sensible place to stop: it handles the direct case and the reflexive edges made by the transitive pass. I added a regression for the direct case.
cc/ @BoxyUwU o/