chore: have library search drop star only symbols (#3534)

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -57,9 +57,6 @@ inductive DeclMod
   | /-- the backward direction of an `iff` -/ mpr
 deriving DecidableEq, Inhabited, Ord
 
-instance : ToString DeclMod where
-  toString m := match m with | .none => "" | .mp => "mp" | .mpr => "mpr"
-
 /--
 LibrarySearch has an extension mechanism for replacing the function used
 to find candidate lemmas.
@@ -285,6 +282,26 @@ def mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr := do
   | .mp => mapForallTelescope (fun e => mkAppM ``Iff.mp #[e]) lem
   | .mpr => mapForallTelescope (fun e => mkAppM ``Iff.mpr #[e]) lem
 
+private def isVar (e : Expr) : Bool :=
+  match e with
+  | .bvar _ => true
+  | .fvar _ => true
+  | .mvar _ => true
+  | _ => false
+
+private def isNonspecific (type : Expr) : MetaM Bool := do
+  forallTelescope type fun _ tp =>
+    match tp.getAppFn with
+    | .bvar _ => pure true
+    | .fvar _ => pure true
+    | .mvar _ => pure true
+    | .const nm _ =>
+      if nm = ``Eq then
+        pure (tp.getAppArgsN 3 |>.all isVar)
+      else
+        pure false
+    | _ => pure false
+
 /--
 Tries to apply the given lemma (with symmetry modifier) to the goal,
 then tries to close subsequent goals using `solveByElim`.
@@ -294,9 +311,14 @@ otherwise the full list of subgoals is returned.
 private def librarySearchLemma (cfg : ApplyConfig) (act : List MVarId → MetaM (List MVarId))
     (allowFailure : MVarId → MetaM Bool) (cand : Candidate)  : MetaM (List MVarId) := do
   let ((goal, mctx), (name, mod)) := cand
-  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name} with {mod} ") do
+  let ppMod (mod : DeclMod) : MessageData :=
+        match mod with | .none => "" | .mp => " with mp" | .mpr => " with mpr"
+  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name}{ppMod mod} ") do
     setMCtx mctx
     let lem ← mkLibrarySearchLemma name mod
+    let lemType ← instantiateMVars (← inferType lem)
+    if ← isNonspecific lemType then
+      failure
     let newGoals ← goal.apply lem cfg
     try
       act newGoals

tests/lean/librarySearch.lean

@@ -1,5 +1,3 @@
-set_option autoImplicit true
-
 -- Enable this option for tracing:
 -- set_option trace.Tactic.stdLibrarySearch true
 -- And this option to trace all candidate lemmas before application.
@@ -41,10 +39,6 @@ example (n m k : Nat) : n ≤ m → n + k ≤ m + k := by apply?
 #guard_msgs in
 example (ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
 
--- Could be any number of results (`Int.one`, `Int.zero`, etc)
-#guard_msgs (drop info) in
-example : Int := by apply?
-
 /-- info: Try this: Nat.lt.base x -/
 #guard_msgs in
 example : x < x + 1 := exact?%
@@ -249,3 +243,9 @@ example {x : Int} (h : x ≠ 0) : 2 * x ≠ 0 := by
 #guard_msgs in
 example (_h : List.range 10000 = List.range 10000) (n m : Nat) : n + m = m + n := by
   with_reducible exact?
+
+/--
+error: apply? didn't find any relevant lemmas
+-/
+#guard_msgs in
+example {α : Sort u} (x y : α) : Eq x y := by apply?