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)