From 08595c5f8fdeeead943eee92c33b4fc788130edb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 23 Mar 2026 11:03:26 +0100
Subject: [PATCH] fix: interaction of extern annotations and calls to functions
 with borrowed parameters (#13052)

This PR fixes a bug in the borrow inference in connection with `export`
annotations.

Previously parameters of `export` functions were presumed as owned from
the beginning of the
analysis. However, they were not added into the set of owned parameters
and thus sometimes failed to
force necessary changes to borrowedness of other values that the
parameters flowed into.
---
 src/Lean/Compiler/LCNF/InferBorrow.lean | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/InferBorrow.lean b/src/Lean/Compiler/LCNF/InferBorrow.lean
index ca6aa9066b..e7eafa5d0d 100644
--- a/src/Lean/Compiler/LCNF/InferBorrow.lean
+++ b/src/Lean/Compiler/LCNF/InferBorrow.lean
@@ -213,6 +213,8 @@ inductive OwnReason where
   | jpArgPropagation (jpFVar : FVarId)
   /-- Tail call preservation at a join point jump. -/
   | jpTailCallPreservation (jpFVar : FVarId)
+  /-- Annotated as an owned parameter (currently only triggerable through `@[export]`)-/
+  | ownedAnnotation
 
 def OwnReason.toString (reason : OwnReason) : CompilerM String := do
   PP.run do
@@ -229,6 +231,7 @@ def OwnReason.toString (reason : OwnReason) : CompilerM String := do
     | .tailCallPreservation funcName => return s!"tail call preservation of {funcName}"
     | .jpArgPropagation jpFVar => return s!"backward propagation from JP {← PP.ppFVar jpFVar}"
     | .jpTailCallPreservation jpFVar => return s!"JP tail call preservation {← PP.ppFVar jpFVar}"
+    | .ownedAnnotation => return s!"Annotated as owned"
 
 /--
 Determine whether an `OwnReason` is necessary for correctness (forced) or just an optimization
@@ -245,7 +248,7 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
   | .forwardProjectionProp .. | .backwardProjectionProp .. => true
 
 /--
@@ -256,10 +259,19 @@ partial def infer (decls : Array (Decl .impure)) : CompilerM ParamMap := do
   return map.paramMap
 where
   go : InferM Unit := do
+    for (_, params) in (← get).paramMap.map do
+      for param in params do
+        if !param.borrow && param.type.isPossibleRef then
+          -- if the param already disqualifies as borrow now this is because of an annotation
+          ownFVar param.fvarId .ownedAnnotation
+    modify fun s => { s with modified := false }
+    loop
+
+  loop : InferM Unit := do
     step
     if (← get).modified then
       modify fun s => { s with modified := false }
-      go
+      loop
     else
       return ()