diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 45b05c0c..7e9a9ee5 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -76,6 +76,10 @@ - [Move paths](./borrow_check/moves_and_initialization/move_paths.md) - [MIR type checker](./borrow_check/type_check.md) - [Region inference](./borrow_check/region_inference.md) + - [Constraint propagation](./borrow_check/region_inference/constraint_propagation.md) + - [Placeholders and universes](./borrow_check/region_inference/placeholders_and_universes.md) + - [Closure constraints](./borrow_check/region_inference/closure_constraints.md) + - [Errror reporting](./borrow_check/region_inference/error_reporting.md) - [Two-phase-borrows](./borrow_check/two_phase_borrows.md) - [Constant evaluation](./const-eval.md) - [miri const evaluator](./miri.md) diff --git a/src/borrow_check/region_inference.md b/src/borrow_check/region_inference.md index fc397843..5279d210 100644 --- a/src/borrow_check/region_inference.md +++ b/src/borrow_check/region_inference.md @@ -234,460 +234,3 @@ tests and universal regions, as discussed above. [`check_type_tests`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_type_tests [`check_universal_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_universal_regions -## Closures - -When we are checking the type tests and universal regions, we may come across a -constraint that we can't prove yet if we are in a closure body! However, the -necessary constraints may actually hold (we just don't know it yet). Thus, if -we are inside a closure, we just collect all the constraints we can't prove yet -and return them. Later, when we are borrow check the MIR node that created the -closure, we can also check that these constraints hold. At that time, if we -can't prove they hold, we report an error. - -## Placeholders and universes - -(This section describes ongoing work that hasn't landed yet.) - -From time to time we have to reason about regions that we can't -concretely know. For example, consider this program: - -```rust,ignore -// A function that needs a static reference -fn foo(x: &'static u32) { } - -fn bar(f: for<'a> fn(&'a u32)) { - // ^^^^^^^^^^^^^^^^^^^ a function that can accept **any** reference - let x = 22; - f(&x); -} - -fn main() { - bar(foo); -} -``` - -This program ought not to type-check: `foo` needs a static reference -for its argument, and `bar` wants to be given a function that that -accepts **any** reference (so it can call it with something on its -stack, for example). But *how* do we reject it and *why*? - -### Subtyping and Placeholders - -When we type-check `main`, and in particular the call `bar(foo)`, we -are going to wind up with a subtyping relationship like this one: - -```text -fn(&'static u32) <: for<'a> fn(&'a u32) ----------------- ------------------- -the type of `foo` the type `bar` expects -``` - -We handle this sort of subtyping by taking the variables that are -bound in the supertype and replacing them with -[universally quantified](../appendix/background.html#quantified) -representatives, written like `!1`. We call these regions "placeholder -regions" – they represent, basically, "some unknown region". - -Once we've done that replacement, we have the following relation: - -```text -fn(&'static u32) <: fn(&'!1 u32) -``` - -The key idea here is that this unknown region `'!1` is not related to -any other regions. So if we can prove that the subtyping relationship -is true for `'!1`, then it ought to be true for any region, which is -what we wanted. - -So let's work through what happens next. To check if two functions are -subtypes, we check if their arguments have the desired relationship -(fn arguments are [contravariant](../appendix/background.html#variance), so -we swap the left and right here): - -```text -&'!1 u32 <: &'static u32 -``` - -According to the basic subtyping rules for a reference, this will be -true if `'!1: 'static`. That is – if "some unknown region `!1`" lives -outlives `'static`. Now, this *might* be true – after all, `'!1` -could be `'static` – but we don't *know* that it's true. So this -should yield up an error (eventually). - -### What is a universe - -In the previous section, we introduced the idea of a placeholder -region, and we denoted it `!1`. We call this number `1` the **universe -index**. The idea of a "universe" is that it is a set of names that -are in scope within some type or at some point. Universes are formed -into a tree, where each child extends its parents with some new names. -So the **root universe** conceptually contains global names, such as -the the lifetime `'static` or the type `i32`. In the compiler, we also -put generic type parameters into this root universe (in this sense, -there is not just one root universe, but one per item). So consider -this function `bar`: - -```rust,ignore -struct Foo { } - -fn bar<'a, T>(t: &'a T) { - ... -} -``` - -Here, the root universe would consist of the lifetimes `'static` and -`'a`. In fact, although we're focused on lifetimes here, we can apply -the same concept to types, in which case the types `Foo` and `T` would -be in the root universe (along with other global types, like `i32`). -Basically, the root universe contains all the names that -[appear free](../appendix/background.html#free-vs-bound) in the body of `bar`. - -Now let's extend `bar` a bit by adding a variable `x`: - -```rust,ignore -fn bar<'a, T>(t: &'a T) { - let x: for<'b> fn(&'b u32) = ...; -} -``` - -Here, the name `'b` is not part of the root universe. Instead, when we -"enter" into this `for<'b>` (e.g., by replacing it with a placeholder), we will create -a child universe of the root, let's call it U1: - -```text -U0 (root universe) -│ -└─ U1 (child universe) -``` - -The idea is that this child universe U1 extends the root universe U0 -with a new name, which we are identifying by its universe number: -`!1`. - -Now let's extend `bar` a bit by adding one more variable, `y`: - -```rust,ignore -fn bar<'a, T>(t: &'a T) { - let x: for<'b> fn(&'b u32) = ...; - let y: for<'c> fn(&'b u32) = ...; -} -``` - -When we enter *this* type, we will again create a new universe, which -we'll call `U2`. Its parent will be the root universe, and U1 will be -its sibling: - -```text -U0 (root universe) -│ -├─ U1 (child universe) -│ -└─ U2 (child universe) -``` - -This implies that, while in U2, we can name things from U0 or U2, but -not U1. - -**Giving existential variables a universe.** Now that we have this -notion of universes, we can use it to extend our type-checker and -things to prevent illegal names from leaking out. The idea is that we -give each inference (existential) variable – whether it be a type or -a lifetime – a universe. That variable's value can then only -reference names visible from that universe. So for example is a -lifetime variable is created in U0, then it cannot be assigned a value -of `!1` or `!2`, because those names are not visible from the universe -U0. - -**Representing universes with just a counter.** You might be surprised -to see that the compiler doesn't keep track of a full tree of -universes. Instead, it just keeps a counter – and, to determine if -one universe can see another one, it just checks if the index is -greater. For example, U2 can see U0 because 2 >= 0. But U0 cannot see -U2, because 0 >= 2 is false. - -How can we get away with this? Doesn't this mean that we would allow -U2 to also see U1? The answer is that, yes, we would, **if that -question ever arose**. But because of the structure of our type -checker etc, there is no way for that to happen. In order for -something happening in the universe U1 to "communicate" with something -happening in U2, they would have to have a shared inference variable X -in common. And because everything in U1 is scoped to just U1 and its -children, that inference variable X would have to be in U0. And since -X is in U0, it cannot name anything from U1 (or U2). This is perhaps easiest -to see by using a kind of generic "logic" example: - -```text -exists { - forall { ... /* Y is in U1 ... */ } - forall { ... /* Z is in U2 ... */ } -} -``` - -Here, the only way for the two foralls to interact would be through X, -but neither Y nor Z are in scope when X is declared, so its value -cannot reference either of them. - -### Universes and placeholder region elements - -But where does that error come from? The way it happens is like this. -When we are constructing the region inference context, we can tell -from the type inference context how many placeholder variables exist -(the `InferCtxt` has an internal counter). For each of those, we -create a corresponding universal region variable `!n` and a "region -element" `placeholder(n)`. This corresponds to "some unknown set of other -elements". The value of `!n` is `{placeholder(n)}`. - -At the same time, we also give each existential variable a -**universe** (also taken from the `InferCtxt`). This universe -determines which placeholder elements may appear in its value: For -example, a variable in universe U3 may name `placeholder(1)`, `placeholder(2)`, and -`placeholder(3)`, but not `placeholder(4)`. Note that the universe of an inference -variable controls what region elements **can** appear in its value; it -does not say region elements **will** appear. - -### Placeholders and outlives constraints - -In the region inference engine, outlives constraints have the form: - -```text -V1: V2 @ P -``` - -where `V1` and `V2` are region indices, and hence map to some region -variable (which may be universally or existentially quantified). The -`P` here is a "point" in the control-flow graph; it's not important -for this section. This variable will have a universe, so let's call -those universes `U(V1)` and `U(V2)` respectively. (Actually, the only -one we are going to care about is `U(V1)`.) - -When we encounter this constraint, the ordinary procedure is to start -a DFS from `P`. We keep walking so long as the nodes we are walking -are present in `value(V2)` and we add those nodes to `value(V1)`. If -we reach a return point, we add in any `end(X)` elements. That part -remains unchanged. - -But then *after that* we want to iterate over the placeholder `placeholder(x)` -elements in V2 (each of those must be visible to `U(V2)`, but we -should be able to just assume that is true, we don't have to check -it). We have to ensure that `value(V1)` outlives each of those -placeholder elements. - -Now there are two ways that could happen. First, if `U(V1)` can see -the universe `x` (i.e., `x <= U(V1)`), then we can just add `placeholder(x)` -to `value(V1)` and be done. But if not, then we have to approximate: -we may not know what set of elements `placeholder(x)` represents, but we -should be able to compute some sort of **upper bound** B for it – -some region B that outlives `placeholder(x)`. For now, we'll just use -`'static` for that (since it outlives everything) – in the future, we -can sometimes be smarter here (and in fact we have code for doing this -already in other contexts). Moreover, since `'static` is in the root -universe U0, we know that all variables can see it – so basically if -we find that `value(V2)` contains `placeholder(x)` for some universe `x` -that `V1` can't see, then we force `V1` to `'static`. - -### Extending the "universal regions" check - -After all constraints have been propagated, the NLL region inference -has one final check, where it goes over the values that wound up being -computed for each universal region and checks that they did not get -'too large'. In our case, we will go through each placeholder region -and check that it contains *only* the `placeholder(u)` element it is known to -outlive. (Later, we might be able to know that there are relationships -between two placeholder regions and take those into account, as we do -for universal regions from the fn signature.) - -Put another way, the "universal regions" check can be considered to be -checking constraints like: - -```text -{placeholder(1)}: V1 -``` - -where `{placeholder(1)}` is like a constant set, and V1 is the variable we -made to represent the `!1` region. - -## Back to our example - -OK, so far so good. Now let's walk through what would happen with our -first example: - -```text -fn(&'static u32) <: fn(&'!1 u32) @ P // this point P is not imp't here -``` - -The region inference engine will create a region element domain like this: - -```text -{ CFG; end('static); placeholder(1) } - --- ------------ ------- from the universe `!1` - | 'static is always in scope - all points in the CFG; not especially relevant here -``` - -It will always create two universal variables, one representing -`'static` and one representing `'!1`. Let's call them Vs and V1. They -will have initial values like so: - -```text -Vs = { CFG; end('static) } // it is in U0, so can't name anything else -V1 = { placeholder(1) } -``` - -From the subtyping constraint above, we would have an outlives constraint like - -```text -'!1: 'static @ P -``` - -To process this, we would grow the value of V1 to include all of Vs: - -```text -Vs = { CFG; end('static) } -V1 = { CFG; end('static), placeholder(1) } -``` - -At that point, constraint propagation is complete, because all the -outlives relationships are satisfied. Then we would go to the "check -universal regions" portion of the code, which would test that no -universal region grew too large. - -In this case, `V1` *did* grow too large – it is not known to outlive -`end('static)`, nor any of the CFG – so we would report an error. - -## Another example - -What about this subtyping relationship? - -```text -for<'a> fn(&'a u32, &'a u32) - <: -for<'b, 'c> fn(&'b u32, &'c u32) -``` - -Here we would replace the bound region in the supertype with a placeholder, as before, yielding: - -```text -for<'a> fn(&'a u32, &'a u32) - <: -fn(&'!1 u32, &'!2 u32) -``` - -then we instantiate the variable on the left-hand side with an -existential in universe U2, yielding the following (`?n` is a notation -for an existential variable): - -```text -fn(&'?3 u32, &'?3 u32) - <: -fn(&'!1 u32, &'!2 u32) -``` - -Then we break this down further: - -```text -&'!1 u32 <: &'?3 u32 -&'!2 u32 <: &'?3 u32 -``` - -and even further, yield up our region constraints: - -```text -'!1: '?3 -'!2: '?3 -``` - -Note that, in this case, both `'!1` and `'!2` have to outlive the -variable `'?3`, but the variable `'?3` is not forced to outlive -anything else. Therefore, it simply starts and ends as the empty set -of elements, and hence the type-check succeeds here. - -(This should surprise you a little. It surprised me when I first realized it. -We are saying that if we are a fn that **needs both of its arguments to have -the same region**, we can accept being called with **arguments with two -distinct regions**. That seems intuitively unsound. But in fact, it's fine, as -I tried to explain in [this issue][ohdeargoditsallbroken] on the Rust issue -tracker long ago. The reason is that even if we get called with arguments of -two distinct lifetimes, those two lifetimes have some intersection (the call -itself), and that intersection can be our value of `'a` that we use as the -common lifetime of our arguments. -nmatsakis) - -[ohdeargoditsallbroken]: https://github.com/rust-lang/rust/issues/32330#issuecomment-202536977 - -## Final example - -Let's look at one last example. We'll extend the previous one to have -a return type: - -```text -for<'a> fn(&'a u32, &'a u32) -> &'a u32 - <: -for<'b, 'c> fn(&'b u32, &'c u32) -> &'b u32 -``` - -Despite seeming very similar to the previous example, this case is going to get -an error. That's good: the problem is that we've gone from a fn that promises -to return one of its two arguments, to a fn that is promising to return the -first one. That is unsound. Let's see how it plays out. - -First, we replace the bound region in the supertype with a placeholder: - -```text -for<'a> fn(&'a u32, &'a u32) -> &'a u32 - <: -fn(&'!1 u32, &'!2 u32) -> &'!1 u32 -``` - -Then we instantiate the subtype with existentials (in U2): - -```text -fn(&'?3 u32, &'?3 u32) -> &'?3 u32 - <: -fn(&'!1 u32, &'!2 u32) -> &'!1 u32 -``` - -And now we create the subtyping relationships: - -```text -&'!1 u32 <: &'?3 u32 // arg 1 -&'!2 u32 <: &'?3 u32 // arg 2 -&'?3 u32 <: &'!1 u32 // return type -``` - -And finally the outlives relationships. Here, let V1, V2, and V3 be the -variables we assign to `!1`, `!2`, and `?3` respectively: - -```text -V1: V3 -V2: V3 -V3: V1 -``` - -Those variables will have these initial values: - -```text -V1 in U1 = {placeholder(1)} -V2 in U2 = {placeholder(2)} -V3 in U2 = {} -``` - -Now because of the `V3: V1` constraint, we have to add `placeholder(1)` into `V3` (and -indeed it is visible from `V3`), so we get: - -```text -V3 in U2 = {placeholder(1)} -``` - -then we have this constraint `V2: V3`, so we wind up having to enlarge -`V2` to include `placeholder(1)` (which it can also see): - -```text -V2 in U2 = {placeholder(1), placeholder(2)} -``` - -Now constraint propagation is done, but when we check the outlives -relationships, we find that `V2` includes this new element `placeholder(1)`, -so we report an error. - -## Borrow Checker Errors - -TODO: we should discuss how to generate errors from the results of these analyses. diff --git a/src/borrow_check/region_inference/closure_constraints.md b/src/borrow_check/region_inference/closure_constraints.md new file mode 100644 index 00000000..13230d03 --- /dev/null +++ b/src/borrow_check/region_inference/closure_constraints.md @@ -0,0 +1,10 @@ +# Propagating closure constraints + +When we are checking the type tests and universal regions, we may come +across a constraint that we can't prove yet if we are in a closure +body! However, the necessary constraints may actually hold (we just +don't know it yet). Thus, if we are inside a closure, we just collect +all the constraints we can't prove yet and return them. Later, when we +are borrow check the MIR node that created the closure, we can also +check that these constraints hold. At that time, if we can't prove +they hold, we report an error. diff --git a/src/borrow_check/region_inference/constraint_propagation.md b/src/borrow_check/region_inference/constraint_propagation.md new file mode 100644 index 00000000..2e69629b --- /dev/null +++ b/src/borrow_check/region_inference/constraint_propagation.md @@ -0,0 +1,3 @@ +# Constraint propagation + +The main work of the region inference is **constraint propagation**. diff --git a/src/borrow_check/region_inference/error_reporting.md b/src/borrow_check/region_inference/error_reporting.md new file mode 100644 index 00000000..79b3e077 --- /dev/null +++ b/src/borrow_check/region_inference/error_reporting.md @@ -0,0 +1,3 @@ +# Reporting region errors + +TODO: we should discuss how to generate errors from the results of these analyses. diff --git a/src/borrow_check/region_inference/placeholders_and_universes.md b/src/borrow_check/region_inference/placeholders_and_universes.md new file mode 100644 index 00000000..0d4068e0 --- /dev/null +++ b/src/borrow_check/region_inference/placeholders_and_universes.md @@ -0,0 +1,441 @@ +# Placeholders and universes + +From time to time we have to reason about regions that we can't +concretely know. For example, consider this program: + +```rust,ignore +// A function that needs a static reference +fn foo(x: &'static u32) { } + +fn bar(f: for<'a> fn(&'a u32)) { + // ^^^^^^^^^^^^^^^^^^^ a function that can accept **any** reference + let x = 22; + f(&x); +} + +fn main() { + bar(foo); +} +``` + +This program ought not to type-check: `foo` needs a static reference +for its argument, and `bar` wants to be given a function that that +accepts **any** reference (so it can call it with something on its +stack, for example). But *how* do we reject it and *why*? + +## Subtyping and Placeholders + +When we type-check `main`, and in particular the call `bar(foo)`, we +are going to wind up with a subtyping relationship like this one: + +```text +fn(&'static u32) <: for<'a> fn(&'a u32) +---------------- ------------------- +the type of `foo` the type `bar` expects +``` + +We handle this sort of subtyping by taking the variables that are +bound in the supertype and replacing them with +[universally quantified](../appendix/background.html#quantified) +representatives, written like `!1`. We call these regions "placeholder +regions" – they represent, basically, "some unknown region". + +Once we've done that replacement, we have the following relation: + +```text +fn(&'static u32) <: fn(&'!1 u32) +``` + +The key idea here is that this unknown region `'!1` is not related to +any other regions. So if we can prove that the subtyping relationship +is true for `'!1`, then it ought to be true for any region, which is +what we wanted. + +So let's work through what happens next. To check if two functions are +subtypes, we check if their arguments have the desired relationship +(fn arguments are [contravariant](../appendix/background.html#variance), so +we swap the left and right here): + +```text +&'!1 u32 <: &'static u32 +``` + +According to the basic subtyping rules for a reference, this will be +true if `'!1: 'static`. That is – if "some unknown region `!1`" lives +outlives `'static`. Now, this *might* be true – after all, `'!1` +could be `'static` – but we don't *know* that it's true. So this +should yield up an error (eventually). + +## What is a universe + +In the previous section, we introduced the idea of a placeholder +region, and we denoted it `!1`. We call this number `1` the **universe +index**. The idea of a "universe" is that it is a set of names that +are in scope within some type or at some point. Universes are formed +into a tree, where each child extends its parents with some new names. +So the **root universe** conceptually contains global names, such as +the the lifetime `'static` or the type `i32`. In the compiler, we also +put generic type parameters into this root universe (in this sense, +there is not just one root universe, but one per item). So consider +this function `bar`: + +```rust,ignore +struct Foo { } + +fn bar<'a, T>(t: &'a T) { + ... +} +``` + +Here, the root universe would consist of the lifetimes `'static` and +`'a`. In fact, although we're focused on lifetimes here, we can apply +the same concept to types, in which case the types `Foo` and `T` would +be in the root universe (along with other global types, like `i32`). +Basically, the root universe contains all the names that +[appear free](../appendix/background.html#free-vs-bound) in the body of `bar`. + +Now let's extend `bar` a bit by adding a variable `x`: + +```rust,ignore +fn bar<'a, T>(t: &'a T) { + let x: for<'b> fn(&'b u32) = ...; +} +``` + +Here, the name `'b` is not part of the root universe. Instead, when we +"enter" into this `for<'b>` (e.g., by replacing it with a placeholder), we will create +a child universe of the root, let's call it U1: + +```text +U0 (root universe) +│ +└─ U1 (child universe) +``` + +The idea is that this child universe U1 extends the root universe U0 +with a new name, which we are identifying by its universe number: +`!1`. + +Now let's extend `bar` a bit by adding one more variable, `y`: + +```rust,ignore +fn bar<'a, T>(t: &'a T) { + let x: for<'b> fn(&'b u32) = ...; + let y: for<'c> fn(&'b u32) = ...; +} +``` + +When we enter *this* type, we will again create a new universe, which +we'll call `U2`. Its parent will be the root universe, and U1 will be +its sibling: + +```text +U0 (root universe) +│ +├─ U1 (child universe) +│ +└─ U2 (child universe) +``` + +This implies that, while in U2, we can name things from U0 or U2, but +not U1. + +**Giving existential variables a universe.** Now that we have this +notion of universes, we can use it to extend our type-checker and +things to prevent illegal names from leaking out. The idea is that we +give each inference (existential) variable – whether it be a type or +a lifetime – a universe. That variable's value can then only +reference names visible from that universe. So for example is a +lifetime variable is created in U0, then it cannot be assigned a value +of `!1` or `!2`, because those names are not visible from the universe +U0. + +**Representing universes with just a counter.** You might be surprised +to see that the compiler doesn't keep track of a full tree of +universes. Instead, it just keeps a counter – and, to determine if +one universe can see another one, it just checks if the index is +greater. For example, U2 can see U0 because 2 >= 0. But U0 cannot see +U2, because 0 >= 2 is false. + +How can we get away with this? Doesn't this mean that we would allow +U2 to also see U1? The answer is that, yes, we would, **if that +question ever arose**. But because of the structure of our type +checker etc, there is no way for that to happen. In order for +something happening in the universe U1 to "communicate" with something +happening in U2, they would have to have a shared inference variable X +in common. And because everything in U1 is scoped to just U1 and its +children, that inference variable X would have to be in U0. And since +X is in U0, it cannot name anything from U1 (or U2). This is perhaps easiest +to see by using a kind of generic "logic" example: + +```text +exists { + forall { ... /* Y is in U1 ... */ } + forall { ... /* Z is in U2 ... */ } +} +``` + +Here, the only way for the two foralls to interact would be through X, +but neither Y nor Z are in scope when X is declared, so its value +cannot reference either of them. + +## Universes and placeholder region elements + +But where does that error come from? The way it happens is like this. +When we are constructing the region inference context, we can tell +from the type inference context how many placeholder variables exist +(the `InferCtxt` has an internal counter). For each of those, we +create a corresponding universal region variable `!n` and a "region +element" `placeholder(n)`. This corresponds to "some unknown set of other +elements". The value of `!n` is `{placeholder(n)}`. + +At the same time, we also give each existential variable a +**universe** (also taken from the `InferCtxt`). This universe +determines which placeholder elements may appear in its value: For +example, a variable in universe U3 may name `placeholder(1)`, `placeholder(2)`, and +`placeholder(3)`, but not `placeholder(4)`. Note that the universe of an inference +variable controls what region elements **can** appear in its value; it +does not say region elements **will** appear. + +## Placeholders and outlives constraints + +In the region inference engine, outlives constraints have the form: + +```text +V1: V2 @ P +``` + +where `V1` and `V2` are region indices, and hence map to some region +variable (which may be universally or existentially quantified). The +`P` here is a "point" in the control-flow graph; it's not important +for this section. This variable will have a universe, so let's call +those universes `U(V1)` and `U(V2)` respectively. (Actually, the only +one we are going to care about is `U(V1)`.) + +When we encounter this constraint, the ordinary procedure is to start +a DFS from `P`. We keep walking so long as the nodes we are walking +are present in `value(V2)` and we add those nodes to `value(V1)`. If +we reach a return point, we add in any `end(X)` elements. That part +remains unchanged. + +But then *after that* we want to iterate over the placeholder `placeholder(x)` +elements in V2 (each of those must be visible to `U(V2)`, but we +should be able to just assume that is true, we don't have to check +it). We have to ensure that `value(V1)` outlives each of those +placeholder elements. + +Now there are two ways that could happen. First, if `U(V1)` can see +the universe `x` (i.e., `x <= U(V1)`), then we can just add `placeholder(x)` +to `value(V1)` and be done. But if not, then we have to approximate: +we may not know what set of elements `placeholder(x)` represents, but we +should be able to compute some sort of **upper bound** B for it – +some region B that outlives `placeholder(x)`. For now, we'll just use +`'static` for that (since it outlives everything) – in the future, we +can sometimes be smarter here (and in fact we have code for doing this +already in other contexts). Moreover, since `'static` is in the root +universe U0, we know that all variables can see it – so basically if +we find that `value(V2)` contains `placeholder(x)` for some universe `x` +that `V1` can't see, then we force `V1` to `'static`. + +## Extending the "universal regions" check + +After all constraints have been propagated, the NLL region inference +has one final check, where it goes over the values that wound up being +computed for each universal region and checks that they did not get +'too large'. In our case, we will go through each placeholder region +and check that it contains *only* the `placeholder(u)` element it is known to +outlive. (Later, we might be able to know that there are relationships +between two placeholder regions and take those into account, as we do +for universal regions from the fn signature.) + +Put another way, the "universal regions" check can be considered to be +checking constraints like: + +```text +{placeholder(1)}: V1 +``` + +where `{placeholder(1)}` is like a constant set, and V1 is the variable we +made to represent the `!1` region. + +## Back to our example + +OK, so far so good. Now let's walk through what would happen with our +first example: + +```text +fn(&'static u32) <: fn(&'!1 u32) @ P // this point P is not imp't here +``` + +The region inference engine will create a region element domain like this: + +```text +{ CFG; end('static); placeholder(1) } + --- ------------ ------- from the universe `!1` + | 'static is always in scope + all points in the CFG; not especially relevant here +``` + +It will always create two universal variables, one representing +`'static` and one representing `'!1`. Let's call them Vs and V1. They +will have initial values like so: + +```text +Vs = { CFG; end('static) } // it is in U0, so can't name anything else +V1 = { placeholder(1) } +``` + +From the subtyping constraint above, we would have an outlives constraint like + +```text +'!1: 'static @ P +``` + +To process this, we would grow the value of V1 to include all of Vs: + +```text +Vs = { CFG; end('static) } +V1 = { CFG; end('static), placeholder(1) } +``` + +At that point, constraint propagation is complete, because all the +outlives relationships are satisfied. Then we would go to the "check +universal regions" portion of the code, which would test that no +universal region grew too large. + +In this case, `V1` *did* grow too large – it is not known to outlive +`end('static)`, nor any of the CFG – so we would report an error. + +## Another example + +What about this subtyping relationship? + +```text +for<'a> fn(&'a u32, &'a u32) + <: +for<'b, 'c> fn(&'b u32, &'c u32) +``` + +Here we would replace the bound region in the supertype with a placeholder, as before, yielding: + +```text +for<'a> fn(&'a u32, &'a u32) + <: +fn(&'!1 u32, &'!2 u32) +``` + +then we instantiate the variable on the left-hand side with an +existential in universe U2, yielding the following (`?n` is a notation +for an existential variable): + +```text +fn(&'?3 u32, &'?3 u32) + <: +fn(&'!1 u32, &'!2 u32) +``` + +Then we break this down further: + +```text +&'!1 u32 <: &'?3 u32 +&'!2 u32 <: &'?3 u32 +``` + +and even further, yield up our region constraints: + +```text +'!1: '?3 +'!2: '?3 +``` + +Note that, in this case, both `'!1` and `'!2` have to outlive the +variable `'?3`, but the variable `'?3` is not forced to outlive +anything else. Therefore, it simply starts and ends as the empty set +of elements, and hence the type-check succeeds here. + +(This should surprise you a little. It surprised me when I first realized it. +We are saying that if we are a fn that **needs both of its arguments to have +the same region**, we can accept being called with **arguments with two +distinct regions**. That seems intuitively unsound. But in fact, it's fine, as +I tried to explain in [this issue][ohdeargoditsallbroken] on the Rust issue +tracker long ago. The reason is that even if we get called with arguments of +two distinct lifetimes, those two lifetimes have some intersection (the call +itself), and that intersection can be our value of `'a` that we use as the +common lifetime of our arguments. -nmatsakis) + +[ohdeargoditsallbroken]: https://github.com/rust-lang/rust/issues/32330#issuecomment-202536977 + +## Final example + +Let's look at one last example. We'll extend the previous one to have +a return type: + +```text +for<'a> fn(&'a u32, &'a u32) -> &'a u32 + <: +for<'b, 'c> fn(&'b u32, &'c u32) -> &'b u32 +``` + +Despite seeming very similar to the previous example, this case is going to get +an error. That's good: the problem is that we've gone from a fn that promises +to return one of its two arguments, to a fn that is promising to return the +first one. That is unsound. Let's see how it plays out. + +First, we replace the bound region in the supertype with a placeholder: + +```text +for<'a> fn(&'a u32, &'a u32) -> &'a u32 + <: +fn(&'!1 u32, &'!2 u32) -> &'!1 u32 +``` + +Then we instantiate the subtype with existentials (in U2): + +```text +fn(&'?3 u32, &'?3 u32) -> &'?3 u32 + <: +fn(&'!1 u32, &'!2 u32) -> &'!1 u32 +``` + +And now we create the subtyping relationships: + +```text +&'!1 u32 <: &'?3 u32 // arg 1 +&'!2 u32 <: &'?3 u32 // arg 2 +&'?3 u32 <: &'!1 u32 // return type +``` + +And finally the outlives relationships. Here, let V1, V2, and V3 be the +variables we assign to `!1`, `!2`, and `?3` respectively: + +```text +V1: V3 +V2: V3 +V3: V1 +``` + +Those variables will have these initial values: + +```text +V1 in U1 = {placeholder(1)} +V2 in U2 = {placeholder(2)} +V3 in U2 = {} +``` + +Now because of the `V3: V1` constraint, we have to add `placeholder(1)` into `V3` (and +indeed it is visible from `V3`), so we get: + +```text +V3 in U2 = {placeholder(1)} +``` + +then we have this constraint `V2: V3`, so we wind up having to enlarge +`V2` to include `placeholder(1)` (which it can also see): + +```text +V2 in U2 = {placeholder(1), placeholder(2)} +``` + +Now constraint propagation is done, but when we check the outlives +relationships, we find that `V2` includes this new element `placeholder(1)`, +so we report an error.