invalid match-expression, type of pattern variable 'match_eq✝' contains metavariables

[eric-wieser]

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.

[eric-wieser]

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.

[eric-wieser]

(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)

[eric-wieser]

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.