fix: do not export private instances (#9407)

Fixes #9383

src/Lean/Meta/Instances.lean

@@ -90,6 +90,8 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In
   registerSimpleScopedEnvExtension {
     initial  := {}
     addEntry := addInstanceEntry
+    exportEntry? := fun level e =>
+      guard (level == .private || e.globalName?.any (!isPrivateName ·)) *> e
   }
 
 private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do

src/Lean/ScopedEnvExtension.lean

@@ -37,6 +37,7 @@ structure Descr (α : Type) (β : Type) (σ : Type) where
   toOLeanEntry   : β → α
   addEntry       : σ → β → σ
   finalizeImport : σ → σ := id
+  exportEntry?   : OLeanLevel → α → Option α := fun _ => some
 
 instance [Inhabited α] : Inhabited (Descr α β σ) where
   default := {
@@ -90,8 +91,10 @@ def addEntryFn (descr : Descr α β σ) (s : StateStack α β σ) (e : Entry β)
             s
       }
 
-def exportEntriesFn (s : StateStack α β σ) : Array (Entry α) :=
-  s.newEntries.toArray.reverse
+def exportEntriesFn (descr : Descr α β σ) (level : OLeanLevel) (s : StateStack α β σ) : Array (Entry α) :=
+  s.newEntries.toArray.reverse.filterMap fun
+    | .global e => .global <$> descr.exportEntry? level e
+    | .scoped ns e => .scoped ns <$> descr.exportEntry? level e
 
 end ScopedEnvExtension
 
@@ -110,7 +113,7 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope
     mkInitial       := mkInitial descr
     addImportedFn   := addImportedFn descr
     addEntryFn      := addEntryFn descr
-    exportEntriesFn := exportEntriesFn
+    exportEntriesFnEx := fun _ s level => exportEntriesFn descr level s
     statsFn         := fun s => format "number of local entries: " ++ format s.newEntries.length
     -- We restrict addition of global and `scoped` entries to the main thread but allow addition of
     -- scopes and local entries in any thread, which are visible only in that thread (see uses of
@@ -212,6 +215,7 @@ structure SimpleScopedEnvExtension.Descr (α : Type) (σ : Type) where
   addEntry       : σ → α → σ
   initial        : σ
   finalizeImport : σ → σ := id
+  exportEntry?   : OLeanLevel → α → Option α := fun _ => some
 
 def registerSimpleScopedEnvExtension (descr : SimpleScopedEnvExtension.Descr α σ) : IO (SimpleScopedEnvExtension α σ) := do
   registerScopedEnvExtension {
@@ -221,6 +225,7 @@ def registerSimpleScopedEnvExtension (descr : SimpleScopedEnvExtension.Descr α
     toOLeanEntry   := id
     ofOLeanEntry   := fun _ a => return a
     finalizeImport := descr.finalizeImport
+    exportEntry?   := descr.exportEntry?
   }
 
 end Lean

tests/pkg/module/Module/Basic.lean

@@ -13,6 +13,11 @@ public def f := 1
 /-- A theorem. -/
 public theorem t : f = 1 := testSorry
 
+public class X
+
+/-- A local instance of a public class. -/
+instance : X := ⟨⟩
+
 -- Check that the theorem types are checked in exported context, where `f` is not defeq to `1`
 -- (but `fexp` is)
 

tests/pkg/module/Module/Imported.lean

@@ -28,6 +28,18 @@ info: theorem trfl : f = 1 :=
 #guard_msgs in
 #print trfl
 
+/-! Metadata of private decls should not be exported. -/
+
+-- Should not fail with 'unknown constant `inst*`
+/--
+error: failed to synthesize
+  X
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+def fX : X := inferInstance
+
 /-- error: dsimp made no progress -/
 #guard_msgs in
 example : P f := by dsimp only [t]; exact hP1