chore: refine module imports (#8120)

* bump whole imported module closure to private if necessary
* disallow import of non-`module` from `module`

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

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

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]

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]