From e32ebc62c0efab20d03d3bc23ce48edbee09fd51 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Aug 2020 14:34:31 -0700
Subject: [PATCH] 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 | 4 +++-
 tests/lean/match3.lean  | 6 ++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 47f2e9b68e..128675951c 100644
--- a/src/Lean/Elab/Term.lean
+++ b/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
diff --git a/tests/lean/match3.lean b/tests/lean/match3.lean
index e503022776..5c861c8d17 100644
--- a/tests/lean/match3.lean
+++ b/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