Strange error "invalid match-expression, type of pattern variable contains metavariables"

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

I'm getting the error "invalid match-expression, type of pattern variable '...' contains metavariables" on simple code. The precise conditions that trigger the error are unclear; trivial unrelated changes can eliminate the error. It would be nice to have this fixed or have a clearer error message.

Steps to Reproduce

Example 1

def demo : List Bool :=
  let s : String := "test"
  let l : List Nat := [1, 2, 3]
  let r := match 1 with | _ => l.map (fun n => let (x) := s; true)
  []

Expected behavior:

I think the program should compile without errors.

Actual behavior:

I get the error message

invalid match-expression, type of pattern variable 'n' contains metavariables

The location shown for the error is the subexpression let (x) := s; true.

Variations:

Adding the type annotation let r : List Bool := ... eliminates the error, as does changing the last line from [] to r.
Each of the following trivial variations of the line let r eliminate the error:

  let r := match 1 with | _ => l.map (fun n => let x := s; true)        -- `let x` instead of `let (x)`
  let r := match 1 with | n => l.map (fun n => let (x) := s; true)      -- `n` instead of `_`
  let r := match 1 with | _ => l.map (fun n => let (x) := "test"; true) -- `"test"` instead of `s`

Example 2

The following example produces the same error. I'm including it because it shows that the error can happen without using _ and without using the somewhat unusual syntax let (x) :=.

def demo : List Bool :=
  let p : String × String := ("test", "test")
  let l : List Nat := [1, 2, 3]
  let o : Option Nat := none
  let r :=
    match o with
    | none => [false]
    | some m => l.map (fun n => let (x, y) := p; true)
  []

Again, this program should compile, but it fails with the error

invalid match-expression, type of pattern variable 'n' contains metavariables

The location shown for the error is the subexpression let (x, y) := p; true.

As in the first example, adding a type annotation to let r eliminates the error.

Versions

Lean versions 4.18.0, 4.19.0, 4.20.0 (using https://live.lean-lang.org).

Start by reproducing both minimal examples in Lean nightly, focusing on the match expressions, inferred let binding, and reported metavariable error. The issue does not name source files or tests; done would mean establishing whether the examples should compile or produce a clearer diagnostic and documenting a reproducible regression check.