fix: allow users to disable builtin simprocs in simp args

src/Lean/Elab/Tactic/Simp.lean

@@ -178,13 +178,24 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
-            let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
-            if (← Simp.isSimproc declName) then
-              simprocs := simprocs.erase declName
-            else if ctx.config.autoUnfold then
-              thms := thms.eraseCore (.decl declName)
+            let id := arg[1]
+            let declNames? ← try pure (some (← resolveGlobalConst id)) catch _ => pure none
+            if let some declNames := declNames? then
+              let declName ← ensureNonAmbiguous id declNames
+              if (← Simp.isSimproc declName) then
+                simprocs := simprocs.erase declName
+              else if ctx.config.autoUnfold then
+                thms := thms.eraseCore (.decl declName)
+              else
+                thms ← thms.erase (.decl declName)
             else
-              thms ← thms.erase (.decl declName)
+              -- If `id` could not be resolved, we should check whether it is a builtin simproc.
+              -- before returning error.
+              let name := id.getId.eraseMacroScopes
+              if (← Simp.isBuiltinSimproc name) then
+                simprocs := simprocs.erase name
+              else
+                throwUnknownConstant name
         else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
           let post :=
             if arg[0].isNone then

src/Lean/ResolveName.lean

@@ -285,6 +285,17 @@ def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m
       return pre
   | stx => throwErrorAt stx s!"expected identifier"
 
+/--
+Given a list of names produced by `resolveGlobalConst`, throw an error if the list does not contain
+exactly one element.
+Recall that `resolveGlobalConst` does not return empty lists.
+-/
+def ensureNonAmbiguous [Monad m] [MonadError m] (id : Syntax) (cs : List Name) : m Name := do
+  match cs with
+  | []  => unreachable!
+  | [c] => pure c
+  | _   => throwErrorAt id s!"ambiguous identifier '{id}', possible interpretations: {cs.map mkConst}"
+
 /-- Interpret the syntax `n` as an identifier for a global constant, and return a resolved
 constant name. If there are multiple possible interpretations it will throw.
 
@@ -305,10 +316,7 @@ After `open Foo open Boo`, we have
 - `resolveGlobalConstNoOverload x.z.w` => error: unknown constant
 -/
 def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do
-  let cs ← resolveGlobalConst id
-  match cs with
-  | [c] => pure c
-  | _   => throwErrorAt id s!"ambiguous identifier '{id}', possible interpretations: {cs.map mkConst}"
+  ensureNonAmbiguous id (← resolveGlobalConst id)
 
 def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) : m Name := do
   if n₀.hasMacroScopes then return n₀

tests/lean/run/simproc_disable_issue.lean

@@ -0,0 +1,14 @@
+example : 2^64 = 0+x := by
+  simp [-Nat.reducePow]
+  guard_target =ₛ 2^64 = x
+  sorry
+
+example : 2^64 = x := by
+  fail_if_success simp only
+  guard_target =ₛ 2^64 = x
+  sorry
+
+example : 2^8 = x := by
+  simp only [Nat.reducePow]
+  guard_target =ₛ256 = x
+  sorry