RFC: private/public/protected in local where/let rec

Proposal

While local let declarations are properly private, local where and let rec declarations float to top-level definitions (namespaced within the enclosing definiton’s name).

To downstream tooling (doc generation, linters), these look like normal public definitions, e.g show up in the module API description. I find this surprising, and would assume them to be an implementation detail of the enclosing function, and not or only hard to get your hands on from the outside.

One possible fix is to treat them always like private definitions (as experimented with in #2717). But there seem to be use case where you do want outside access to local definitions (otherwise why would docstrings be supported, and presumably in proofs it might be useful).

A more refined fix is to allow the visibility modifiers public, private and protected to be used in where and let rec, giving the developer control over whether these definitions should or should not be externally visible. Possibly with private being the default.

Another direction would be to simply somehow mark these definitions as “lifted from local definitions”, and let the tooling decide what to with it (e.g. the docstring linter could not complain about them; the API documentation could omit them unless there is a docstring).

Community Feedback

Previously briefly discussed on Zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading the proposal, the referenced experiment in #2717, and the linked Zulip discussion. Compare the proposed visibility modifiers, private-by-default behavior, and tooling-based handling; done requires an agreed direction for local where and let rec visibility.