chore: overhaul meta error messages (#10569)

Author: Kha

src/Lean/Compiler/LCNF/Visibility.lean

@@ -74,21 +74,44 @@ where go (isMeta isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit
       if (← get).contains ref then
         continue
       modify (·.insert ref)
+      let env ← getEnv
       if isMeta && isPublic then
-        if let some modIdx := (← getEnv).getModuleIdxFor? ref then
-          if (← getEnv).header.modules[modIdx]?.any (!·.isExported) then
-            throwError "Invalid `meta` definition `{.ofConstName origDecl.name}`, `{.ofConstName ref}` not publicly marked or imported as `meta`"
-      match getIRPhases (← getEnv) ref, isMeta with
+        if let some modIdx := env.getModuleIdxFor? ref then
+          if Lean.isMeta env ref then
+            if env.header.modules[modIdx]?.any (!·.isExported) then
+              throwError "Invalid public `meta` definition `{.ofConstName origDecl.name}`, \
+                `{.ofConstName ref}` is not accessible here; consider adding \
+                `public import {env.header.moduleNames[modIdx]!}`"
+          else
+            -- TODO: does not account for `public import` + `meta import`, which is not the same
+            if env.header.modules[modIdx]?.any (!·.isExported) then
+              throwError "Invalid public `meta` definition `{.ofConstName origDecl.name}`, \
+                `{.ofConstName ref}` is not accessible here; consider adding \
+                `public meta import {env.header.moduleNames[modIdx]!}`"
+      match getIRPhases env ref, isMeta with
       | .runtime, true =>
-        throwError "Invalid `meta` definition `{.ofConstName origDecl.name}`, may not access declaration `{.ofConstName ref}` not marked or imported as `meta`"
+        if let some modIdx := env.getModuleIdxFor? ref then
+          throwError "Invalid `meta` definition `{.ofConstName origDecl.name}`, \
+            `{.ofConstName ref}` is not accessible here; consider adding \
+            `meta import {env.header.moduleNames[modIdx]!}`"
+        else
+          throwError "Invalid `meta` definition `{.ofConstName origDecl.name}`, \
+            `{.ofConstName ref}` not marked `meta`"
       | .comptime, false =>
-        throwError "Invalid definition `{.ofConstName origDecl.name}`, may not access declaration `{.ofConstName ref}` marked or imported as `meta`"
-      | _, _ =>
+        if let some modIdx := env.getModuleIdxFor? ref then
+          if !Lean.isMeta env ref then
+            throwError "Invalid definition `{.ofConstName origDecl.name}`, may not access \
+              declaration `{.ofConstName ref}` imported as `meta`; consider adding \
+              `import {env.header.moduleNames[modIdx]!}`"
+        throwError "Invalid definition `{.ofConstName origDecl.name}`, may not access \
+          declaration `{.ofConstName ref}` marked as `meta`"
+      | irPhases, _ =>
         -- We allow auxiliary defs to be used in either phase but we need to recursively check
         -- *their* references in this case. We also need to do this for non-auxiliary defs in case a
         -- public meta def tries to use a private meta import via a local private meta def :/ .
-        if let some refDecl ← getLocalDecl? ref then
-          go isMeta isPublic refDecl
+        if irPhases == .all || isPublic && isPrivateName ref then
+          if let some refDecl ← getLocalDecl? ref then
+            go isMeta isPublic refDecl
 
 /--
 Checks meta availability just before `evalConst`. This is a "last line of defense" as accesses

tests/pkg/module/Module.lean

@@ -6,6 +6,7 @@ import Module.ImportedPrivateImported
 import Module.PrivateImported
 import Module.ImportedAllPrivateImported
 import Module.NonModule
+import Module.MetaImported
 
 /-! # Module system basic tests -/
 

tests/pkg/module/Module/Basic.lean

@@ -408,6 +408,8 @@ inst✝
 #guard_msgs in
 #print instTypeNameFoo
 
+public meta def pubMeta := 1
+
 /-! Prop `instance`s should have direct access to the private scope. -/
 
 public class PropClass : Prop where

tests/pkg/module/Module/Imported.lean

@@ -147,3 +147,9 @@ info: f_exp_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case
 -/
 #guard_msgs(pass trace, all) in
 #check f_exp_wfrec.induct_unfolding
+
+/-! Basic non-`meta` check. -/
+
+/-- error: Invalid definition `nonMeta`, may not access declaration `pubMeta` marked as `meta` -/
+#guard_msgs in
+def nonMeta := pubMeta

tests/pkg/module/Module/MetaImported.lean

@@ -0,0 +1,21 @@
+module
+
+prelude
+meta import Module.Basic
+
+/-! Basic phase restriction tests. -/
+/--
+error: Invalid definition `nonMeta`, may not access declaration `f` imported as `meta`; consider adding `import Module.Basic`
+-/
+#guard_msgs in
+def nonMeta := f
+
+/-- error: Invalid `meta` definition `veryMeta`, `nonMeta` not marked `meta` -/
+#guard_msgs in
+meta def veryMeta := nonMeta
+
+/--
+error: Invalid public `meta` definition `pubMetaImp`, `pubMeta` is not accessible here; consider adding `public import Module.Basic`
+-/
+#guard_msgs in
+public meta def pubMetaImp := pubMeta