Linting against internal constructors

Sometimes, we want a constructor to be public for definitional equality reasons, but to discourage access by the user. However, even internal names (e.g. _mkInternal) can be used without error via anonymous constructor notation ⟨...⟩. This linter assumes internal constructors are internal for a reason, and lints against using them.

Future work

• This linter could be extensible in multiple ways:
  • Custom predicates (e.g. the ability to register non-internal constructors as forbidden)
  • Custom lint messages (e.g. saying "please use fooMk instead")
• This linter could be accompanied by an environment linter to ensure that no forbidden constructor is used in final expressions. Currently this is an elaboration-time linter.
• This linter could be generalized to allow forbidding other sorts of API besides constructors.
• Performance. Currently, this linter has a small but non-negligible performance cost. Depending on where exactly the performance cost is coming from, it might be useful to either:
  • merge the ContextInfos lazily (e.g. only when we need its Environment)
  • run this linter in parallel alongside other similar infotree-traversing linters, within a single infotree traversal

opaque Mathlib.Tactic.Linter.linter.internalConstructors : Lean.Option Bool

Forbid internal constructors (e.g. _mkInternal) from being referenced during elaboration. By default, this is true, and disallows references arising from notation as well (including e.g. anonymous constructor notation).

Internal constructors may be used freely in the module in which they were defined.

def Mathlib.Tactic.Linter.internalConstructor : Lean.Linter

Lints against using constructors with internal names during elaboration.

Equations

• One or more equations did not get rendered due to their size.