apply_rules with discharger

[hrmacbeth]

Using apply_rules with a discharger is a cheap way to write a nontrivial tactic. This worked before #3480 but now seems to be broken:

import Mathlib.Tactic.Positivity
import Mathlib.Tactic.SolveByElim

open Lean Mathlib

def PositivityDischarge (g : MVarId) : MetaM (Option (List MVarId)) :=
do Meta.Positivity.positivity g; pure (some []) <|> pure none

-- works
example (x : ℤ) : 0 ≤ x ^ 2 := by
  solve_by_elim (config := { discharge := PositivityDischarge })

-- fails
example (x : ℤ) : 0 ≤ x ^ 2 := by
  solve_by_elim (config := { discharge := PositivityDischarge, backtracking := false })

-- fails
example (x : ℤ) : 0 ≤ x ^ 2 := by
  apply_rules (config := { discharge := PositivityDischarge })

See Zulip