fix: improve recall impl / error reporting (leanprover-community#8740)

This PR fixes `recall` to work inside namespaces and with `open` declarations, as reported on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/recall.20doesn.27t.20work.20in.20namespaces/near/430877189).

Previously, `recall` used raw `id.getId` to extract the declaration name, which ignored the current namespace. Now it uses `resolveGlobalConstNoOverload`, the standard Lean name resolution function.

```lean
-- Previously failed with "Unknown constant 'myDef'"
namespace Foo
def myDef := 42
end Foo

namespace Foo
recall myDef : Nat  -- now works
end Foo

-- Also works with `open`
open Foo in
recall myDef : Nat
```

🤖 Prepared with Claude Code

Co-authored-by: Kim Morrison <kim@tqft.net>

Author: digama0

Mathlib/Tactic/Recall.lean

@@ -52,7 +52,7 @@ elab_rules : command
     -- `recall` doesn't introduce new definitions, so suppress the unused variable linter.
     withScope (fun sc => { sc with opts := sc.opts.set `linter.unusedVariables false }) <|
     withoutModifyingEnv do
-    let declName := id.getId
+    let declName ← resolveGlobalConstNoOverload id
     addConstInfo id declName
     let info ← getConstInfo declName
     let declConst : Expr := mkConst declName <| info.levelParams.map Level.param

MathlibTest/Recall.lean

@@ -112,3 +112,16 @@ recall RecallUnivTest (R : Type v) : Prop
 -- Test that `recall` works with `Type*`.
 set_option linter.unusedVariables false in
 recall RecallUnivTest (R : Type*) : Prop
+
+-- Test that `recall` works inside namespaces (https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/recall.20doesn.27t.20work.20in.20namespaces/near/430877189)
+namespace RecallTest
+def myDef := 42
+end RecallTest
+
+namespace RecallTest
+recall myDef : Nat
+end RecallTest
+
+-- Test that `recall` works with `open` namespaces.
+open RecallTest in
+recall myDef : Nat