Unclear "mismatched types" error message

[clemsys]

Hi all,

On the following code, Verus reports the following error :

use vstd::prelude::*;

verus! {
    trait HasData {
        type Data;
    }

    struct Foo<T>(T);

    impl<T> HasData for Foo<T> {
        type Data = u8;
    }

    impl<T: HasData> Foo<T> {
        #[verifier(external_body)]
        fn data(&self) -> T::Data {
            unimplemented!()
        }
    }

    fn bar<T: HasData<Data = u8>>(bar: Foo<T>) {
        let a = bar.data();
    }

    fn main() { }
}

error: mismatched types
  --> src/main.rs:22:16
   |
22 |         let a = bar.data();
   |                ^^   ^^^^^^

error: aborting due to 1 previous error

note: This error was found in Verus pass: ownership checking of tracked code

error: aborting due to 2 previous errors

This error message is unclear because I did not type hint a. In my opinion, Verus should either say that I'm doing something unsupported, or accept this code as valid.

Thanks for your help !

[Chris-Hawblitzel]

Fortunately, there has been a series of bug fixes and feature implementations for https://github.com/verus-lang/verus/issues/1158 and https://github.com/verus-lang/verus/issues/1161 . These were in a separate branch, but I just merged them into main. I believe your example should work now. Let me know if you have further problems with this.

[clemsys]

Indeed it works now. Thank you very much!