rcases doesn't complain about unsynthesized placeholder

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

If you write rcases x and x still has metavariables, this is not reported until the tactic is finished (and no new goals are generated for the metavariables)

Steps to Reproduce

example (p q : Prop) (h : Nat → p ∨ q) : True := by
  rcases h _ with h|h
  · trivial
  -- · trivial 
  -- if you uncomment the previous line, the expected error "don't know how to synthesize placeholder" is shown

Expected behavior: already display the error in the rcases tactic (or potentially create a new goal for it - maybe if you write ?_ for the metavariable)

Actual behavior: no warning/error (besides "unsolved goals")

Context

Zulip

This bug also affects cases' (from Mathlib)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproduction in the issue against the latest Lean nightly and compare the behavior of rcases with the commented line enabled. No source file or test path is named; investigate the rcases tactic behavior, including the related cases' case, and consider the issue done when the unsynthesized placeholder is reported during the tactic or becomes an explicit goal.