fix: tryPostponeIfMVar

Must not postpone if there is a term `t` (which is not a metavariable)
assigned to the metavariable `e.getAppFn`.

src/Lean/Elab/Term.lean

@@ -752,7 +752,9 @@ when ctx.mayPostpone $ throw Exception.postpone
 
 /-- If `mayPostpone == true` and `e`'s head is a metavariable, throw `Exception.postpone`. -/
 def tryPostponeIfMVar (e : Expr) : TermElabM Unit := do
-when e.getAppFn.isMVar $ tryPostpone
+when e.getAppFn.isMVar do
+  e ← instantiateMVars e;
+  when e.getAppFn.isMVar $ tryPostpone
 
 def tryPostponeIfNoneOrMVar (e? : Option Expr) : TermElabM Unit :=
 match e? with

tests/lean/match3.lean

@@ -48,3 +48,9 @@ def head {α} (xs : List α) (h : xs = [] → False) : α :=
 match he:xs with
 | []   => False.elim $ h he
 | x::_ => x
+
+variables {α : Type u} {p : α → Prop}
+
+theorem ex8 {a1 a2 : {x // p x}} (h : a1.val = a2.val) : a1 = a2 :=
+match a1, a2, h with
+| ⟨_, _⟩, ⟨_, _⟩, rfl => rfl