Meta initializer uses runtime-initialized data with specialized instance

Description

Consider the following project

lakefile.toml

name = "repro"
leanOptions = { experimental.module = true }

[[lean_lib]]
name = "Repro"

Repro/Helper.lean

module

public section

class Description (α : Type) where
  pieces : List String

def describe (α : Type) [Description α] : Option String :=
  some <| (Description.pieces α).foldl (init := "") (· ++ ·)

instance : Description Unit where
  pieces := ["un", "it"]

Repro/A.lean

module

public meta import Repro.Helper

public section

meta def unitDescription : Option String :=
  describe Unit

Repro/B.lean

module

public import Repro.A

Then running

lake env $(elan which lean) ./Repro/B.lean \
  --load-dynlib=$(lake query Repro.A:dynlib) \
  --load-dynlib=$(lake query Repro.Helper:dynlib)

will result in a segfault.

The compiler puts code to initialize the generated specialization lp_repro_describe___at___00unitDescription_spec__0 in runtime_initialize_repro_Repro_A, while the meta def that reads it is initialized in meta_initialize_repro_Repro_A. With --load-dynlib, only the latter is run.

Context

Exposed by #14326.

Expected behavior: Project builds.

Actual behavior: Crash.

Versions

nightly-2026-07-10
Darwin Kernel Version 25.4.0

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the crash with lakefile.toml and the Repro/Helper.lean, Repro/A.lean, and Repro/B.lean files using the shown lake and lean command. Start by tracing the generated runtime_initialize_repro_Repro_A and meta_initialize_repro_Repro_A entry points, then verify that the project builds without a segmentation fault when using --load-dynlib.