Commit 2025-11-27 23:09 37726fd6
View on Github →fix(Linter/PrivateModule): do not consider reserved names as public (#32140)
As discovered on zulip.
The declarations associated with reserved names are added to the environment lazily, and may therefore be added in downstream files. Further, they may be added to the public scope if their originating modules are public imports.
For example, if foo is public in M.Foo, this causes foo.eq_1 to be reserved as a name in downstream modules. If M.Bar uses public import M.Foo, then when the declaration for foo.eq_1 is realized and added to the environment, it will end up in the public scope. We should still fire the linter in these cases if every non-reserved name is private. Hence, we ignore reserved names in the main loop and do not count them as public declarations from the current module.