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 leanprover/lean4#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:

quote4/Qq/Match.lean

Lines 208 to 212 in ccba5d3

	let argLvlExpr ← mkFreshExprMVarQ q(Level)
	let argTyExpr ← mkFreshExprMVarQ q(Quoted (.sort $argLvlExpr))
	let e' ← elabTermEnsuringTypeQ e q(Quoted $argTyExpr)
	let argTyExpr ← instantiateMVarsQ argTyExpr

but this doesn't seem to make any difference.