`mkValueTypeClosure` doesn't consider 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 providing an expression with level metavariables to mkValueTypeClosure while there are postponed universe constraints on the level metavariables, mkValueTypeClosure will incorrectly abstract the level metavariables as level parameters, potentially creating ill-typed expressions. This is, among other things, relevant for match expressions which use mkValueTypeClosure to create auxiliary match declarations.

Context

Further investigation after #13875.

Steps to Reproduce

theorem min_injective {β : ι → Type v} [I : Nonempty ι] : False ∧ ∃ i, Nonempty (∀ j, β i → β j) := sorry

/--
error: (kernel) application type mismatch
  bif i then ULift α else ULift β
argument has type
  Type (max u_1 u_3)
but function has type
  Type (max u_1 u_2) → Type (max u_1 u_2)
---
error: (kernel) incorrect number of universe levels parameters for 'total.match_1_1', #0 expected, #3 provided
-/
#guard_msgs in
theorem total (α : Type u) (β : Type v) : True :=
  nomatch @min_injective Bool (fun b => cond b (ULift α) (ULift.{max u v, v} β)) ⟨true⟩

In this example, we have ULift.{?w, u} α, creating a universe constraint max ?w u =?= max u v.

Expected behavior:
Before the auxiliary matcher declaration is created, the metavariable ?w should be identified as part of the universe constraint max ?w u =?= max u v, causing it to process the constraint without postponing.

Actual behavior:
mkValueTypeClosure ignores the constraint and abstract it as ULift.{w, u}, causing a kernel type mismatch error (because ULift.{w, u} α : Sort (max w u) but ULift.{max u v, v} β : Sort (max u v) in the same cond).

Versions

Lean 4.32.0-nightly-2026-05-29

Impact

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

Start with mkValueTypeClosure and the minimal reproduction in the issue, especially the postponed constraint max ?w u =?= max u v. Run the #guard_msgs example against the stated Lean nightly version and inspect how the auxiliary matcher declaration handles universe metavariables. Done means the reproduction no longer produces the kernel type mismatch or incorrect universe-level parameter errors.