Invalid AIR generation when returning unit type

[pratapsingh1729]

The following code:

use vstd::prelude::*;

verus! {

pub fn owl_unit() -> (res: ())
    ensures res == ()
{ () }

fn main() {
    owl_unit()
}

}

panics the verifier, as follows:

thread '<unnamed>' panicked at rust_verify/src/verifier.rs:728:21:
internal error: generated ill-typed AIR code: error 'in call to ens%main!owl_unit., expected 2 arguments, found 1 arguments' in expression '(ens%main!owl_unit. 0)'
note: [run with `RUST_BACKTRACE=1` environment variable to display a backtrace](https://play.verus-lang.org/?version=stable&mode=basic&edition=2021#)
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:339:17:
dropped, expected call to `into_inner` instead
stack backtrace:
...

Minimal playground link with full backtrace

On the other hand, removing the ensures res == () on owl_unit() makes the panic go away (link).

Thanks to parametricity, the ensures res == () spec is not actually needed, but noting in case it points to a bigger bug.

[Chris-Hawblitzel]

I'm adding other cases to this issue where using a unit return type can result in invalid AIR code. For example (from #1161 ):

trait T {
    spec fn f();
}

spec fn f<A: T>() {
    A::f()
}

[tjhance]

Here's another one:

trait Tr : Sized {
    fn get() -> (r: Self)
        ensures r == r;
}

impl Tr for () {
    fn get() -> (r: Self)
    {
    }
}