feat: improve error message when passing local hypotheses to grind (#8891)

This PR improves the error message produced when passing (automatically
redundant) local hypotheses to `grind`.

src/Lean/Elab/Tactic/Grind.lean

@@ -91,7 +91,13 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
       else
         params := { params with ematch := (← params.ematch.eraseDecl declName) }
     | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
-      let declName ← realizeGlobalConstNoOverloadWithInfo id
+      let declName ← try
+        realizeGlobalConstNoOverloadWithInfo id
+      catch err =>
+        if (← resolveLocalName id.getId).isSome then
+          throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically"
+        else
+          throw err
       let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
       match kind with
       | .ematch .user =>

tests/lean/run/grind_local_hyps.lean

@@ -0,0 +1,40 @@
+/-! This test ensures that local declarations explicitly passed to `grind` produce an appropriate
+    error message, instead of just `unknown constant '...'`. -/
+
+-- Checks that (invalid) identifiers which are not local declarations are still elaborated as global
+-- constants.
+/-- error: Unknown constant `h` -/
+#guard_msgs in
+example : 0 = 0 := by
+  grind [h]
+
+-- Checks the same property as before, but in the presence of the modifier `=`, which should not
+-- affect how the subsequent identifier is resolved.
+/-- error: Unknown constant `h` -/
+#guard_msgs in
+example : 0 = 0 := by
+  grind [= h]
+
+-- Checks that (valid) identifiers which are not local declarations are still elaborated as global
+-- constants.
+theorem t : 0 = 0 := rfl
+example : 0 = 0 := by
+  grind [= t]
+
+-- Checks that local hypotheses do not shadow global constants.
+def P := 0 = 0
+example : 0 = 0 := by
+  have P : 0 = 0 := rfl
+  grind [P]
+
+/-- error: redundant parameter `h`, `grind` uses local hypotheses automatically -/
+#guard_msgs in
+example : 0 = 0 := by
+  have h : 1 = 1 := rfl
+  grind [h]
+
+/-- error: redundant parameter `h`, `grind` uses local hypotheses automatically -/
+#guard_msgs in
+example : 0 = 0 := by
+  have h : 1 = 1 := rfl
+  grind only [h]