TryInto for converting Vec to array of fixed size has the wrong error type

[maximebuyse]

fn main() {
    let x = vec![1];
    let y : Result<[u8; 32], _> = x.try_into();
}

Open this code snippet in the playground

The previous example gets rejected by F*:

* Error 19 at Playground.fst(36,4-40,7):
  - Subtyping check failed
  - Expected type
      Core.Result.t_Result (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.u8
            (Rust_primitives.Integers.mk_usize 32))
        (Rust_primitives.Arrays.t_Slice Rust_primitives.Integers.u8)
    got type
      Core.Result.t_Result (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.u8
            (Rust_primitives.Integers.mk_usize 32))
        (Core.Convert.impl_6 Rust_primitives.Integers.u8
            (Rust_primitives.Integers.mk_usize 32))
          .f_Error
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also /home/.cargo/git/checkouts/hax-310c6deb65d920f9/f7ecc0c/proof-libs/fstar/core/Alloc.Vec.fst(4,32-4,41)
Verified module: Playground
1 error was reported (see above)
make[1]: *** [Makefile:79: Playground.fst.checked] Error 1
make: *** [Makefile:12: all] Error 2

This is because when trying to convert for example &[u8] to [u8, 32] , the error type is TryFromSliceError, but when converting Vec<u8> to [u8, 32], the error type is Vec<u8>.

I am afraid we cannot solve this because Vecs and slices have the same encoding in our F* core lib so this means we cannot provide a different error type for the two type class implementations of TryInto because both types are the same so the type class implementation must be the same as well.

[maximebuyse]

A workaround for this can be to write (&x[..]).try_into()