Does the lifetime parameter denote any lifetime in HRTB if it is constrainted?

help
1

Consider this example:

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>(mut f:F)
where F:  for<'a> FnOnce(&'a Scope<'a,'b>){
}
fn main(){
    let mut i = 0;
    scope_spawn(|s|{
        s.spawn(||{
            i = 1;
        });
    });
}

This example is Ok. However, if change the above code to the following:

use std::marker::PhantomData;

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

impl<'a,'env> Scope<'a>{
	fn spawn<F>(&'a self,mut f:F) where F:FnMut()+'a{
		f();
	}
}
fn scope_spawn<'b,F>(mut f:F)
where F:  for<'a> FnOnce(&'a Scope<'a>){
}
fn main(){
    let mut i = 0;
    scope_spawn(|s|{
        s.spawn(||{
            i = 1;  // #1
        });
    });
}

Simply remove the second lifetime for Scope, the compiler will report an error at #1

argument requires that i is borrowed for 'static

What's the reason here? I suspect, in the second example, where F: for<'a> FnOnce(&'a Scope<'a>), the lifetime 'a denotes any lifetime, the trait bound F:FnMut()+'a in Scope::spawn can only be satisfied if F:FnMut() + 'static, so, i is required to borrow for 'static.

In the first example, I think, since the reference type&'a Scope<'a,'b> in where F: for<'a> FnOnce(&'a Scope<'a,'b>) implicit 'b:'a and 'b is a specific lifetime when instantiate the function scope_spawn, hence it constraints that 'a cannot be any lifetime. I don't know whether this is a correct understanding.

If my understanding is right, It seems that where F: for<'a> FnOnce(&'a Scope<'a,'b>) is not a HRTB anymore because 'a does not denote any lifetime?

2

Close. 'a can be any lifetime, one such lifetime is 'static, F doesn't meet a 'static bound (it can't borrow i for 'static), so it can't meet the higher-ranked bound.

No, 'a doesn't become a single lifetime. Now it's "any lifetime less than or equal to 'b". The implicit bound adds an upper limit to the 'a that need to be handled (but there's still no lower limit).

And the caller gets to pick 'b, so they can just pick something that F can satisfy. If F: 'b, then for<'a where 'b: 'a> F: 'a.

3

So, the type formed in the HRTB does implicit the 'b:'a, right?

Consider this example:

trait MyTrait<'a>{}

impl<'a,'b:'a> MyTrait<'a> for &'a &'b i32{}

fn test<'b>(v:&'b i32) where for<'a> &'a &'b i32 : MyTrait<'a>{

}
fn main(){
	let i = 0;
	test(&i);
}

The compiler says argument requires that i is borrowed for 'static. resemble the first example, the type &'a &'b i32 should implicit that 'b:'a, that is for<'a where 'b:'a>, however, this example is not compiled like the first example above. IMO, the first example implies that we have higher-ranked lifetime 'a such that it's any lifetime that is outlived by 'b. I expected the same behavior for this example, however, according to the reported error, the actual meaning implicated is: we have any lifetime 'a such that 'b must outlive that 'a, which in turn requires that 'b:'static.

I don't know why forms the difference here, merely the reference type is on RHS of the HRTB in the first example while the reference type is on LHS in this example. If remove the explicit trait bound 'b:'a in the implementation for MyTrait<'a>, the example is OK, however, the first example is still OK even though adding the explicit one 'b:"a in Scope.

In other words, in the first example, the implicit or explicit lifetime trait bound gives the upper limited to the higer-ranked lifetime, in contrast, the explicit lifetime in the implementation of &'a &'b i32 for MyTrait<'a> instead requires that 'b outlives any lifetime 'a(including 'staitc). I don't understand what results the difference here.

4

This example is a different phenomenon. From what I understand, putting an explicit bound on the parameter of the implementation means that it is checked during higher-ranked trait solving, and it looks like a "leak" and the higher-ranked trait bound fails.

