From 78ba71a35e4221a0f06ec9ac084cc94fd6445240 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 14:56:58 -0400
Subject: [PATCH 1/9] chore: move trace message

---
 ImportGraph/Shake/DeclNeeds.lean | 2 ++
 ImportGraph/Shake/Workspace.lean | 2 --
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/ImportGraph/Shake/DeclNeeds.lean b/ImportGraph/Shake/DeclNeeds.lean
index 6b7aec2..3fa2921 100644
--- a/ImportGraph/Shake/DeclNeeds.lean
+++ b/ImportGraph/Shake/DeclNeeds.lean
@@ -828,3 +828,5 @@ def withElabCommandCapturingNeeds (cmd : Syntax.Command) :
     declNeeds ← declNeeds.calcSyntaxNeeds env newDecls cmd
     declNeeds ← liftCoreM <| declNeeds.calcIRNeeds.run'
     return (declNeeds, newDecls)
+
+initialize registerTraceClass `ImportGraph.Shake
diff --git a/ImportGraph/Shake/Workspace.lean b/ImportGraph/Shake/Workspace.lean
index c4b816b..85d54b0 100644
--- a/ImportGraph/Shake/Workspace.lean
+++ b/ImportGraph/Shake/Workspace.lean
@@ -109,5 +109,3 @@ def ImportNeeds.providersByLib (w : WorkspaceModel) (needs : ImportNeeds)
       |>.then (compare pᵢ.size pⱼ.size)
       |>.then (Name.cmp (w.getMod! i).name (w.getMod! j).name) -- for stability if all else fails
       |>.isLT).map (·.1)
-
-initialize registerTraceClass `ImportGraph.Shake

From 63a5de966bc203864aede67b82207585046cdfbc Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:03:13 -0400
Subject: [PATCH 2/9] chore: change name

---
 ImportGraph/Shake/DeclNeeds.lean | 3 +--
 ImportGraph/Tools/FindHome.lean  | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/ImportGraph/Shake/DeclNeeds.lean b/ImportGraph/Shake/DeclNeeds.lean
index 3fa2921..05a0594 100644
--- a/ImportGraph/Shake/DeclNeeds.lean
+++ b/ImportGraph/Shake/DeclNeeds.lean
@@ -798,8 +798,7 @@ open Lean Elab Command in
 /-- Elaborates the command and captures the `DeclNeeds` of all new declarations. Attaches the needs
 implied by the command's syntax to each new declaration. Note: does **not** capture extra rev mod
 uses influencing the file as a whole. -/
-def withElabCommandCapturingNeeds (cmd : Syntax.Command) :
-    CommandElabM (DeclNeeds × Array Name) := do
+def elabCommandCapturingNeeds (cmd : Syntax.Command) : CommandElabM (DeclNeeds × Array Name) := do
   withFreshShakeRecords do
     let oldEnv ← getEnv
     elabCommand cmd
diff --git a/ImportGraph/Tools/FindHome.lean b/ImportGraph/Tools/FindHome.lean
index fcd88dc..d0c3760 100644
--- a/ImportGraph/Tools/FindHome.lean
+++ b/ImportGraph/Tools/FindHome.lean
@@ -113,7 +113,7 @@ elab_rules : command
       {m!"\n\n".joinSep (w.errors.map toMessageData |>.toList)}"
 
   -- Elaborate command and capture new decls and decl needs
-  let (declNeeds, newDecls) ← withElabCommandCapturingNeeds cmd
+  let (declNeeds, newDecls) ← elabCommandCapturingNeeds cmd
   if ← MonadLog.hasErrors then -- Also stop if the command produced errors
     return
   unless (← getEnv).header.isModule do

From 44e9eedc4d12bd6214d866fe18f42ef514f047ec Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:03:21 -0400
Subject: [PATCH 3/9] .

---
 ImportGraph/Shake/DeclNeeds.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ImportGraph/Shake/DeclNeeds.lean b/ImportGraph/Shake/DeclNeeds.lean
