fix: anonymous constructor elaborator

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;

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)