apply? nonsense with universes

Stream: lean4

[Nir Paz]

For some reason it never occured to me to ask about this, but exact? and apply? basically always ignore universe constraints. Is this expected?

import Mathlib

universe u v

example (α : Type v) : Small.{u} α := by
  apply? -- Try this: exact small_lift α

An error message is displayed in the infoview, but this seems to stop the search right away, for example in

import Mathlib

universe u v

example (α : Type v) (β : Type*) (f : α → β) (hf : Function.Injective f) [Small.{u} β] :
    Small.{u} α := by
  apply? -- Try this: exact small_lift α

apply? immediately suggests the incorrect small_lift and misses the correct small_of_injective hf.

[Daniel Weber]

This might be related to lean4#2297, as even for Small.{v} α it doesn't work

[Kim Morrison]

For reference, the error message here is

stuck at solving universe constraint
  max (max v ?u.65919) ?u.65974 =?= u
while trying to unify
  Small.{max (max v ?u.65974) ?u.65919, v} α : Prop
with
  Small.{u, v} α : Prop

[Kim Morrison]

If someone could come up with a Mathlib-free minimization of this, I'd like to take a look. apply? should definitely be able to proceed past a universe unification error for one lemma.