feat: throw an error when export declarations have borrow annotations

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -11,6 +11,7 @@ import Lean.Compiler.Options
 import Lean.Meta.Transform
 import Lean.Meta.Match.MatcherInfo
 import Init.While
+import Lean.Compiler.ExportAttr
 
 public section
 
@@ -169,6 +170,8 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
     decl ← decl.etaExpand
     if compiler.ignoreBorrowAnnotation.get (← getOptions) then
       decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
+    if isExport env decl.name && decl.params.any (·.borrow) then
+      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration."
     return decl
 
 end Lean.Compiler.LCNF

src/Lean/LoadDynlib.lean

@@ -64,7 +64,7 @@ If multiple libraries share common symbols, those symbols should be linked
 and loaded as separate libraries.
 -/
 @[export lean_load_dynlib]
-def loadDynlib (path : @& System.FilePath) : IO Unit := do
+def loadDynlib (path : System.FilePath) : IO Unit := do
   let dynlib ← Dynlib.load path
   -- Lean never unloads libraries.
   -- Safety: There are no concurrent accesses to `dynlib` at this point.

tests/elab/lcnf_export_borrow_error.lean

@@ -0,0 +1,12 @@
+module
+
+/-! Assert that putting a borrow annotation on an export errors -/
+
+/--
+error:  Declaration bar is marked as `export` but some of its parameters have borrow annotations.
+ Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.
+ If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration.
+-/
+#guard_msgs in
+@[export foo]
+public def bar (x : @& String) := x