feat: message kinds

src/Lean/Elab/Command.lean

@@ -214,7 +214,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
+    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
     log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
   return log
 

src/Lean/Message.lean

@@ -116,7 +116,7 @@ variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
 is true.
 
-This does not descend into lazily generated subtress (`.ofLazy`); message tags
+This does not descend into lazily generated subtrees (`.ofLazy`); message tags
 of interest (like those added by `logLinter`) are expected to be near the root
 of the `MessageData`, and not hidden inside `.ofLazy`.
 -/
@@ -130,6 +130,19 @@ partial def hasTag : MessageData → Bool
   | trace data msg msgs     => p data.cls || hasTag msg || msgs.any hasTag
   | _                       => false
 
+/--
+Returns the top-level tag of the message.
+If none, returns `Name.anonymous`.
+
+This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
+The message kind is expected to describe the whole message.
+-/
+def kind : MessageData → Name
+  | withContext _ msg       => kind msg
+  | withNamingContext _ msg => kind msg
+  | tagged n _              => n
+  | _                       => .anonymous
+
 /-- An empty message. -/
 def nil : MessageData :=
   ofFormat Format.nil
@@ -307,8 +320,9 @@ structure BaseMessage (α : Type u) where
   endPos        : Option Position := none
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
-  severity      : MessageSeverity := MessageSeverity.error
+  severity      : MessageSeverity := .error
   caption       : String          := ""
+
   /-- The content of the message. -/
   data          : α
   deriving Inhabited, ToJson, FromJson
@@ -320,7 +334,10 @@ abbrev Message := BaseMessage MessageData
 /-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
 serialized and is thus appropriate for use in pure contexts where the effectful
 `MessageData.toString` cannot be used. -/
-abbrev SerialMessage := BaseMessage String
+structure SerialMessage extends BaseMessage String where
+  /-- The message kind (i.e., the top-level tag). -/
+  kind          : Name := .anonymous
+  deriving ToJson, FromJson
 
 namespace SerialMessage
 
@@ -346,8 +363,11 @@ end SerialMessage
 
 namespace Message
 
+abbrev kind (msg : Message) :=
+  msg.data.kind
+
 @[inline] def serialize (msg : Message) : IO SerialMessage := do
-  return {msg with data := ← msg.data.toString}
+  return {msg with kind := msg.kind, data := ← msg.data.toString}
 
 protected def toString (msg : Message) (includeEndPos := false) : IO String := do
   -- Remark: The inline here avoids a new message allocation when `msg` is shared

tests/lean/run/messageKind.lean

@@ -0,0 +1,26 @@
+import Lean.Elab.Command
+
+open Lean Elab Command
+
+elab tk:"#guard_msg_kind " kind:ident " in " cmd:command : command => do
+  let initMsgs ← modifyGet fun st => (st.messages, {st with messages := {}})
+  elabCommandTopLevel cmd
+  let msgs ← modifyGet fun st => (st.messages, {st with messages := initMsgs})
+  let kind := kind.getId
+  for msg in msgs.toList do
+    if msg.kind != kind then
+      logErrorAt tk s!"expected {kind}, got {msg.kind}"
+
+/- Test inferring kind from a tag. -/
+#guard_msg_kind custom in
+run_cmd do logInfo <| .tagged `custom ""
+
+/- Test trace message kind. -/
+#guard_msg_kind trace in
+set_option trace.Elab.step true in
+def trace := ()
+
+/- Test linter kind. -/
+#guard_msg_kind linter.unusedVariables in
+#guard_msgs (info) in -- hack to avoid re-triggering the linter
+def unused (x : Unit) := ()