grind fails because of universe variable name

Stream: lean4

[Floris van Doorn]

Below is an example where the name of a universe variable influences whether grind succeeds.
Shall I open this as an issue to the Lean repository?

universe u v

-- We use `ULift Nat` as our (artificial) universe polymorphic type
def z : ULift.{u} Nat := ⟨0⟩
def f : ULift.{u} Nat → ULift.{u} Nat := id

-- replacing `.{v}` by `.{u}` makes the `grind` below succeed
theorem foo : f z.{v} = z := rfl

theorem bar : f z.{u} = z := by
  -- `grind [foo.{u}]` works.
  grind [foo] -- fails

[Jovan Gerbscheid]

Wow, grind must be not instantiating the universes in foo.{u}, and if another universe happens to already be called u, then that matches with this u.

[Kim Morrison]

Thanks for the report! This is now fixed in lean#12226.

The bug was in instantiateGroundTheorem (used for theorems with no quantified parameters like your foo). It was passing thm.proof directly instead of calling getProofWithFreshMVarLevels, so ground theorems retained their original universe level params (like foo.{v}) instead of getting fresh level metavariables that could unify with the goal's universe levels.