diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index c95f60778e..7ca0752265 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -401,6 +401,7 @@ patternVarDecls.foldlM
         assignExprMVar newMVarId (mkFVar fvarId);
         trace `Elab.match fun _ => "finalizePatternDecls: " ++ mkMVar newMVarId ++ " := " ++ mkFVar fvarId;
         decl ← getLocalDecl fvarId;
+        decl ← liftMetaM $ Meta.instantiateLocalDeclMVars decl;
         pure $ decls.push decl
       | _ => pure decls)
   #[]
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 383aa5994d..2c7ad79b3c 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -429,6 +429,16 @@ if e.hasMVar then
 else
   pure e
 
+def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl :=
+match localDecl with
+  | LocalDecl.cdecl idx id n type bi  => do
+    type ← instantiateMVars type;
+    pure $ LocalDecl.cdecl idx id n type bi
+  | LocalDecl.ldecl idx id n type val => do
+    type ← instantiateMVars type;
+    val ← instantiateMVars val;
+    pure $ LocalDecl.ldecl idx id n type val
+
 @[inline] private def liftMkBindingM {α} (x : MetavarContext.MkBindingM α) : MetaM α :=
 fun ctx s =>
   match x ctx.lctx { mctx := s.mctx, ngen := s.ngen } with