Why does the closure that satisfies the upper limiting lifetime not satisfy the constrained lifetime?

help
1

This is a subsequent question of Does the lifetime parameter denote any lifetime in HRTB if it is constrainted?

#![feature(fn_traits)]
#![feature(unboxed_closures)]
use std::marker::PhantomData;

struct Scope<'a, 'b>(PhantomData<*mut &'a ()>, PhantomData<*mut &'b ()>);

impl<'a, 'env> Scope<'a, 'env> {
    fn spawn<F>(&'a self, mut f: F) where F: FnMut() + 'a {
        f();
    }
}

fn scope_spawn<'b, F>(_f: F) where F: for<'a> FnOnce(&'a Scope<'a, 'b>) {}

struct Closure<F>(F);

impl<'a, 'b, F> FnOnce<(&'a Scope<'a, 'b>,)> for Closure<F>
where
    F: FnMut() + 'b,  // #1
    //'b: 'a,
{
    type Output = ();
    extern "rust-call" fn call_once(self, (scope,): (&'a Scope<'a, 'b>,)) {
        scope.spawn(self.0);
    }
}

fn main() {
    let mut i = 0;
    scope_spawn(Closure(|| { i = 1; }));
}

Notice the trait bound in the Fn trait's implementation for type Closure<F>, this example is Ok. The type &'a Scope<'a, 'b> formed in the parameter implies 'b:'a. Specifically, it implies something like for<'a where 'b:'a>, which means that: The implicit bound adds an upper limit to the 'a that needs to be handled (but there's still no lower limit). However, if changing #1 to F: FnMut() + 'a, the compiler will report an error:

closure may outlive the current function, but it borrows `i`, which is owned by the current function

This is confused. Why F:FnMut() + 'b is ok, and 'a is any lifetime less than or equal to 'b(implcited by the formed type), however, F:FnMut() +'a causes the above error?

Update:

I suspect that F: FnMut() +'a has the same reason as why explicit trait bound 'b:'a can cause the error too. That is, in the trait's implementation for which the HRTB checks, any explicit use of the lifetime corresponding to the lifetime introduced by for in HRTB will be considered as if it were rewritten as for<'a>, in this example, F:FnMut() +'a is F: for<'a> FnMut() +'a, which requires F outlives 'static.

2

I could be wrong, but my current interpretation.

impl<'a> Trait<'a> for Struct

Here one type implements many traits; Known in category generalisation. When you add a where clause you switch to a one-to-one. For a lot of code, variance rules are all that is needed but you eventually hit more complex cases when pushing the bounds.

3

That's my take as well.

4

I decided to walk through it for practice. The OP highlights the syntactical aspect of the check pretty well IMO. AFAIU the check goes something like:

// Replace bound regions in the obligation with placeholders
Closure<{line 30 closure}>: FnOnce(&'0 Scope<'0, 'b>)

// Create trait ref from impl, using inference vars for bound regions
Closure<{line 30 closure}>: FnOnce(&'$x Scope<'$x, '$y>)
obligation: {line 30 closure}: FnMut() + '$x

// Relate the two
'$x = '0, '$y = 'b
(obligation: {line 30 closure}: FnMut() + '0)

// Taint set: things related to placeholders
'0 => { '0, '$x }

// Only the placeholder and bound regions from the impl, so that's ok (no leaks)

// Obligations: reverse map placeholders to higher-ranked obligations
obligation: {line 30 closure}: for<'a> FnMut() + 'a

// Can only succeed if `{line 30 closure}: 'static`

But if you have F: FnMut() + 'b instead, there's no placeholders in the obligation.

And some syntactical examples are:

impl<'a, 'b, F> FnOnce<(&'a Scope<'a, 'b>,)> for Closure<F>
where
    F: FnMut() + 'a + 'b,

Or even

    F: FnMut() + 'b, 'b: 'a

Which ends up forcing 'b to be 'static due to

for<'a> 'b: 'a

Which does parallel how late-bound and early-bound parameters work I suppose.

From a higher-level view, I believe you can take

fn scope_spawn<'b, F>(_f: F) where F: for<'a> FnOnce(&'a Scope<'a, 'b>) {}

As a directive to transitively prove every bound B in F's implementation under for<'a>.[1] Taking care to keep our generic names aligned, we have:

F = Closure<G>
given 'b we need, for<'a>:

impl<'a, 'b, G> FnOnce<(&'a Scope<'a, 'b>,)> for Closure<G>
where
    G: FnMut() + 'a,

Which includes proving

for<'a> G: FnMut() + 'a

It was pretty straightforward in this case, but probably gets trickier when lifetimes get related, making the check less mechanically syntactical.

  1. Under the current trait solver, anyway. ↩︎

5

So, in short, when checking the trait's implementation for the HRTB, any lifetime in the implementation that relates to the lifetime introduced by for in HRTB will be viewed as if it were introduced by for<'any> to check the obligation.