diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 43b5c9f09e..8be94e99eb 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -742,7 +742,10 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
     let motiveBody ← kabstract motive discr
     /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
     let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
-    return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
+    let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
+    unless (← isTypeCorrect motive) do
+      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
+    return motive
 
 /-- If the eliminator is over-applied, we "revert" the extra arguments. -/
 def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=
diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean
index 1b1352bd97..da254e3a58 100644
--- a/tests/lean/elabAsElim.lean
+++ b/tests/lean/elabAsElim.lean
@@ -87,3 +87,12 @@ noncomputable def f : Nat → Nat :=
 
 example : ∀ x, x ≥ 0 :=
   Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
+
+@[elab_as_elim]
+def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
+
+example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct
+
+example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct
+
+example {n : Type} : {T : n} → T = T := @(Foo.induction n)
diff --git a/tests/lean/elabAsElim.lean.expected.out b/tests/lean/elabAsElim.lean.expected.out
index 6df215ff45..07450ee119 100644
--- a/tests/lean/elabAsElim.lean.expected.out
+++ b/tests/lean/elabAsElim.lean.expected.out
@@ -1,3 +1,8 @@
 elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type:
   Nat
 elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a]
+elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry'
+elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T = T
+elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T✝ = T✝