`refine'` elaborated to a type-incorrect term

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

Playground

/-- info: Try this: ne_of_beq_false (Eq.refl false) -/
#guard_msgs (info) in
example : ¬0 = 0 := show_term by
  refine' ne_of_beq_false (by rfl : ↑_ = _)

/-- info: Try this: ne_of_beq_false (sorryAx ((0 == 0) = false) true) -/
#guard_msgs (info) in
example : ¬0 = 0 := show_term by
  refine ne_of_beq_false (by rfl : ↑_ = _)

/-- info: Try this: ne_of_beq_false (sorryAx ((0 == 0) = false) true) -/
#guard_msgs (info) in
example : ¬0 = 0 := show_term by
  refine' ne_of_beq_false (by rfl : _ = _)


/-- info: Try this: ne_of_beq_false (sorryAx ((0 == 0) = false) true) -/
#guard_msgs (info) in
example : ¬0 = 0 := show_term by
  refine' ne_of_beq_false (rfl : ↑_ = _)

The difference between the first and second examples seems attributable to withAssignableSyntheticOpaque.

Context

This was discovered while doing a tactic proof and not seeing an error message at the tactic.

Steps to Reproduce

1. Build the above code or open it in an LSP-enabled editor or web playground

Expected behavior: The tactic fails in all cases, thus elaborating with sorry

Actual behavior: The tactic succeeds in the first case, elaborating to a type-incorrect term

Versions

4.10.0-rc2

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 reproducible Lean code in the issue, either in a local build or the linked playground, and compare the four refine' and refine cases. Inspect the elaboration path involving refine' and withAssignableSyntheticOpaque. Done means the problematic case fails like the others instead of producing a type-incorrect term.