Qq strange behaviours

Stream: lean4

[Kenny Lau]

Another strange behaviour with Qq:

import Lean
import Qq

open Qq Lean Meta

def foo : MetaM Unit := do
  let α : Q(Type) ← mkFreshExprMVarQ q(Type) .natural `α
  let s ← mkFreshExprMVarQ q(Setoid $α) .natural `s
  let s' : Q(Setoid $α) := s
  return ()

[Kenny Lau]

If you delete : Q(Type) from Line 7, you get an error "cannot quote level mvar ?u.144", despite the fact that if you place your cursor before let in Line 9, the expected type window doesn't change

[Kenny Lau]

Expected type:

α : Q(Type)
s : Q(Setoid «$α»)
⊢ MetaM Unit

[Kenny Lau]

i.e. Lean already knows that α has type Q(Type), even though Lean claims to not know it afte I delete : Q(Type)

[Aaron Liu]

Probably something is forgetting to instantiate mvars

[Kenny Lau]

import Lean
import Qq

open Qq Lean Elab Meta Tactic

def foo (a : Option Unit) (e : Expr) : TacticM Unit := do
  let ⟨0, ~q(($x : Nat) = $y), e⟩ ← inferTypeQ e | return ()
  match a with
  | .none => return ()
  | .some _ => return ()

[Kenny Lau]

so after the let apparently Lean creates a metavariable in match_eq✝' : $x✝¹ =Q («$x» = «$y»)

[Kenny Lau]

if I click into it, I see that the metavariable is the level of the defeq

[Kenny Lau]

but the level is clearly 0 because these are props

[Kenny Lau]

and then because of this metavariable, Lean complains when I match on something irrelevant later

[Kenny Lau]

anyone knows about this?

[Eric Wieser]

(generalizing := false) on the match is the workaround