pattern matching ignores inaccessibility annotation

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

example : (x : Bool × Bool) → x.fst = x.snd ⊕' Unit → Unit
  | (.(b), b), .inl rfl => ()
  | (_, false), _ => ()
  | (_, true), _ => ()

During elaboration, Lean.Elab.Term.ToDepElimPattern.normalize ignores the explicit inaccessible pattern in (.(b), b) and rewrites it to (b, .(b)), which causes an error since the second component is now neither a constructor nor a variable pattern.

Steps to Reproduce

Run the code above.

Expected behavior: The code succeeds with no errors.

Actual behavior: The code results in the following error:

dependent match elimination failed, inaccessible pattern found
  .(fst✝)
constructor expected

Versions

Lean 4.16.0-nightly-2025-01-06
This behavior has existed since Lean 4.0.0-m1

Impact

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

Start with the Lean.Elab.Term.ToDepElimPattern.normalize entry point named in the report and run the minimal reproducer against the specified nightly version. Trace how the explicit inaccessible pattern in (.(b), b) is normalized; done means the example elaborates successfully without the reported dependent match elimination error.