Unknown constant in `mkCongrSimp`/`getFunInfo`

Prerequisites

• 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

An "unknown constant" error thrown during simp/grind, complaining about a private field in the same module.

Context

Sebastian and I already did some preliminary diagnosis. The error seems to be somewhere in mkCongrSimp, probably in getFunInfo. It might be related to https://github.com/leanprover/lean4/issues/11436.

Steps to Reproduce

module

public structure State where
  private count : Nat

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  simp [*]

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  omega

private example {P : State → Prop} (h : P ⟨State.count s⟩) :
    P ⟨State.count s⟩ := by
  grind

Expected behavior: No error

Actual behavior: "unknown constant" error because of use of private field State.count.

Versions

Lean 4.27.0-rc1
Target: x86_64-unknown-linux-gnu

Impact

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

Reproduce the minimal examples for simp, omega, and grind, then inspect the mkCongrSimp entry point and its getFunInfo path mentioned in the report. Trace how the private State.count reference is resolved and add a regression test for the reported case. Done means all examples complete without an unknown constant error.