Just a quick re-contextualization. I wouldn't say > "It basically says that the returned value (Term) must not outlive the input values (env and args)." It do

Just a quick re-contextualization. I wouldn't say > "It basically says that the returned value (Term) must not outlive the input values (env and args)." It doesn't say that it must not, it says that it doesn't. Because lifetime information can only be inferred about callees and not callers, the lifetime annotation tells the compiler what it needs to know about the caller's environment. It tells the compiler "the lifetimes of these two things are tied together in my caller". The compiler can then use that information when the borrow checker is doing its magic. I've got an article written in my head about how to think about lifetimes in terms of visibility up and down the call stack.