index 05a0594..be0f31c 100644
--- a/ImportGraph/Shake/DeclNeeds.lean
+++ b/ImportGraph/Shake/DeclNeeds.lean
@@ -31,7 +31,7 @@ Note that, crucially, `DeclNeeds` is agnostic to the source of our import hierar
 module names instead of e.g. `ModuleIdx`s/`ModIdx`s. Hence these functions are compatible with both
 a `WorkspaceModel` approach and an `Environment` approach.
 
-This file culminates in `withElabCommandCapturingNeeds`, which elaborates a command and captures
+This file culminates in `elabCommandCapturingNeeds`, which elaborates a command and captures
 the (transitive) `DeclNeeds` of declarations produced in that command, including e.g. the needs
 implied by the command's syntax.
 

From f31ed5203f3f8eee114fe807aae84044b635e22b Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:03:33 -0400
Subject: [PATCH 4/9] feat: messagedata

---
 ImportGraph/Shake/DeclNeeds.lean | 69 +++++++++++++++++++++++++++++---
 1 file changed, 64 insertions(+), 5 deletions(-)

diff --git a/ImportGraph/Shake/DeclNeeds.lean b/ImportGraph/Shake/DeclNeeds.lean
index be0f31c..6481864 100644
--- a/ImportGraph/Shake/DeclNeeds.lean
+++ b/ImportGraph/Shake/DeclNeeds.lean
@@ -337,6 +337,14 @@ inductive ComptimeDependency where
   stx (kind : SyntaxNodeKind) (pos? : Option Syntax.Range) -- TODO: just record syntax?
 deriving Inhabited, BEq, Repr, Hashable, Ord
 
+def ComptimeDependency.toMessageData : ComptimeDependency → MessageData
+  | .indirect { kind, declName } mods =>
+    m!"indirect({kind} for {.ofConstName declName} from {mods})"
+  | .stx kind pos? => m!"syntax({.ofConstName kind (fullNames := true)}\
+    {if let some pos := pos? then m!"@⟨{pos.start},{pos.stop}⟩" else ""})"
+
+instance : ToMessageData ComptimeDependency := ⟨(·.toMessageData)⟩
+
 /-- A location at which a `ConstantInfo` can reference another. -/
 inductive ConstLocation where | type | value
 deriving Inhabited, BEq, Repr, Hashable, Ord
@@ -392,15 +400,17 @@ deriving Inhabited, BEq, Repr, Hashable, Ord
 namespace DeclDeclNeedsKind
 
 /-- An English-language description of a `DeclDeclNeedsKind`. -/
-def pretty : DeclDeclNeedsKind → String
-  | .expr down reExported up => s!"uses {up} in {down}{
+def toMessageData : DeclDeclNeedsKind → MessageData
+  | .expr down reExported up => m!"{if up matches .type then "used" else s!"uses {up}"} in {down}{
     match reExported with
     | some true => " (public)"
     | some false => " (private)"
     | none => ""}"
   | .runtimeIR => "used in runtime IR"
   | .metaIR _ _ => "used in meta IR" -- TODO
-  | .comptime _ => "comptime dependency" -- TODO
+  | .comptime source => m!"{source}"
+
+instance : ToMessageData DeclDeclNeedsKind := ⟨(·.toMessageData)⟩
 
 /-- `some .comptime` if this demands the source declaration's `IRPhases` includes `.comptime`;
 `some .runtime` if this demands the source declaration's `IRPhases` includes `.runtime`. (`.all`
@@ -440,6 +450,19 @@ structure Stance where
 /-- Whether a `Stance` is not `isPublic`. -/
 @[expose, macro_inline, grind] public def Stance.isPrivate (s : Stance) := !s.isPublic
 
