fix: use resolveGlobalConstNoOverload at implementedBy attribute handler

src/Lean/Compiler/ImplementedByAttr.lean

@@ -14,6 +14,7 @@ registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) f
   decl ← getConstInfo declName;
   match attrParamSyntaxToIdentifier stx with
   | some fnName => do
+    fnName ← resolveGlobalConstNoOverload fnName;
     fnDecl ← getConstInfo fnName;
     if decl.type == fnDecl.type then pure fnName
     else throwError ("invalid function '" ++ fnName ++ "' type mismatch")

tests/lean/run/impByNameResolution.lean

@@ -0,0 +1,9 @@
+new_frontend
+
+namespace Foo
+
+def f (x : Nat) : Nat := x + 1
+
+@[implementedBy f] constant g : Nat → Nat
+
+end Foo