Unpacking Subtype leads to recursor error

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

In the presence of Subtype and a destructuring let-binding, the recursor seems to be incorrectly synthesized before being sent off to the kernel.

def Option.attach {α: Type} (o : Option α): Option { x : α // o = .some x } :=
  match o with
  | .some x => .some ⟨x, rfl⟩
  | .none => .none

-- works
def g' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let res := Option.attach (g' T tl)
      res.bind fun x => x.val
  | [] => .none

-- doesn't
def g'' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let res := Option.attach (g'' T tl)
      res.bind fun ⟨x,h⟩ => x
  | [] => .none

Thanks to @JamesGallicchio and @digama0 for helping reproduce this error. Link to original Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/naming.20hypotheses.20when.20using.20do-notation/near/326891317 onwards

Versions

Lean (version 4.0.0-nightly-2023-01-29, commit 38a0d1e3733e, Release) (OSX)

Start with the self-contained definitions of Option.attach, g', and g'' in the issue, comparing the working val projection with the failing destructuring let-binding. Investigate recursor synthesis before kernel elaboration and reproduce the error with the supplied Lean version; done means g'' elaborates and accepts the destructured Subtype binding.