generalize not failing when match fails

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

I am trying to write a tactic that generalizes patterns in a program. My tactic calls generalize_or_fail in repeat until all occurrences of the pattern are generalized. I cannot just use generalize as it does not fail, but just keeps creating meta-variables in case the match pattern cannot be found. I managed to create a workaround, as shown below. However, this workaround is also
not working for us as conv seems to solve goals by reflection, as visible in test_solved_but_should_not. In this specific case, this leads to generalize failing, which I can work around with try. While this resolves the error it leads to a solved goal state
while I just wanted to generalize. In our framework, I would much prefer if our tactic does not start solving the goal.

local macro "generalize_or_fail" : tactic =>
  `(tactic|
   (
       conv in ((_ : ℕ) + (_ : ℕ)) => skip
       generalize h : ((_ : ℕ) + (_ : ℕ)) = c
    )
  )

def test_succeed (a b c : ℕ): a + b + c = c + (a + b) := by
  generalize_or_fail
  -- a b c c✝ : ℕ
  -- h✝ : a + b + c = c✝
  -- ⊢ c✝ = c + (a + b)
  sorry

def test_fail (a b c : ℕ): a * b * c = c * (a * b) := by
  generalize_or_fail
  -- 'pattern' conv tactic failed, pattern was not found
  -- fun x_0 x_1 => x_0 + x_1
  sorry

def test_solved_but_should_not (a b c : ℕ): a + b = a + b := by
  generalize_or_fail
  -- no goals to be solved

Steps to Reproduce

Run the code above.

Expected behavior:

• generalize should fail if it cannot match a pattern
  or
• conv should not simplify by refl

Actual behavior:

• generalize introduces a new meta-variable even if no pattern is found
• conv simplifies by reflection

Versions

"4.7.0"

Start by running the minimal reproducer from the issue and inspect the behavior of the generalize, conv, and generalize_or_fail tactics. The fix should make generalization fail when no pattern matches, or prevent conv from solving the goal by reflection, without introducing unintended metavariables or ending with no goals.