`View` and `DeepView` only partially supported for `&[T]`

[y1ca1]

Description

This is related to #1070 and was tested after #1078.

Consider the following code:

// fn id<T: DeepView>(t: T) -> T { // won't work for &[T]
fn id<T: View>(t: T) -> T { // won't work for &[T]
    t
}
fn test() {
    let bytes: [u8; 4] = [0, 0, 0, 0];
    let byte_slice: &[u8] = bytes.as_slice();
    id(byte_slice);
}

When a DeepView/View trait bound is specified, any type implementing them should be compatible. However, Verus outputs:

error[E0277]: the size for values of type `[u8]` cannot be known at compilation time
  --> foo.rs:11:12
   |
11 |         id(byte_slice);
   |         -- ^^^^^^^^^^ doesn't have a size known at compile-time
   |         |
   |         required by a bound introduced by this call
   |
   = help: the trait `std::marker::Sized` is not implemented for `[u8]`
   = help: the following other types implement trait `vstd::view::View`:
             [T; N]
             [T]
   = note: required for `&[u8]` to implement `vstd::view::View`
note: required by a bound in `id`
  --> foo.rs:4:14
   |
4  |     fn id<T: View>(t: T) -> T {
   |              ^^^^ required by this bound in `id`

error: aborting due to 1 previous error

This is because vstd only implements View/DeepView for &A where A: Sized (implicit):

impl<A: View> View for &A {
    type V = A::V;

    #[verifier::inline]
    open spec fn view(&self) -> A::V {
        (**self).view()
    }
}

impl<A: DeepView> DeepView for &A {
    type V = A::V;

    #[verifier::inline]
    open spec fn deep_view(&self) -> A::V {
        (**self).deep_view()
    }
}

However, [T] is a dynamically sized type and hence the error.

Possible solution

Adding ?Sized to the trait bound won't work for some reason:

impl<A: View + ?Sized> View for &A {
    type V = A::V;

    #[verifier::inline]
    open spec fn view(&self) -> A::V {
        (**self).view()
    }
}

error: the size for values of type `[u8]` cannot be known at compilation time
  --> foo.rs:12:14
   |
12 |         id(byte_slice);
   |              ^^^^^

error: aborting due to 1 previous error

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

Explicitly implementing e.g. DeepView for &[T] does work:

impl<T: DeepView> DeepView for &[T] {
    type V = Seq<T::V>;

    open spec fn deep_view(&self) -> Self::V {
        (**self).deep_view()
    }
}

verification results:: 2 verified, 0 errors