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

@@ -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

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