From 2daaa50afbb72f986ae7202d45d481304f9be8a0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 3 Mar 2026 11:20:21 +1100
Subject: [PATCH] chore: constructorNameAsVariable linter respects linter.all
 (#4966)

This PR ensures `linter.all` disables `constructorNameAsVariable`.

The issue was discovered by @eric-wieser while investigating a quote4
issue.

This seems like an easy mistake to make when setting up a new linter,
and perhaps we need a better structure to make it easy to do the right
thing.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Lean/Linter/ConstructorAsVariable.lean |  6 ++--
 tests/elab/1132.lean.out.expected          |  3 --
 tests/elab/casesRec.lean.out.expected      |  6 ----
 tests/elab/constructor_as_variable.lean    | 37 +++++++++++++++++-----
 4 files changed, 33 insertions(+), 19 deletions(-)
 delete mode 100644 tests/elab/1132.lean.out.expected
 delete mode 100644 tests/elab/casesRec.lean.out.expected

diff --git a/src/Lean/Linter/ConstructorAsVariable.lean b/src/Lean/Linter/ConstructorAsVariable.lean
index 034640d2db..bbf026d233 100644
--- a/src/Lean/Linter/ConstructorAsVariable.lean
+++ b/src/Lean/Linter/ConstructorAsVariable.lean
@@ -34,6 +34,8 @@ matches a particular constructor. Use `linter.constructorNameAsVariable` to disa
 -/
 def constructorNameAsVariable : Linter where
   run cmdStx := do
+    unless getLinterValue linter.constructorNameAsVariable (← getLinterOptions) do
+      return
     let some cmdStxRange := cmdStx.getRange?
       | return
 
@@ -55,9 +57,9 @@ def constructorNameAsVariable : Linter where
               -- 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
+              let opts ← ci.options.toLinterOptions
               -- we have to check for the option again here because it can be set locally
-              if !linter.constructorNameAsVariable.get opts then return
+              if !getLinterValue linter.constructorNameAsVariable 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 ←
diff --git a/tests/elab/1132.lean.out.expected b/tests/elab/1132.lean.out.expected
deleted file mode 100644
index e5c705a3c5..0000000000
--- a/tests/elab/1132.lean.out.expected
+++ /dev/null
@@ -1,3 +0,0 @@
-1132.lean:17:15-17:16: warning: Local variable 'a' resembles constructor 'Baz.a' - write '.a' (with a dot) or 'Baz.a' to use the constructor.
-
-Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
diff --git a/tests/elab/casesRec.lean.out.expected b/tests/elab/casesRec.lean.out.expected
deleted file mode 100644
index ba8eb725cd..0000000000
--- a/tests/elab/casesRec.lean.out.expected
+++ /dev/null
@@ -1,6 +0,0 @@
-casesRec.lean:39:13-39:14: warning: Local variable 'a' resembles constructor 'Ex3.Foo.a' - write '.a' (with a dot) or 'Ex3.Foo.a' to use the constructor.
-
-Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
-casesRec.lean:39:15-39:16: warning: Local variable 'b' resembles constructor 'Ex3.Foo.b' - write '.b' (with a dot) or 'Ex3.Foo.b' to use the constructor.
-
-Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
diff --git a/tests/elab/constructor_as_variable.lean b/tests/elab/constructor_as_variable.lean
index a21a8bfe47..86f40dab94 100644
--- a/tests/elab/constructor_as_variable.lean
+++ b/tests/elab/constructor_as_variable.lean
@@ -1,3 +1,5 @@
+import Lean.Elab.Command
+
 /-!
 Testing for linter.constructorNameAsVariable
 
@@ -10,6 +12,15 @@ will be guided to the right qualified names. Thus, both are tested together here
 -/
 set_option linter.unusedVariables false
 
+-- The test harness passes `-Dlinter.all=false`, which would disable this linter.
+-- We unset `linter.all` so that the linter uses its default value (`true`).
+-- This is a minimal inline version of Mathlib's `unset_option`.
+open Lean Elab Command in
+elab "unset_option " opt:ident : command => do
+  modifyScope fun scope => { scope with opts := scope.opts.erase opt.getId.eraseMacroScopes }
+
+unset_option linter.all
+
 inductive A where
   | x | y
 
@@ -41,6 +52,12 @@ set_option linter.constructorNameAsVariable false in
 def g' : A → Unit
   | x => ()
 
+-- Check that turning it off via `linter.all` works
+#guard_msgs in
+set_option linter.all false in
+def g'' : A → Unit
+  | x => ()
+
 -- Avoid false positives
 #guard_msgs in
 def h : A → Unit
@@ -108,16 +125,18 @@ def ctorSuggestion1 (pair : MyProd) : Nat :=
 error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`
 
 Hint: Using one of these would be valid:
-  [apply] `List.Sublist.cons`
+  [apply] `Std.DHashMap.Internal.AssocList.cons`
+  [apply] `List.Pairwise.cons`
   [apply] `Lean.Grind.AC.Seq.cons`
   [apply] `List.Lex.cons`
+  [apply] `List.Sublist.below.cons`
+  [apply] `List.Perm.cons`
+  [apply] `List.Sublist.cons`
+  [apply] `Lean.AssocList.cons`
   [apply] `List.Perm.below.cons`
   [apply] `List.Lex.below.cons`
   [apply] `List.Pairwise.below.cons`
   [apply] `List.cons`
-  [apply] `List.Sublist.below.cons`
-  [apply] `List.Perm.cons`
-  [apply] `List.Pairwise.cons`
 ---
 warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
 
@@ -138,16 +157,18 @@ inductive StringList : Type where
 error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`
 
 Hint: Using one of these would be valid:
-  [apply] `List.Sublist.cons`
+  [apply] `Std.DHashMap.Internal.AssocList.cons`
+  [apply] `List.Pairwise.cons`
   [apply] `Lean.Grind.AC.Seq.cons`
   [apply] `List.Lex.cons`
+  [apply] `List.Sublist.below.cons`
+  [apply] `List.Perm.cons`
+  [apply] `List.Sublist.cons`
+  [apply] `Lean.AssocList.cons`
   [apply] `List.Perm.below.cons`
   [apply] `List.Lex.below.cons`
   [apply] `List.Pairwise.below.cons`
   [apply] `List.cons`
-  [apply] `List.Sublist.below.cons`
-  [apply] `List.Perm.cons`
-  [apply] `List.Pairwise.cons`
   [apply] `StringList.cons`
 ---
 warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.