Type inference for closure return types

[y1ca1]

The problem

Consider the following simple closure:

use vstd::prelude::*;

verus! {

fn main() {
    let ok1 = |x: u8| -> _ { x }; // ok1: impl Fn(u8) -> u8 (inferred)
}

} // verus!

The use of type hole _ here is valid in both Rust and Verus. However, when we want to add spec to the closure, one has to explicitly annotate the return type like let ok1 = |x: u8| -> (o: u8) ensures x == o { x }. Otherwise, Verus complains.

use vstd::prelude::*;

verus! {

fn main() {
    let err1 = |x: u8| -> (o: _)
        ensures
            o == x,
        { x };
}

} // verus!

Verus outputs:

error[E0282]: type annotations needed
  --> /playground/src/main.rs:10:13
   |
10 |             o == x,
   |             ^^^^^^ cannot infer type of the type parameter `Lhs` declared on the function `spec_eq`
   |
help: consider specifying the generic arguments
   |
10 |             o == x::<Lhs, u8>,
   |                   +++++++++++

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0282`.

Why care

Type inference for closure return types is especially useful when it comes to nested closures. Consider the following valid Rust/Verus code:

let ok2 = |x: u8| -> _ { move |y: u8| { (x, y) } };

The inferred closure type is impl Fn(u8) -> impl Fn(u8) -> (u8, u8). Specifically, the type of the inner closure (or the return type of the outer closure) is impl Fn(u8) -> (u8, u8), which is not allowed to be written explicitly in Rust for reasons I have yet to explore.

let ok2 = |x: u8| -> impl Fn(u8) -> (u8, u8) { move |y: u8| { (x, y) } };

error[[E0562]](https://doc.rust-lang.org/stable/error_codes/E0562.html): `impl Trait` only allowed in function and inherent method argument and return types, not in closure return types
 --> /playground/src/main.rs:7:26
  |
7 |     let ok2 = |x: u8| -> impl Fn(u8) -> (u8, u8) { move |y: u8| { (x, y) } };
  |                          ^^^^^^^^^^^^^^^^^^^^^^^

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0562`.

So there is no way if we want to add some specs for a nested closure like:

let err2 = |x: u8| -> (o: _)
        ensures
            forall|i| o.requires((i,)),
        { move |y: u8| { (x, y) } };

error[[E0282]](https://doc.rust-lang.org/stable/error_codes/E0282.html): type annotations needed
  --> /playground/src/main.rs:14:23
   |
14 |             forall|i| o.requires((i,)),
   |                       ^ cannot infer type

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0282`.

Link to code

I am curious if it's inherently hard to support this feature/there's any workaround/pointers to code if I decide to make a PR? Thanks!