fix: miscompilation resulting in minor memory leak on extern projections with unboxed arguments (#11383)

This PR fixes the compilation of structure projections with unboxed
arguments marked `extern`, adding missing `dec` instructions. It led to
leaking single allocations when such functions were used as closures or
in the interpreter.

This is the minimal working fix; `extern` should not replicate parts of
the compilation pipeline, which will be possible via #10291.

Author: Kha

src/Lean/Compiler/IR/AddExtern.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Lean.Compiler.IR.Boxing
+import Lean.Compiler.IR.RC
 
 public section
 
@@ -26,11 +27,12 @@ def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit :
     type := b
     nextVarIndex := nextVarIndex + 1
   let irType ← toIRType type
-  let decl := .extern declName params irType externAttrData
-  addDecl decl
-  if !isPrivateName decl.name then
-    modifyEnv (Compiler.LCNF.setDeclPublic · decl.name)
-  if ExplicitBoxing.requiresBoxedVersion (← Lean.getEnv) decl then
-    addDecl (ExplicitBoxing.mkBoxedVersion decl)
+  let decls := #[.extern declName params irType externAttrData]
+  if !isPrivateName declName then
+    modifyEnv (Compiler.LCNF.setDeclPublic · declName)
+  let decls := ExplicitBoxing.addBoxedVersions (← Lean.getEnv) decls
+  let decls ← explicitRC decls
+  logDecls `result decls
+  addDecls decls
 
 end Lean.IR

tests/lean/externBoxing.lean

@@ -0,0 +1,9 @@
+module
+
+/-! Applying `[extern]` to a projection should insert necessary `dec`s in `_boxed`. -/
+
+structure Foo where
+  bar : UInt64 → UInt64
+
+set_option trace.compiler.ir.result true
+attribute [extern "does_not_exist"] Foo.bar

tests/lean/externBoxing.lean.expected.out

@@ -0,0 +1,8 @@
+[Compiler.IR] [result]
+    extern _private.lean.externBoxing.0.Foo.bar (x_0 : obj) (x_1 : u64) : u64
+    def _private.lean.externBoxing.0.Foo.bar._boxed (x_1 : obj) (x_2 : tobj) : tobj :=
+      let x_3 : u64 := unbox x_2;
+      dec x_2;
+      let x_4 : u64 := _private.lean.externBoxing.0.Foo.bar x_1 x_3;
+      let x_5 : tobj := box x_4;
+      ret x_5