Bug in rcases?

Stream: mathlib4

[Frédéric Dupuis]

While working on mathlib4#1293, I think I encountered a bug in the Lean 4 version of rcases. Here's an MWE. The following works in Lean 3, with rcases generating a goal for the underscore:

example (p : Prop) (h : p → false) (hp : p) : false :=
begin
  rcases h _ with h',
  exact h',
  exact hp,
end

The corresponding code in Lean 4 fails:

example (p : Prop) (h : p → False) (hp : p) : False := by
  rcases h ?_ with h'
  exact h'

Here rcases doesn't generate a goal for ?_ and we just get the error don't know how to synthesize placeholderwhen the main goal is closed.

Is this a known issue? Should I just work around it in the PR for now?

[Heather Macbeth]

I encountered the same issue in Order.Zorn, see the two porting notes in that file. (It also happens for obtain.)