-
Notifications
You must be signed in to change notification settings - Fork 13.5k
Consider WF of coroutine witness when proving outlives assumptions #143545
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
base: master
Are you sure you want to change the base?
Conversation
r? @spastorino rustbot has assigned @spastorino. Use |
Some changes occurred to the core trait solver cc @rust-lang/initiative-trait-system-refactor |
@bors2 try @rust-timer queue |
This comment has been minimized.
This comment has been minimized.
[experiment] Consider WF of coroutine witness when proving outlives assumptions This needs to be majorly cleaned up --- cc #110338 Consider, for example: ```rust use std::future::Future; trait Client { type Connecting<'a>: Future + Send where Self: 'a; fn connect(&'_ self) -> Self::Connecting<'_>; } fn call_connect<C>(c: &'_ C) -> impl Future + Send where C: Client + Send + Sync, { async move { c.connect().await } } ```
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
Finished benchmarking commit (c9e8f2f): comparison URL. Overall result: ❌✅ regressions and improvements - please read the text belowBenchmarking this pull request means it may be perf-sensitive – we'll automatically label it not fit for rolling up. You can override this, but we strongly advise not to, due to possible changes in compiler perf. Next Steps: If you can justify the regressions found in this try perf run, please do so in sufficient writing along with @bors rollup=never Instruction countOur most reliable metric. Used to determine the overall result above. However, even this metric can be noisy.
Max RSS (memory usage)Results (primary 1.1%, secondary -0.2%)A less reliable metric. May be of interest, but not used to determine the overall result above.
CyclesResults (primary 2.2%, secondary 0.7%)A less reliable metric. May be of interest, but not used to determine the overall result above.
Binary sizeThis benchmark run did not return any relevant results for this metric. Bootstrap: 460.528s -> 463.281s (0.60%) |
☔ The latest upstream changes (presumably #143538) made this pull request unmergeable. Please resolve the merge conflicts. |
69dda47
to
a7ec91c
Compare
@bors2 try |
[experiment] Consider WF of coroutine witness when proving outlives assumptions This needs to be majorly cleaned up --- cc #110338 Consider, for example: ```rust use std::future::Future; trait Client { type Connecting<'a>: Future + Send where Self: 'a; fn connect(&'_ self) -> Self::Connecting<'_>; } fn call_connect<C>(c: &'_ C) -> impl Future + Send where C: Client + Send + Sync, { async move { c.connect().await } } ```
Don't expect this to fix any code, but I want to see whether it causes new issues. @craterbot check |
👌 Experiment ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more |
🚧 Experiment ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more |
🎉 Experiment
|
a7ec91c
to
b5d740d
Compare
There are changes to the cc @jieyouxu |
b5d740d
to
6999485
Compare
@bors2 try @rust-timer queue |
This comment has been minimized.
This comment has been minimized.
[experiment] Consider WF of coroutine witness when proving outlives assumptions This needs to be majorly cleaned up --- cc #110338 Consider, for example: ```rust use std::future::Future; trait Client { type Connecting<'a>: Future + Send where Self: 'a; fn connect(&'_ self) -> Self::Connecting<'_>; } fn call_connect<C>(c: &'_ C) -> impl Future + Send where C: Client + Send + Sync, { async move { c.connect().await } } ```
This comment has been minimized.
This comment has been minimized.
Finished benchmarking commit (fd967a6): comparison URL. Overall result: ❌✅ regressions and improvements - please read the text belowBenchmarking this pull request means it may be perf-sensitive – we'll automatically label it not fit for rolling up. You can override this, but we strongly advise not to, due to possible changes in compiler perf. Next Steps: If you can justify the regressions found in this try perf run, please do so in sufficient writing along with @bors rollup=never Instruction countOur most reliable metric. Used to determine the overall result above. However, even this metric can be noisy.
Max RSS (memory usage)Results (primary 0.8%, secondary -2.9%)A less reliable metric. May be of interest, but not used to determine the overall result above.
CyclesResults (primary -2.5%, secondary 2.6%)A less reliable metric. May be of interest, but not used to determine the overall result above.
Binary sizeThis benchmark run did not return any relevant results for this metric. Bootstrap: 464.056s -> 465.213s (0.25%) |
TL;DR
This PR introduces an unstable flag
-Zhigher-ranked-assumptions
which tests out a new algorithm for dealing with some of the higher-ranked outlives problems that come from auto trait bounds on coroutines. See:While it doesn't fix all of the issues, it certainly fixed many of them, so I'd like to get this landed so people can test the flag on their own code.
Background
Consider, for example:
Due to the fact that we erase the lifetimes in a coroutine, we can think of the interior type of the async block as something like:
exists<'r, 's> { C, &'r C, C::Connecting<'s> }
. The first field is thec
we capture, the second is the auto-ref that we perform on the call to.connect()
, and the third is the resulting future we're awaiting at the first and only await point. Note that every region is uniquified differently in the interior types.For the async block to be
Send
, we must prove that both of the interior types areSend
. First, we have anexists<'r, 's>
binder, which needs to be instantiated universally since we treat the regions in this binder as unknown1. This gives us two types:{ &'!r C, C::Connecting<'!s> }
. Proving&'!r C: Send
is easy due to aSend
impl for references.Proving
C::Connecting<'!s>: Send
can only be done via the item bound, which then requiresC: '!s
to hold (due to thewhere Self: 'a
on the associated type definition). Unfortunately, we don't know thatC: '!s
since we stripped away any relationship between the interior type and the paramC
. This leads to a bogus borrow checker error today!Approach
Coroutine interiors are well-formed by virtue of them being borrow-checked, as long as their callers are invoking their parent functions in a well-formed way, then substitutions should also be well-formed. Therefore, in our example above, we should be able to deduce the assumption that
C: '!s
holds from the well-formedness of the interior typeC::Connecting<'!s>
.This PR introduces the notion of coroutine assumptions, which are the outlives assumptions that we can assume hold due to the well-formedness of a coroutine's interior types. These are computed alongside the coroutine types in the
CoroutineWitnessTypes
struct. When we instantiate the binder when proving an auto trait for a coroutine, we instantiate theCoroutineWitnessTypes
and stash these newly instantiated assumptions in the region storage in theInferCtxt
. Later on in lexical region resolution or MIR borrowck, we use these registered assumptions to discharge any placeholder outlives obligations that we would otherwise not be able to prove.How well does it work?
I've added a ton of tests of different reported situations that users have shared on issues like #110338, and an (anecdotally) large number of those examples end up working straight out of the box! Some limitations are described below.
How badly does it not work?
The behavior today is quite rudimentary, since we currently discharge the placeholder assumptions pretty early in region resolution. This manifests itself as some limitations on the code that we accept.
For example,
tests/ui/async-await/higher-ranked-auto-trait-11.rs
continues to fail. In that test, we must prove that a placeholder is equal to a universal for a param-env candidate to hold when proving an auto trait, e.g.'!1 = 'a
is required to proveT: Trait<'!1>
in a param-env that hasT: Trait<'a>
. Unfortunately, at that point in the MIR body, we only know that the placeholder is equal to some body-local existential NLL var'?2
, which only gets equated to the universal'a
when being stored into the return local later on in MIR borrowck.This could be fixed by integrating these assumptions into the type outlives machinery in a more first-class way, and delaying things to the end of MIR typeck when we know the full relationship between existential and universal NLL vars. Doing this integration today is quite difficult today.
tests/ui/async-await/higher-ranked-auto-trait-11.rs
fails because we don't compute the full transitive outlives relations between placeholders. In that test, we have in our region assumptions that some'!1 = '!2
and'!2 = '!3
, but we must prove'!1 = '!3
.This can be fixed by computing the set of coroutine outlives assumptions in a more transitive way, or as I mentioned above, integrating these assumptions into the type outlives machinery in a more first-class way, since it's already responsible for the transitive outlives assumptions of universals.
Moving forward
I'm still quite happy with this implementation, and I'd like to land it for testing. I may work on overhauling both the way we compute these coroutine assumptions and also how we deal with the assumptions during (lexical/nll) region checking. But for now, I'd like to give users a chance to try out this new
-Zhigher-ranked-assumptions
flag to uncover more shortcomings.Footnotes
Instantiating this binder with infer regions would be incomplete, since we'd be asking for some instantiation of the interior types, not proving something for all instantiations of the interior types. ↩