Perhaps more intuitively: The explicit 'b: 'a makes the trait solver try to prove for<'a> 'b: 'a, which can only be proven if 'b is 'static.

In contrast implicit bounds in the implementation don't result in failures, as demonstrated by the success when you replace 'b: 'a with 'b in the implementations.

Using explicit bounds in the implementation in combination with, like the error says, current limitations of the compiler.

Try adding 'b: 'a to the implementation of FnOnce in this playground based on the first example.

5

So, the reason of the explicit trait bound in the declaration of Scope won't impose for<'a> 'b:'a is it's self not the implementation of the trait with which we use the HRTB?

6

Sorry, I don't understand what you're asking.

7

I meant, why the explicit trait bound in the following example does not required 'b:'static

struct Scope<'a,'b>(PhantomData<* mut &'a ()>,PhantomData<* mut &'b ()>); 
// #1
impl<'a,'b:'a> Scope<'a,'b>{
	fn spawn<F>(&'a self,mut f:F) where F:FnMut()+'a{
		f();
	}
}
fn scope_spawn<'b,F>(mut f:F)
where F:  for<'a> FnOnce(&'a Scope<'a,'b>){  // #2
}
fn main(){
    let mut i = 0;
    scope_spawn(|s|{
        s.spawn(||{
            i = 1;
        });
    });
}

There is a implicit trait bound in #2 that 'b:'a for any lifetime 'a, which is similar to the example in above comment. At #1, I explicitly gives the trait bound 'b:'a, why the compiler does not required 'b outlives 'staitc this time?

8

That implementation isn't something that shows up in a HRTB. It's not a trait implementation at all. And the HRTB that does exist in the code is a bound on the closure, not on Scope. So why would the implementation header of a non-trait result in the same compiler limitation?

Adding limitations to the implementation of the HRTB in question is what my (nightly) playground is about. The implementation of FnOnce -- the trait in the HRTB -- corresponds to the implementation of MyTrait. The non-trait implementation on Scope isn't related.

9

Ok. Let me try to understand the difference here. Given an HRTB like Type: for<'a> Trait<'a>, if, in the implementation of Trait<'a> for Type, there is an explicit trait bound to the lifetime that will correspond to 'a here, for example, impl<'a,'b:'a> Trait<'a> for &'b (), then 'b:'a will be like something for<'a> 'b:'a, this results that 'b:'static.

If there is a type, regardless of appears in LHS or RHS of a HRTB, something like &'a S<'b>:Trait<'a> or T: Trait2<&'a &'b ()> where 'a is introduced by for<'a>, they both introduce a implicit bound that 'b:'a, and that means 'a is any lifetime upper bounded by 'b, instead of 'b must outlive any lifetime 'a, right?

10

I agree with everything you said :+1:.

This phrasing really pinpoints a source of confusion I feel. I'll have to think about it there's a clearer way to present that from the beginning.

11

Maybe, a simple way to conclude these examples is: To determine whether a type satisfies the HRTB, we first look up the possible impl item and find out the corresponding lifetime parameters that would correspond to the higher-ranked lifetimes in HRTB, rewrite them as for<'l0>, for<'l1>, ... to introduce them, then these explicit trait bounds associated with them is headed by that for<'l0>, and in this context, we consider how the trait bound should satisfy.

So, the difference would be distinguished by the different syntax, for example for<'a> 'b:'a means 'b outlives any lifetime 'a, for<'a where 'b:'a>(if we had this syntax), it means 'a is any lifetime that is outlived/upper bound by 'b. Explicit trait bound is the former form, and the implicit trait bound is the latter one. This is my mental model.

And this mental model seems to be consistent with what I have for type parameter Why can `async_fn_traits` bypass the issue of the high-ranked lifetime in `Future`? - #6 by quinedot

the type parameters introduced in the implementation of trait for type T that have not been substituted by those that appear in HRTB from the signature of the item, I prefer to name them as higher-ranked type parameters as if they were introduced by for<T,U,...>. So, it's true for lifetimes.

12

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.