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.

Author: Kha

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -83,26 +83,29 @@ 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
       throwError "\
         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,15 +215,15 @@ 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) }
   let (output, exOrRes) ← IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
     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
 -/