Accessing `Expr` of a def across modules

Stream: lean4

[Snir Broshi]

module
import Lean.Elab.Term
open Lean

run_elab do
  let env ← getEnv
  let k : SyntaxNodeKind := `Lean.Parser.Tactic.exact
  if let some constantInfo := env.find? k then
    match constantInfo with
    | .axiomInfo _ => logInfo m!"axiomInfo"
    | .defnInfo _ => logInfo m!"defnInfo"
    | .thmInfo _ => logInfo m!"thmInfo"
    | .opaqueInfo _ => logInfo m!"opaqueInfo"
    | .quotInfo _ => logInfo m!"quotInfo"
    | .inductInfo _ => logInfo m!"inductInfo"
    | .ctorInfo _ => logInfo m!"ctorInfo"
    | .recInfo _ => logInfo m!"recInfo"
    logInfo m!"Has expr: {constantInfo.value?.isSome}"

This prints axiomInfo and Has expr: false, and after removing the module line it prints defnInfo and Has expr: true.
Is this a bug, or an intended feature of the module system? I know the module system can be used to avoid @[expose]ing defs, but I expected opaqueInfo if it was the problem. Why axiomInfo?

The context is that Batteries' #help is currently broken in modules:

module
import Batteries

/-- error: no tactic declarations start with exact -/
#guard_msgs in
#help tactic exact

It gets ConstantInfos from the environment then extracts the first token of their syntax using the Expr.
Is there a way to fix it or is #help in modules fundamentally broken?
Perhaps all the tactics just need to be @[expose]d?

[Robin Arnez]

Well, opaqueInfo wouldn't work because OpaqueVal still contains a value and the whole premise of @[no_expose] is that you don't get the value by default in imported modules (to avoid needing the memory for that and to avoid build dependencies). Now, when you have an axiom and want to find out what it originally was, you can use docs#Lean.getOriginalConstKind?. This will obviously not help you at all in fixing #help though, for that you can use docs#Lean.Parser.mkParserOfConstant:

import Mathlib

open Lean Parser
run_meta
  let cat := `term
  let categories := (parserExtension.getState (← getEnv)).categories
  let some category := categories.find? cat | throwError "non-existent category {cat}"
  for (kind, _) in category.kinds do
    let (leading, parser) ← Lean.Parser.mkParserOfConstant categories kind
    IO.println s!"{if leading then "leading" else "trailing"} parser {kind}: {parser.info.firstTokens}"