chore: add warning comments about findM?

src/Lean/Meta/Injective.lean

@@ -58,6 +58,9 @@ def occursOrInType (e : Expr) (t : Expr) : MetaM Bool := do
       return s == e
     let ty ← inferType s
     return s == e || e.occurs ty
+  -- Note here that we are calling `findM?` with a non-pure function, which is dangerous!
+  -- The non-pure behaviour arises from `inferType` interacting with caches,
+  -- however `inferType` is only called on `Expr.fvar`s, which should be effectively pure.
   return (← t.findM? f).isSome
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do

src/Lean/Util/FindExpr.lean

@@ -40,8 +40,21 @@ unsafe def findUnsafeM? {m} [Monad m] (p : Expr → m Bool) (e : Expr) : m (Opti
 
 end FindImpl
 
+/--
+Find a subexpression on which the (monadic) predicate `p` returns true.
+
+In compiled code, this is replaced by a fast implementation which uses a cache.
+
+Note that if `p` is not pure (e.g. it uses a cache), then this reference implementation may not
+match the compiled behavior! In particular, the compiled implementation will not re-evaluate `p`
+on repeated subterms.
+
+Please use this function cautiously; if it becomes a source of bugs, we may remove it.
+
+(See `find?` below for a pure version.)
+-/
+
 @[implemented_by FindImpl.findUnsafeM?]
-/- This is a reference implementation for the unsafe one above -/
 def findM? [Monad m] (p : Expr → m Bool) (e : Expr) : m (Option Expr) := do
   if ← p e then
     return some e