From ba7135d73c85b74be49f6fd3df5de0d22dae686b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 3 Jul 2025 18:48:15 +0200
Subject: [PATCH] fix: exposed wellfounded recursion (#9173)

This PR fixes an incompatibility in the experimental module system when
trying to combine wellfounded recursion with public exposed definitions.
---
 src/Lean/Meta/Transform.lean |  3 +++
 tests/lean/run/8938.lean     | 22 ++++++++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 tests/lean/run/8938.lean

diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index aaa968f565..0a3b0d8505 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -187,6 +187,9 @@ def zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr :=
 def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
   withoutModifyingEnv do
     let env ← getEnv
+    -- There might have been nested proof abstractions, which yield private helper theoresms, so
+    -- make sure we can find them. They will later be re-abstracted again.
+    let biggerEnv := biggerEnv.setExporting false
     setEnv biggerEnv -- `e` has declarations from `biggerEnv` that are not in `env`
     let pre (e : Expr) : CoreM TransformStep := do
       let .const declName us := e | return .continue
diff --git a/tests/lean/run/8938.lean b/tests/lean/run/8938.lean
new file mode 100644
index 0000000000..71f4c0e4d0
--- /dev/null
+++ b/tests/lean/run/8938.lean
@@ -0,0 +1,22 @@
+module
+
+/-! Wellfounded recursion should not break under `@[expose] public`. -/
+
+@[expose] public def ackermann : Nat → Nat → Nat
+| 0, m => m+1
+| n + 1, 0 => ackermann n 1
+| n + 1, m + 1 => ackermann n (ackermann (n + 1) m)
+termination_by n m => (n,m)
+
+/-- info: ackermann.eq_2 (n : Nat) : ackermann n.succ 0 = ackermann n 1 -/
+#guard_msgs in
+#check ackermann.eq_2
+
+@[expose] public def foo : Nat → Nat → Nat
+| 0, m => m
+| n + 1, m => foo n (m+1)
+termination_by n m => (n, m)
+
+/-- info: foo.eq_2 (x✝ n : Nat) : foo n.succ x✝ = foo n (x✝ + 1) -/
+#guard_msgs in
+#check foo.eq_2