A Whole Wide Universe @WaffleLapkin @BoxyUwU

fn identity(x: &u32) -> &u32 { x }

fn consume_fn<R, F: for<'a> FnOnce(&'a u32) -> R>(_: F) {}

fn main() {
    let fnptr: for<'b> fn(&'b u32) -> &'b u32 = identity;
    consume_fn(fnptr);
}
Solution
error[E0308]: mismatched types
 --> examples/borrowck_2.rs:7:5
  |
7 |     consume_fn(fnptr);
  |     ^^^^^^^^^^^^^^^^^ one type is more general than the other
  |
  = note: expected reference `&'a _`
             found reference `&_`
note: the lifetime requirement is introduced here
 --> examples/borrowck_2.rs:3:48
  |
3 | fn consume_fn<R, F: for<'a> FnOnce(&'a u32) -> R>(_: F) {}
  |                                                ^

For more information about this error, try `rustc --explain E0308`.
error: could not compile `code` (example "borrowck_2") due to 1 previous error

In order for this code to compile the type parameter R on consume_fn must be able to be given a type argument of &'b u32 by the caller in main.

The type &'b u32 mentions a higher-ranked lifetime 'b from the for-all for<'b>. Only types inside of the for-all can name lifetimes introduced by the for-all.

If the compiler allowed this we would wind up with a function call that looks something like: consume_fn::<&'b u32, for<'b> fn(&'b u32) -> &'b u32>(...).

This would be quite incoherent as the lifetime 'b can be chosen to be a different lifetime by every caller of fnptr. There's no way to know what &'b u32 actually means outside of the for<'b>.

This concept is very closely related to existential and universal quantifiers in formal logic. exists<T> forall<U> T == U cannot be proven, however forall<U> exists<T> T == U can.

In Rust terms this roughly corresponds to inferences variables being existential quantifiers, and for<...> in types as being universal quantifiers. Though, it's worth noting that in some cases for<...> in types is actually treated as an existential quantifier.