Contracts: Error refers to nonvisible *e_renamed expression

[adpaco-aws]

Requested feature: When trying out the contracts feature in one of my projects, I got the following errors:

error[E0507]: cannot move out of `*e_renamed` which is behind a shared reference
  --> src/lib.rs:79:5
   |
79 |     #[kani::ensures(match result { Ok(t) => Self::typecheck_2(*e, t), Err(_) => true})]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ move occurs because `*e_renamed` has type `Expr`, which does not implement the `Copy` trait
   |
   = note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0507]: cannot move out of `*e_renamed` which is behind a shared reference
  --> src/lib.rs:79:5
   |
79 |     #[kani::ensures(match result { Ok(t) => Self::typecheck_2(*e, t), Err(_) => true})]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ move occurs because `*e_renamed` has type `Expr`, which does not implement the `Copy` trait
   |
   = note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to 2 previous errors

For more information about this error, try `rustc --explain E0507`.
error: could not compile `interpreter` (lib) due to 3 previous errors
error: Failed to execute cargo (exit status: 101). Found 3 compilation errors.

The error refers to an unknown *e_renamed expression which may be confusing for users. Moreover, the error message is printed twice despite the diagnostic being the same for both errors.

This error can be reproduced using the kani-contracts branch of my project. Is it possible to improve the error message in this case?

[JustusAdam]

Just a comment: I don't think the double error message can be fixed at the moment because we create two functions independently that both incorporate the contract code and then we rely on the rust compiler to type check it.

In terms of the renaming I think it would be interesting to try and rely on macro hygiene to distinguish the Idents. It's possible it could work even if they both have the same name.

There may also be ways to preserve the spans more accurately through the macro by the way that AST is composed to make the error location in the contract code better.