`theorem_wanted` and universe levels

[riccardobrasca]

It seems that theorem_wanted have problems with universes sometimes. Here are various examples, with different errors.

import Batteries.Util.ProofWanted

set_option autoImplicit false

section

universe v

theorem_wanted foo (a : Type v) : a = a

end

def_wanted bar : Nat :=
  have _ := ❰foo❱ Nat
  0
-- error: unknown universe level `v`

import Batteries.Util.ProofWanted

universe v

theorem_wanted foo (a : Type v) : a = a

def_wanted bar : Nat :=
  have _ := ❰foo❱ Nat
  0
-- error: Application type mismatch: The argument Nat has type Type ...
-- but is expected to have type Type v

import Batteries.Util.ProofWanted

set_option autoImplicit true

theorem_wanted foo (a : Type v) : a = a

def_wanted bar : Nat :=
have _ := ❰foo❱ Nat   -- Application type mismatch: Type vs Type v
0

import Mathlib.Tactic.TypeStar
import Batteries.Util.ProofWanted

set_option autoImplicit false

variable (K : Type*)        -- burns `u_1`

theorem_wanted zzfoo (K : Type*) : K = K  -- shadows the variable; gets `u_2`

set_option pp.universes true in
#check @zzfoo
-- zzfoo.{u_2} : (K : Type u_2) → ProofWanted.{0} (Eq.{u_2 + 2} K K)
-- (`u_1` is dropped entirely: the shadowed variable is unused)

def_wanted zzbar : Nat :=
  have _ := ❰zzfoo❱ K
  0
-- error (at line 1): unknown universe level `u_2`

Here is a Claude analysis.

❰…❱ leaks the referenced declaration's universe level names through the generated binder types

Summary

When ❰foo❱ desugars to a parameter binder, classifyWantedRef.mkBinderSyn deliberately
replaces the universe levels of the top-level application with holes (@foo.{_}), per the
comment in the implementation:

Each universe level is a hole _ rather than nm's own level name: a named level would
auto-bind to a fresh, distinct param of the enclosing declaration, leaving the hypothesis
monomorphic at a universe that can never match the use site

But the binder types of the generated Π-type are produced by PrettyPrinter.delab, which
prints foo's universe parameters by name (e.g. (a : Type v) → ProofWanted.Stmt (@foo.{_} @a)).
That syntax is then re-elaborated at the reference site, where the name v need not be in
scope — and whatever it resolves to there pins the hole, defeating the hole-out entirely.

Depending on scope, this is either a hard error with no usable position, or silent universe
capture.

Root cause and possible fix

In classifyWantedRef.mkBinderSyn (Batteries/Util/ProofWanted.lean): levelStxs holes out
the levels of the applied constant, but the per-binder typeSyn ← PrettyPrinter.delab decl.type
keeps info.levelParams' names in the emitted syntax.

Since the binder-type syntax is already post-processed to rename fvar names (renameInTy), the
same traversal could also replace occurrences of the referenced declaration's own level
parameters with _. The resulting level metavariables are all re-linked by the final
application ProofWanted.Stmt (@foo.{_} @a …), whose typing constraints unify each binder's
level with the corresponding hole, so consistency across binders is preserved.

(This is orthogonal to the known, documented limitation that a single ❰…❱ binder cannot be
used at two different universes — the ulift/TODO tests in BatteriesTest/theorem_wanted.lean.
Here the binder ends up at the wrong universe, or at an unbound one.)

[Chessing234]

Fixing in a PR with #1910.

[Chessing234]

PR #1914.

[Chessing234]

Same PR holes out leaked universe level names in binder delab.

[fgdorais]

Closed by #1861 and #1914