Autoparam helper decls are always private

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

(Strictly speaking, this is just about autoParam helper decls coming from variable.)

When a variable has an autoParam, the associated autoParam helper declaration is private even if the declaration it is elaborated for is public.

Because Lean assumes that any errors produced by re-elaboration of variables during declaration elaboration are duplicates of errors at the original variable command, Lean resets the message log and erases the logged error, meaning that the declaration fails only with "depends on sorry".

module

public section

variable (h : True := by trivial)

/-- warning: declaration uses `sorry` -/
#guard_msgs in
theorem foo : h = h := rfl

/-- info: foo (h : autoParam True sorry) : h = h -/
#guard_msgs in #check foo

open Lean Meta Elab Command in
/--
info: without exporting := _private.external:file:///lean-nightly/lean-nightly.lean.0._auto_7
---
info: with exporting := sorry
-/
#guard_msgs in
run_cmd do
  withoutExporting do runTermElabM fun vars => do
    logInfo m!"without exporting := \
      {format (← inferType vars[0]!).getAutoParamTactic?.get!}"
  withExporting do runTermElabM fun vars => do
    logInfo m!"with exporting := \
      {(← inferType vars[0]!).getAutoParamTactic?.get!}"

Context

This is responsible for a few backward.privateInPublics in Mathlib.

Steps to Reproduce

1. Make a variable with an autoParam.
2. Make a declaration with visibility v that uses that variable in its type.

Expected behavior: The autoParam helper declaration in that declaration's type lives at visibility v, or fails at the declaration if parts of that type cannot be used at this visibility.

Actual behavior: The autoParam helper declaration is provided as sorry. (The elaboration of the private constant fails under withExporting, and runTermElabM eats the error.)

Versions

4.34.0, commit f2bcf2e8660ab2d16cf3cb50c8e127de0439a337

Additional Information

1. If variable elaboration is ultimately declaration-specific, perhaps the presence of errors at each original variable binder should be recorded in the Scope somewhere along with the corresponding variable syntax. Later, in runTermElabM, if we encounter new errors despite the original binder elaboration being error-free, do not reset the message log. (If there were originally errors, do reset the message log.) Currently we just always reset the message log.
2. mkUniqueName should perhaps respect isExporting, and deprivatize the name under withExporting. But this encounters the issue that the private name prefix in the default state of the name generator from CommandElabM is also used to make names module-specific. So, would care need to be taken to have a non-private module-specific header, and also check the environment for branches corresponding to those declarations? Or maybe elabMutualDef should just set the name generator name to something appropriate before runTermElabM :)

(I'm not sure if it's okay for these declarations to be private somehow, and they merely need to be elaborated correctly, but it would surprise me to have a private constant anywhere in a public type!)

Aside: I previously opened #11569, which unintentionally led to the current state of affairs! 🙃 Strictly speaking this issue's title should mention variable, but then we'd lose the symmetry. :)

Impact

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

Start by reproducing the issue with the provided variable/autoParam example and inspect runTermElabM, withExporting, and the message-log reset behavior. Then trace mkUniqueName and elabMutualDef to determine how helper visibility is assigned. Done means a public declaration either gets a correctly exported helper or fails with the relevant elaboration error instead of silently producing sorry.