`apply_rules` with discharger

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

Reproduce the three examples using the Mathlib.Tactic.Positivity and Mathlib.Tactic.SolveByElim imports, comparing apply_rules with solve_by_elim and backtracking enabled or disabled. Trace the apply_rules and solve_by_elim entry points and their discharge handling; done means the discharger succeeds in the apply_rules example and in the non-backtracking solve_by_elim case.