leanprover-community
invalid match-expression, type of pattern variable 'match_eq✝' contains metavariables
The following example:
import Qq
open Qq Lean.Meta
example (qo : Q(Option Nat)) (o : Option Nat) : MetaM Unit := do
match qo with
| ~q(some $qx) => match o with
| some x => pure ()
| _ => pure ()
gives the error:
invalid match-expression, type of pattern variable 'match_eq✝' contains metavariables
«$qo» =Q some «$qx»
Indeed, the type of match_eq✝ in the goal in
example (qo : Q(Option Nat)) : MetaM Unit := do
match qo with
| ~q(some $qx) => sorry
has a metavariable for the Level argument.
Replacing the inner match with match (generalizing := false) o with or match id o with is sufficient as a workaround, though of course this disables generalization.
(And with https://github.com/leanprover/lean4/pull/3060, this obviously also affects let some x := o which must be written as let some x := id o)
My initial thought was that these lines are missing a let argLvlExpr ← instantiateMVarsQ argLvlExpr:
https://github.com/leanprover-community/quote4/blob/ccba5d35d07a448fab14c0e391c8105df6e2564c/Qq/Match.lean#L208-L212
but this doesn't seem to make any difference.
I'm facing this issue too; in my case, the match was sensitive to the order of the arguments, and swapping them allowed me to work around this bug.
import Lean
import Qq
open Lean Meta Qq
def test : (P : Q(Prop)) → (args : List Nat) → MetaM String
| ~q($A ∧ $B), [] => return "and"
| _, _ => return "other"
def test' : (args : List Nat) → (P : Q(Prop)) → MetaM String
| [], ~q($A ∧ $B) => return "and"
| _, _ => return "other"
When I edit this line:
https://github.com/leanprover-community/quote4/blob/ad942fdf0b15c38bface6acbb01d63855a2519ac/Qq/Match.lean#L262
to hard-code the universe level, everything seems to work. I suspect that argLvlExpr actually needs to be a Level metavariable created by mkFreshLevelMVar, but I haven't been able to figure out how to quote such a thing into the type of argTyExpr.
mkFreshLevelMVar is not correct here; we're building a metavariable to hold an Expr corresponding to a Level, not a metavariable for a level itself.
A metavariable for a Level created that way doesn't seem to play well with unification, so I was hoping that argTyExpr could somehow be defined as
let argTyExpr ← mkFreshExprMVarQ q(Quoted (.sort (← mkFreshLevelMVar))
instead of
let argTyExpr ← mkFreshExprMVarQ q(Quoted (.sort $argLvlExpr))
(the code I've written doesn't work with the quote interpolation.)
I think the confusion here is between metavariables which are created at match time (resolved with defeq), and metavariables which are created and resolved while elaborating the ~q syntax itself. I'm pretty sure this is the former, though most likely one type of metavariable ends up instantiated with the other which makes the whole thing rather confusing.