Subtrait of View in exec mode

Consider the following code:

use vstd::prelude::*;

verus! {
pub struct Int<T: Bar>(pub T);

exec fn test1() -> Int<u8> {
    Int::<u8>(0)
}

pub trait Bar: View {
}

impl Bar for u8 {
}

} // verus!

test1 should be valid as Bar: View, u8 implements View and we impl Bar for u8.

However, current Verus outputs:

error: the trait bound `u8: T33_Bar` is not satisfied
  --> /playground/src/main.rs:11:15
   |
11 |     Int::<u8>(0)
   |               ^

error: the trait bound `u8: T33_Bar` is not satisfied
  --> /playground/src/main.rs:11:5
   |
11 |     Int::<u8>(0)
   |     ^^^^^^^^^^^^

error: aborting due to 2 previous errors

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

error: aborting due to 3 previous errors

Replacing exec with spec/proof won't trigger this error. Also, a custom super-trait won't have this error. Link to code.

After some preliminary debugging, I believe this was introduced by the commit https://github.com/verus-lang/verus/commit/dc49f920dcb597afdc5a1f59c7b22a2516664e2c.

verus-lang / verus

Subtrait of View in exec mode #1144