diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean
index 2426393286..27258d7942 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/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")
diff --git a/tests/lean/run/impByNameResolution.lean b/tests/lean/run/impByNameResolution.lean
new file mode 100644
index 0000000000..b89909c1a8
--- /dev/null
+++ b/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