diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index d551ce2c0f..e7ca64f106 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -498,6 +498,21 @@ def isCurrVarInductive (p : Problem) : MetaM Bool := do
     let val? ← getInductiveVal? x
     pure val?.isSome
 
+private def checkNextPatternTypes (p : Problem) : MetaM Unit := do
+  match p.vars with
+  | []   => return ()
+  | x::_ => withGoalOf p do
+    for alt in p.alts do
+      withRef alt.ref do
+        match alt.patterns with
+        | []   => pure ()
+        | p::_ =>
+          let e ← p.toExpr
+          let xType ← inferType x
+          let eType ← inferType e
+          unless (← isDefEq xType eType) do
+            throwError! "pattern{indentExpr e}\n{← mkHasTypeButIsExpectedMsg eType xType}"
+
 private partial def process (p : Problem) : StateRefT State MetaM Unit := withIncRecDepth do
   traceState p
   let isInductive ← liftM $ isCurrVarInductive p
@@ -528,7 +543,8 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := withIn
     let ps ← processArrayLit p
     ps.forM process
   else
-    liftM $ throwNonSupported p
+    checkNextPatternTypes p
+    throwNonSupported p
 
 private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (Option Nat) :=
   if uElim == levelZero then
diff --git a/tests/lean/typeIncorrectPat.lean b/tests/lean/typeIncorrectPat.lean
new file mode 100644
index 0000000000..d5cd7cdba5
--- /dev/null
+++ b/tests/lean/typeIncorrectPat.lean
@@ -0,0 +1,3 @@
+def f : (α : Type) × α → Nat
+ | ⟨_, true⟩ => 1
+ | _ => 2
diff --git a/tests/lean/typeIncorrectPat.lean.expected.out b/tests/lean/typeIncorrectPat.lean.expected.out
new file mode 100644
index 0000000000..09bae8a93e
--- /dev/null
+++ b/tests/lean/typeIncorrectPat.lean.expected.out
@@ -0,0 +1,6 @@
+typeIncorrectPat.lean:2:1: error: pattern
+  true
+has type
+  Bool
+but is expected to have type
+  fst✝