`casesOn` allows accessing private structure fields

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

The automatically generated casesOn implementation for structures allows access to private fields. This works even when the constructor is private, which prevents pattern matching.

Steps to Reproduce

File A:

structure Test where
  private mk ::
  private field : Nat

File B that imports File A:

def Test.field' (self : Test) : Nat :=
  self.casesOn id

Expected behavior: field cannot be accessed outside of File A since it is private.

Actual behavior: File B can access field.

Versions

Lean 4.21.0-nightly-2025-06-06

Impact

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

Start by reading the reproduced two-file example in the issue and investigate how Lean generates casesOn for structures, especially when the constructor and fields are private. Verify that File B cannot access the private field while pattern matching remains unavailable. The issue does not identify a source file or test, so locate the relevant implementation and add a regression test.