omega fails to synthesize metavariables in the right order with structure arguments

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

• Link to live.lean-lang.org

Consider the following MWE:

def Nat' (_n : Nat) : Type := Unit

structure S where
  n : Nat
  foo : Nat' n
  hn : 0 < n

def nonzeroNat' (n : Nat) : Nat' (n + 1) := ()

def s : S where
  foo := nonzeroNat' 0
  hn := by
    -- ⊢ 0 < 0 + 1
    fail_if_success omega
    sorry

def sWorks : S where
  n := 1
  foo := nonzeroNat' 0
  hn := by omega -- We seem to be missing a call to synthesizeMVar

Essentially, have lean infer the field S.n seems to trip the omega preprocessor, where it does not notice that ?n has already been unified to 0+1. I guess we're missing a call to synthesizeMVarNoPostponing or such somewhere in the preprocessor. Happy to take a look later in the day :)

Context

Discovered when verifying an implementation of a Simplex tableau with @superty

Versions

Lean 4.15.0-nightly-2024-11-28
Target: x86_64-unknown-linux-gnu

Impact

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

Start with the linked live.lean.org minimal example and compare the failing structure definition with sWorks, focusing on omega's preprocessing and metavariable synthesis. Investigate the suggested synthesizeMVar or synthesizeMVarNoPostponing path; done means the inferred S.n case succeeds and has a regression test covering the MWE.