simp doesn't rewrite in definitions because of unassigned metavariables

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

The following code fails:

set_option trace.Meta.Tactic.simp true
def foo {ι : Type _} (n m : ι) (h h' : n = m) : ℕ := by
  simp only [id h] at h' -- no progress
  simp only [h] at h' -- works

The trace message is

[Meta.Tactic.simp.rewrite] id h:1000, has unassigned metavariables after unification 

Note that the unassigned metavariable is the universe metavariable of ι

Expected behavior: simp only [id h] should succeed, just like simp only [h] already does.

Related Issues

#4398 is basically the same issue, and #4493 didn't really fix the underlying issue.

Impact

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

Start with the minimal reproducer in the issue and enable the shown Meta.Tactic.simp trace to compare simp only [id h] with simp only [h]. Trace the simp rewrite and unification path that reports an unassigned universe metavariable, using related issues #4398 and #4493 for context. Done means the first form succeeds like the second without breaking the existing behavior.