Cannot match implicit arg using constructor

The second match fails with 'syntax error', but the fact that the argument is implicit should not make a difference.
```fstar
noeq
type t2 = | Mk2 : _:int -> t2

let test2 (x:t2) : int =
match x with
| Mk2 0 -> 0
| _ -> 1

noeq
type t1 = | Mk1 : #_:int -> t1

let test1 (x:t1) : int =
match x with
| Mk1 #0 -> x
| _ -> 1
```

Start by reproducing the two F* match expressions in the issue, comparing the explicit Mk2 pattern with the implicit-argument Mk1 pattern. Trace constructor-pattern parsing and matching, then add regression coverage showing that matching the implicit argument does not produce a syntax error.

Written by the indexing model from the issue text.