As described in the NLL RFC, this subtyping relation holds if '1: '0. In NLL, we called this an outlives relation. But in polonius, because '0 and '1 are origins representing sets of loans, we call it a subset relation. In other words, '1: '0 could be written '1 ⊆ '0, and it means that whatever loans '1 may be referencing, '0 may reference too.
With a radical example 'static: 'x, according to the meaning of the blog, 'static is a subset of 'x, this is confusion. We say 'static outlives 'x, which means, 'static is valid everywhere where 'x is valid. In other words, 'static has a larger region than that of 'x, furthermore, saying set A is a subset of set B has a strict definition on mathematical, see Subset - Wikipedia
If A and B are sets and every element of A is also an element of B, then:
A is a subset of B, denoted by A ⊆ B
when we say 'static outlives 'x, which means, 'static has a larget region than 'x, it obviously to say 'x should be a subset of 'static, because every element of 'x is also an element of 'static but not the vice versa.
So, I don't understand why the blog says a lifetime with a larger lifetime is a subset of a lifetime with a smaller lifetime.
"valid everywhere" indicates you're still thinking of lifetimes in NLL terms, that is, a set of points, and not a set of loans (the things that get borrowed, like *x.0 in &*x.0). If 'a is associated with loans L0 and L1, uses of the places of those loans could conflict with 'a being alive. But if 'b is associated with loans L0, uses of the place of L1 can't conflict with 'b being alive.
Maybe think of it as "invalid nowhere" and instead of "valid a superset of places", "invalid a subset of places"? (Haven't given this much thought myself.)
There are less loans in 'b; 'b is a subset of the loans of 'a; 'b is a subtype of 'a; in Rust oulives notation, 'b: 'a.
Note that this "larger region => subtype" notion exists under the NLL formulation already; that's why you can coerce a 'static lifetime (the bottom-most type) to a non-'static lifetime (a supertype) in covariant position. You can let a: &'a str = ""; // : &'static str like you can do something like let a: Animal = cat in language with class subtyping. 'static: 'a always holds.
In the polonius forumulation, 'static is the empty set. I'd have to go review to think about how reborrows of &'static mut resolve, though it's probably similar or the same as to how other named lifetimes resolve in a function body.
For all of this, keep in mind that the borrow checker is a constraint solver and not a lifetime assigner per se. It just has to prove that there exists a sound solution given the function body and any additional constraints from the annotations, Rust's semantics, etc.
No, that's wrong. You've got it backwards. As it should be obvious from the '1: '0 syntax, the snippet is talking about lifetime bounds, which are validity constraints on types; they refer to sets of types and not to the lifetime regions themselves.
The T: 'static constraint designates types that are potentially valid to keep around for the 'static lifetime. The T: 'x constraint designates types that are potentially valid for 'x. The former, 'static, is a stricter requirement, therefore the set of types satisfying it is smaller. So types satisfying : 'static are a subset of types satisfying : 'x.
For example, an owning type such as String is 'static and also 'x for any lifetime 'x, whereas a reference type &'x T is only 'x, not 'static (unless 'x == 'static).
Protip: if you are not even sure about the different meanings of lifetime annotations vs. bounds, then it's futile (and slightly arrogant) to assume that you've got it right and people who designed the very language got it wrong.
Here "set" is not "set of statements" or something like this that corresponds to the code structure. It's "set of types" or "set of values", depending on the specific case.