diff --git a/Qq/Match.lean b/Qq/Match.lean
index 2344abb..1f02ca0 100644
--- a/Qq/Match.lean
+++ b/Qq/Match.lean
@@ -268,7 +268,7 @@ scoped elab "_qq_match" pat:term " ← " e:term " | " alt:term " in " body:term
   let argLvlExpr ← mkFreshExprMVarQ q(Level)
   let argTyExpr ← mkFreshExprMVarQ q(Quoted (.sort $argLvlExpr))
   let e' ← elabTermEnsuringTypeQ e q(Quoted $argTyExpr)
-  let argTyExpr ← instantiateMVarsQ argTyExpr
+  let ⟨argTyExpr, _⟩ ← instantiateMVarsQ argTyExpr
 
   let ((lctx, localInsts, type), s) ← (unquoteForMatch argTyExpr).run { mayPostpone := (← read).mayPostpone }
   let (pat, patVarDecls, newLevels) ← elabPat pat lctx localInsts type s.levelNames
diff --git a/Qq/MetaM.lean b/Qq/MetaM.lean
index d54018f..9857d25 100644
--- a/Qq/MetaM.lean
+++ b/Qq/MetaM.lean
@@ -27,8 +27,14 @@ def trySynthInstanceQ (α : Q(Sort u)) : MetaM (LOption Q($α)) := do
 def synthInstanceQ (α : Q(Sort u)) : MetaM Q($α) := do
   synthInstance α
 
-def instantiateMVarsQ {α : Q(Sort u)} (e : Q($α)) : MetaM Q($α) := do
-  instantiateMVars e
+/-- `Lean.instantiateMVars`, with the guarantee that the result is defeq to the original. -/
+def instantiateMVarsQ {α : Q(Sort u)} (e : Q($α)) : MetaM ((e' : Q($α)) ×' $e' =Q $e) :=
+  return ⟨← instantiateMVars e, ⟨⟩⟩
+
+set_option linter.unusedVariables false in
+/-- `Lean.instantiateLevelMVars`, with the guarantee that the result is defeq to the original. -/
+def instantiateLevelMVarsQ (u : Level) : MetaM ((u' : Level) ×' u' =QL u) :=
+  return ⟨← instantiateLevelMVars u, ⟨⟩⟩
 
 def elabTermEnsuringTypeQ (stx : Syntax) (expectedType : Q(Sort u))
     (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) :