diff --git a/tests/compiler/module.lean b/tests/compiler/module.lean
new file mode 100644
index 0000000000..a653848e33
--- /dev/null
+++ b/tests/compiler/module.lean
@@ -0,0 +1,11 @@
+module
+
+public meta import Lean
+
+/-! Binary size should be independent of `meta` import closure. -/
+
+elab "mk_str" : term =>
+  return Lean.mkStrLit "world!"
+
+public def main : IO Unit :=
+  IO.println ("Hello, " ++ mk_str)
diff --git a/tests/compiler/module.lean.expected.out b/tests/compiler/module.lean.expected.out
new file mode 100644
index 0000000000..af5626b4a1
--- /dev/null
+++ b/tests/compiler/module.lean.expected.out
@@ -0,0 +1 @@
+Hello, world!
diff --git a/tests/compiler/module.lean.meta.c b/tests/compiler/module.lean.meta.c
new file mode 100644
index 0000000000..6e3c6c6f2c
--- /dev/null
+++ b/tests/compiler/module.lean.meta.c
@@ -0,0 +1,268 @@
+// Lean compiler output
+// Module: module
+// Imports: public import Init public meta import Lean
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+static lean_object* l_termMk__str___closed__0;
+static lean_object* l_termMk__str___closed__4;
+static lean_object* l_termMk__str___closed__2;
+static lean_object* l___aux__module______elabRules__termMk__str__1___redArg___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg();
+static lean_object* l_termMk__str___closed__3;
+uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
+static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0;
+lean_object* l_Lean_mkStrLit(lean_object*);
+static lean_object* l_termMk__str___closed__1;
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_termMk__str;
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___boxed(lean_object*);
+static lean_object* l___aux__module______elabRules__termMk__str__1___redArg___closed__0;
+static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1;
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Name_mkStr1(lean_object*);
+extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId;
+static lean_object* _init_l_termMk__str___closed__0() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked("termMk_str", 10, 10);
+return x_1;
+}
+}
+static lean_object* _init_l_termMk__str___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_termMk__str___closed__0;
+x_2 = l_Lean_Name_mkStr1(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_termMk__str___closed__2() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked("mk_str", 6, 6);
+return x_1;
+}
+}
+static lean_object* _init_l_termMk__str___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_termMk__str___closed__2;
+x_2 = lean_alloc_ctor(5, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_termMk__str___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_termMk__str___closed__3;
+x_2 = lean_unsigned_to_nat(1024u);
+x_3 = l_termMk__str___closed__1;
+x_4 = lean_alloc_ctor(3, 3, 0);
+lean_ctor_set(x_4, 0, x_3);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_1);
+return x_4;
+}
+}
+static lean_object* _init_l_termMk__str() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_termMk__str___closed__4;
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_Elab_unsupportedSyntaxExceptionId;
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0;
+x_3 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg() {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1;
+x_3 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_3, 0, x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_9; 
+x_9 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg();
+return x_9;
+}
+}
+static lean_object* _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__0() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked("elab'd", 6, 6);
+return x_1;
+}
+}
+static lean_object* _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l___aux__module______elabRules__termMk__str__1___redArg___closed__0;
+x_2 = l_Lean_mkStrLit(x_1);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_9; uint8_t x_10; 
+x_9 = l_termMk__str___closed__1;
+x_10 = l_Lean_Syntax_isOfKind(x_1, x_9);
+if (x_10 == 0)
+{
+lean_object* x_11; 
+x_11 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg();
+return x_11;
+}
+else
+{
+lean_object* x_12; lean_object* x_13; 
+x_12 = l___aux__module______elabRules__termMk__str__1___redArg___closed__1;
+x_13 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_13, 0, x_12);
+return x_13;
+}
+}
+}
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+_start:
+{
+lean_object* x_10; 
+x_10 = l___aux__module______elabRules__termMk__str__1___redArg(x_1, x_3, x_4, x_5, x_6, x_7, x_8);
+return x_10;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+_start:
+{
+lean_object* x_9; 
+x_9 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_7);
+lean_dec_ref(x_6);
+lean_dec(x_5);
+lean_dec_ref(x_4);
+lean_dec(x_3);
+lean_dec_ref(x_2);
+return x_9;
+}
+}
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; 
+x_10 = l___aux__module______elabRules__termMk__str__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+lean_dec(x_8);
+lean_dec_ref(x_7);
+lean_dec(x_6);
+lean_dec_ref(x_5);
+lean_dec(x_4);
+lean_dec_ref(x_3);
+lean_dec(x_2);
+return x_10;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg();
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l___aux__module______elabRules__termMk__str__1___redArg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+_start:
+{
+lean_object* x_9; 
+x_9 = l___aux__module______elabRules__termMk__str__1___redArg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_7);
+lean_dec_ref(x_6);
+lean_dec(x_5);
+lean_dec_ref(x_4);
+lean_dec(x_3);
+lean_dec_ref(x_2);
+return x_9;
+}
+}
+lean_object* meta_initialize_Init(uint8_t builtin);
+lean_object* meta_initialize_Lean(uint8_t builtin);
+static bool _G_initialized = false;
+LEAN_EXPORT lean_object* initialize_module(uint8_t builtin) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = meta_initialize_Init(builtin);
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = meta_initialize_Lean(builtin);
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_termMk__str___closed__0 = _init_l_termMk__str___closed__0();
+lean_mark_persistent(l_termMk__str___closed__0);
+l_termMk__str___closed__1 = _init_l_termMk__str___closed__1();
+lean_mark_persistent(l_termMk__str___closed__1);
+l_termMk__str___closed__2 = _init_l_termMk__str___closed__2();
+lean_mark_persistent(l_termMk__str___closed__2);
+l_termMk__str___closed__3 = _init_l_termMk__str___closed__3();
+lean_mark_persistent(l_termMk__str___closed__3);
+l_termMk__str___closed__4 = _init_l_termMk__str___closed__4();
+lean_mark_persistent(l_termMk__str___closed__4);
+l_termMk__str = _init_l_termMk__str();
+lean_mark_persistent(l_termMk__str);
+l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0 = _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0();
+lean_mark_persistent(l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__0);
+l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1 = _init_l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1();
+lean_mark_persistent(l_Lean_Elab_throwUnsupportedSyntax___at___00__aux__module______elabRules__termMk__str__1_spec__0___redArg___closed__1);
+l___aux__module______elabRules__termMk__str__1___redArg___closed__0 = _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__0();
+lean_mark_persistent(l___aux__module______elabRules__termMk__str__1___redArg___closed__0);
+l___aux__module______elabRules__termMk__str__1___redArg___closed__1 = _init_l___aux__module______elabRules__termMk__str__1___redArg___closed__1();
+lean_mark_persistent(l___aux__module______elabRules__termMk__str__1___redArg___closed__1);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif