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.