feat: add a linter for local vars that clash with their constructors (#4301)

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`.

releases_drafts/varCtorNameLint.md

@@ -0,0 +1,45 @@
+A new linter flags situations where a local variable's name is one of
+the argumentless constructors of its type. This can arise when a user either
+doesn't open a namespace or doesn't add a dot or leading qualifier, as
+in the following:
+
+````
+inductive Tree (α : Type) where
+  | leaf
+  | branch (left : Tree α) (val : α) (right : Tree α)
+
+def depth : Tree α → Nat
+  | leaf => 0
+````
+
+With this linter, the `leaf` pattern is highlighted as a local
+variable whose name overlaps with the constructor `Tree.leaf`.
+
+The linter can be disabled with `set_option linter.constructorNameAsVariable false`.
+
+Additionally, the error message that occurs when a name in a pattern that takes arguments isn't valid now suggests similar names that would be valid. This means that the following definition:
+
+```
+def length (list : List α) : Nat :=
+  match list with
+  | nil => 0
+  | cons x xs => length xs + 1
+```
+
+now results in the following warning:
+
+```
+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:
+
+```
+invalid pattern, constructor or constant marked with '[match_pattern]' expected
+
+Suggestion: 'List.cons' is similar
+```
+
+
+#4301

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -333,8 +333,8 @@ def SemanticTokenType.names : Array String :=
     "event", "method", "macro", "modifier", "comment", "string", "number",
     "regexp", "operator", "decorator", "leanSorryLike"]
 
-def SemanticTokenType.toNat (type : SemanticTokenType) : Nat :=
-  type.toCtorIdx
+def SemanticTokenType.toNat (tokenType : SemanticTokenType) : Nat :=
+  tokenType.toCtorIdx
 
 -- sanity check
 -- TODO: restore after update-stage0

src/Lean/Data/SMap.lean

@@ -74,6 +74,12 @@ def forM [Monad m] (s : SMap α β) (f : α → β → m PUnit) : m PUnit := do
   s.map₁.forM f
   s.map₂.forM f
 
+instance : ForM m (SMap α β) (α × β) where
+  forM s f := forM s fun x y => f (x, y)
+
+instance : ForIn m (SMap α β) (α × β) where
+  forIn := ForM.forIn
+
 /-- Move from stage 1 into stage 2. -/
 def switch (m : SMap α β) : SMap α β :=
   if m.stage₁ then { m with stage₁ := false } else m

src/Lean/Elab/PatternVar.lean

@@ -47,8 +47,51 @@ structure State where
 
 abbrev M := StateRefT State TermElabM
 
