Yeah, and as a matter of fact, I'm personally an advocate of comparing lifetimes as the regions they represent ("set ordering"), rather than as "subtypes", especially given that since there are no "var"/instances of the "lifetime type" (i.e., since a lifetime is a not a type), talking of subtyping for lifetimes makes no sense. It is a kind with arbitrary polarity based on which the variance of types such as 'x -> &'x [mut] T is defined.
In order to avoid ambiguity, though, I usually go for the ⊇ symbol:
- it goes in the same order as Rust's
:.
- it does convey the notion of
≥, but with emphasis on set semantics.
(I also prefer writing down T : 'r as T : UsableFor<'r>, and 'static as 'forever.)
Finally, once we consider set semantics, we can talk of 'intersections and 'unions.
-
Better than 'max or 'min since those suggest there being a total order between lifetimes/regions, which is not true: there exist uncomparable lifetimes, such as those of the respective borrows of a and b in:
let [a, b] = ::core::array::from_fn(|_| String::from("…"));
let it = Demo { at_a: &a, at_b: &b };
if ::rand::random() {
let Demo { at_b, .. } = it;
drop(a);
dbg!(at_b);
drop(b);
} else {
let Demo { at_a, .. } = it;
drop(b);
dbg!(at_a);
drop(a);
}
With this, "the maximal region of usability" of a type T = …<'a, 'b, …, 'x> is indeed the 'intersection<'a, 'b, …, 'x>.
//! Given some `'r`, and `T = …<'a, 'b, …, 'x>`
T : UsableFor<'r>,
⇔
…<'a, 'b, …, 'x> : UsableFor<'r>,
⇔ // WF rule.
{ 'a ⊇ 'r, 'b ⊇ 'r, …, 'x ⊇ 'r }
⇔
('a ∩ 'b ∩ … ∩ 'x) ⊇ 'r
⇔
'intersection<'a, 'b, …, 'x> ⊇ 'r
⇔
'intersection<T> ⊇ 'r
// let's write it down as `'T`:
'T ⊇ 'r
Back to the OP
So, back to your question, you want to express, for two types T, and U, the following equivalent properties:
for<'r where T : 'r>
U : UsableFor<'r>
,
U : UsableFor<'T>,
'U ⊇ 'T,
'inter<'u1, 'u2, …> ⊇ 'inter<'t1, 't2, …>,
Since Rust does most definitely not have notation for the 'inter<…> operation, or the 'T "extraction", we have to rule out the last three.
So you are right that a HRTB/for<> quantification is necessary to express this property.
Now, the final struggle is that we don't (yet) have where-in-for<> either, "to keep Rust simple" (it just means that whenever these properties are needed, some more obscure hoops and convolutions are needed, making the whole thing significantly less clear than if we did have where-in-for<>).
- (Rust is a language which is self-conscious/has a complex about, heh, complexity, and thus its designers have been going down a path of simplicity-through-obscurity and "white lies" which, in turn, is more detrimental to the actual accessibility of the language than if it did acknowledged, recognized, and embraced, the actual theoretical patterns on which Rust hinges, and just made even more effort in teaching and documenting about them.)
So the way to hack our way around where-in-for<> is through implicit bounds: types such as &'r X, by the act of merely naming them, introduce an implicit where X : UsableFor<'r> i.e., where 'X ⊇ 'r bound —a well-formedness (WF) bound—, in order for the containing predicate to ever make sense.
macro_rules! ImplicitBound {(
where $T:ty : $region:lifetime $(,)?
) => (
&$region $T
)}
- e.g.,
ImplicitBound! { where T : 'r } becomes &'r T.
Knowing that, we could define:
trait UsableFor<'region, _UnusedWFBounds = ()> : 'region {}
impl<'r, T : 'r, _UnusedWFBounds>
UsableFor<'r, _UnusedWFBounds>
for
T
{}
that way we could express:
for<'r /* where 'T : 'r */>
// ^
// |
// +-<-----------<------------<-+
// |
U : UsableFor<'r, ImplicitBound! { where T : 'r }>
,
Does it work?
No. 
. Rust gets confused about this for now, and still treats it as for<'r> U : UsableFor<'r>, i.e., 'U ⊇ 'union<for<'r> 'r> i.e. 'U ⊇ 'forever.
But maybe one day it will? 