fix(unfold?): improved implementation of isUserFriendly (#31608)

This PR fixes `isUserFriendly`, in `unfold?`, for two reasons:
- We should only worry about bad constants in the expression if they appear in the visible part of the expression. They should be allowed in e.g. instance implicit arguments.
- We don't want to get raw projections, because these are generally not what we want to work with.

Author: JovanGerb

Mathlib/Tactic/Widget/InteractiveUnfold.lean

@@ -47,8 +47,8 @@ are not presented in the list of suggested rewrites.
 This is implemented with `unfoldProjDefaultInst?`.
 
 Additionally, we don't want to unfold into expressions involving `match` terms or other
-constants marked as `Name.isInternalDetail`. So all such results are filtered out.
-This is implemented with `isUserFriendly`.
+constants marked as `Name.isInternalDetail`, and we don't want raw projections.
+So, all such results are filtered out. This is implemented with `isUserFriendly`.
 
 -/
 
@@ -106,13 +106,24 @@ where
       fun _ =>
         return acc
 
-/-- Determine whether `e` contains no internal names. -/
-def isUserFriendly (e : Expr) : Bool :=
-  !e.foldConsts (init := false) (fun name => (· || name.isInternalDetail))
+/-- Determine whether `e` contains no internal names or raw projections.
+We only consider the explicit parts of `e`, because it may happen that an
+instance implicit argument is marked as an internal detail, but that is not a problem. -/
+partial def isUserFriendly (e : Expr) : MetaM Bool := do
+  match e with
+  | .const name _ => return !name.isInternalDetail
+  | .proj .. => return false
+  | .app .. =>
+    e.withApp fun f args => do
+    (isUserFriendly f) <&&> do
+      let finfo ← getFunInfoNArgs f e.getAppNumArgs
+      e.getAppNumArgs.allM fun i _ =>
+        if finfo.paramInfo[i]?.all (·.isExplicit) then isUserFriendly args[i]! else return true
+  | _ => return true
 
 /-- Return the consecutive unfoldings of `e` that are user friendly. -/
-def filteredUnfolds (e : Expr) : MetaM (Array Expr) :=
-  return (← unfolds e).filter isUserFriendly
+def filteredUnfolds (e : Expr) : MetaM (Array Expr) := do
+  (← unfolds e).filterM isUserFriendly
 
 end InteractiveUnfold
 

MathlibTest/interactiveUnfold.lean

@@ -111,3 +111,20 @@ info: Unfolds for fun x => id x:
 -/
 #guard_msgs in
 #unfold? fun x => id x
+
+-- We don't want to get the suggestion `inst✝.toMulOneClass.toMul.1 a a` because it isn't useful:
+variable {α : Type} [Group α] (a : α) in
+/-- info: No unfolds found for a * a -/
+#guard_msgs in
+#unfold? a * a
+
+-- The proof `aux._proof_1` is an implementation detail. It should not be a problem if
+-- that appears in the expression, as long as it appears inside an implicit argument.
+def aux {α : Type} [Semiring α] := (3 : α)
+/--
+info: Unfolds for 3 + 3:
+· Nat.add 3 3
+· 6
+-/
+#guard_msgs in
+#unfold? 3 + @OfNat.ofNat _ _ (@instOfNatAtLeastTwo Nat (nat_lit 3) inferInstance aux._proof_1)