Verus lifetimes verification fails due to misplaced lifetime parameter

[clemsys]

Hi all,

Verus fails when verifying lifetimes on the following (valid) Rust code:

pub trait Borrowable {
    type Borrowed<'a>;

    fn borrow<'a>() -> <Self as Borrowable>::Borrowed<'a>;
}

I tried to understand what's going on. When printing the content of the variable rust_code from the function checked_tracked_lifetimes in rust_verify/src/lifetime.rs, I get the following:

trait T25_Borrowable {
    type A23_Borrowed : ;
}

fn f28_borrow<'a24_a, A26_Self, >(
) -> <A26_Self as T25_Borrowable<'a24_a, >>::A23_Borrowed where A26_Self: T25_Borrowable, A26_Self : ?Sized, 
{
    panic!()
}

As you can see, the 'a24_a is in the wrong place on line 6. It should rather be

<A26_Self as T25_Borrowable>::A23_Borrowed<'a24_a, >

Thanks for your help !

[Chris-Hawblitzel]

Can you try with the latest commit?

[clemsys]

It indeed solves my issue ! Thank you so much, it really helps me !