The one caller of ~hidden is named, and the pair it must never form is refused

Emit.program ~hidden and ~dev are opposites: a dev build exports its cells,
globals and flan.abi.* so that a redefinition module can bind against them, and
hiding those would give a host that links, runs and silently installs nothing.
Nothing in the types stopped the combination being written, so it fails with a
sentence instead. Build.macro_module is the only caller that asks for hidden and
it never asks for dev.

The handoff's verification is narrowed to what it actually covers: the 540-file
IR diff is about Emit.program's default, and the new path is read off nm -D on
the linked module. It also now says why sand-headless.flan is the fixture that
checks 65d14f4 -- it reaches rl/with-drawing through an import, which is the
package-macro shape the reproduced bug had.

docs/handoffs/HANDOFF-x86-macro-visibility.md

@@ -91,6 +91,13 @@ is what it was. Item by item, with what says so:
 The one thing that did change is stated in §The correction above, and it changed *back*: the macro module's
 calls into the C runtime bind to the host's copy again, as they did before 65d14f4.
 
+**The invariant that keeps it that way: `~hidden:true` is passed by exactly one caller, `Build.macro_module`,
+and it never passes `~dev`.** `Emit.program` refuses the pair outright now, because nothing in the types stops
+someone writing it and the consequence would be a merged host that links, runs, and silently installs nothing:
+a dev build's cells, globals and `flan.abi.*` marker are in the dynamic symbol table *on purpose*, for a
+redefinition module to bind against. The other four call sites (`Build.executable`, `Dev.merged_executable`,
+`bin/main.ml`'s `emit`, and the tests) take the default.
+
 ## Verification
 
 | | before (`9e80147`) | after |
@@ -103,8 +110,13 @@ calls into the C runtime bind to the host's copy again, as they did before 65d14
 **The IR comparison is how "the LLVM path did not move" was verified, and it is the check worth repeating.**
 Every `test/programs/*.flan` plus `sand.flan` and `calc-me.flan`, emitted twice — once release, once `--dev` —
 by the compiler at `9e80147` and by this one: 540 files, `diff -rq` reports nothing. `hidden` defaults to
-`false` and the only other edit to a format string adds an empty interpolation, so this is the argument made
+`false` and the only other edit to a format string adds an empty interpolation, so for those two paths this is
-mechanical rather than a sample.
+the argument made mechanical rather than a sample.
+
+Be clear about what that diff does *not* say: it covers `Emit.program`'s default, which is every path but the
+new one. `macro_module` deletes its `.ll` unless `opts.keep`, so the `hidden:true` output is not in it. What
+stands behind the new path is `nm -D` on the linked object above — three thunks and nothing else of Flan's,
+which is the property being claimed, read off the artefact rather than off the text that made it.
 
 `spike/x86/survey.sh` was **not** run here — it is forty minutes and this lane changes no lowering. It will
 report one more `runs-forever` when it next runs: `dev-macro.flan` waits on an agent that is not there, which
@@ -112,9 +124,12 @@ is what `dev-loop.flan` and `dev-repl.flan` already do.
 
 The two properties that had to hold together, in one run each:
 
-- **LLVM merged, `sand-headless.flan`.** Its package is `sand.flan`, which calls `rl/with-drawing`. If hidden
+- **LLVM merged, `sand-headless.flan`.** This is the one that checks 65d14f4, and the fixture is chosen for
-  visibility did not cover 65d14f4's bug, the daemon would have died with the checker refusing an unqualified
+  it: `sand-headless.flan` imports `sand.flan` as a package, `sand.flan` imports `vendor:raylib` and calls
-  `begin-drawing`. It came up and ran.
+  `rl/with-drawing` — a *package's* `defmacro`, reached through an import, which is exactly the shape the
+  reproduced bug had. A prelude macro would not have covered it, because the prelude's macros are not the ones
+  whose bodies were qualified after the quasiquote became a literal. If hidden visibility did not cover that
+  bug the daemon would have died with the checker refusing an unqualified `begin-drawing`. It came up and ran.
 - **`--x86` merged, same program.** Both runs print the same grid hash, `15595743031174623232`, which is the
   simulation having produced identical output through two backends in a process that also expanded macros.
 

lib/emit.ml

@@ -2971,6 +2971,18 @@ let macro_thunk m (fn : Tast.fn) =
 let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = [])
       ?(sanitize = false) ?(macros = []) ?(hidden = false)
       (p : Tast.program) : string =
+  (* [hidden] and [dev] are opposites and the refusal is here so that they
+     cannot be written together by accident. A dev build's whole point is that
+     its cells, its globals and [flan.abi.*] are in the dynamic symbol table
+     for a redefinition module to bind against; hiding them would leave a host
+     that links, runs, and silently installs nothing. There is no such thing as
+     a reloadable macro module, so nothing is lost by saying so out loud. *)
+  if hidden && dev then
+    failwith
+      "Emit.program ~hidden ~dev: a dev build exports its cells so that a \
+       redefinition module can reach them, and hiding them would break every \
+       reload. [hidden] is the macro module's flag and a macro module is not a \
+       dev build.";
   let m = new_module ~checks ~dev ~known:(fun _ -> true) ~debug ~sanitize p in
   (* One cell per function, initialised to the function this build compiled.
      Nothing has been redefined yet, so a dev build starts out behaving exactly