-private def throwCtorExpected {α} : M α :=
-  throwError "invalid pattern, constructor or constant marked with '[match_pattern]' expected"
+private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
+  let message : MessageData :=
+    "invalid pattern, constructor or constant marked with '[match_pattern]' expected"
+  let some idStx := ident | throwError message
+  let name := idStx.getId
+  if let .anonymous := name then throwError message
+  let env ← getEnv
+  let mut candidates : Array Name := #[]
+  for (c, _) in env.constants do
+    if isPrivateName c then continue
+    if !(name.isSuffixOf c) then continue
+    if env.isConstructor c || hasMatchPatternAttribute env c then
+      candidates := candidates.push c
+
+  if candidates.size = 0 then
+    throwError message
+  else if h : candidates.size = 1 then
+    throwError message ++ m!"\n\nSuggestion: '{candidates[0]}' is similar"
+  else
+    let sorted := candidates.qsort (·.toString < ·.toString)
+    let diff :=
+      if candidates.size > 10 then [m!" (or {candidates.size - 10} others)"]
+      else []
+    let suggestions : MessageData := .group <|
+      .joinSep ((sorted.extract 0 10 |>.toList |>.map (showName env)) ++ diff)
+        ("," ++ Format.line)
+    throwError message ++ .group ("\n\nSuggestions:" ++ .nestD (Format.line ++ suggestions))
+where
+  -- Create some `MessageData` for a name that shows it without an `@`, but with the metadata that
+  -- makes infoview hovers and the like work. This technique only works because the names are known
+  -- to be global constants, so we don't need the local context.
+  showName (env : Environment) (n : Name) : MessageData :=
+      let params :=
+        env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
+      .ofFormatWithInfos {
+        fmt := "'" ++ .tag 0 (format n) ++ "'",
+        infos :=
+          .fromList [(0, .ofTermInfo {
+            lctx := .empty,
+            expr := .const n params,
+            stx := .ident .none (toString n).toSubstring n [.decl n []],
+            elaborator := `Delab,
+            expectedType? := none
+          })] _
+      }
 
 private def throwInvalidPattern {α} : M α :=
   throwError "invalid pattern"
@@ -169,9 +212,9 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     -- Check whether the `binop%` operator is marked with `[match_pattern]`,
     -- We must check that otherwise Lean will accept operators that are not tagged with this annotation.
     let some (.const fName _) ← resolveId? stx[1] "pattern"
-      | throwCtorExpected
+      | throwCtorExpected none
     unless hasMatchPatternAttribute (← getEnv) fName do
-      throwCtorExpected
+      throwCtorExpected none
     let lhs ← collect stx[2]
     let rhs ← collect stx[3]
     return stx.setArg 2 lhs |>.setArg 3 rhs
@@ -255,7 +298,7 @@ where
             processCtor stx
           else
             processVar stx
-        | none => throwCtorExpected
+        | none => throwCtorExpected (some stx)
       | _ => processVar stx
 
   pushNewArg (accessible : Bool) (ctx : Context) (arg : Arg) : M Context := do
@@ -307,7 +350,7 @@ where
       | `($fId:ident)  => pure (fId, false)
       | `(@$fId:ident) => pure (fId, true)
       | _              => throwError "identifier expected"
-    let some (Expr.const fName _) ← resolveId? fId "pattern" (withInfo := true) | throwCtorExpected
+    let some (Expr.const fName _) ← resolveId? fId "pattern" (withInfo := true) | throwCtorExpected (some fId)
     let fInfo ← getConstInfo fName
     let paramDecls ← forallTelescopeReducing fInfo.type fun xs _ => xs.mapM fun x => do
       let d ← getFVarLocalDecl x
@@ -321,7 +364,7 @@ where
         processCtorAppContext
           { funId := fId, explicit := explicit, ctorVal? := none, paramDecls := paramDecls, namedArgs := namedArgs, args := args, ellipsis := ellipsis }
       else
-        throwCtorExpected
+        throwCtorExpected (some fId)
 
 def main (alt : MatchAltView) : M MatchAltView := do
   let patterns ← alt.patterns.mapM fun p => do

src/Lean/Linter.lean

@@ -6,6 +6,7 @@ Authors: Lars König
 prelude
 import Lean.Linter.Util
 import Lean.Linter.Builtin
+import Lean.Linter.ConstructorAsVariable
 import Lean.Linter.Deprecated
 import Lean.Linter.UnusedVariables
 import Lean.Linter.MissingDocs

src/Lean/Linter/ConstructorAsVariable.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+set_option linter.missingDocs true
+
+namespace Lean.Linter
+
+open Lean Elab Command
+open Lean.Linter (logLint)
+
+/--
+A linter that warns when bound variable names are the same as constructor names for their types,
+modulo namespaces.
+ -/
+register_builtin_option linter.constructorNameAsVariable : Bool := {
+  defValue := true,
+  descr := "enable the linter that warns when bound variable names are nullary constructor names"
+}
+
+/--
+Reports when bound variables' names overlap with constructor names for their type. This is to warn
+especially new users that they have built a pattern that matches anything, rather than one that
+matches a particular constructor. Use `linter.constructorNameAsVariable` to disable.
+-/
+def constructorNameAsVariable : Linter where
+  run cmdStx := do
+    let some cmdStxRange := cmdStx.getRange?
+      | return
+
+    let infoTrees := (← get).infoState.trees.toArray
+    let warnings : IO.Ref (Lean.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
+
+    for tree in infoTrees do
+      tree.visitM' (preNode := fun ci info _ => do
+        match info with
+        | .ofTermInfo ti =>
+          match ti.expr with
+          | .fvar id .. =>
+            let some range := info.range? | return
+            if (← warnings.get).contains range then return
+            let .original .. := info.stx.getHeadInfo | return
+            if ti.isBinder then
+              -- This is a local variable declaration.
+              let some ldecl := ti.lctx.find? id | return
+              -- Skip declarations which are outside the command syntax range, like `variable`s
+              -- (it would be confusing to lint these), or those which are macro-generated
+              if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
+              let opts := ci.options
+              -- we have to check for the option again here because it can be set locally
+              if !linter.constructorNameAsVariable.get opts then return
+              if let n@(.str .anonymous s) := info.stx.getId then
+                -- Check whether the type is an inductive type, and get its constructors
+                let ty ←
+                  if let some t := ti.expectedType? then pure t
+                  else ti.runMetaM ci (Meta.inferType ti.expr)
+                let ty ← ti.runMetaM ci (instantiateMVars ty >>= Meta.whnf)
+                if let .const tn _ := ty.getAppFn' then
+                  if let some (.inductInfo i) := (← getEnv).find? tn then
+                    for c in i.ctors do
+                      -- Only warn when the constructor has 0 fields. Pattern variables can't be
+                      -- confused with constructors that want arguments.
+                      if let some (.ctorInfo ctorInfo) := (← getEnv).find? c then
+                        if ctorInfo.numFields > 0 then continue
+                      if let .str _ cn := c then
+                        if cn == s then
+                          warnings.modify (·.insert range (info.stx, n, c))
+            else pure ()
+          | _ => pure ()
+        | _ => pure ())
+
+    -- Sort the outputs by position
+    for (_range, declStx, userName, ctorName) in (← warnings.get).toArray.qsort (·.1.start < ·.1.start) do
+      logLint linter.constructorNameAsVariable declStx <|
+        m!"Local variable '{userName}' resembles constructor '{ctorName}' - " ++
+        m!"write '.{userName}' (with a dot) or '{ctorName}' to use the constructor."
+
+builtin_initialize addLinter constructorNameAsVariable

src/Lean/Meta/Tactic/AC/Main.lean

@@ -101,11 +101,10 @@ def buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Lean.Expr ×
 where
   mkContext (α : Expr) (u : Level) (vars : Array Expr) : MetaM (Array Bool × Expr) := do
     let arbitrary := vars[0]!
-    let zero := mkLevelZeroEx ()
-    let plift := mkApp (mkConst ``PLift [zero])
-    let pliftUp := mkApp2 (mkConst ``PLift.up [zero])
-    let noneE tp   := mkApp  (mkConst ``Option.none [zero]) (plift tp)
-    let someE tp v := mkApp2 (mkConst ``Option.some [zero]) (plift tp) (pliftUp tp v)
+    let plift := mkApp (mkConst ``PLift [.zero])
+    let pliftUp := mkApp2 (mkConst ``PLift.up [.zero])
+    let noneE tp   := mkApp  (mkConst ``Option.none [.zero]) (plift tp)
+    let someE tp v := mkApp2 (mkConst ``Option.some [.zero]) (plift tp) (pliftUp tp v)
     let vars ← vars.mapM fun x => do
       let isNeutral :=
         let isNeutralClass := mkApp3 (mkConst ``LawfulIdentity [u]) α preContext.op x

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -468,11 +468,11 @@ def computeAbsoluteLspSemanticTokens
     (endPos?  : Option String.Pos)
     (tokens   : Array LeanSemanticToken)
     : Array AbsoluteLspSemanticToken :=
-  tokens.filterMap fun ⟨stx, type⟩ => do
+  tokens.filterMap fun ⟨stx, tokenType⟩ => do
     let (pos, tailPos) := (← stx.getPos?, ← stx.getTailPos?)
     guard <| beginPos <= pos && endPos?.all (pos < ·)
     let (lspPos, lspTailPos) := (text.utf8PosToLspPos pos, text.utf8PosToLspPos tailPos)
-    return ⟨lspPos, lspTailPos, type⟩
+    return ⟨lspPos, lspTailPos, tokenType⟩
 
 /-- Filters all duplicate semantic tokens with the same `pos`, `tailPos` and `type`. -/
 def filterDuplicateSemanticTokens (tokens : Array AbsoluteLspSemanticToken) : Array AbsoluteLspSemanticToken :=
@@ -488,11 +488,11 @@ def computeDeltaLspSemanticTokens (tokens : Array AbsoluteLspSemanticToken) : Se
     pos1 < pos2 || pos1 == pos2 && tailPos1 <= tailPos2
   let mut data : Array Nat := Array.mkEmpty (5*tokens.size)
   let mut lastPos : Lsp.Position := ⟨0, 0⟩
-  for ⟨pos, tailPos, type⟩ in tokens do
+  for ⟨pos, tailPos, tokenType⟩ in tokens do
     let deltaLine := pos.line - lastPos.line
     let deltaStart := pos.character - (if pos.line == lastPos.line then lastPos.character else 0)
     let length := tailPos.character - pos.character
-    let tokenType := type.toNat
+    let tokenType := tokenType.toNat
     let tokenModifiers := 0
     data := data ++ #[deltaLine, deltaStart, length, tokenType, tokenModifiers]
     lastPos := pos

tests/lean/autoImplicitChain.lean

@@ -1,3 +1,5 @@
+set_option linter.constructorNameAsVariable false
+
 inductive A where
   | a
 

tests/lean/inductionMutual.lean

@@ -6,7 +6,7 @@ inductive B : Type
 | b : B
 end
 
-example (x : PSigma fun (a : A) => True) : A := by
+example (x : PSigma fun (_ : A) => True) : A := by
   cases x with | mk x₁ x₂ => ?_
   induction x₁
   done

tests/lean/run/constructor_as_variable.lean

@@ -0,0 +1,149 @@
+/-!
+Testing for linter.constructorNameAsVariable
+
+This linter checks warns when a bound variable's name is the name of a constructor of the variable's
+type, which probably indicates a namespace mistake, but can be otherwise hard to find.
+
+The linter is designed to interact well with the suggestions provided when a non-constructor is used
+where a constructor would be expected in a pattern, so that users who don't know Lean namespaces
+will be guided to the right qualified names. Thus, both are tested together here.
+-/
+set_option linter.unusedVariables false
+
+inductive A where
+  | x | y
+
+-- Test that the linter works even in the presence of errors (making it useful for confused new
+-- users)
+
+/--
+warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
+note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+-/
+#guard_msgs(drop error, warning) in
+def f : A → Unit
+  | x => _
+
+-- Show that the linter also works when there are no errors
+/--
+warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
+note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+-/
+#guard_msgs(warning) in
+def g : A → Unit
+  | x => ()
+
+-- Check that turning it off works
+#guard_msgs in
+set_option linter.constructorNameAsVariable false in
+def g' : A → Unit
+  | x => ()
+
+-- Avoid false positives
+#guard_msgs in
+def h : A → Unit
+  | z => ()
+
+-- Check that it works for let-bindings
+/--
+warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
+note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+---
+warning: Local variable 'y' resembles constructor 'A.y' - write '.y' (with a dot) or 'A.y' to use the constructor.
+note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+-/
+#guard_msgs in
+def i (a : A × A) : Unit :=
+  let (x, y) := a
+  ()
+
+/--
+warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
+note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+-/
+#guard_msgs in
+def i' : Unit :=
+  let x : A := .x
+  ()
+
+-- Check that it works in tactic proofs
+/--
+warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
+note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+-/
+#guard_msgs in
+theorem j (a : A ⊕ A) : True := by
+  cases a with
+  | inl x => trivial
+  | inr z => trivial
+
+-- Top-level names do not trigger the lint
+#guard_msgs in
+def x : A := A.x
+
+/-! Test the interaction with the invalid match pattern error messages -/
+
+/--
+error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
+
+Suggestions:
+  'Add.mk',
+  'Alternative.mk',
+  'AndOp.mk',
+  'AndThen.mk',
+  'Antisymm.mk',
+  'Append.mk',
+  'Applicative.mk',
+  'Array.Mem.mk',
+  'Array.mk',
+  'BEq.mk',
+   (or 199 others)
+-/
+#guard_msgs in
+def ctorSuggestion1 (pair : α × β) : β :=
+  match pair with
+  | mk x y => y
+
+-- This test is a realistic situation if a user doesn't know how Lean namespaces work
+/--
+error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
+
+Suggestion: 'List.cons' is similar
+---
+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`
+-/
+#guard_msgs in
+def ctorSuggestion2 (list : List α) : Nat :=
+  match list with
+  | nil => 0
+  | cons x xs => 1 + ctorSuggestion2 xs
+
+-- Adding another `cons` also adds a suggestion
+inductive StringList : Type where
+  | nil
+  | cons (s : String) (ss : StringList)
+
+/--
+error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
+
+Suggestions: 'List.cons', 'StringList.cons'
+---
+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`
+-/
+#guard_msgs in
+def ctorSuggestion3 (list : List α) : Nat :=
+  match list with
+  | nil => 0
+  | cons x xs => 1 + ctorSuggestion2 xs
+
+-- There isn't always a suggestion to provide
+
+/--
+error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
+-/
+#guard_msgs in
+def ctorNoSuggestion (x : α) :=
+  match x with
+  | notAConstructor a b c => 42