Description
The following program compiles successfully:
fn impossible() where for<'a> &'a (): 'static {
}
fn main() {}
The where
clause on impossible
is impossible to satisfy, since it is not the case that every choice of 'a
outlives 'static
. However, we never call impossible
, so this program compiles (similar to an unsatisfiable trait bound like where String: Copy
).
If we add a closure to the function:
fn impossible() where for<'a> &'a (): 'static {
let _ = || {};
}
fn main() {}
then it stops compiling (note that this occurs both with and without #![feature(nll)]
):
error: higher-ranked lifetime error
--> src/main.rs:2:13
|
2 | let _ = || {};
| ^^^^^
|
= note: could not prove for<'a> &'a (): 'static
error: could not compile `playground` due to previous error
The issue occurs here:
When we instantiate the predicates of the closure during type-checking of impossible
, we also instantiate the predicates for the parent of the closure - that is, the predicates of impossible
. This results in us trying to prove that for<'a> &'a (): 'static
holds, leading to an error. Normally, we will not try to prove this predicate during type-checking of impossible
itself.