fix: instantiate metavariables in alternative local decls

src/Lean/Elab/Match.lean

@@ -401,7 +401,6 @@ 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)
   #[]

src/Lean/Meta/EqnCompiler/DepElim.lean

@@ -89,7 +89,7 @@ instance : Inhabited Alt := ⟨⟨0, arbitrary _, [], []⟩⟩
 
 partial def toMessageData (alt : Alt) : MetaM MessageData := do
 withExistingLocalDecls alt.fvarDecls do
-  let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")";
+  let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")" ++ toString d.type ++ ",ctorName:" ++ d.type.ctorName;
   let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs;
   addContext msg
 
@@ -211,7 +211,8 @@ private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt
   withLocalDecl minorName minorType BinderInfo.default fun minor => do
     let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs;
     let minors := minors.push minor;
-    let alts   := { idx := idx, rhs := rhs, fvarDecls := lhs.fvarDecls, patterns := lhs.patterns : Alt } :: alts;
+    fvarDecls ← lhs.fvarDecls.mapM instantiateLocalDeclMVars;
+    let alts   := { idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns : Alt } :: alts;
     withAltsAux lhss alts minors k
 
 /- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/

tests/lean/match2.lean

@@ -44,3 +44,28 @@ match b, x with
 
 #eval h3 Foo.bar
 #eval h3 Foo.baz
+
+#print "---- Op 2"
+
+def h4 (x : List Node) : Bool :=
+match x with
+| _ :: ⟨1, 1, Op.mk 1⟩ :: _  => true
+| _                          => false
+
+#eval h4 [mkNode 1, mkNode 0, mkNode 3]
+#eval h4 [mkNode 1, mkNode 1, mkNode 3]
+#eval h4 [mkNode 0]
+#eval h4 []
+
+#print "---- Foo 3"
+set_option pp.all true
+
+def h5 {b : Bool} (x : Foo b) : Bool :=
+match b, x with
+| _, Foo.bar => true
+| c, y       => false
+
+def h6 {b : Bool} (x : Foo b) : Bool :=
+match b, x with
+| _, Foo.bar => true
+| b, x       => false

tests/lean/match2.lean.expected.out

@@ -9,3 +9,9 @@ false
 ---- Foo 2
 true
 false
+---- Op 2
+false
+true
+false
+false
+---- Foo 3