Qq with mkFreshLevelMVar

Stream: mathlib4

[Eric Wieser]

Is there a way to make this work?

def FinEta.prove (m n : ℕ) : MetaM (Expr × Expr) :=
do
  let u ← mkFreshLevelMVar
  let α ← mkFreshExprMVarQ q(Sort $u) (userName := `α)
  sorry

It complains with "incompatible metavariable _uniq.1356"

[Thomas Murrills]

I don't fully understand why, but Levels seem to transcend (anti)quotation in Qq. That means that this no longer complains once we also include the required Qq type annotation:

def FinEta.prove (m n : ℕ) : MetaM (Expr × Expr) := do
  let u ← mkFreshLevelMVar
  let α ← mkFreshExprMVarQ (q(Sort u) : Q(Type u)) (userName := `α)
  sorry

However, since I don't understand why it works, I can't guarantee some other error won't pop up later. But at least it's a start :)

[Eric Wieser]

Indeed, duplicating my types everywhere seemed to solve the problem

[Eric Wieser]

(The code in question is FinEta.prove from #5863)

[Wojciech Nawrocki]

Note that universe levels are not dollar-quoted (issue). One can also write

def FinEta.prove (m n : ℕ) : MetaM (Expr × Expr) :=
do
  let u ← mkFreshLevelMVar
  let α ← mkFreshExprMVarQ (u := u.succ) q(Sort u) (userName := `α)
  sorry