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

---
 src/Lean/Compiler/InitAttr.lean | 1 +
 tests/compiler/init.lean        | 5 +++++
 2 files changed, 6 insertions(+)

diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
index c19ae21b86..4afd5cb05b 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -26,6 +26,7 @@ registerParametricAttribute `init "initialization procedure for global reference
   decl ← getConstInfo declName;
   match attrParamSyntaxToIdentifier stx with
   | some initFnName => do
+    initFnName ← resolveGlobalConstNoOverload initFnName;
     initDecl ← getConstInfo initFnName;
     match getIOTypeArg initDecl.type with
     | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO <type>`")
diff --git a/tests/compiler/init.lean b/tests/compiler/init.lean
index af07656556..66bc172bee 100644
--- a/tests/compiler/init.lean
+++ b/tests/compiler/init.lean
@@ -1,5 +1,7 @@
 new_frontend
 
+namespace Foo
+
 initialize ref : IO.Ref Nat ← IO.mkRef 10
 
 initialize vals : IO.Ref (Array String) ← IO.mkRef #[]
@@ -20,6 +22,9 @@ initialize
 initialize
   registerVal "foo"
 
+end Foo
+open Foo
+
 def main : IO Unit := do
 IO.println "hello world"
 IO.println (← ref.get)