`variable` may cause sorry

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

Using variable for a binder may cause an otherwise-silent sorry in private declarations using private constants.

Context

The following example was found when using non-publicly importing the real-life versions of A, B, and the instances in a test file.

I suspect that this is related to #14708, but may have to do specifically with what isExporting setting is provided to runTermElabM in elabMutualDef. (This is just a hunch.)

Steps to Reproduce

module

public section

private def A := Bool
private def B := Bool

private instance : Coe A B := ⟨id⟩
private instance : Membership Bool A := ⟨fun _ _ => true⟩

private def l (s : A) : A := s

axiom notSorry {α} : α

variable (s : A)
/-- warning: declaration uses `sorry` -/
#guard_msgs in
private theorem bad {a : Bool} : a ∈ l s := notSorry
/-- info: bad {a : Bool} : a ∈ l sorry -/
#guard_msgs in
#check bad

private theorem good {a : Bool} (s : A) : a ∈ l s := notSorry

I would expect bad to behave like good. (Apologies, this is minimized from a real example, and I don't have a generic procedure.)

Note: removing public section or making the definitions public/exposed fixes bad.

Versions

4.34.0-nightly-2026-08-08, web

Impact

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

Start by running the minimized Lean example in the issue against the nightly version and confirm that bad emits a sorry warning while good does not. Read the elaboration paths named in the report, especially elabMutualDef and the runTermElabM isExporting setting. Done means the private theorem using a variable binder behaves like the explicitly bound version without an otherwise-silent sorry.