diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 6edf9ad042..3bde3e64da 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -409,6 +409,8 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
          let h ← elabTerm hStx none
          let hType ← inferType h
          let hTypeAbst ← kabstract hType lhs
+         unless hTypeAbst.hasLooseBVars do
+           throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut its left hand side is not mentioned in the type{indentExpr hType}"
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"
diff --git a/tests/lean/substFails.lean b/tests/lean/substFails.lean
new file mode 100644
index 0000000000..612cd7acd5
--- /dev/null
+++ b/tests/lean/substFails.lean
@@ -0,0 +1,16 @@
+def foo := 3
+def bar := 4
+
+def ex1  (heq : foo = bar) (P : Nat → Prop) (h : P foo)         := heq ▸ h
+def ex2  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h -- error
+def ex3  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
+def ex4  (heq : foo = bar) (P : Nat → Prop) (h : P 3)           := heq ▸ h -- error
+def ex5  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P 4   := heq ▸ h -- error
+def ex6  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P bar := heq ▸ h
+
+def ex7  (heq : bar = foo) (P : Nat → Prop) (h : P foo)         := heq ▸ h -- error
+def ex8  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h -- error
+def ex9  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
+def ex10 (heq : bar = foo) (P : Nat → Prop) (h : P 3)           := heq ▸ h -- error
+def ex11 (heq : bar = foo) (P : Nat → Prop) (h : P 3)   : P 4   := heq ▸ h -- error
+def ex12 (heq : bar = foo) (P : Nat → Prop) (h : P 3)   : P bar := heq ▸ h
diff --git a/tests/lean/substFails.lean.expected.out b/tests/lean/substFails.lean.expected.out
new file mode 100644
index 0000000000..f046afa8c9
--- /dev/null
+++ b/tests/lean/substFails.lean.expected.out
@@ -0,0 +1,46 @@
+substFails.lean:5:67-5:74: error: invalid `▸` notation, expected result type of cast is 
+  P 4
+however, the equality 
+  heq
+of type 
+  foo = bar
+does not contain the expected result type on either the left or the right hand side
+substFails.lean:7:67-7:74: error: invalid `▸` notation, the equality
+  heq
+has type 
+  foo = bar
+but its left hand side is not mentioned in the type
+  P 3
+substFails.lean:8:67-8:74: error: invalid `▸` notation, expected result type of cast is 
+  P 4
+however, the equality 
+  heq
+of type 
+  foo = bar
+does not contain the expected result type on either the left or the right hand side
+substFails.lean:11:67-11:74: error: invalid `▸` notation, the equality
+  heq
+has type 
+  bar = foo
+but its left hand side is not mentioned in the type
+  P foo
+substFails.lean:12:67-12:74: error: invalid `▸` notation, expected result type of cast is 
+  P 4
+however, the equality 
+  heq
+of type 
+  bar = foo
+does not contain the expected result type on either the left or the right hand side
+substFails.lean:14:67-14:74: error: invalid `▸` notation, the equality
+  heq
+has type 
+  bar = foo
+but its left hand side is not mentioned in the type
+  P 3
+substFails.lean:15:67-15:74: error: invalid `▸` notation, expected result type of cast is 
+  P 4
+however, the equality 
+  heq
+of type 
+  bar = foo
+does not contain the expected result type on either the left or the right hand side