diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e177fd10a8f2..ad0f7b4fce82 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2660,7 +2660,8 @@ instance : Max UInt32 := maxOfLe
 instance : Min UInt32 := minOfLe
 
 /-- The number of distinct values representable by `UInt64`, that is, `2^64 = 18446744073709551616`. -/
-abbrev UInt64.size : Nat := 18446744073709551616
+@[noinline, reducible]
+def UInt64.size : Nat := 18446744073709551616
 
 /--
 Unsigned 64-bit integers.
@@ -2718,7 +2719,8 @@ instance : Inhabited UInt64 where
   default := UInt64.ofNatLT 0 (of_decide_eq_true rfl)
 
 /-- The number of distinct values representable by `USize`, that is, `2^System.Platform.numBits`. -/
-abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
+@[noinline, reducible]
+def USize.size : Nat := (hPow 2 System.Platform.numBits)
 
 theorem USize.size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
   show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
diff --git a/src/Lean/Compiler/LCNF/ExtractClosed.lean b/src/Lean/Compiler/LCNF/ExtractClosed.lean
index 26461d3df1b9..be9fc2552aa0 100644
--- a/src/Lean/Compiler/LCNF/ExtractClosed.lean
+++ b/src/Lean/Compiler/LCNF/ExtractClosed.lean
@@ -10,6 +10,7 @@ public import Lean.Compiler.ClosedTermCache
 public import Lean.Compiler.NeverExtractAttr
 public import Lean.Compiler.LCNF.Internalize
 public import Lean.Compiler.LCNF.ToExpr
+import Lean.Compiler.LCNF.PrettyPrinter
 
 public section
 
@@ -55,31 +56,55 @@ structure State where
 
 abbrev M := ReaderT Context $ StateRefT State CompilerM
 
+def extractionAllowlist : Std.HashSet Name := .ofArray #[
+  ``Lean.Name.mkStr,
+  ``Lean.Name.mkNum,
+  ``Lean.Name.mkStr1,
+  ``Lean.Name.mkStr2,
+  ``Lean.Name.mkStr3,
+  ``Lean.Name.mkStr4,
+  ``Lean.Name.mkStr5,
+  ``Lean.Name.mkStr6,
+  ``Lean.Name.mkStr7,
+  ``Lean.Name.mkStr8,
+  ``Lean.Name.str._override,
+  ``Lean.Name.num._override,
+  ``ByteArray.mk,
+]
+
 mutual
 
 partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
   match v with
   | .lit (.str _) => return true
-  | .lit (.nat v) =>
-    -- The old compiler's implementation used the runtime's `is_scalar` function, which
-    -- introduces a dependency on the architecture used by the compiler.
-    return !isRoot || v >= Nat.pow 2 63
+  | .lit (.nat v) => return !isRoot || v >= Nat.pow 2 63
   | .lit _ | .erased => return !isRoot
   | .const name _ args =>
+    -- TODO: overapproximating, like this we never extract closed terms from our SCC even if the SCC
+    -- has actually been split open by now
     if (← read).sccDecls.any (·.name == name) then
       return false
+    -- TODO: cleanup never extract annotations in core
     if hasNeverExtractAttribute (← getEnv) name then
       return false
-    if isRoot then
-      if let some constInfo := (← getEnv).find? name then
-        let shouldExtract := match constInfo with
-        | .defnInfo val => val.type.isForall
-        | .ctorInfo _ => !(args.all isIrrelevantArg)
-        | _ => true
-        if !shouldExtract then
-          return false
+    let isPap := (← getMonoDecl? name).map (decide <| args.size < ·.getArity ) |>.getD false
+    if let some constInfo := (← getEnv).find? name then
+      let shouldExtractCtor :=
+        constInfo.isCtor &&
+        !(isExtern (← getEnv) name) &&
+        (!(args.all isIrrelevantArg) || !isRoot)
+      -- TODO: check fully applied ctor
+      let shouldExtract := shouldExtractCtor || extractionAllowlist.contains name || isPap
+      if !shouldExtract then
+        return false
+    else
+      let isClosedApp := (!isRoot && isClosedTermName (← getEnv) name)
+      if !(isClosedApp || isPap) then
+        return false
     args.allM shouldExtractArg
-  | .fvar fnVar args => return (← shouldExtractFVar fnVar) && (← args.allM shouldExtractArg)
+  | .fvar fnVar args =>
+    -- TODO: finetune, this could make a pap an fap which we want to avoid
+    return (← shouldExtractFVar fnVar) && (← args.allM shouldExtractArg)
   | .proj _ _ baseVar => shouldExtractFVar baseVar
 
 partial def shouldExtractArg (arg : Arg) : M Bool := do
@@ -89,7 +114,8 @@ partial def shouldExtractArg (arg : Arg) : M Bool := do
 
 partial def shouldExtractFVar (fvarId : FVarId) : M Bool := do
   if let some letDecl ← findLetDecl? fvarId then
-    shouldExtractLetValue false letDecl.value
+    let ret ← shouldExtractLetValue false letDecl.value
+    return ret
   else
     return false
 
@@ -100,7 +126,9 @@ mutual
 partial def visitCode (code : Code) : M Code := do
   match code with
   | .let decl k =>
-    if (← shouldExtractLetValue true decl.value) then
+    let should ← shouldExtractLetValue true decl.value
+    trace[Meta.debug] m!"Should extract: {← ppLetValue decl.value}? {should}"
+    if should then
       let ⟨_, decls⟩ ← extractLetValue decl.value |>.run {}
       let decls := decls.reverse.push (.let decl)
       let decls ← decls.mapM Internalize.internalizeCodeDecl |>.run' {}