fix: detect private references in inferred type of public def (#10762)

This PR fixes an inconsistency in the module system around defs with
elided types.

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -83,19 +83,21 @@ where
     let (args, _, _) ← forallMetaBoundedTelescope (← inferType m) 1
     return mkAppN m args
 
-private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorry := false) : TermElabM Unit := do
+private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorry := false) : TermElabM Name := do
   -- Use the `elabMutualDef` machinery to be able to support `let rec`.
   -- Hack: since we are using the `TermElabM` version, we can insert the `value` as a metavariable via `exprToSyntax`.
   -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
   -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
   -- such as "failed to infer definition type" can surface.
-  let defView := mkDefViewOfDef { isUnsafe := true, visibility := .public }
+  let defView := mkDefViewOfDef { isUnsafe := true, visibility := .private }
     (← `(Parser.Command.definition|
           def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
+  let declName := mkPrivateName (← getEnv) declName
   -- Allow access to both `meta` and non-`meta` declarations as the compilation result does not
   -- escape the current module.
   withOptions (Compiler.compiler.checkMeta.set · false) do
     Term.elabMutualDef #[] { header := "" } #[defView]
+  assert! (← getEnv).contains declName
   unless allowSorry do
     let axioms ← collectAxioms declName
     if axioms.contains ``sorryAx then
@@ -103,6 +105,7 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr
         aborting evaluation since the expression depends on the 'sorry' axiom, \
         which can lead to runtime instability and crashes.\n\n\
         To attempt to evaluate anyway despite the risks, use the '#eval!' command."
+  return declName
 
 /--
 Try to make a `@projFn ty inst e` application, even if it takes unfolding the type `ty` of `e` to synthesize the instance `inst`.
@@ -181,13 +184,13 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
         | return none
       let eType := e.appFn!.appArg!
       if ← isDefEq eType (mkConst ``Unit) then
-        addAndCompileExprForEval declName e (allowSorry := bang)
+        let declName ← addAndCompileExprForEval declName e (allowSorry := bang)
         let mf : m Unit ← evalConst (m Unit) declName (checkMeta := !Elab.inServer.get (← getOptions))
         return some { eval := do MonadEvalT.monadEval mf; pure "", printVal := none }
       else
         let rf ← withLocalDeclD `x eType fun x => do mkLambdaFVars #[x] (← mkT x)
         let r ← mkAppM ``Functor.map #[rf, e]
-        addAndCompileExprForEval declName r (allowSorry := bang)
+        let declName ← addAndCompileExprForEval declName r (allowSorry := bang)
         let mf : m t ← evalConst (m t) declName (checkMeta := !Elab.inServer.get (← getOptions))
         return some { eval := toMessageData <$> MonadEvalT.monadEval mf, printVal := some eType }
     if let some act ← mkMAct? ``CommandElabM CommandElabM e
@@ -212,7 +215,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
         throwError m!"unable to synthesize `{.ofConstName ``MonadEval}` instance \
           to adapt{indentExpr (← inferType e)}\n\
           to `{.ofConstName ``IO}` or `{.ofConstName ``CommandElabM}`."
-      addAndCompileExprForEval declName r (allowSorry := bang)
+      let declName ← addAndCompileExprForEval declName r (allowSorry := bang)
       -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
       let r ← toMessageData <$> evalConst t declName (checkMeta := !Elab.inServer.get (← getOptions))
       return { eval := pure r, printVal := some (← inferType e) }
@@ -220,7 +223,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
     try
       -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
       -- we don't pollute the environment with auxiliary declarations.
-      let act : EvalAction ← liftTermElabM do Term.withDeclName declName do withoutModifyingEnv do
+      let act : EvalAction ← liftTermElabM do Term.withDeclName (mkPrivateName (← getEnv) declName) do withoutModifyingEnv do
         withSaveInfoContext do -- save the environment post-elaboration (for matchers, let rec, etc.)
           let e ← elabTermForEval term expectedType?
           -- If there is an elaboration error, don't evaluate!

src/Lean/Elab/MutualDef.lean

@@ -547,6 +547,14 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
               -- leads to more section variables being included than necessary
               instantiateMVarsProfiling val
         let val ← mkLambdaFVars xs val
+        if header.type?.isNone && (← getEnv).header.isModule && !(← getEnv).isExporting &&
+            !isPrivateName header.declName && header.kind != .example then
+          -- If the type of a non-exposed definition was elided, we need to check after the fact
+          -- whether it is in fact well-formed.
+          withRef header.declId do
+          withExporting do
+            let type ← instantiateMVars type
+            Meta.check type
         if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do
             let varDecl ← var.fvarId!.getDecl
@@ -1194,6 +1202,8 @@ where
       Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
     withExporting (isExporting :=
       -- `example`s are always private unless explicitly marked `public`
+      -- (it would be more consistent to give them a private name as well but that exposes that
+      -- encoded name in e.g. kernel errors where it's hard to replace it)
       views.any (fun view => view.kind != .example || view.modifiers.isPublic) &&
       expandedDeclIds.any (!isPrivateName ·.declName)) do
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises

src/lake/Lake/Config/Pattern.lean

@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Array.Basic
 public import Init.System.FilePath
+public import Std.Data.TreeMap.Basic
+public import Lean.Data.Name
 import Lake.Util.Name
 
 open System Lean

tests/lakefile.toml

@@ -3,3 +3,7 @@ name = "tests"
 # Allow `module` in tests when opened in the language server.
 # Enabled during actual test runs in the respective test_single.sh.
 moreGlobalServerArgs = ["-Dexperimental.module=true"]
+
+[[lean_lib]]
+name = "Tests"
+globs = ["lean.*"]

tests/lean/binopInfoTree.lean.expected.out

@@ -60,7 +60,7 @@ fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int
                 • [Term] n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent
                   • [Completion-Id] n : none @ ⟨7, 29⟩-⟨7, 30⟩
                   • [Term] n : Nat @ ⟨7, 29⟩-⟨7, 30⟩
-                • [Term] ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1»
+                • [Term] ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_lean_binopInfoTree___macroRules_term_+'__1»
                   • [MacroExpansion]
                     m +' l
                     ===>

tests/lean/dbgMacros.lean.expected.out

@@ -1,10 +1,10 @@
-PANIC at f dbgMacros:2:14: unexpected zero
+PANIC at f lean.dbgMacros:2:14: unexpected zero
 0
 9
-PANIC at g dbgMacros:10:14: unreachable code has been reached
+PANIC at g lean.dbgMacros:10:14: unreachable code has been reached
 0
 0
-PANIC at h dbgMacros:16:0: assertion violation: x != 0
+PANIC at h lean.dbgMacros:16:0: assertion violation: x != 0
 0
 f2, x: 10
 11

tests/lean/ppNotationCode.lean.expected.out

@@ -1,7 +1,7 @@
 [Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr :=
     Lean.ParserDescr.trailingNode `«term_+++_» 45 46
       (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
-[Elab.definition.body] «_aux_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
+[Elab.definition.body] «_aux_lean_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
     fun x =>
       have __discr := x;
       if __discr.isOfKind `«term_+++_» = true then
@@ -24,7 +24,7 @@
       else
         have __discr := x;
         throw Lean.Macro.Exception.unsupportedSyntax
-[Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
+[Elab.definition.body] _aux_lean_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
     fun x =>
       have __discr := x;
       if __discr.isOfKind `Lean.Parser.Term.app = true then

tests/lean/root.lean.expected.out

@@ -7,7 +7,7 @@ root.lean:35:14-35:22: error: protected declarations must be in a namespace
 root.lean:41:7-41:8: error(lean.unknownIdentifier): Unknown identifier `h`
 root.lean:43:7-43:8: error(lean.unknownIdentifier): Unknown identifier `f`
 Bla.f (x : Nat) : Nat
-_private.root.0.prv : Nat -> Nat
+_private.lean.root.0.prv : Nat -> Nat
 root.lean:90:89-90:93: error: unsolved goals
 x : Nat
 ⊢ isEven (x + 1 + 1) = isEven x

tests/lean/run/decideNative.lean

@@ -126,5 +126,7 @@ instance : Decidable ItsTrue2 :=
   panic! "oh no"
 
 -- Note: this test fails within VS Code
-/-- info: output: PANIC at instDecidableItsTrue2 decideNative:126:2: oh no -/
+/--
+info: output: PANIC at instDecidableItsTrue2 lean.run.decideNative:126:2: oh no
+-/
 #guard_msgs in example : ItsTrue2 := by collect_stdout native_decide

tests/lean/run/emptyLcnf.lean

@@ -12,7 +12,8 @@ trace: [Compiler.result] size: 0
       ⊥
 ---
 trace: [Compiler.result] size: 5
-    def _eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
+    def _private.lean.run.emptyLcnf.0._eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result
+      Lean.Exception lcRealWorld PUnit :=
       let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
       cases _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit
       | EStateM.Result.ok a.11 a.12 =>
@@ -21,34 +22,34 @@ trace: [Compiler.result] size: 5
       | EStateM.Result.error a.14 a.15 =>
         return _x.10
 [Compiler.result] size: 1
-    def _eval._closed_0 : String :=
+    def _private.lean.run.emptyLcnf.0._eval._closed_0 : String :=
       let _x.1 := "f";
       return _x.1
 [Compiler.result] size: 2
-    def _eval._closed_1 : Lean.Name :=
-      let _x.1 := _eval._closed_0;
+    def _private.lean.run.emptyLcnf.0._eval._closed_1 : Lean.Name :=
+      let _x.1 := _eval._closed_0.2;
       let _x.2 := Lean.Name.mkStr1 _x.1;
       return _x.2
 [Compiler.result] size: 2
-    def _eval._closed_2 : Array Lean.Name :=
+    def _private.lean.run.emptyLcnf.0._eval._closed_2 : Array Lean.Name :=
       let _x.1 := 1;
       let _x.2 := Array.mkEmpty ◾ _x.1;
       return _x.2
 [Compiler.result] size: 3
-    def _eval._closed_3 : Array Lean.Name :=
-      let _x.1 := _eval._closed_1;
-      let _x.2 := _eval._closed_2;
+    def _private.lean.run.emptyLcnf.0._eval._closed_3 : Array Lean.Name :=
+      let _x.1 := _eval._closed_1.2;
+      let _x.2 := _eval._closed_2.2;
       let _x.3 := Array.push ◾ _x.2 _x.1;
       return _x.3
 [Compiler.result] size: 8
-    def _eval a.1 a.2 a.3 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
-      let _x.4 := _eval._closed_0;
-      let _x.5 := _eval._closed_1;
+    def _private.lean.run.emptyLcnf.0._eval a.1 a.2 a.3 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
+      let _x.4 := _eval._closed_0.2;
+      let _x.5 := _eval._closed_1.2;
       let _x.6 := 1;
-      let _x.7 := _eval._closed_2;
-      let _x.8 := _eval._closed_3;
+      let _x.7 := _eval._closed_2.2;
+      let _x.8 := _eval._closed_3.2;
       let _x.9 := PUnit.unit;
-      let _f.10 := _eval._lam_0 _x.8 _x.9;
+      let _f.10 := _eval._lam_0.2 _x.8 _x.9;
       let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
       return _x.11
 -/

tests/lean/run/erased.lean

@@ -26,7 +26,7 @@ trace: [Compiler.result] size: 1
       return _x.1
 ---
 trace: [Compiler.result] size: 5
-    def _eval._lam_0 (_x.1 : Array
+    def _private.lean.run.erased.0._eval._lam_0 (_x.1 : Array
        Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : lcRealWorld) : EStateM.Result
       Lean.Exception lcRealWorld PUnit :=
       let _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit := compile _x.1 _y.7 _y.8 _y.9;
@@ -37,46 +37,46 @@ trace: [Compiler.result] size: 5
       | EStateM.Result.error (a.14 : Lean.Exception) (a.15 : lcRealWorld) =>
         return _x.10
 [Compiler.result] size: 1
-    def _eval._closed_0 : String :=
+    def _private.lean.run.erased.0._eval._closed_0 : String :=
       let _x.1 : String := "Erased";
       return _x.1
 [Compiler.result] size: 1
-    def _eval._closed_1 : String :=
+    def _private.lean.run.erased.0._eval._closed_1 : String :=
       let _x.1 : String := "mk";
       return _x.1
 [Compiler.result] size: 3
-    def _eval._closed_2 : Lean.Name :=
-      let _x.1 : String := _eval._closed_1;
-      let _x.2 : String := _eval._closed_0;
+    def _private.lean.run.erased.0._eval._closed_2 : Lean.Name :=
+      let _x.1 : String := _eval._closed_1.2;
+      let _x.2 : String := _eval._closed_0.2;
       let _x.3 : Lean.Name := Lean.Name.mkStr2 _x.2 _x.1;
       return _x.3
 [Compiler.result] size: 2
-    def _eval._closed_3 : Array Lean.Name :=
+    def _private.lean.run.erased.0._eval._closed_3 : Array Lean.Name :=
       let _x.1 : Nat := 1;
       let _x.2 : Array Lean.Name := Array.mkEmpty ◾ _x.1;
       return _x.2
 [Compiler.result] size: 3
-    def _eval._closed_4 : Array Lean.Name :=
-      let _x.1 : Lean.Name := _eval._closed_2;
-      let _x.2 : Array Lean.Name := _eval._closed_3;
+    def _private.lean.run.erased.0._eval._closed_4 : Array Lean.Name :=
+      let _x.1 : Lean.Name := _eval._closed_2.2;
+      let _x.2 : Array Lean.Name := _eval._closed_3.2;
       let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
       return _x.3
 [Compiler.result] size: 9
-    def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcRealWorld) : EStateM.Result Lean.Exception
-      lcRealWorld PUnit :=
-      let _x.4 : String := _eval._closed_0;
-      let _x.5 : String := _eval._closed_1;
-      let _x.6 : Lean.Name := _eval._closed_2;
+    def _private.lean.run.erased.0._eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcRealWorld) : EStateM.Result
+      Lean.Exception lcRealWorld PUnit :=
+      let _x.4 : String := _eval._closed_0.2;
+      let _x.5 : String := _eval._closed_1.2;
+      let _x.6 : Lean.Name := _eval._closed_2.2;
       let _x.7 : Nat := 1;
-      let _x.8 : Array Lean.Name := _eval._closed_3;
-      let _x.9 : Array Lean.Name := _eval._closed_4;
+      let _x.8 : Array Lean.Name := _eval._closed_3.2;
+      let _x.9 : Array Lean.Name := _eval._closed_4.2;
       let _x.10 : PUnit := PUnit.unit;
       let _f.11 : Lean.Elab.Term.Context →
         lcAny →
           Lean.Meta.Context →
             lcAny →
               Lean.Core.Context →
-                lcAny → lcRealWorld → EStateM.Result Lean.Exception lcRealWorld PUnit := _eval._lam_0 _x.9 _x.10;
+                lcAny → lcRealWorld → EStateM.Result Lean.Exception lcRealWorld PUnit := _eval._lam_0.2 _x.9 _x.10;
       let _x.12 : EStateM.Result Lean.Exception lcRealWorld
         PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
       return _x.12

tests/lean/run/sorry.lean

@@ -70,9 +70,9 @@ Showing source position when surfacing differences.
 error: Type mismatch
   sorry
 has type
-  sorry `«sorry:77:43»
+  sorry `«lean.run.sorry:77:43»
 but is expected to have type
-  sorry `«sorry:77:25»
+  sorry `«lean.run.sorry:77:25»
 -/
 #guard_msgs in example : sorry := (sorry : sorry)
 
@@ -98,7 +98,7 @@ error: Unknown identifier `a`
 ---
 error: Unknown identifier `b`
 ---
-trace: ⊢ sorry `«sorry:106:10» = sorry `«sorry:106:14»
+trace: ⊢ sorry `«lean.run.sorry:106:10» = sorry `«lean.run.sorry:106:14»
 -/
 #guard_msgs in
 set_option autoImplicit false in

tests/lean/run/test_single.sh

@@ -1,5 +1,6 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
+# `--root` to infer same private names as in the server
 # Elab.inServer to allow for arbitrary `#eval`
-exec_check_raw lean -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f"
+exec_check_raw lean --root=../.. -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f"

tests/lean/sint_basic.lean.expected.out

@@ -73,11 +73,11 @@ true
 true
 true
 [Compiler.IR] [result]
-    def _private.sint_basic.0.myId8 (x_1 : u8) : u8 :=
+    def _private.lean.sint_basic.0.myId8 (x_1 : u8) : u8 :=
       ret x_1
-    def _private.sint_basic.0.myId8._boxed (x_1 : tagged) : tagged :=
+    def _private.lean.sint_basic.0.myId8._boxed (x_1 : tagged) : tagged :=
       let x_2 : u8 := unbox x_1;
-      let x_3 : u8 := _private.sint_basic.0.myId8 x_2;
+      let x_3 : u8 := _private.lean.sint_basic.0.myId8 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 Int16 : Type
@@ -155,11 +155,11 @@ true
 true
 true
 [Compiler.IR] [result]
-    def _private.sint_basic.0.myId16 (x_1 : u16) : u16 :=
+    def _private.lean.sint_basic.0.myId16 (x_1 : u16) : u16 :=
       ret x_1
-    def _private.sint_basic.0.myId16._boxed (x_1 : tagged) : tagged :=
+    def _private.lean.sint_basic.0.myId16._boxed (x_1 : tagged) : tagged :=
       let x_2 : u16 := unbox x_1;
-      let x_3 : u16 := _private.sint_basic.0.myId16 x_2;
+      let x_3 : u16 := _private.lean.sint_basic.0.myId16 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 Int32 : Type
@@ -237,12 +237,12 @@ true
 true
 true
 [Compiler.IR] [result]
-    def _private.sint_basic.0.myId32 (x_1 : u32) : u32 :=
+    def _private.lean.sint_basic.0.myId32 (x_1 : u32) : u32 :=
       ret x_1
-    def _private.sint_basic.0.myId32._boxed (x_1 : tobj) : tobj :=
+    def _private.lean.sint_basic.0.myId32._boxed (x_1 : tobj) : tobj :=
       let x_2 : u32 := unbox x_1;
       dec x_1;
-      let x_3 : u32 := _private.sint_basic.0.myId32 x_2;
+      let x_3 : u32 := _private.lean.sint_basic.0.myId32 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 Int64 : Type
@@ -320,12 +320,12 @@ true
 true
 true
 [Compiler.IR] [result]
-    def _private.sint_basic.0.myId64 (x_1 : u64) : u64 :=
+    def _private.lean.sint_basic.0.myId64 (x_1 : u64) : u64 :=
       ret x_1
-    def _private.sint_basic.0.myId64._boxed (x_1 : tobj) : tobj :=
+    def _private.lean.sint_basic.0.myId64._boxed (x_1 : tobj) : tobj :=
       let x_2 : u64 := unbox x_1;
       dec x_1;
-      let x_3 : u64 := _private.sint_basic.0.myId64 x_2;
+      let x_3 : u64 := _private.lean.sint_basic.0.myId64 x_2;
       let x_4 : tobj := box x_3;
       ret x_4
 ISize : Type
@@ -403,11 +403,11 @@ true
 true
 true
 [Compiler.IR] [result]
-    def _private.sint_basic.0.myIdSize (x_1 : usize) : usize :=
+    def _private.lean.sint_basic.0.myIdSize (x_1 : usize) : usize :=
       ret x_1
-    def _private.sint_basic.0.myIdSize._boxed (x_1 : tobj) : tobj :=
+    def _private.lean.sint_basic.0.myIdSize._boxed (x_1 : tobj) : tobj :=
       let x_2 : usize := unbox x_1;
       dec x_1;
-      let x_3 : usize := _private.sint_basic.0.myIdSize x_2;
+      let x_3 : usize := _private.lean.sint_basic.0.myIdSize x_2;
       let x_4 : tobj := box x_3;
       ret x_4

tests/lean/test_single.sh

@@ -2,5 +2,7 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f" || true
+# `--root` to infer same private names as in the server
+# Elab.inServer to allow for arbitrary `#eval`
+exec_capture lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f" || true
 diff_produced

tests/pkg/module/Module/Basic.lean

@@ -80,6 +80,16 @@ Note: A private declaration `fpriv` (from the current module) exists but would n
 #guard_msgs in
 public theorem tpriv : fpriv = 1 := rfl
 
+/-! Type inference should not be able to smuggle out private references. -/
+
+/--
+error: Unknown constant `_private.Module.Basic.0.fpriv`
+
+Note: A private declaration `fpriv` (from the current module) exists but would need to be public to access here.
+-/
+#guard_msgs in
+public def inferredPrivRef := (rfl : fpriv = 1)
+
 public class X
 
 /-- A local instance of a public class. -/

tests/pkg/module/Module/MetaImported.lean

@@ -1,6 +1,5 @@
 module
 
-prelude
 meta import Module.Basic
 
 /-! Basic phase restriction tests. -/