Wrong type ascription pattern in generated F*

[maximebuyse]

struct Other<'a>(&'a i32);

enum Test<'a> {
    C1(Other<'a>)
}

impl<'a> Test<'a> {
    fn test(&self) -> i32 {
        match self {
            Self::C1(c) => *c.0

        }
    }
}

Open this code snippet in the playground

The generated F* for the test method from the example is:

let impl__test (self: t_Test) : i32 =
  match self with
  | (Test_C1 c: t_Test) -> c._0

F* rejects it with Type ascriptions within patterns are only allowed on variables

[franziskuskiefer]

Don't put any type annotations here.

[maximebuyse]

As F* allows type ascription patterns only on variables, my first attempt is to remove the type ascription (and keep only the underlying pattern) except when the underlying pattern is a binding pattern.

However what I understand from the Rust doc on patterns an this canceled feature is that type ascription patterns in Rust are allowed only in let bindings so I think we could actually completely ignore them in the F* backend (even when they wrap a binding pattern) but both solutions are probably fine.