diff --git a/src/Lean/Compiler/MetaAttr.lean b/src/Lean/Compiler/MetaAttr.lean
index e1f9e11144..6649deded9 100644
--- a/src/Lean/Compiler/MetaAttr.lean
+++ b/src/Lean/Compiler/MetaAttr.lean
@@ -17,31 +17,11 @@ private builtin_initialize metaExt : TagDeclarationExtension ←
   -- set by `addPreDefinitions`; if we ever make `def` elaboration async, it should be moved to
   -- remain on the main environment branch
   mkTagDeclarationExtension (asyncMode := .async .mainEnv)
-/--
-Environment extension collecting declarations *could* have been marked as `meta` by the user but
-were not, so should not allow access to `meta` declarations to surface phase distinction errors as
-soon as possible.
--/
-private builtin_initialize notMetaExt : EnvExtension NameSet ←
-  registerEnvExtension
-    (mkInitial := pure {})
-    (asyncMode := .async .mainEnv)
-    (replay? := some fun _ _ newEntries s => newEntries.foldl (·.insert) s)
 
 /-- Marks in the environment extension that the given declaration has been declared by the user as `meta`. -/
 def markMeta (env : Environment) (declName : Name) : Environment :=
   metaExt.tag env declName
 
-/--
-Marks the given declaration as not being annotated with `meta` even if it could have been by the
-user.
--/
-def markNotMeta (env : Environment) (declName : Name) : Environment :=
-  if declName.isAnonymous then  -- avoid panic from `modifyState` on partial input
-    env
-  else
-    notMetaExt.modifyState (asyncDecl := declName) env (·.insert declName)
-
 /-- Returns true iff the user has declared the given declaration as `meta`. -/
 def isMarkedMeta (env : Environment) (declName : Name) : Bool :=
   metaExt.isTagged env declName
@@ -102,13 +82,12 @@ def getIRPhases (env : Environment) (declName : Name) : IRPhases := Id.run do
     else
       env.header.modules[idx]?.map (·.irPhases) |>.get!
   | none =>
-    if isMarkedMeta env declName then
-      .comptime
-    else if notMetaExt.getState env |>.contains declName then
-      .runtime
-    else
-      -- Allow `meta`->non-`meta` references in the same module for auxiliary declarations the user
-      -- could not have marked as `meta` themselves.
+    if env.find? declName |>.all (·.isCtor) then
+      -- Do not check ctors (trivial) or decls not in env (compiler-generated)
       .all
+    else if isMarkedMeta env declName then
+      .comptime
+    else
+      .runtime
 
 end Lean
diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean
index 1975ad4852..548df6b0e3 100644
--- a/src/Lean/Data/Lsp/LanguageFeatures.lean
+++ b/src/Lean/Data/Lsp/LanguageFeatures.lean
@@ -11,6 +11,7 @@ public import Lean.Data.Lsp.Basic
 public import Lean.Expr
 public import Init.Data.String.Search
 public import Init.Data.Array.GetLit
+meta import Lean.Data.Json.FromToJson.Basic
 
 public section
 
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 23f74ccfde..4013c7b95d 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -559,10 +559,14 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     let t ← elabTermAndSynthesize t expectedType?
     if (← logUnassignedUsingErrorInfos (← getMVars t)) then
       throwAbortTerm
