Possible bug with @[reducible]

Stream: lean4

[Luke West]

In the same project as with the autoImplicit issue, I just ran into this puzzle. In the MRE below, when val is annotated with reducible, rewrite can NOT reduce val in the first branch of not_reducing. When the annotation is removed, rewrite succeeds.

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

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

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