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

Also update the error message for invalid names in application
position to suggest valid alternatives.

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