+def Stance.toString : Stance → String
+  | { isPublic, isExposed, isMeta, isExact, .. } =>
+    s!"{if isExact then "" else "(≥) "}\
+      {if let some isExposed := isExposed then
+        if isExposed then "@[expose] " else "@[no_expose] "
+      else ""}\
+      {if isPublic then "public" else "private"}\
+      {if let some isMeta := isMeta then
+        if isMeta then " meta" else " runtime"
+      else ""}"
+
+instance : ToString Stance := ⟨(·.toString)⟩
+
 /-- A set of declaration needs. -/
 /- TODO: make this more efficient, ideally a tiny `BitsetOf`, if such API were created. Also
 consider just a small `List` or `Array` that avoids duplication at insertion time. -/
@@ -453,7 +476,7 @@ structure DeclNeed where
   -- TODO: more efficient data structure?
   /-- Declarations whose location may not be altered. A map
   `[module name] ↦ [needs of declarations from that module]`. -/
-  fixedDecls : Std.TreeMap Name (NameMap DeclDeclNeedsKindSet) := {}
+  fixedDecls : NameMap (NameMap DeclDeclNeedsKindSet) := {}
   /--
   Extra module uses recorded in shake extensions during the command. Note that if several
   declarations were created during the command, the extra mod uses are the same among all of them.
@@ -466,6 +489,37 @@ structure DeclNeed where
   childDecls : List Name := []
 deriving Inhabited, Repr
 
+/-- Render a `NameMap` as `{ key₁ ↦ val₁, key₂ ↦ val₂, ... }`. -/
+private def NameMap.toMessageData (n : NameMap α) (f : α → MessageData)
+    (isConst := false) : MessageData :=
+  if n.isEmpty then "{}" else
+    let ns := n.toList.map fun (n, a) =>
+      m!"{if isConst then MessageData.ofConstName n else m!"{n}"} ↦ {f a}"
+    .bracket "{" ((m!"," ++ Format.line).joinSep ns) "}"
+
+def DeclNeed.toMessageData : DeclNeed → MessageData
+  | { freeDecls, fixedDecls, extraModUses, parentDecls, childDecls } => Id.run do
+    let mut msgs := #[]
+    unless freeDecls.isEmpty do
+      msgs := msgs.push m!"freeDecls := \
+        {NameMap.toMessageData freeDecls (m!"{·.toList.map (·.toMessageData)}") (isConst := true)}"
+    unless fixedDecls.isEmpty do
+      msgs := msgs.push m!"fixedDecls := \
+        {NameMap.toMessageData fixedDecls fun n =>
+          NameMap.toMessageData n (m!"{·.toList.map (·.toMessageData)}") (isConst := true)}"
+    unless extraModUses.isEmpty do
+      msgs := msgs.push m!"extraModUses := \
+        {NameMap.toMessageData extraModUses fun ks =>
+          m!"{ks.toList.map toString}"}"
+    unless parentDecls.isEmpty do
+      msgs := msgs.push m!"parentDecls := {parentDecls.map MessageData.ofConstName}"
+    unless childDecls.isEmpty do
+      msgs := msgs.push m!"parentDecls := {childDecls.map MessageData.ofConstName}"
+    if msgs.isEmpty then return "{}" else
+      return .bracket "{" ((m!"," ++ Format.line).joinSep msgs.toList) "}"
+
+instance : ToMessageData DeclNeed := ⟨(·.toMessageData)⟩
+
 /-- Records that the ambient declaration needs the declaration `decl` at availability `k`, where
 the module of `decl` is left free. -/
 @[inline] def DeclNeed.insertFreeDecl (k : DeclDeclNeedsKind) (decl : Name) (declNeed : DeclNeed) :
