`..` patterns in matches should throw an error

[clementblaudeau]

As show in this playground, the .. pattern in matches is not properly supported by hax, yet it does not throw an error but produces ill-typed code. The following (valid) rust code:

fn main () {
    match (1,2,3) {
        (0, 0, 0) => 0,
        (x, ..) => x
    };
}

produces the ill-typed:

let main (_: Prims.unit) : Prims.unit =
  let _:i32 =
    match
      mk_i32 1, mk_i32 2, mk_i32 3
      <:
      (i32 & i32 & i32)
    with
    | Rust_primitives.Integers.MkInt 0,
    Rust_primitives.Integers.MkInt 0,
    Rust_primitives.Integers.MkInt 0 ->
      mk_i32 0
    | x -> x
  in
  ()

where, in the second case of the match, x matches the whole triple instead of the just the first value (!). The engine could either throw an error, or implement support for the .. pattern.

[W95Psp]

Still relevant

[clementblaudeau]

Probably coming from import_thir. It should look at the size of the tuple.