Error for missing model lifetime specifier recommends invalid syntax, has unclear fix

[csgordon]

Here's a minimized example:

use prusti_contracts::*;

struct Blah<T> {
    _x: std::marker::PhantomData<T>,
}
#[model]
struct Blah<#[generic] T> {
    r: &T,
}

This complains because the r field in the model doesn't have a lifetime for the &T. But the error message I get is:

error[E0106]: missing lifetime specifier
 --> src/lib.rs:8:8
  |
8 |     r: &T,
  |        ^ expected named lifetime parameter
  |
help: consider introducing a named lifetime parameter
  |
6 ~ #[model]'a,
7 | struct Blah<#[generic] T> {
8 ~     r: &'a T,
  |

For more information about this error, try `rustc --explain E0106`.
error: could not compile `repro` (lib) due to previous error

But of course, the suggested fix is syntactically invalid, because you can't write a lifetime parameter there.

If I remove the T parameter and replace all of its occurrences with, say, u8, I get an error message that suggests adding a lifetime parameter to Blah and using it with that field. So it seems like there's an issue with the suggested fix just in the case where the affected struct already has generic parameters.

[csgordon]

Things get a little weirder; compiling what I thought was the intended fix

use prusti_contracts::*;

struct Blah<T> {
    _x: std::marker::PhantomData<T>,
}
#[model]
struct Blah<'a, #[generic] T> {
    r: &'a T,
}

results in:

error[E0261]: use of undeclared lifetime name `'a`
 --> src/lib.rs:8:9
  |
6 | #[model]
  | -------- lifetime `'a` is missing in item created through this procedural macro
7 | struct Blah<'a, #[generic] T> {
8 |     r: &'a T,
  |         ^^ undeclared lifetime

For more information about this error, try `rustc --explain E0261`.
error: could not compile `repro` (lib) due to previous error

[csgordon]

This second error persists even if I additionally add the 'a parameter to the original model as well, and even if I mark it #[generic].

[fpoli]

Hi @csgordon! Thank you for reporting this. The high-level reason of the weird lifetime error is that specifications are implemented as a macro that desugars attributes into Rust code (we have a debugging flag to show that when running prusti-rustc from the command line). When lifetimes are involved, in some cases the desugarding would have to introduce lifetimes names to generate valid Rust code, but we didn't implement that. @Aurel300 might correct me, but I believe that type models with #[generic] are still very experimental.