Some `impl View`s seem to disappear when compiling Verus code with `cargo`

[pratapsingh1729]

Suppose I have the following code in src/main.rs in some crate:

use vstd::prelude::*;
use std::rc::Rc;

verus! {

#[verifier(external_body)]
pub exec fn rc_clone<T:View>(t: &Rc<T>) -> (r: Rc<T>)
    ensures r.view() == t.view()
{ Rc::clone(t) }

pub exec fn foo(x: Rc<Vec<u8>>) -> (y: Rc<Vec<u8>>)
    ensures y.view() == x.view()
{
    rc_clone(&x)
}

}

fn main() {}

This verifies just fine with Verus, run as verus main.rs. Indeed, if I run verus main.rs --compile, it compiles just fine as well.

However, suppose my Cargo.toml then contains the following:

[dependencies]
builtin = { git = "https://github.com/verus-lang/verus", branch = "main" }
builtin_macros = { git = "https://github.com/verus-lang/verus", branch = "main" }
vstd = { git = "https://github.com/verus-lang/verus", branch = "main" }

I then compile the crate using cargo build. This gives me the following bizarre error:

   Compiling verus-vec-view-issue v0.1.0 (/usr0/home/prataps/src/verus-vec-view-issue)
error[E0277]: the trait bound `Vec<u8>: vstd::view::View` is not satisfied
  --> src/main.rs:14:14
   |
14 |     rc_clone(&x)
   |     -------- ^^ the trait `vstd::view::View` is not implemented for `Vec<u8>`
   |     |
   |     required by a bound introduced by this call
   |
   = help: the following other types implement trait `vstd::view::View`:
             bool
             isize
             i8
             i16
             i32
             i64
             i128
             usize
           and 19 others
note: required by a bound in `rc_clone`
  --> src/main.rs:7:24
   |
7  | pub exec fn rc_clone<T:View>(t: &Rc<T>) -> (r: Rc<T>)
   |                        ^^^^ required by this bound in `rc_clone`

For more information about this error, try `rustc --explain E0277`.
error: could not compile `verus-vec-view-issue` (bin "verus-vec-view-issue") due to 1 previous error

It seems as though Vec<u8> should definitely implement View? The code for that is here. I am not sure why Cargo doesn't get to see that impl---maybe it is getting erased during compilation?

Tested using Verus commit dc49f92. Archive of the crate: verus-vec-view-issue.zip