feat: add a linter for local vars that clash with their constructors

[david-christiansen]

This came up when watching new Lean users in a class situation. A number of them were confused when they omitted a namespace on a constructor name, and Lean treated the variable as a pattern that matches anything.

For example, this program is accepted but may not do what the user thinks:

inductive Tree (α : Type) where
  | leaf
  | branch (left : Tree α) (val : α) (right : Tree α)

def depth : Tree α → Nat
  | leaf => 0

Adding a branch case to depth results in a confusing message.

With this linter, Lean marks leaf with:

Local variable 'leaf' resembles constructor 'Tree.leaf' - write '.leaf' (with a dot) or 'Tree.leaf' to use the constructor.
note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`

Additionally, the error message that occurs when invalid names are applied in patterns now suggests similar names. This means that:

def length (list : List α) : Nat :=
  match list with
  | nil => 0
  | cons x xs => length xs + 1

now results in the following warning on nil:

warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`

and error on cons:

invalid pattern, constructor or constant marked with '[match_pattern]' expected

Suggestion: 'List.cons' is similar

The list of suggested constructors is generated before the type of the pattern is known, so it's less accurate, but it truncates the list to ten elements to avoid being overwhelming. This mostly comes up with mk.

[david-christiansen]

CC @leodemoura - this is what we talked about yesterday

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4301 build failed against this PR. (2024-05-28 22:55:38) View Log
• ❌ Mathlib branch lean-pr-testing-4301 built against this PR, but testing failed. (2024-05-30 23:38:35) View Log
• ❌ Mathlib branch lean-pr-testing-4301 built against this PR, but testing failed. (2024-06-01 07:58:10) View Log
• ❌ Mathlib branch lean-pr-testing-4301 built against this PR, but testing failed. (2024-06-12 05:38:57) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c5120c1d0dd5a23f1432b6432e6d897659ebb63f --onto bedcbfcfeed429428c3e7f008b6984fc8c2b2b76. (2024-06-13 13:44:42)
• 💥 Mathlib branch lean-pr-testing-4301 build failed against this PR. (2024-06-14 04:50:54) View Log

[david-christiansen]

This is a draft until I fix the linter warnings during bootstrapping - but I think the linter itself is ready for review

[mhuisi]

Should this new linter be limited to situations where denoting a constructor makes sense?

[david-christiansen]

I don't think so, but it's a good question to ask.

There's two reasons:

1. For new Lean users, it may not be clear where a constructor can or can't be denoted by a name. Having the linter fire may help make it clear that this is a variable.
2. For less-new Lean users, avoiding this lint can make it more difficult to introduce bugs during refactoring. While I've been going through trying to make the compiler avoid this lint, there's been a few cases where renaming the argument to the function but skipping its use sites results in a program that still type checks, because the function is defined in the datatype's namespace and the constructor in question is nullary. I'm being careful while I do the renaming, and using "rename symbol", but it seems useful to have code in general that's robust in the face of incomplete renamings.

What do you think?

[mhuisi]

I think both of those are valid concerns, but I'm also not sure whether they outweigh the potential annoyance of not being able to use a specific name in a position where you know it's safe and you can't even accidentally mess it up because constructors are not allowed in this position. I don't have a strong opinion either way!

[nomeata]

Can you think of an example where using a constructor name is actually better? Maybe using fvar to bind an Expr known to be a .fvar n. Hmm.

[mhuisi]

There are plenty of examples in the diff of this PR where people felt like the constructor name was the most natural name to use (both because it is known to be the constructor and by accident) :-)

[david-christiansen]

Though whether it's firing in places where constructor patterns are allowed is a bit of a red herring for this kind of situation, because we have a fair number of instances of let fvar := ...

[david-christiansen]

OK, I'm going to aim for less disturbance right now, and then we can have the discussion later. I'll add an option to disable it for certain constructors, set the default to false, update-stage0, then set the default to true with all of the cases that we frequently use set to exceptions. Then we can take it case by case, and not all in one ginormous diff.

[david-christiansen]

This has now been changed so that the linter only fires for nullary constructors that overlap bound variable names of the same type - only one constructor was hit by this in all of Lean.

At the same time, I also updated the error message for non-constructor things being applied in patterns so that it suggests valid names if any exist. This should also catch similar misunderstandings in those cases.

Now it doesn't need to be selectively disabled, which is a good sign.

[tydeu]

@david-christiansen

only one constructor was hit by this in all of Lean.

I am curious what the one example was? Was it just this one (SemanticTokenType)? If so, I see how the linter here makes sense as I can imagine a very perplexing bug caused by some pattern match confusion between a variable match type and constructor match .type.

[david-christiansen]

Turns out I was wrong - there was this one, and then also https://github.com/leanprover/lean4/pull/4301/files#diff-ec4d9d868e0d4a5702d821884ef44382eb312b8de8fab76db01879ee97fead78L104-R108 .

So two places - not too terrible, I suppose, and I think both are easier to read with this change.

[david-christiansen]

Simulating the next PR post-stage0-update is showing that there's something I don't understand about attributes and bootstrapping, so I'm marking draft until the followup PR also works locally.

[david-christiansen]

OK, I locally have a followup change that enables and cleanly suppresses the warning after an update-stage0. I think this is ready to go.

Stage0 update will no longer be needed after latest updates :)

[david-christiansen]

All right, I'm now pretty happy with this. Three questions:

1. https://github.com/leanprover/lean4/pull/4301/files#diff-0c5c74cee876dff8618e1b4aac6bde00a14373979b53e906b9ffa3c5bf297bbbR78-R94 feels like a bit of a kludge, but I couldn't find a better way to get the hovers to work, and having the hovers is really useful. Am I missing something here? And does something like this deserve wider use in Lean when showing constant names in messages?
2. In https://github.com/leanprover/lean4/pull/4301/files#diff-01b77c950c105319996018cc460d4342e69e79a613383d179ead26dffab60324R77-R82 , I'm assuming that the omission of the ForIn instance was not intentional - after all, there's already a forM operator and a fold. If it was intentional, let me know and I'll work around it.
3. Any bike-shedding for the updated error message texts at https://github.com/leanprover/lean4/pull/4301/files#diff-b183f2ae0639e45df010d4b1f1ec343a5d0f8c04d141ced325cec20efd21a871R86-R139 ?

[david-christiansen]

Rebase and squash to try to fix CI failure