Interaction with `symm` attribute makes `apply?` nearly unusable

[MichaelStollBayreuth]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

If there are hypotheses in the context involving relations marked with the symm attribute, apply? does not work as expected, degrading its usefulness substantially:

• its suggestions contain expresions like (?_ (id (r.symm h₁))), which produce an error when used to replace the call to apply?, so the resulting code has to be fixed manually;
• the list of resulting subgoals contains many spurious entries (usually of the type h → g when g is already present as a subgoal);
• a side effect of the latter is that it blows up the amount of text in the infoview with the result that VSCode reacts extremely slowly to keystrokes/mouse wheel when scrolling. EDIT: This seems to have been exacerbated by a different problem that was fixed in vscode-lean#432.

Context

Since equality is a symm relation, this issue occurs whenever one tries to use apply? when there are equality hypotheses around (which is very common).

See this Zulip thread (in particular the poll there) and also this one.

Steps to Reproduce

Here is an MWE showing the effect of marking a relation symm on apply?:

-- set up a binary relation
axiom r : Nat → Nat → Prop

-- that is symmetric
theorem r.symm {a b : Nat} : r a b → r b a := sorry

-- and has some other property
theorem r.trans {a b c : Nat} : r a b → r b c → r a c := sorry

-- now try `apply?`
example (a b c : Nat) (h₁ : r b a) (h₂ : r b c) : r c a := by
  apply?
/-
Try this: refine r.trans ?_ ?_
Remaining subgoals:
⊢ Nat
⊢ r c ?b
⊢ r ?b a

Try this: refine r.symm ?_
Remaining subgoals:
⊢ r a c

which looks fine.
-/

-- now attach the `symm` attribute to `r.symm`
attribute [symm] r.symm

-- and repeat
example (a b c : Nat) (h₁ : r b a) (h₂ : r b c) : r c a := by
  -- `exact?` → `exact?` could not close the goal.
  -- I think that attaching `symm` *should* enable `exact?` to come up with
  -- `exact r.trans h₂.symm h₁` or `exact (r.trans h₁.symm h₂).symm`
  apply?
/-
Try this: refine r.trans (?_ (id (r.symm h₁))) (?_ (id (r.symm h₁)))
Remaining subgoals:
⊢ r a b → Nat
⊢ r a b → r c (?m.239 ⋯)
⊢ r a b → r (?m.239 ⋯) a
⊢ r c b → Nat
⊢ Nat
⊢ r c b → r c (?m.239 ⋯)
⊢ r c (?m.239 ⋯)
⊢ r c b → r (?m.239 ⋯) a
⊢ r (?m.239 ⋯) a

Try this: refine r.symm (r.trans (?_ (id (r.symm h₁))) (?_ (id (r.symm h₁))))
Remaining subgoals:
⊢ r a b → Nat
⊢ r a b → r a (?m.331 ⋯)
⊢ r a b → r (?m.331 ⋯) c
⊢ r c b → Nat
⊢ Nat
⊢ r c b → r a (?m.331 ⋯)
⊢ r a (?m.331 ⋯)
⊢ r c b → r (?m.331 ⋯) c
⊢ r (?m.331 ⋯) c

Try this: refine r.symm (?_ (id (r.symm h₁)))
Remaining subgoals:
⊢ r a b → r a c
⊢ r c b → r a c
⊢ r a c

Try this: refine r.symm (r.symm (?_ (id (r.symm h₁))))
Remaining subgoals:
⊢ r a b → r c a
⊢ r c b → r c a

... and clicking on any of these results in an error of the kind
  function expected at
    ?m.5099
  term has type
    ?m.5098
-/

Expected behavior:
apply? should make suggestions (including applying symmetry lemmas) that work without manual editing when clicked on (in particular, without ?_ in function positions) and give the actual list of subgoals generated.

Actual behavior:
In the presence of symm relations in the context, apply? produces suggestions involving ?_ in function positions (hence leading to an error when transferred to the code) and bloats the list of remaining subgoals with redundant statements. See here for a particulary egregious example (this is just the first suggestion shown).

Versions

4.7.0 / Linux (my laptop). 4.7.0 on https://live.lean-lang.org

Impact

This bug makes apply? almost unusable in most real-life situations, which would otherwise be a very helpful tool.
See this poll.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.