diff --git a/tests/lean/motiveNotTypeCorect.lean b/tests/lean/motiveNotTypeCorect.lean
new file mode 100644
index 0000000000..a999327af0
--- /dev/null
+++ b/tests/lean/motiveNotTypeCorect.lean
@@ -0,0 +1,8 @@
+inductive D : Nat -> Type
+def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t)
+  (d : D (f t))
+  (P : (t : Nat) -> D t -> Prop)
+  : P (f t) d
+  := by
+  rw [h] -- tactic 'rewrite' failed, motive is not type correct
+  sorry
diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorect.lean.expected.out
new file mode 100644
index 0000000000..cee57716ed
--- /dev/null
+++ b/tests/lean/motiveNotTypeCorect.lean.expected.out
@@ -0,0 +1,7 @@
+motiveNotTypeCorect.lean:7:6-7:7: error: tactic 'rewrite' failed, motive is not type correct
+t : Nat
+f : Nat → Nat
+h : f t = t
+d : D (f t)
+P : (t : Nat) → D t → Prop
+⊢ P (f t) d