change _ at h fails

[sven-manthe]

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

When rewriting creates a metavariable, this leads to unexpected type mismatches with later metavariables, even in expressions like change _ at h

Context

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/change.20_.20at.20h.20fails

Steps to Reproduce

def g (_ : Nat) : Nat := 0
theorem iff (a : Nat) :
  0 = g 0 ↔ 0 = a := by sorry
theorem test
  (T : Unit)
  (h : 0 = g 0)
  (ih : T = T) --removing this, or even swapping it with h, parameter makes change succeed below
  : 0 = g 0 := by
  rw [iff] at h
  change _ at h --fails with type mismatch
  /-
  type mismatch
    this
  has type
    ?m.158 : Sort ?u.157
  but is expected to have type
    0 = ?m.129 : Prop
  -/

Expected behavior:

change succeeds and does nothing

Actual behavior:

change fails with type mismatch

Versions

Lean 4.10.0 (also earlier)

Impact

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

[Kha]

Unfortunately, as described at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/change.20_.20at.20h.20fails/near/445730313, there is nothing to fix here - this is just how mvars (must) work