Can't use omega as a simp discharger

[fpfu]

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

Context

Steps to Reproduce

--import Mathlib.Tactic.Linarith

variable {x y: Nat} {p: Nat → Nat → Prop}
theorem Foo (h: ¬ y < x): p x y := sorry

set_option trace.Meta.Tactic.simp.discharge true
  example (h:   x < y): p x y := by simp (discharger:= omega     ) only [Foo] -- [Meta.Tactic.simp.discharge] @Foo discharge ❌ ¬y < x
  example (h:  ¬y < x): p x y := by simp (discharger:= assumption) only [Foo] -- [Meta.Tactic.simp.discharge] @Foo discharge ✅ ¬y < x
--example (h:   x < y): p x y := by simp (discharger:= linarith  ) only [Foo] -- also works

Expected behavior: omega can be used as discharger

Actual behavior: omega fails to discharge ¬y < x target

Versions

4.7.0-rc2

Additional Information

Impact

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

[kim-em]

It appears that omega is not even being called here: not even the first analyzing n hypotheses: trace message from omega gets printed:

import Mathlib.Tactic.Linarith

variable {x y: Nat} {p: Nat → Nat → Prop}
theorem Foo (h: ¬ y < x): p x y := sorry

set_option trace.omega true 
set_option trace.linarith true
set_option trace.Meta.Tactic.simp.discharge true

example (h:   x < y): p x y := by apply Foo; omega 
example (h:   x < y): p x y := by simp (discharger:= omega     ) only [Foo] -- [Meta.Tactic.simp.discharge] @Foo discharge ❌ ¬y < x
example (h:  ¬y < x): p x y := by simp (discharger:= assumption) only [Foo] -- [Meta.Tactic.simp.discharge] @Foo discharge ✅ ¬y < x
example (h:   x < y): p x y := by simp (discharger:= linarith  ) only [Foo] -- also works

[fpfu]

I assume that the log from the user's discharger is simply discarded

[kim-em]

Possibly, I haven't had a chance to look at the code yet. Notice that the log from linarith is not discarded, however. It's possible that logs only from failed dischargers are discarded, but it seems unlikely.