diff --git a/library/init/io.lean b/library/init/io.lean
index f5c52c5ec9..ca0af83a54 100644
--- a/library/init/io.lean
+++ b/library/init/io.lean
@@ -45,9 +45,14 @@ id
 
 abbrev IO : Type → Type := EIO IO.Error
 
-@[inline]
-unsafe def unsafeIO {α : Type} (fn : IO α) : Option α :=
+section
+/- After we inline `EState.run'`, the closed term `((), ())` is generated, where the second `()`
+   represents the "initial world". We don't want to cache this closed term. So, we disable
+   the "extract closed terms" optimization. -/
+set_option compiler.extract_closed false
+@[inline] unsafe def unsafeIO {α : Type} (fn : IO α) : Option α :=
 fn.run' ()
+end
 
 @[extern 4 "lean_io_timeit"]
 constant timeit {α : Type} (msg : @& String) (fn : IO α) : IO α := default _
diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean
index df5b54321e..3e17751eeb 100644
--- a/library/init/lean/environment.lean
+++ b/library/init/lean/environment.lean
@@ -309,6 +309,11 @@ def CPPExtensionState := NonScalar
 
 instance CPPExtensionState.inhabited : Inhabited CPPExtensionState := inferInstanceAs (Inhabited NonScalar)
 
+section
+/- It is not safe to use "extract closed term" optimization in the following code because of `unsafeIO`.
+   If `compiler.extract_closed` is set to true, then the compiler will cache the result of
+   `exts ← envExtensionsRef.get` during initialization which is incorrect. -/
+set_option compiler.extract_closed false
 @[export lean.register_extension_core]
 unsafe def registerCPPExtension (initial : CPPExtensionState) : Option Nat :=
 unsafeIO (do ext ← registerEnvExtension initial; pure ext.idx)
@@ -320,6 +325,7 @@ unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).setState env s
 @[export lean.get_extension_core]
 unsafe def getCPPExtensionState (env : Environment) (idx : Nat) : Option CPPExtensionState :=
 unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).getState env)
+end
 
 /- Legacy support for Modification objects -/
 
diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index 06ea50f9eb..6e2713b09b 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -31,10 +31,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name * g_codegen = nullptr;
+static name * g_extract_closed = nullptr;
 
-bool is_codegen_enabled(options const & opts) {
-    return opts.get_bool(*g_codegen, true);
-}
+bool is_codegen_enabled(options const & opts) { return opts.get_bool(*g_codegen, true); }
+bool is_extract_closed_enabled(options const & opts) { return opts.get_bool(*g_extract_closed, true); }
 
 static name get_real_name(name const & n) {
     if (optional<name> new_n = is_unsafe_rec_name(n))
@@ -222,10 +222,12 @@ environment compile(environment const & env, options const & opts, names cs) {
     trace_compiler(name({"compiler", "simp"}), ds);
     new_env = cache_stage2(new_env, ds);
     trace_compiler(name({"compiler", "stage2"}), ds);
-    std::tie(new_env, ds) = extract_closed(new_env, ds);
-    ds = apply(elim_dead_let, ds);
-    ds = apply(esimp, new_env, ds);
-    trace_compiler(name({"compiler", "extract_closed"}), ds);
+    if (is_extract_closed_enabled(opts)) {
+        std::tie(new_env, ds) = extract_closed(new_env, ds);
+        ds = apply(elim_dead_let, ds);
+        ds = apply(esimp, new_env, ds);
+        trace_compiler(name({"compiler", "extract_closed"}), ds);
+    }
     new_env = cache_new_stage2(new_env, ds);
     ds = apply(esimp, new_env, ds);
     trace_compiler(name({"compiler", "simp"}), ds);
@@ -260,9 +262,10 @@ extern "C" object * lean_add_and_compile(object * env, object * opts, object * d
 }
 
 void initialize_compiler() {
-    g_codegen = new name("codegen");
+    g_codegen        = new name("codegen");
+    g_extract_closed = new name{"compiler", "extract_closed"};
     register_bool_option(*g_codegen, true, "(compiler) enable/disable code generation");
-
+    register_bool_option(*g_extract_closed, true, "(compiler) enable/disable closed term caching");
     register_trace_class("compiler");
     register_trace_class({"compiler", "input"});
     register_trace_class({"compiler", "eta_expand"});
@@ -302,5 +305,6 @@ void initialize_compiler() {
 
 void finalize_compiler() {
     delete g_codegen;
+    delete g_extract_closed;
 }
 }