`@[reducible]` causes seemingly noop-rewrites

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The MRE is below. The proposition being proved in not_reducing below is false, but is the simplest one I could think of that still triggered the issue.

In the first arm of not_reducing, the goal is ((val x✝), (val (Test.atom a✝))) = (0, 0). My understanding is that rewrite [val] should be able to turn this into ((val x✝), a✝)) = (0, 0) by unfolding the definition of val. However, that rewrite does nothing, despite reporting success. The second rewrite DOES successfully unfold the definition.

The weirdest part is that commenting out the @[reducible] annotation makes the first rewrite actually work.

inductive Test : Type 
| atom : Nat → Test
| app : Test → Test

@[reducible]
def val : Test → Nat
| Test.atom a => a
| Test.app a => (val a)

theorem not_reducing (a0 a1 : Test) :
  ((val a0), (val a1)) = (0, 0) := by
match a0, a1 with
| _, Test.atom _ => rewrite [val]; sorry -- rewrite does nothing
| Test.atom _, _ => rewrite [val]; sorry -- rewrite works
| _, _ => sorry

Versions

Lean (version 4.0.0-nightly-2023-05-18, commit df49512880fd, Release)
OS: Pop!_OS 22.04 LTS

Start with the self-contained Lean reproducer in not_reducing, especially the two rewrite [val] branches and the @[reducible] annotation on val. Investigate why the first rewrite reports success without changing the goal, then verify that the reproducer's first branch unfolds val as expected while the second branch continues to work.