fix: subst notation (heq ▸ h) should fail if it does't subst (#3994)

The subst notation substitues in the expected type, if present, or in
the type of the argument, if no expected type is known.

If there is an expected type it already fails if it cannot find the
equations' left hand side or right hand side. But if the expected type
is not known and the equation's lhs is not present in the second
argument's type, it will happily do a no-op-substitution.

This is inconsistent and unlikely what the user intended to do, so we
now print an error message now.

This still only looks for the lhs; search for the rhs as well seems
prudent, but I’ll leave that for a separate PR, to better diagnose the
impact on mathlib.

This triggers a small number of pointless uses of subst in mathlib, see
https://github.com/leanprover-community/mathlib4/pull/12451

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"

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

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