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.

[0art0]

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:

quote4/Qq/Match.lean

Line 262 in ad942fd

let argLvlExpr ← mkFreshExprMVarQ q(Level)

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.

[eric-wieser]

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.

[0art0]

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

[eric-wieser]

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.