fix: do not rename metavariables that are already in the patternVars array

It fixes a regression introduced yesterday.

src/Lean/Elab/Match.lean

@@ -504,11 +504,11 @@ where
       modify fun s => { s with patternVars := s.patternVars.push e }
 
   processVar (e : Expr) : M Expr := do
-    if e.isMVar then
-      setMVarTag e.mvarId! (← read).userName
     if (← get).patternVars.contains e then
       return mkInaccessible e
     else
+      if e.isMVar then
+        setMVarTag e.mvarId! (← read).userName
       modify fun s => { s with patternVars := s.patternVars.push e }
       return e
 

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -1,11 +1,11 @@
 1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
 context:
-α β✝ : Type
-a✝ : α
-x : Fam2 α β✝
-β : Type
-a : β
-⊢ β
+α✝ β : Type
+a✝ : α✝
+x : Fam2 α✝ β
+α : Type
+a : α
+⊢ α
 [Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
   α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
     α : Type @ ⟨7, 13⟩-⟨7, 14⟩
@@ -25,7 +25,7 @@ a : β
     β : Type @ ⟨7, 33⟩-⟨7, 34⟩
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
   x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-  _example.match_1 (fun α β x a => β) α β x a (fun β_1 a_1 => ?m a x β_1 a_1) fun n a =>
+  _example.match_1 (fun α β x a => β) α β x a (fun α_1 a_1 => ?m a x α_1 a_1) fun n a =>
     n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
     x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
     [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
@@ -40,18 +40,18 @@ a : β
     [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
     @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
     a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
-      ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
-    ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
-      ?β : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
-    Fam2.any : Fam2 ?β ?β @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp
+    ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
+      ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
+    ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
+      ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
+    Fam2.any : Fam2 ?α ?α @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp
       [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.618]) ([mdata _inaccessible:1 ?_uniq.619]) @ ⟨9, 4⟩-⟨9, 12⟩
       @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-      ?β : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible
-        ?β : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole
-    a : ?β @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
-      a : ?β @ ⟨8, 2⟩†-⟨10, 19⟩†
-    ?m a✝ x β a : β @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
+      ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible
+        ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole
+    a : ?α @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
+      a : ?α @ ⟨8, 2⟩†-⟨10, 19⟩†
+    ?m a✝ x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
     [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
     Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
     [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩

tests/lean/syntheticHolesAsPatterns.lean.expected.out

@@ -8,20 +8,20 @@ n : Nat
 ⊢ Nat
 syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
 context:
-α β✝ : Type
-a✝ : α
-x : Fam2 α β✝
-β : Type
-a : β
-⊢ β
+α✝ β : Type
+a✝ : α✝
+x : Fam2 α✝ β
+α : Type
+a : α
+⊢ α
 syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
 context:
-α β✝ : Type
-a✝ : α
-x : Fam2 α β✝
-β : Type
-a : β
-⊢ β
+α✝ β : Type
+a✝ : α✝
+x : Fam2 α✝ β
+α : Type
+a : α
+⊢ α
 syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
 context:
 α β : Type