`withSynthesize` tries to solve unrelated universe constraints

Prerequisites

• 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

When there are existing postponed universe constraints before running withSynthesize, withSynthesize k (postpone := .no) will attempt to solve them and throw if it failed to solve them. This means that when there is a not yet solvable universe constraint, withSynthesize k will fail, no matter what action k is (even a no-op)!

Context

That nasty problem when using String pattern functions with a (·.someCharFunction) pattern and somewhere after a match. This was originally discussed at #general > deprecated_module @ 💬 but someone independently reported this issue on Discord, causing me to look deeper into the root cause.

Steps to Reproduce

set_option pp.mvars false

/--
error: stuck at solving universe constraint
  1 =?= imax _ _
while trying to unify
  (x : ?_) → ?_ x : Sort (imax _ _)
with
  (x : ?_) → ?_ x : Sort (imax _ _)
-/
#guard_msgs in
example (s : String) (x : Nat) : String :=
  let := s.all (·.isAlphanum) -- creates a universe constraint `1 =?= imax _ _`
  match x with
  | _ => s -- runs withSynthesize for elaborating `_` and thus tries to solve `1 =?= imax _ _` (oh no!)

Expected behavior:
Elaborating _ doesn't produce any new universe constraints, so withSynthesize shouldn't try to solve any and just succeed.

Actual behavior:
withSynthesize tries to solve all universe constraints and fails, giving an error to the user.

Versions

Lean 4.31.0, commit c47a0c7cf035381a2bcdd4cdf2442782eb4a5214

Impact

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

Start with the supplied minimal Lean reproducer and the withSynthesize entry point. Reproduce the existing postponed universe constraint, then inspect how withSynthesize k (postpone := .no) handles constraints created before and during k. Done means the example succeeds when elaborating _ creates no new universe constraints, while newly created constraints retain their expected behavior.