From d059d28c220247d51310c4ea437807c3446d36d7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Aug 2020 17:32:11 -0700
Subject: [PATCH] fix: anonymous constructor elaborator

---
 src/Lean/Elab/BuiltinNotation.lean | 1 +
 tests/lean/match4.lean             | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 6aad291695..d3b2454153 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -42,6 +42,7 @@ fun stx expectedType? => match_syntax stx with
   | some expectedType => do
     expectedType ← instantiateMVars expectedType;
     let expectedType := expectedType.consumeMData;
+    expectedType ← whnf expectedType;
     match expectedType.getAppFn with
     | Expr.const constName _ _ => do
       env ← getEnv;
diff --git a/tests/lean/match4.lean b/tests/lean/match4.lean
index ed7b88458b..8ce3060fb9 100644
--- a/tests/lean/match4.lean
+++ b/tests/lean/match4.lean
@@ -46,7 +46,7 @@ match x with
 def Vector (α : Type) (n : Nat) := { a : Array α // a.size = n }
 
 def mkVec {α : Type} (n : Nat) (a : α) : Vector α n :=
-Subtype.mk (mkArray n a) rfl
+⟨mkArray n a, rfl⟩
 
 structure S :=
 (n : Nat)