@@ -497,6 +551,11 @@ def DeclNeed.insertExtraModUses (extraModUses : List ExtraModUse) (declNeed : De
 -- TODO: more efficient data structure
 abbrev DeclNeeds := NameMap DeclNeed
 
+def DeclNeeds.toMessageData (needs : DeclNeeds) : MessageData :=
+  NameMap.toMessageData needs (·.toMessageData) (isConst := true)
+
+instance : ToMessageData DeclNeeds := ⟨(·.toMessageData)⟩
+
 @[inline] def DeclNeeds.insertAutoDeclLink (autoDecl parentDecl : Name) (declNeeds : DeclNeeds) :
     DeclNeeds :=
   declNeeds.alter autoDecl (fun need? =>
@@ -735,7 +794,7 @@ instead of being duplicated across different declarations. -/
 def DeclNeeds.calcSyntaxNeeds (env : Environment) (decls : Array Name) (cmd : Syntax)
     (declNeeds : DeclNeeds) : CommandElabM DeclNeeds := do
   trace[ImportGraph.Shake] "Calculating syntax needs for:\
-    {indentD <| toMessageData <| decls.map MessageData.ofConstName}"
+    {indentD m!"{decls.map MessageData.ofConstName}"}"
   let indirectModUses := indirectModUseExt.getState env
   let mut declNeeds := declNeeds
   for stx in cmd.topDown do

From 34c29c6bc71644ecf7502b6392ebc6896317ed0f Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:04:15 -0400
Subject: [PATCH 5/9] chore: fixups

---
 ImportGraph/Shake/Environment.lean | 2 +-
 ImportGraph/Shake/Workspace.lean   | 2 +-
 ImportGraph/Tools/FindHome.lean    | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/ImportGraph/Shake/Environment.lean b/ImportGraph/Shake/Environment.lean
index 6424fb7..6301c96 100644
--- a/ImportGraph/Shake/Environment.lean
+++ b/ImportGraph/Shake/Environment.lean
@@ -105,7 +105,7 @@ def toSimultaneousImportNeeds (env : Environment)
         let some usedStance ← getStance? usedDecl | continue
         let mut usedKs : DeclDeclNeedsKindSet := {}
         for k in ks do
-          trace[ImportGraph.Shake] "{k.pretty}"
+          trace[ImportGraph.Shake] "{k}"
           if usedKs.contains k then continue
           usedKs := usedKs.insert k
           if let .comptime <| .indirect _ mods := k then
diff --git a/ImportGraph/Shake/Workspace.lean b/ImportGraph/Shake/Workspace.lean
index 85d54b0..cdf6573 100644
--- a/ImportGraph/Shake/Workspace.lean
+++ b/ImportGraph/Shake/Workspace.lean
@@ -72,7 +72,7 @@ def DeclNeeds.toSimultaneousImportNeeds
           (fun _ => return m!"Uses decl `{.ofConstName usedDecl}`") do←
         let some usedStance ← getStance? usedDecl | continue
         for k in ks do
-          trace[ImportGraph.Shake] "{k.pretty}"
+          trace[ImportGraph.Shake] "{k}"
           if let .comptime <| .indirect _ mods := k then
             for modName in mods do
               let some modIdx := w.idxOfMod[modName]? | continue
diff --git a/ImportGraph/Tools/FindHome.lean b/ImportGraph/Tools/FindHome.lean
index d0c3760..7d45560 100644
--- a/ImportGraph/Tools/FindHome.lean
+++ b/ImportGraph/Tools/FindHome.lean
@@ -147,7 +147,7 @@ elab_rules : command
       let modName := w.getMod! modIdx |>.name
       let mut decls : NameSet := {}
       for (_, need) in declNeeds do
-        let some declsFromMod := need.fixedDecls[modName]? | continue
+        let some declsFromMod := need.fixedDecls.get? modName | continue
         decls := decls.insertMany declsFromMod.keysArray
       let declsArray := decls.toArray
       links := links.push <|← goToModuleOfDecls declsArray (fallbackModule := modName)

From 227269680cb8ba884518d2a3d664ff56981c028b Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:04:27 -0400
Subject: [PATCH 6/9] test: DeclNeeds basic tests

---
 ImportGraphTest/Shake/DeclNeeds.lean | 74 ++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 ImportGraphTest/Shake/DeclNeeds.lean

diff --git a/ImportGraphTest/Shake/DeclNeeds.lean b/ImportGraphTest/Shake/DeclNeeds.lean
new file mode 100644
index 0000000..269c357
--- /dev/null
+++ b/ImportGraphTest/Shake/DeclNeeds.lean
@@ -0,0 +1,74 @@
+module
+
+public meta import ImportGraph.Shake.Workspace
+public import Lean.Elab.Command
+
+import ImportGraphTest.Shake.Algebra
+
+open ImportGraph Shake Lean Elab Command
+
+elab "#show_decl_needs" colGe cmd:command : command => do
+  let (declNeeds, newDecls) ← elabCommandCapturingNeeds cmd
+  let w ← getWorkspaceModel (extraMods := #[← getMainModule])
+  let (importNeeds, stances) ← liftCoreM <| declNeeds.toSimultaneousImportNeeds w |>.run
+  let stanceMsg : MessageData := .bracket (l := "{") (r := "}") <|
+    (m!"," ++ Format.line).joinSep <|
+      stances.toList.mergeSort (·.1.cmp ·.1 |>.isLE) |>.map fun (n, s) =>
+        m!"{.ofConstName n} ↦ {match s with | some s => s.toString | _ => "none"}"
+  logInfo m!"\
+    New decls:{indentD (newDecls.toList.map MessageData.ofConstName)}\
+    \nNeeds:{indentD declNeeds.toMessageData}\
+    \nStances:{indentD stanceMsg}\
+    \nImportNeeds:{indentD <| importNeeds.toString}"
+
+/--
+info: New decls:
+  [x]
+Needs:
+  {x ↦ {fixedDecls := {Init.Prelude ↦ {true ↦ [used in value, used in runtime IR], Bool ↦ [used in type]}}}}
+Stances:
+  {Bool ↦ @[no_expose] public, x ↦ private runtime, true ↦ @[no_expose] public}
+ImportNeeds:
+  │⠒⠀│
+-/
+#guard_msgs in
+#show_decl_needs def x : Bool := true
+
+/--
+info: New decls:
+  [x']
+Needs:
+  {x' ↦ {fixedDecls := {Init.Prelude ↦ {true ↦ [used in value, used in runtime IR], Bool ↦ [used in type]}}}}
+Stances:
+  {Bool ↦ @[no_expose] public, x' ↦ public runtime, true ↦ @[no_expose] public}
+ImportNeeds:
+  │⠚⠀│
+-/
+#guard_msgs in
+#show_decl_needs public def x' : Bool := true
+
+/--
+info: New decls:
+  [x'']
+Needs:
+  {x'' ↦ {fixedDecls := {Init.Prelude ↦ {true ↦ [used in value, used in runtime IR], Bool ↦ [used in type]}}}}
+Stances:
+  {Bool ↦ @[no_expose] public, x'' ↦ @[expose] public runtime, true ↦ @[no_expose] public}
+ImportNeeds:
+  │⠊⠀│
+-/
+#guard_msgs in
+#show_decl_needs @[expose] public def x'' : Bool := true
+
+/--
+info: New decls:
+  [x''']
+Needs:
+  {x''' ↦ {fixedDecls := {Init.Prelude ↦ {true ↦ [used in value], Bool ↦ [used in type]}}}}
+Stances:
+  {Bool ↦ @[no_expose] public, x''' ↦ @[expose] public, true ↦ @[no_expose] public}
+ImportNeeds:
+  │⠈⠀│
+-/
+#guard_msgs in
+#show_decl_needs @[expose] public noncomputable def x''' : Bool := true

From 46c0d89fc17d11fc63c29a80011f7a82984ba6cb Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:06:22 -0400
Subject: [PATCH 7/9] Revert "chore: change name"

This reverts commit 63a5de966bc203864aede67b82207585046cdfbc.
---
 ImportGraph/Shake/DeclNeeds.lean | 3 ++-
 ImportGraph/Tools/FindHome.lean  | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/ImportGraph/Shake/DeclNeeds.lean b/ImportGraph/Shake/DeclNeeds.lean
index 6481864..4683241 100644
--- a/ImportGraph/Shake/DeclNeeds.lean
+++ b/ImportGraph/Shake/DeclNeeds.lean
@@ -857,7 +857,8 @@ open Lean Elab Command in
 /-- Elaborates the command and captures the `DeclNeeds` of all new declarations. Attaches the needs
 implied by the command's syntax to each new declaration. Note: does **not** capture extra rev mod
 uses influencing the file as a whole. -/
-def elabCommandCapturingNeeds (cmd : Syntax.Command) : CommandElabM (DeclNeeds × Array Name) := do
+def withElabCommandCapturingNeeds (cmd : Syntax.Command) :
+    CommandElabM (DeclNeeds × Array Name) := do
   withFreshShakeRecords do
     let oldEnv ← getEnv
     elabCommand cmd
diff --git a/ImportGraph/Tools/FindHome.lean b/ImportGraph/Tools/FindHome.lean
index 7d45560..33f6e25 100644
--- a/ImportGraph/Tools/FindHome.lean
+++ b/ImportGraph/Tools/FindHome.lean
@@ -113,7 +113,7 @@ elab_rules : command
       {m!"\n\n".joinSep (w.errors.map toMessageData |>.toList)}"
 
   -- Elaborate command and capture new decls and decl needs
-  let (declNeeds, newDecls) ← elabCommandCapturingNeeds cmd
+  let (declNeeds, newDecls) ← withElabCommandCapturingNeeds cmd
   if ← MonadLog.hasErrors then -- Also stop if the command produced errors
     return
   unless (← getEnv).header.isModule do

From aa844f51b01dcd9c57e79831bec6a0a9fb4bf506 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:06:33 -0400
Subject: [PATCH 8/9] Revert "."

This reverts commit 44e9eedc4d12bd6214d866fe18f42ef514f047ec.
---
 ImportGraph/Shake/DeclNeeds.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ImportGraph/Shake/DeclNeeds.lean b/ImportGraph/Shake/DeclNeeds.lean
index 4683241..13ddd68 100644
--- a/ImportGraph/Shake/DeclNeeds.lean
+++ b/ImportGraph/Shake/DeclNeeds.lean
@@ -31,7 +31,7 @@ Note that, crucially, `DeclNeeds` is agnostic to the source of our import hierar
 module names instead of e.g. `ModuleIdx`s/`ModIdx`s. Hence these functions are compatible with both
 a `WorkspaceModel` approach and an `Environment` approach.
 
-This file culminates in `elabCommandCapturingNeeds`, which elaborates a command and captures
+This file culminates in `withElabCommandCapturingNeeds`, which elaborates a command and captures
 the (transitive) `DeclNeeds` of declarations produced in that command, including e.g. the needs
 implied by the command's syntax.
 

From 6ea618a0a28f44df754c66696dcdadf426c379ee Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 28 Sep 2026 15:08:23 -0400
Subject: [PATCH 9/9] chore: change name back

---
 ImportGraphTest/Shake/DeclNeeds.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ImportGraphTest/Shake/DeclNeeds.lean b/ImportGraphTest/Shake/DeclNeeds.lean
index 269c357..324ace6 100644
--- a/ImportGraphTest/Shake/DeclNeeds.lean
+++ b/ImportGraphTest/Shake/DeclNeeds.lean
@@ -8,7 +8,7 @@ import ImportGraphTest.Shake.Algebra
 open ImportGraph Shake Lean Elab Command
 
 elab "#show_decl_needs" colGe cmd:command : command => do
-  let (declNeeds, newDecls) ← elabCommandCapturingNeeds cmd
+  let (declNeeds, newDecls) ← withElabCommandCapturingNeeds cmd
   let w ← getWorkspaceModel (extraMods := #[← getMainModule])
   let (importNeeds, stances) ← liftCoreM <| declNeeds.toSimultaneousImportNeeds w |>.run
   let stanceMsg : MessageData := .bracket (l := "{") (r := "}") <|