feat(Tactic/ToFun): warn if the provided name matches the autogenerated one

Author: grunweg

Mathlib/Tactic/ToFun.lean

@@ -47,9 +47,10 @@ def toFunImpl (src : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Name :=
   if (kind != AttributeKind.global) then
     throwError "`to_fun` can only be used as a global attribute"
   let name := match id with
-    | some name =>
-      (src.splitAt name.getId.getNumParts).1 ++ name.getId
+    | some name => (src.splitAt name.getId.getNumParts).1 ++ name.getId
     | none => src.appendBefore "fun_"
+  if id.isSome && name == src.appendBefore "fun_" then
+    logWarningAt tk "the autogenerated name `name` matches the one provided"
   MetaM.run' <| addRelatedDecl src name tk optAttr
     (docstringPrefix? := s!"Eta-expanded form of `{src}`") (hoverInfo := true)
     fun value levels => do

MathlibTest/ToFun.lean

@@ -1,12 +1,18 @@
+
+
 import Mathlib.Tactic.ToFun
 import Mathlib.Analysis.Normed.Ring.Basic
 
 set_option pp.unicode.fun true
 
-variable {R : Type*}
+/-- warning: the autogenerated name `name` matches the one provided -/
+#guard_msgs in
+@[to_fun fun_id_eq']
+lemma id_eq' {R : Type*} : (@id R) = id := id_eq _
 
 @[to_fun baz]
 lemma Foo.bar (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
+
 /-- info: Foo.baz (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
 #guard_msgs in #check Foo.baz
 
@@ -52,6 +58,11 @@ theorem Function.mul_comm (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm
 #guard_msgs in
 #check Function.fun_mul_comm
 
+/-- warning: the autogenerated name `name` matches the one provided -/
+#guard_msgs in
+@[to_fun fun_bar]
+theorem bar (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm f g
+
 /-- Look I am the doc-string of `foo`. -/
 @[to_fun]
 theorem foo : (1 : Nat → Nat) = 1 := rfl