From f84fa475667cd44c9a210a26e61afaf70966fb00 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Oct 2020 11:40:18 -0700
Subject: [PATCH] fix: use `resolveGlobalConstNoOverload` at `implementedBy`
 attribute handler

---
 src/Lean/Compiler/ImplementedByAttr.lean | 1 +
 tests/lean/run/impByNameResolution.lean  | 9 +++++++++
 2 files changed, 10 insertions(+)
 create mode 100644 tests/lean/run/impByNameResolution.lean

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