UX Improvement: Ensures clause requires type annotation

[celinval]

Requested feature: Improve UX for ensure clauses.
Use case: Since #3207, ensures are now represented as closures that receive a reference of the return value. However, when using this annotation, we often get an error that requires the type to be specified.
Link to relevant documentation (Rust reference, Nomicon, RFC):

Test case:

#[kani::ensures(|result| *result == Foo::A)]
pub fn foo_a() -> Foo {
    Foo::A
}

I get the following compilation error:

error[E0282]: type annotations needed
  --> promoted_constants_enum.rs:16:18
   |
16 | #[kani::ensures(|result| *result == Foo::A)]
   |                  ^^^^^^  ------- type must be known at this point
   |
help: consider giving this closure parameter an explicit type
   |
16 | #[kani::ensures(|result: /* Type */| *result == Foo::A)]

[pi314mm]

I think this might actually relate to this issue: rust-lang/rust#12679