extend NLL checker to understand 'empty combined with universes
#70950
Conversation
This file contains 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 comment has been minimized.
This comment has been minimized.
rust-highfive
added
the
S-waiting-on-review
nikomatsakis
force-pushed
the
leak-check-nll-2
branch
from
b01f8c5 to
1cbd39f
Compare
| // type checking prevents it (and stops compilation) for now. | ||
| f == g; // OK | ||
| f == g; | ||
| //~^ ERROR higher-ranked subtype error |
There was a problem hiding this comment.
Hmm, I guess the code here isn't doing what I thought it was
rust/src/librustc_mir/borrow_check/type_check/mod.rs
Lines 2302 to 2333 in 96d77f0
I think I was expecting this to implicitly do self.infcx.resolve_vars_if_possible(common_ty) in the second sub_types call.
There was a problem hiding this comment.
I don't think that would have any effect. What happens in the first call is that we instantiate common_ty to a version of ty_left, but with distinct region variables (which are related to the regions in ty_left). It sounds like you were expecting common_ty and ty_left to get unified?
There was a problem hiding this comment.
No, I was expecting common_ty to be a generalized version of ty_left. I was then expecting the next call to relate the same generalized type to ty_right, but it is instead equating common_ty to a generalized version of ty_right.
In this specific case I was expecting common_ty to be instantiated as fn(&'? i32) and then be constrained to be a supertype of fn(&'a i32) and fn(&i32). Instead it's instantiated as both fn(&'? i32) and fn(&i32), which is an error.
There was a problem hiding this comment.
I can't tell if you're suggesting a change here or not =)
There was a problem hiding this comment.
That said, I think I was expecting the same as you. Also, re-reading the code, I'm a bit.. surprised by it. It seems like there's a baked-in assumption about the sort of types that we'll apply the comparison operator to that probably ought to be checked (i.e., it seems like we're assuming that in all other cases, the values are trivially of the same type, I guess?).
Still, I'm not entirely sure how you are deriving your conclusions. I think I expected:
common_tygets instantiated tofn(&'? i32)(where'a: '?, unless I got something backward)- we then require that
fn(&'? i32) <: fn(&i32), which yields a requirement thatfor<'b> { 'b: '? }, which we cannot satisfy (though, prior to this PR, we could) - hence we get a higher-ranked error
In particular I don't really know what this means:
Instead it's instantiated as both
fn(&'? i32)andfn(&i32), which is an error.
How can a single variable be instantiated as two types? Maybe we mean something different by 'instantiated'.
There was a problem hiding this comment.
Looking at the code again, I was wrong what the problem was. The types are being related the opposite way to they actually should be.
common_ty is the type that the comparison is being done at, so each of the operand should be a subtype of common_ty, that is common_ty should be a common super-type.
It seems like there's a baked-in assumption about the sort of types that we'll apply the comparison operator to that probably ought to be checked (i.e., it seems like we're assuming that in all other cases, the values are trivially of the same type, I guess?).
Yes, this should probably be changed to match the remaining types where BinOp::Eq is allowed (ints, bool, char) and assert equality I guess this can be done separately.
There was a problem hiding this comment.
@matthewjasper good point, I suppose we do want a common super-type, not a common sub-type! I'll push a commit making this change.
There was a problem hiding this comment.
Update: it wasn't easy to change the order. This is because, I think, the relate_tys code still has some hard-coded assumptions that assume that the super-type is not an uninstantiated variable, or something like that. This may have been what led to the code being written this way in the first place.
|
☔ The latest upstream changes (presumably #71031) made this pull request unmergeable. Please resolve the merge conflicts. |
nikomatsakis
force-pushed
the
leak-check-nll-2
branch
from
1cbd39f to
87ff84e
Compare
|
The job Click to expand the log.I'm a bot! I can only do what humans tell me to, so if this was not helpful or you have suggestions for improvements, please ping or otherwise contact |
|
☔ The latest upstream changes (presumably #71162) made this pull request unmergeable. Please resolve the merge conflicts. |
nikomatsakis
force-pushed
the
leak-check-nll-2
branch
from
87ff84e to
0749721
Compare
lqd
reviewed
Apr 16, 2020
|
The job Click to expand the log.I'm a bot! I can only do what humans tell me to, so if this was not helpful or you have suggestions for improvements, please ping or otherwise contact |
|
I don't understand these mir-opt failures though -- I have run |
|
Since the CI failure is on 64 bit and I'm assuming you're on 64 bit, too, platform differences can't be the cause of it I think. We have a flag (https://github.com/rust-lang/rust/tree/master/src/test/mir-opt#--blessable-test-format) to emit one file per bit size, but you need to run with I can't tell with the inference variables, but the rest of the failures look like you added two lines at the top of the file and didn't rerun --bless. |
oli-obk
reviewed
Apr 16, 2020
|
@oli-obk huh. But I did re-run bless.. ok, I'll investigate, thanks! |
|
I wonder if it's just outdated stamp files... |
|
Sorry, I hid the comment. You need to run once with |
|
The job Click to expand the log.I'm a bot! I can only do what humans tell me to, so if this was not helpful or you have suggestions for improvements, please ping or otherwise contact |
|
So, I re-read our algorithm for SCCs, and I think @lqd is right that the In terms of the reference files, I can't run the 32-bit tests locally yet, I get some weird errors, I am probably missing packages on my machine. |
We don't need the `scc_dependency_order` vector, `all_sccs` is already in dependency order.
nikomatsakis
force-pushed
the
leak-check-nll-2
branch
from
d107e07 to
cb9458d
Compare
|
OK, I think I fixed the mir-opt test, and we now document (and take advantage) of the fact that |
|
@matthewjasper do you consider this a blocker? It seems kind of orthogonal from this PR to me. |
|
No, I'll try to fix it once this is merged. @bors r+ |
|
📌 Commit cb9458d has been approved by |
bors
added
S-waiting-on-bors
RalfJung
added a commit
to RalfJung/rust
that referenced
this pull request
Apr 30, 2020
…tthewjasper
extend NLL checker to understand `'empty` combined with universes
This PR extends the NLL region checker to understand `'empty` combined with universes. In particular, it means that the NLL region checker no longer considers `exists<R2> { forall<R1> { R1: R2 } }` to be provable. This is work towards rust-lang#59490, but we're not all the way there. One thing in particular it does not address is error messages.
The modifications to the NLL region inference code turned out to be simpler than expected. The main change is to require that if `R1: R2` then `universe(R1) <= universe(R2)`.
This constraint follows from the region lattice (shown below), because we assume then that `R2` is "at least" `empty(Universe(R2))`, and hence if `R1: R2` (i.e., `R1 >= R2` on the lattice) then `R1` must be in some universe that can name `'empty(Universe(R2))`, which requires that `Universe(R1) <= Universe(R2)`.
```
static ----------+-----...------+ (greatest)
| | |
early-bound and | |
free regions | |
| | |
scope regions | |
| | |
empty(root) placeholder(U1) |
| / |
| / placeholder(Un)
empty(U1) -- /
| /
... /
| /
empty(Un) -------- (smallest)
```
I also made what turned out to be a somewhat unrelated change to add a special region to represent `'empty(U0)`, which we use (somewhat hackily) to indicate well-formedness checks in some parts of the compiler. This fixes rust-lang#68550.
I did some investigation into fixing the error message situation. That's a bit trickier: the existing "nice region error" code around placeholders relies on having better error tracing than NLL currently provides, so that it knows (e.g.) that the constraint arose from applying a trait impl and things like that. I feel like I was hoping *not* to do such fine-grained tracing in NLL, and it seems like we...largely...got away with that. I'm not sure yet if we'll have to add more tracing information or if there is some sort of alternative.
It's worth pointing out though that I've not kind of shifted my opinion on whose job it should be to enforce lifetimes: I tend to think we ought to be moving back towards *something like* the leak-check (just not the one we *had*). If we took that approach, it would actually resolve this aspect of the error message problem, because we would be resolving 'higher-ranked errors' in the trait solver itself, and hence we wouldn't have to thread as much causal information back to the region checker. I think it would also help us with removing the leak check while not breaking some of the existing crates out there.
Regardless, I think it's worth landing this change, because it was relatively simple and it aligns the set of programs that NLL accepts with those that are accepted by the main region checker, and hence should at least *help* us in migration (though I guess we still also have to resolve the existing crates that rely on leak check for coherence).
r? @matthewjasper
|
⌛ Testing commit cb9458d with merge 27e245b59b1b76b9c0bf041819a192d4a46e2192... |
|
@bors retry (Yield) |
bors
added a commit
to rust-lang-ci/rust
that referenced
this pull request
Apr 30, 2020
Rollup of 5 pull requests Successful merges: - rust-lang#70950 (extend NLL checker to understand `'empty` combined with universes) - rust-lang#71433 (Add help message for missing right operand in condition) - rust-lang#71449 (Move `{Free,}RegionRelations` and `FreeRegionMap` to `rustc_infer`) - rust-lang#71559 (Detect git version before attempting to use --progress) - rust-lang#71597 (Rename Unique::empty() -> Unique::dangling()) Failed merges: r? @ghost
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This PR extends the NLL region checker to understand
'emptycombined with universes. In particular, it means that the NLL region checker no longer considersexists<R2> { forall<R1> { R1: R2 } }to be provable. This is work towards #59490, but we're not all the way there. One thing in particular it does not address is error messages.The modifications to the NLL region inference code turned out to be simpler than expected. The main change is to require that if
R1: R2thenuniverse(R1) <= universe(R2).This constraint follows from the region lattice (shown below), because we assume then that
R2is "at least"empty(Universe(R2)), and hence ifR1: R2(i.e.,R1 >= R2on the lattice) thenR1must be in some universe that can name'empty(Universe(R2)), which requires thatUniverse(R1) <= Universe(R2).I also made what turned out to be a somewhat unrelated change to add a special region to represent
'empty(U0), which we use (somewhat hackily) to indicate well-formedness checks in some parts of the compiler. This fixes #68550.I did some investigation into fixing the error message situation. That's a bit trickier: the existing "nice region error" code around placeholders relies on having better error tracing than NLL currently provides, so that it knows (e.g.) that the constraint arose from applying a trait impl and things like that. I feel like I was hoping not to do such fine-grained tracing in NLL, and it seems like we...largely...got away with that. I'm not sure yet if we'll have to add more tracing information or if there is some sort of alternative.
It's worth pointing out though that I've not kind of shifted my opinion on whose job it should be to enforce lifetimes: I tend to think we ought to be moving back towards something like the leak-check (just not the one we had). If we took that approach, it would actually resolve this aspect of the error message problem, because we would be resolving 'higher-ranked errors' in the trait solver itself, and hence we wouldn't have to thread as much causal information back to the region checker. I think it would also help us with removing the leak check while not breaking some of the existing crates out there.
Regardless, I think it's worth landing this change, because it was relatively simple and it aligns the set of programs that NLL accepts with those that are accepted by the main region checker, and hence should at least help us in migration (though I guess we still also have to resolve the existing crates that rely on leak check for coherence).
r? @matthewjasper