From 1f732bb3b7fa8e93ca01c1b257668aee14d72d2d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 20 Jun 2024 12:06:24 +0200
Subject: [PATCH] fix: missing unboxing in interpreter when loading initialized
 value (#4512)

Fixes #4457
---
 src/library/compiler/ir_interpreter.cpp    | 2 +-
 tests/pkg/initialize/.gitignore            | 1 +
 tests/pkg/initialize/Initialize.lean       | 5 +++++
 tests/pkg/initialize/Initialize/Basic.lean | 1 +
 tests/pkg/initialize/lakefile.toml         | 5 +++++
 tests/pkg/initialize/test.sh               | 4 ++++
 6 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/pkg/initialize/.gitignore
 create mode 100644 tests/pkg/initialize/Initialize.lean
 create mode 100644 tests/pkg/initialize/Initialize/Basic.lean
 create mode 100644 tests/pkg/initialize/lakefile.toml
 create mode 100755 tests/pkg/initialize/test.sh

diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index cd88e35ba6..6f9f5370d3 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -796,7 +796,7 @@ private:
         }
         if (object * const * o = g_init_globals->find(fn)) {
             // persistent, so no `inc` needed
-            return *o;
+            return type_is_scalar(t) ? unbox_t(*o, t) : *o;
         }
 
         symbol_cache_entry e = lookup_symbol(fn);
diff --git a/tests/pkg/initialize/.gitignore b/tests/pkg/initialize/.gitignore
new file mode 100644
index 0000000000..bfb30ec8c7
--- /dev/null
+++ b/tests/pkg/initialize/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/tests/pkg/initialize/Initialize.lean b/tests/pkg/initialize/Initialize.lean
new file mode 100644
index 0000000000..e205e2493a
--- /dev/null
+++ b/tests/pkg/initialize/Initialize.lean
@@ -0,0 +1,5 @@
+import Initialize.Basic
+
+/-- info: 42 -/
+#guard_msgs in
+#eval initNat
diff --git a/tests/pkg/initialize/Initialize/Basic.lean b/tests/pkg/initialize/Initialize/Basic.lean
new file mode 100644
index 0000000000..d25d1eed68
--- /dev/null
+++ b/tests/pkg/initialize/Initialize/Basic.lean
@@ -0,0 +1 @@
+initialize initNat : Nat ← pure 42
diff --git a/tests/pkg/initialize/lakefile.toml b/tests/pkg/initialize/lakefile.toml
new file mode 100644
index 0000000000..069562dfd3
--- /dev/null
+++ b/tests/pkg/initialize/lakefile.toml
@@ -0,0 +1,5 @@
+name = "initialize"
+defaultTargets = ["Initialize"]
+
+[[lean_lib]]
+name = "Initialize"
diff --git a/tests/pkg/initialize/test.sh b/tests/pkg/initialize/test.sh
new file mode 100755
index 0000000000..b1c0671e59
--- /dev/null
+++ b/tests/pkg/initialize/test.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf .lake/build
+lake build