From d9ebd51c04bb543f2b23da30264d25ff46133bae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 11 Mar 2026 21:59:06 +0100
Subject: [PATCH] feat: option to ignore borrowing annotations completely
 (#12886)

This PR adds support for ignoring user defined borrow annotations. This
can be useful when defining
`extern`/`export` pairs as the `extern` might be infected by borrow
annotations while in `export`
they are already ignored.
---
 src/Lean/Compiler/IR/AddExtern.lean           |  4 +-
 src/Lean/Compiler/LCNF/ToDecl.lean            | 13 +++++--
 src/Lean/Compiler/Options.lean                |  6 +++
 .../compiler_disable_borrow_annotations.lean  | 38 +++++++++++++++++++
 4 files changed, 57 insertions(+), 4 deletions(-)
 create mode 100644 tests/elab/compiler_disable_borrow_annotations.lean

diff --git a/src/Lean/Compiler/IR/AddExtern.lean b/src/Lean/Compiler/IR/AddExtern.lean
index 91de6c2f06..aa9db32b7c 100644
--- a/src/Lean/Compiler/IR/AddExtern.lean
+++ b/src/Lean/Compiler/IR/AddExtern.lean
@@ -15,6 +15,7 @@ import Lean.Compiler.LCNF.ExplicitBoxing
 import Lean.Compiler.LCNF.Internalize
 public import Lean.Compiler.ExternAttr
 import Lean.Compiler.LCNF.ExplicitRC
+import Lean.Compiler.Options
 
 public section
 
@@ -32,9 +33,10 @@ where
     let type ← Compiler.LCNF.getOtherDeclMonoType declName
     let mut typeIter := type
     let mut params := #[]
+    let ignoreBorrow := Compiler.compiler.ignoreBorrowAnnotation.get (← getOptions)
     repeat
       let .forallE binderName ty b _ := typeIter | break
-      let borrow := isMarkedBorrowed ty
+      let borrow := !ignoreBorrow && isMarkedBorrowed ty
       params := params.push {
         fvarId := (← mkFreshFVarId)
         type := ty,
diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean
index fc5c7bac56..a1aa84e88b 100644
--- a/src/Lean/Compiler/LCNF/ToDecl.lean
+++ b/src/Lean/Compiler/LCNF/ToDecl.lean
@@ -7,10 +7,13 @@ module
 prelude
 public import Lean.Compiler.InitAttr
 public import Lean.Compiler.LCNF.ToLCNF
+import Lean.Compiler.Options
 import Lean.Meta.Transform
 import Lean.Meta.Match.MatcherInfo
 import Init.While
+
 public section
+
 namespace Lean.Compiler.LCNF
 /--
 Inline constants tagged with the `[macro_inline]` attribute occurring in `e`.
@@ -127,10 +130,11 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
   let paramsFromTypeBinders (expr : Expr) : CompilerM (Array (Param .pure)) := do
     let mut params := #[]
     let mut currentExpr := expr
+    let ignoreBorrow := compiler.ignoreBorrowAnnotation.get (← getOptions)
     repeat
       match currentExpr with
       | .forallE binderName type body _ =>
-        let borrow := isMarkedBorrowed type
+        let borrow := !ignoreBorrow && isMarkedBorrowed type
         params := params.push (← mkParam binderName type borrow)
         currentExpr := body
       | _ => break
@@ -156,12 +160,15 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
       let value ← macroInline value
       return (type, value)
     let code ← toLCNF value
-    let decl ← if let .fun decl (.return _) := code then
+    let mut decl ← if let .fun decl (.return _) := code then
       eraseFunDecl decl (recursive := false)
       pure { name := declName, params := decl.params, type, value := .code decl.value, levelParams := info.levelParams, safe, inlineAttr? : Decl .pure }
     else
       pure { name := declName, params := #[], type, value := .code code, levelParams := info.levelParams, safe, inlineAttr? }
     /- `toLCNF` may eta-reduce simple declarations. -/
-    decl.etaExpand
+    decl ← decl.etaExpand
+    if compiler.ignoreBorrowAnnotation.get (← getOptions) then
+      decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
+    return decl
 
 end Lean.Compiler.LCNF
diff --git a/src/Lean/Compiler/Options.lean b/src/Lean/Compiler/Options.lean
index cebcfd230e..1663ccdd95 100644
--- a/src/Lean/Compiler/Options.lean
+++ b/src/Lean/Compiler/Options.lean
@@ -35,4 +35,10 @@ register_builtin_option compiler.relaxedMetaCheck : Bool := {
   descr := "Allow mixed `meta`/non-`meta` references in the same module. References to imports are unaffected."
 }
 
+register_builtin_option compiler.ignoreBorrowAnnotation : Bool := {
+  defValue := false
+  descr := "Ignore user defined borrow inference annotations. This is useful for export/extern \
+    forward declarations"
+}
+
 end Lean.Compiler
diff --git a/tests/elab/compiler_disable_borrow_annotations.lean b/tests/elab/compiler_disable_borrow_annotations.lean
new file mode 100644
index 0000000000..170989da7e
--- /dev/null
+++ b/tests/elab/compiler_disable_borrow_annotations.lean
@@ -0,0 +1,38 @@
+module
+
+/-!
+This test asserts that disabling user-defined borrow annotations works. This is sometimes required for
+export/extern pairs
+-/
+
+public abbrev Foo (α : Type) := (x : @& α) → α
+
+/--
+trace: [Compiler.result] size: 0
+    def t1 @&x : tobj :=
+      extern
+[Compiler.result] size: 2
+    def t1._boxed x : tobj :=
+      let res := t1 x;
+      dec x;
+      return res
+-/
+#guard_msgs in
+set_option trace.Compiler.result true in
+@[extern "t1"]
+public opaque t1 : Foo Nat
+
+/--
+trace: [Compiler.result] size: 0
+    def t2 x : tobj :=
+      extern
+[Compiler.result] size: 1
+    def t2._boxed x : tobj :=
+      let res := t2 x;
+      return res
+-/
+#guard_msgs in
+set_option compiler.ignoreBorrowAnnotation true in
+set_option trace.Compiler.result true in
+@[extern "t2"]
+public opaque t2 : Foo Nat