What the widening lane changed, kept, and measured

FIX.org

@@ -2570,3 +2570,86 @@ constant and ~(* w h)~ is — which means dropping a cast that widening made
 unnecessary can turn a run-time computation into an array length. That is
 widening adding a program, the same as everywhere else, and needed no change
 here.
+
+** No overload resolution to disturb
+Worth saying plainly, because widening is exactly the change that breaks
+overloading in a language that has it: this one does not. Every builtin is
+dispatched by *name* in ~named_call~ — there is no set of candidates to pick
+between, so widening cannot change which one fires and cannot make a call
+ambiguous. ~min~/~max~ and the arithmetic builtins looked like they keyed on
+types, and what they actually do is check a predicate (~ordered?~,
+~numeric?~) against the type the operands already agreed on. Widening changes
+what they agree on and nothing about the dispatch.
+
+** Sites changed, and sites kept
+Changed, three of them and no more:
+- lib/types.ml — ~widens_to~ and ~join~, new. ~equal~ and ~fits~ untouched.
+- ~Check.expect~ — one arm, which is the entire annotation surface.
+- ~Check.binary~ — the join, and ~~join:false~ for the shifts.
+
+Kept, with the message saying *narrowing* rather than "no conversions":
+- ~Check.unbox~'s per-width refusal at the dyn boundary. A dyn carries one
+  integer width and one float width, so there is no narrower source to widen
+  from and nothing on the lattice reaches it; what it refuses is a truncation
+  at the one boundary where the value's type was already uncertain, and that
+  is as true as it was.
+- Every numeric refusal that survives ~expect~ now carries ~numeric_note~,
+  which tells the two surviving cases apart: a narrowing names the cast and
+  points out that the other direction is free, and an equal-width cross-signed
+  pair is told that neither direction exists.
+
+Comments rewritten rather than left to rot, each now stating the new invariant
+rather than the old one: lib/types.ml's header, ~equal~'s note (why widening
+is deliberately *not* a loosening of it), ~Check.unbox~, ~Check.binary~, the
+bitwise and shift arms, the ~embed~ two-spellings argument (which turns out
+never to have rested on widening at all — it rests on containers not
+converting), lib/prelude.ml's ~print~ note and both ~sum-~ notes,
+docs/BUILT.md's ~gravity~ and ~#load~ paragraphs, test/programs/embed.flan,
+and the ~+~, ~bit-and~, ~<<~, ~>>~ and ~min~ lines of the ~builtins~ table.
+Left alone: docs/SPIKE-*.md and docs/handoffs/*, which are dated records of
+what was true when they were written.
+
+** What was run
+- ~dune test --root .~ — 0 FAIL lines, every suite reporting passed. It exits
+  1, and it exits 1 on an untouched worktree at dev-loop's tip for the same
+  reason: ~test_dev.ml~'s ~trap_park~ rows race and die with
+  ~Fatal error: exception Flan.Wire.Closed~ at ~dev-trap-null-alloc~. Measured
+  on both sides this lane, and already written up above under "Found while
+  running it".
+- test/programs/widening.flan, new, with three acceptance rows — default, -O0
+  and ~--x86~ — and its output diffed by hand across the two backends before
+  the rows were written. Byte-identical.
+- The lattice's edges pinned in test_flan.ml: what widens, what does not, the
+  two calls that could have gone the other way (int-into-float exact-only, and
+  equal-width cross-signedness), container invariance, the join in both
+  operand orders, the literal rule still standing, and the shift carve-out in
+  both directions.
+- *The corpus sweep, base against lane.* Headless programs (test/programs/)
+  were compiled, ~check~ed and run, and the diff of the whole lot is a single
+  pure addition: widening.flan's own rows. Not one existing program's
+  diagnostics, output or exit status moved.
+
+  examples/ were *not run*. They link raylib and every one of them opens a
+  real window on the author's desktop, so the comparison there is ~check~'s
+  exit status and diagnostics plus a byte-diff of ~emit~ and ~emit --x86~.
+  LLVM output is byte-identical for all of them. The x86 output differs in 28
+  of them and every differing byte is inside a ~<prelude>:line:col~ string —
+  this lane's comment rewrites moved prelude source lines by three, and the
+  x86 backend spells those strings out as ~.byte~ data. Normalising the
+  prelude line number makes both backends byte-identical everywhere.
+- A global-initialiser check by hand, both backends: a widened ~defvar~
+  initialiser, a widened struct field in a struct literal, a widened array
+  element, and a widened ~set~. The concern was that a ~Cast~ in an
+  initialiser would stop being an LLVM constant; it does not, and the two
+  backends print the same six lines. A ~defconst~ of a float *from* an integer
+  constant is refused, with the existing "must be a compile-time constant"
+  sentence — the folder is integers-only and says so.
+
+** What this lane did not do
+- ~dyn~ is untouched in both directions.
+- No ~Vec~, slice or array element type converts, and nothing was added that
+  could make one.
+- The ~@x86~ and ~@sanitize~ sweeps were not run; per the sweep policy they
+  belong to the batch after several lanes land. The individual ~--x86~ builds
+  the policy does require were run, and are the acceptance row and the sweep
+  above.