Failure when metaprogramming a dependent tuple, with top-level pattern

[mtzguido]

open FStar.Tactics.V2

let (| x, y |) =
  (_ by (
    apply (`Mkdtuple2);
    trefl ()
  ))
  <: (y:int & squash (1 == y))

Gives

* Error 54 at tests/tactics/Postprocess.fst(20,10-20,11):
  - (*?u17*) _ is not equal to the expected type x

Raised during solve_deferred_constraints in phase1.

[mtzguido]

Actually not related to tactics at all

let tup = (| 1, () |) <: (y:int & squash (1 == y))
let y = match tup with | Mkdtuple2 _ y -> y

gives the same error. I recall a similar issue but couldn`t find it.