Semantics of lifetime parameters

Consider the following example from the Book:

fn main() {
    let string1 = String::from("abcd");
    let string2 = "xyz";

    let result = longest(string1.as_str(), string2);
    println!("The longest string is {}", result);
}

fn longest<'a>(x: &'a str, y: &'a str) -> &'a str {
    if x.len() > y.len() {
        x
    } else {
        y
    }
}

It is said that (emphasis mine)

The function signature now tells Rust that for some lifetime 'a, the function takes two parameters, both of which are string slices that live at least as long as lifetime 'a. The function signature also tells Rust that the string slice returned from the function will live at least as long as lifetime 'a. In practice, it means that the lifetime of the reference returned by the longest function is the same as the smaller of the lifetimes of the references passed in. These constraints are what we want Rust to enforce.

Shouldn't the bolded sentence be The function signature also tells Rust that the string slice returned from the function will live at most as long as lifetime 'a.? That way, we are assured that as long as both x and y are alive, then the return value would also be valid, because the latter references the former.

To paraphrase, if x, y and the return value all live at least as long as lifetime 'a, then the compiler can simply let 'a be an empty scope (which any item can outlive) to satisfy the restriction, rendering the annotation useless. This doesn't make sense, right?

Expressed in formal language, the annotation translates to:

for all 'a, 'a≤'x and 'a≤'y implies 'a≤'r

With 'x, 'y and 'r the lifetimes of x, y, and the return value respectively.

This links the lifetime of the return value to the lifetimes of the parameters because for that relation to hold for all 'a, then you must necessarily have 'x≤'r or 'y≤'r.

The compiler will use that annotation at two times:

1. When compiling the annotated function, the compiler doesn't know the actual lifetimes of x and y and it doesn't know 'a (since 'a will be chosen at the call site, like all generic parameters). But it knows that when the function gets called, the caller will use some lifetime 'a that matches the input constraints 'a≤'x and 'a≤'y and it checks that the code of the function respects the output constraint 'a≤'r.

2. When calling the annotated function, the compiler will add to its constraint solver an unknown scope 'a in which the return value can be accessed, along with the constraints that 'a≤'x and 'a≤'y plus whatever extra constraints are required due to the surrounding code and in particular where x and y come from and how the return value is used. If the compiler is able to find some scope 'a that matches all the constraints, then the code compiles using that scope. Otherwise compilation fails with a "does not live long enough" error.