`withSynthesize` tries to solve unrelated universe constraints

[Rob23oba]

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 c47a0c7

Impact

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

[Rob23oba]

Hmm seems like this is actually more complicated; my "naive" fix fails at:

structure Function.Embedding (α : Sort u) (β : Sort v) where
  toFun : α → β
  inj : toFun.Injective

notation x " ↪ " y => Function.Embedding x y

variable {ι : Type u} (β : ι → Type v) in

theorem min_injective [I : Nonempty ι] : ∃ i, Nonempty (∀ j, β i ↪ β j) := sorry

theorem total (α : Type u) (β : Type v) : Nonempty (α ↪ β) ∨ Nonempty (β ↪ α) :=
  match @min_injective Bool (fun b => cond b (ULift α) (ULift.{max u v, v} β)) ⟨true⟩
    with
  | ⟨true, ⟨h⟩⟩ =>
    let ⟨f, hf⟩ := h false
    Or.inl sorry
  | ⟨false, ⟨h⟩⟩ =>
    let ⟨f, hf⟩ := h true
    Or.inr sorry