fix(Tactic/Recall): allow different universe variable names (leanprover-community#37145)

Fixes leanprover-community#37144

This PR fixes `recall` failing when the recalled declaration uses a different universe variable name (or `Type*`) compared to the original declaration.

The type-only branch of `recall` compared `info.type` directly against the elaborated type without first instantiating the original declaration's level parameters with fresh level metavariables. The value branch already did this correctly.

🤖 Prepared with Claude Code

Author: kim-em

Mathlib/Tactic/Recall.lean

@@ -88,7 +88,10 @@ elab_rules : command
               Term.synthesizeSyntheticMVarsNoPostponing
               let type ← mkForallFVars xs type
               let type ← mkForallFVars vars type (usedOnly := true)
-              unless (← isDefEq info.type type) do
+              let infoType ← do
+                let mvs ← info.levelParams.mapM fun _ => mkFreshLevelMVar
+                pure <| info.type.instantiateLevelParams info.levelParams mvs
+              unless (← isDefEq infoType type) do
                 throwTypeMismatchError none info.type type declConst
       else
         unless binders.getNumArgs == 0 do

MathlibTest/Recall.lean

@@ -100,3 +100,15 @@ recall Nat.add_comm (n m : Nat) : n + m = m + n
 -- Test that the unused variable linter does not fire on `recall`.
 #guard_msgs in
 recall Eq.symm {α : Sort _} {a b : α} (h : a = b) : b = a
+
+-- Test that `recall` works with different universe variable names (issue #37144).
+universe u v
+class RecallUnivTest (R : Type u) : Prop where
+  test : True
+
+set_option linter.unusedVariables false in
+recall RecallUnivTest (R : Type v) : Prop
+
+-- Test that `recall` works with `Type*`.
+set_option linter.unusedVariables false in
+recall RecallUnivTest (R : Type*) : Prop