Match doesn't rewrite instance implicit parameters

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

Matching on some variable would normally rewrite occurrences of the variable with the context proof. It doesn't happen for class instances though.

Steps to Reproduce

inductive T | T1 | T2
open T

class Cls (t : T) where
  c : t = T1

def foo (t : T) (inst' : Cls t) [inst : Cls t] : Prop :=
 match h : t with
 | T.T2 => by
  rw [h] at inst
  have : T2 = T1 := inst.c

Live Lean Nightly

Put cursor right after by and observer the state.

Expected behavior: inst : Cls T2

Actual behavior: inst : Cls t

Versions

Lean 4.17.0-rc1

Additional Information

Notice that inst' was rewritten.

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 reproducer in the issue against the latest Lean nightly and inspect the match elaboration state after by. Compare how rewriting affects inst' versus the implicit instance inst; done means matching on t makes the context show inst : Cls T2 as expected.