From 1d989523d43cdf25a5dc54432b2f3551311e529b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 8 Oct 2025 14:48:35 +0200
Subject: [PATCH] fix: `simp` should not pick up inaccessible definitional
 equations (#10696)

Fixes #10671
---
 src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 10 ++++++++++
 tests/pkg/module/Module/Basic.lean          |  2 ++
 tests/pkg/module/Module/Imported.lean       |  7 +++++++
 3 files changed, 19 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 6bc3c9dc43..06d94d14c4 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -670,6 +670,16 @@ def mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension :=
     name     := name
     initial  := {}
     addEntry := fun d e => d.addSimpEntry e
+    exportEntry? := fun lvl e => do
+      -- export only annotations on public decls
+      let declName := match e with
+        | .thm t => match t.origin with
+          | .decl n _ _ => n
+          | _ => unreachable!
+        | .toUnfold n => n
+        | .toUnfoldThms n _ => n
+      guard (lvl == .private || !isPrivateName declName)
+      return e
   }
 
 abbrev SimpExtensionMap := Std.HashMap Name SimpExtension
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index ce5d711d23..27b263234f 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -457,3 +457,5 @@ info: @[expose] meta def msecexp : Nat :=
 #guard_msgs in
 #with_exporting
 #print msecexp
+
+attribute [simp] f_struct
diff --git a/tests/pkg/module/Module/Imported.lean b/tests/pkg/module/Module/Imported.lean
index 0082c0b1bf..80bdcd4d62 100644
--- a/tests/pkg/module/Module/Imported.lean
+++ b/tests/pkg/module/Module/Imported.lean
@@ -153,3 +153,10 @@ info: f_exp_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case
 /-- error: Invalid definition `nonMeta`, may not access declaration `pubMeta` marked as `meta` -/
 #guard_msgs in
 def nonMeta := pubMeta
+
+/-! `simp` should not pick up inaccessible definitional equations. -/
+
+/-- error: `simp` made no progress -/
+#guard_msgs in
+theorem f_struct_eq : f_struct 0 = 0 := by
+  simp