-    let t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
+    let t ← mkAuxDefinitionFor (compile := false) (← mkAuxName `unsafe) t
     let .const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
     let .defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
     let implName ← mkAuxName `unsafe_impl
+    if (← read).declName?.any (isMarkedMeta (← getEnv)) then
+      modifyEnv (markMeta · unsafeFn)
+      modifyEnv (markMeta · implName)
+    compileDecls #[unsafeFn]
     addDecl <| Declaration.opaqueDecl {
       name        := implName
       type        := unsafeDefn.type
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index aa9c2a87a2..e43d199f7d 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -388,6 +388,8 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
         if compile then
           -- Inline as changing visibility should not affect run time.
           setInlineAttribute name
+          if (← read).declName?.any (isMarkedMeta (← getEnv)) then
+            modifyEnv (markMeta · name)
           compileDecls #[name]
         return e
     else
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index fcf18b4867..5289bd4dcc 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -76,7 +76,7 @@ inductive RecKind where
 /-- Codegen-relevant modifiers. -/
 inductive ComputeKind where
   | regular | «meta» | «noncomputable»
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Repr
 
 /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
diff --git a/src/Lean/Elab/ErrorExplanation.lean b/src/Lean/Elab/ErrorExplanation.lean
index f1f193f212..1eeaf0e61c 100644
--- a/src/Lean/Elab/ErrorExplanation.lean
+++ b/src/Lean/Elab/ErrorExplanation.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Widget.UserWidget
+meta import Lean.Widget.UserWidget
 
 public section
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 685534cb48..3f6e147999 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1073,6 +1073,8 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
         return if (← inferType c.toLift.type).isProp then .theorem else .def
     else
       pure kind
+    if modifiers.isMeta then
+      modifyEnv (markMeta · c.toLift.declName)
     return preDefs.push {
       ref         := c.ref
       declName    := c.toLift.declName
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 2df9ad63ff..35ddc5e7c9 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -217,9 +217,7 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
     -- Tags may have been added by `elabMutualDef` already, but that is not the only caller
     | .meta          => if !isMarkedMeta (← getEnv) preDef.declName then modifyEnv (markMeta · preDef.declName)
     | .noncomputable => if !isNoncomputable (asyncMode := .local) (← getEnv) preDef.declName then modifyEnv (addNoncomputable · preDef.declName)
-    | _              =>
-      if !preDef.kind.isTheorem then
-        modifyEnv (markNotMeta · preDef.declName)
+    | _              => pure ()
     if compile && shouldGenCodeFor preDef then
       compileDecl decl
     if applyAttrAfterCompilation then
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index efd87b21e3..d61fb08a11 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -289,7 +289,7 @@ builtin_initialize registerBuiltinAttribute {
 
 /-- Elaborate `register_try?_tactic` command -/
 @[builtin_command_elab registerTryTactic]
-meta def elabRegisterTryTactic : Command.CommandElab := fun stx => do
+def elabRegisterTryTactic : Command.CommandElab := fun stx => do
   if `Lean.Elab.Tactic.Try ∉ (← getEnv).header.moduleNames then
     logWarning "Add `import Lean.Elab.Tactic.Try` before using the `register_try?_tactic` command."
     return
diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean
index 822675a719..9c16eef506 100644
--- a/src/Lean/ErrorExplanation.lean
+++ b/src/Lean/ErrorExplanation.lean
@@ -10,6 +10,7 @@ prelude
 public import Lean.Message
 public import Lean.EnvExtension
 public import Lean.DocString.Links
+meta import Lean.Message
 
 public section
 
diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index 25794d312d..0c65bf92bf 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -91,19 +91,24 @@ public def mkCtorIdx (indName : Name) : MetaM Unit :=
       modifyEnv fun env => addProtected env declName
       if info.numCtors = 1 then
         setInlineAttribute declName .macroInline
+      if isMarkedMeta (← getEnv) indName then
+        modifyEnv (markMeta · declName)
       compileDecl decl
       enableRealizationsForConst declName
 
       -- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
       if (← isEnumType indName) then
         let aliasName := mkToCtorIdxName indName
-        addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
+        addDecl (.defnDecl (← mkDefinitionValInferringUnsafe
           (name        := aliasName)
           (levelParams := info.levelParams)
           (type        := declType)
           (value       := mkConst declName us)
           (hints       := ReducibilityHints.abbrev)
         ))
+        if isMarkedMeta (← getEnv) indName then
+          modifyEnv (markMeta · aliasName)
+        compileDecls #[aliasName]
         modifyEnv fun env => addToCompletionBlackList env aliasName
         modifyEnv fun env => addProtected env aliasName
         setReducibleAttribute aliasName
diff --git a/src/Lean/Meta/Eval.lean b/src/Lean/Meta/Eval.lean
index ed02776c90..0d80e6be2d 100644
--- a/src/Lean/Meta/Eval.lean
+++ b/src/Lean/Meta/Eval.lean
@@ -23,7 +23,8 @@ unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit)
     if value.getUsedConstants.all (← getEnv).isImportedConst then
       modifyEnv fun env => env.importEnv?.getD env
 
-    let name ← mkFreshUserName `_tmp
+    -- Private name to ensure we do not check for deps being imported publicly
+    let name := mkPrivateName (← getEnv) (← mkFreshUserName `_tmp)
     let value ← instantiateMVars value
     let us := collectLevelParams {} value |>.params
     if value.hasMVar then
@@ -35,12 +36,14 @@ unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit)
        value, hints := ReducibilityHints.opaque,
        safety
     }
+    modifyEnv (markMeta · name)
     -- compilation will invariably wait on `checked`
     let _ ← traceBlock "compiler env" (← getEnv).checked
     -- now that we've already waited, async would just introduce (minor) overhead and trigger
     -- `Task.get` blocking debug code
     withOptions (Elab.async.set · false) do
     withOptions (Compiler.compiler.postponeCompile.set · false) do
+    withOptions (Compiler.compiler.relaxedMetaCheck.set · true) do
       addAndCompile decl
       evalConst (checkMeta := checkMeta) α name
 
diff --git a/src/Lean/Meta/Native.lean b/src/Lean/Meta/Native.lean
index 8c167e9630..13a36c9408 100644
--- a/src/Lean/Meta/Native.lean
+++ b/src/Lean/Meta/Native.lean
@@ -51,11 +51,13 @@ public def nativeEqTrue (tacticName : Name) (e : Expr) (axiomDeclRange? : Option
       hints := .abbrev
       safety := .safe
     }
+    modifyEnv (markMeta · auxDeclName)
     try
       -- disable async/separate codegen so we can catch its exceptions; we don't want to report
       -- `evalConst` failures below when the actual reason was a codegen failure
       withOptions (Elab.async.set · false) do
       withOptions (Compiler.compiler.postponeCompile.set · false) do
+      withOptions (Compiler.compiler.relaxedMetaCheck.set · true) do
         addAndCompile decl
     catch ex =>
       throwError m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
diff --git a/src/Lean/Meta/Tactic/Grind/CheckResult.lean b/src/Lean/Meta/Tactic/Grind/CheckResult.lean
index b6bd8adebe..f28434e2e4 100644
--- a/src/Lean/Meta/Tactic/Grind/CheckResult.lean
+++ b/src/Lean/Meta/Tactic/Grind/CheckResult.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Data.Repr
-import Init.MetaTypes  -- shake: keep (dependency of `simp +decide`, fix)
+meta import Init.MetaTypes  -- shake: keep (dependency of `simp +decide`, fix)
 public section
 namespace Lean.Meta.Grind
 /--
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index b2a1dedbdb..e05435a849 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -9,6 +9,7 @@ prelude
 import Lean.Server.CodeActions
 import Lean.Meta.Tactic.ExposeNames
 public import Lean.Widget.UserWidget
+meta import Lean.Widget.UserWidget
 
 public section
 
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index d364ed1f69..18f65ea806 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -8,6 +8,8 @@ module
 prelude
 public import Lean.Parser.Do
 import Lean.DocString.Parser
+meta import Lean.Parser.Do
+meta import Lean.DocString.Parser
 
 public section
 
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index 61d8f4e236..024a5c10df 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Parser.Module.Syntax
 meta import Lean.Parser.Module.Syntax
 import Init.While
+meta import Lean.Parser.Extra
 
 public section
 
diff --git a/src/Lean/Parser/Term/Basic.lean b/src/Lean/Parser/Term/Basic.lean
index 9d4882ccd9..a0d7ffe4ba 100644
--- a/src/Lean/Parser/Term/Basic.lean
+++ b/src/Lean/Parser/Term/Basic.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Parser.Attr
 public import Lean.Parser.Level
 public import Lean.Parser.Term.Doc
+meta import Lean.Parser.Basic
 
 /-!
 This module contains the bare minimum of term syntax that's required to get documentation syntax to
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 5738a3c928..b627ee43a4 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -12,6 +12,7 @@ public import Lean.Meta.Structure
 public import Lean.PrettyPrinter.Formatter
 public import Lean.PrettyPrinter.Parenthesizer
 meta import Lean.Parser.Command
+meta import Lean.PrettyPrinter.Delaborator.DeclWithSig
 
 public section
 
@@ -1547,11 +1548,6 @@ def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExp
   else
     withOverApp 2 `(sorry)
 
-open Parser Command Term in
-@[run_builtin_parser_attribute_hooks]
--- use `termParser` instead of `declId` so we can reuse `delabConst`
-private meta def declSigWithId := leading_parser termParser maxPrec >> declSig
-
 private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax :=
   env.evalConstCheck Syntax opts ``Syntax constName
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/DeclWithSig.lean b/src/Lean/PrettyPrinter/Delaborator/DeclWithSig.lean
new file mode 100644
index 0000000000..9cbb426675
--- /dev/null
+++ b/src/Lean/PrettyPrinter/Delaborator/DeclWithSig.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich, Leonardo de Moura, Gabriel Ebner, Mario Carneiro
+-/
+module
+
+prelude
+public import Lean.Parser.Types
+import Lean.Parser.Command
+
+namespace Lean.PrettyPrinter.Delaborator
+
+open Parser Command Term
+
+@[run_builtin_parser_attribute_hooks]
+-- use `termParser` instead of `declId` so we can reuse `delabConst`
+public def declSigWithId : Parser := leading_parser termParser maxPrec >> declSig
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 5fb7b7587d..1afc0f3e0c 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -125,7 +125,7 @@ def registerRpcProcedure (method : Name) : CoreM Unit := do
     let stx ← ``(wrapRpcProcedure $(quote method) _ _ $(mkIdent method))
     let c ← Lean.Elab.Term.elabTerm stx procT
     instantiateMVars c
-  addAndCompile <| Declaration.defnDecl {
+  let decl := Declaration.defnDecl {
         name        := wrappedName
         type        := procT
         value       := proc
@@ -133,6 +133,9 @@ def registerRpcProcedure (method : Name) : CoreM Unit := do
         levelParams := []
         hints := ReducibilityHints.opaque
       }
+  addDecl decl
+  modifyEnv (markMeta · wrappedName)
+  compileDecl decl
   setEnv <| userRpcProcedures.insert (← getEnv) method wrappedName
 
 builtin_initialize registerBuiltinAttribute {
diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean
index 5cd039e45e..656c991fab 100644
--- a/src/lake/Lake/Build/Trace.lean
+++ b/src/lake/Lake/Build/Trace.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Data.Json
 import Init.Data.Nat.Fold
+meta import Init.Data.Nat.Fold
 import Lake.Util.String
 public import Init.Data.String.Search
 public import Init.Data.String.Extra
diff --git a/tests/elab/string.lean b/tests/elab/string.lean
index 636cb2062f..9cdee9b1b6 100644
--- a/tests/elab/string.lean
+++ b/tests/elab/string.lean
@@ -1,5 +1,7 @@
 module
 
+meta import Init.Data.String
+
 /-!
 # Tests for `String` functions
 -/
diff --git a/tests/elab/string_slice.lean b/tests/elab/string_slice.lean
index a9b32ee473..fe0e0387e5 100644
--- a/tests/elab/string_slice.lean
+++ b/tests/elab/string_slice.lean
@@ -1,5 +1,5 @@
 module
-import Std.Data.HashSet.Basic
+meta import Std.Data.HashSet.Basic
 
 /-!
 Tests for `String.Slice` functions