From 1b1c05916f24f635d7b0797553615bf82eb510af Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 27 Apr 2025 22:45:31 +0200
Subject: [PATCH] chore: refine `module` imports (#8120)

* bump whole imported module closure to private if necessary
* disallow import of non-`module` from `module`
---
 src/Init.lean                         |  2 ++
 src/Lean/Environment.lean             | 13 +++++++++++--
 tests/pkg/module/Module.lean          | 18 +-----------------
 tests/pkg/module/Module/Imported.lean | 19 +++++++++++++++++++
 4 files changed, 33 insertions(+), 19 deletions(-)
 create mode 100644 tests/pkg/module/Module/Imported.lean

diff --git a/src/Init.lean b/src/Init.lean
index 54792ce061..d994d04b17 100644
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Prelude
 import Init.Notation
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 08a2c8cfae..ed69c50b6e 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -1769,8 +1769,12 @@ partial def importModulesCore (imports : Array Import) (forceImportAll := true)
     -- import private info if (transitively) used by a non-`module` on any import path
     let importAll := forceImportAll
     if let some mod := (← get).moduleNameMap[i.module]? then
-      modify fun s => { s with moduleNameMap := s.moduleNameMap.insert i.module { mod with
-        importAll := mod.importAll || importAll }}
+      -- when module is already imported, bump entire closure to private if necessary
+      if importAll && !mod.importAll then
+        modify fun s => { s with moduleNameMap := s.moduleNameMap.insert i.module { mod with
+          importAll := true }}
+        if let some mod := mod.mainModule? then
+          importModulesCore mod.imports true
       continue
     let mFile ← findOLean i.module
     unless (← mFile.pathExists) do
@@ -1789,6 +1793,11 @@ partial def importModulesCore (imports : Array Import) (forceImportAll := true)
     -- `imports` is identical for each part
     let some (baseMod, _) := parts[0]? | unreachable!
     importModulesCore (forceImportAll := forceImportAll || !baseMod.isModule) baseMod.imports
+    if baseMod.isModule && !forceImportAll then
+      for i' in baseMod.imports do
+        if let some mod := (← get).moduleNameMap[i'.module]?.bind (·.mainModule?) then
+          if !mod.isModule then
+            throw <| IO.userError s!"cannot import non`-module` {i'.module} from `module` {i.module}"
     modify fun s => { s with
       moduleNameMap := s.moduleNameMap.insert i.module { name := i.module, importAll, parts }
       moduleNames := s.moduleNames.push i.module
diff --git a/tests/pkg/module/Module.lean b/tests/pkg/module/Module.lean
index 4a404bcd39..4ac354587a 100644
--- a/tests/pkg/module/Module.lean
+++ b/tests/pkg/module/Module.lean
@@ -1,7 +1,6 @@
-module
-
 import Lean
 import Module.Basic
+import Module.Imported
 
 /-! # Module system basic tests -/
 
@@ -21,18 +20,3 @@ open Lean
   let _ ← Core.CoreM.toIO (ctx := { fileName := "module.lean", fileMap := default }) (s := { env }) do
     assert! (← findDeclarationRanges? ``f).isSome
     assert! (getModuleDoc? (← getEnv) `Module.Basic).any (·.size == 1)
-
-/-! Theorems should be exported without their bodies -/
-
-/--
-info: theorem t : f = 1 :=
-<not imported>
--/
-#guard_msgs in
-#print t
-
-/-- error: dsimp made no progress -/
-#guard_msgs in
-example : f = 1 := by dsimp only [t]
-
-example : t = t := by dsimp only [trfl]
diff --git a/tests/pkg/module/Module/Imported.lean b/tests/pkg/module/Module/Imported.lean
new file mode 100644
index 0000000000..e29ffc3fc4
--- /dev/null
+++ b/tests/pkg/module/Module/Imported.lean
@@ -0,0 +1,19 @@
+module
+
+prelude
+import Module.Basic
+
+/-! Theorems should be exported without their bodies -/
+
+/--
+info: theorem t : f = 1 :=
+<not imported>
+-/
+#guard_msgs in
+#print t
+
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : f = 1 := by dsimp only [t]
+
+example : t = t := by dsimp only [trfl]