From 080d294bc9e2dd6e8753c29dc1143014f1acab70 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:08:16 +0700
Subject: [PATCH 01/17] The lattice of conversions that cannot change the
 number

---
 FIX.org      | 121 +++++++++++++++++++++++++++++++++++++++++++++++++++
 lib/types.ml |  67 +++++++++++++++++++++++++---
 2 files changed, 183 insertions(+), 5 deletions(-)

diff --git a/FIX.org b/FIX.org
index 9cdda86..d65d942 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2442,3 +2442,124 @@ failures were that row and the sixth was ~dev-trap-free-all~, so what is racy
 is ~trap_park~ itself and every row that calls it — which is exactly what the
 mechanism described there predicts. Per the sweep policy the ~@x86~ and
 ~@sanitize~ sweeps were not run here.
+* Implicit widening, 2026-09-20 — "go with C"
+Answers DISCUSS.org's *implicit numeric conversions with a warning flag,
+instead of hard errors*. The ask there was a warn-instead-of-refuse mode; the
+answer is narrower and needs no mode and no flag.
+
+*The decision.* Implicit numeric *widening* is legal — every conversion that
+cannot change the number. *Narrowing stays a hard error everywhere*, with no
+flag that turns it into a warning. Odin's position roughly; Rust's
+no-conversions-at-all position is rejected, and so is C's, which is what
+DISCUSS.org's ~-Wconversion~ middle ground would have reproduced.
+
+So there is no second type-checking mode, which was the objection in the note:
+one predicate says which conversions exist, one helper inserts the ~Cast~ for
+them, and everything else in the checker is unchanged.
+
+** The lattice
+~Types.widens_to ~from ~into~ (lib/types.ml). One rule decides every row: a
+conversion is admitted exactly when no value of the source can come out the
+other side as a different number.
+
+| from        | widens implicitly into                    |
+|-------------+-------------------------------------------|
+| ~i8~        | ~i16~ ~i32~ ~i64~ ~f32~ ~f64~             |
+| ~i16~       | ~i32~ ~i64~ ~f32~ ~f64~                   |
+| ~i32~       | ~i64~ ~f64~                               |
+| ~i64~       | — (nothing)                               |
+| ~u8~        | ~u16~ ~u32~ ~u64~ ~i16~ ~i32~ ~i64~ ~f32~ ~f64~ |
+| ~u16~       | ~u32~ ~u64~ ~i32~ ~i64~ ~f32~ ~f64~       |
+| ~u32~       | ~u64~ ~i64~ ~f64~                         |
+| ~u64~       | — (nothing)                               |
+| ~f32~       | ~f64~                                     |
+| ~f64~       | — (nothing)                               |
+
+Read off the rule, one clause at a time:
+
+- *Same signedness, strictly wider* — the uncontroversial half.
+- *Unsigned into strictly wider signed* — ~u8~→~i16~, ~u32~→~i64~. Every
+  value of the source is a value of the target, so it is in.
+- *Signed into unsigned* — never, at any width: the negatives have nowhere to
+  go.
+- *Equal width across signedness* (~i32~→~u32~, ~u32~→~i32~) — never, for the
+  same reason. Half the range would have to move.
+- *Integer into float, exact only.* An ~f64~ significand is 53 bits, so
+  everything 32 bits and under reaches it and ~i64~/~u64~ do not — 2^53+1 is
+  not an ~f64~. An ~f32~ significand is 24 bits, so only the 8- and 16-bit
+  integers reach it. Odin allows any integer into any float; this is the
+  tighter rule deliberately. A program that wants ~i64~→~f64~ writes ~(f64 x)~.
+  Loosening this later adds programs; tightening it later would break them,
+  which is why the loose version is not the one that landed.
+- *~dyn~ is not in the lattice.* Crossing into and out of a box is
+  ~box~/~unbox~ and is untouched — in particular a ~dyn~ still only unboxes to
+  ~i64~/~f64~/~bool~, and a narrower want there is still the refusal
+  lib/check.ml's ~unbox~ has always given.
+- *Containers are invariant.* A ~[i32]~ is not a ~[i64]~, a ~(Vec i32)~ is not
+  a ~(Vec i64)~, an ~[8 u8]~ is not an ~[8 u16]~. Widening rewrites a value
+  with a ~Cast~; there is no value to rewrite in a slice that does not own its
+  bytes, and rewriting a ~Vec~ would mean allocating a second one.
+- ~bool~ and an ~Enum~ are not numbers and are not on the list. A keyword still
+  resolves against an enum and a bare integer still does not fit one.
+
+*Not expressed as a loosening of ~equal~ or ~fits~*, deliberately.
+~widens_to~ is a separate predicate precisely so that admitting a conversion
+is always paired with inserting the ~Cast~ that performs it. Had ~fits~ been
+loosened, every site that accepts a value without rewriting it would hand the
+backends a node whose type lies about the bits it holds.
+
+** Where it applies
+~Check.expect~ (lib/check.ml) is the single place a wanted type meets a
+produced one, so one arm there covers the whole surface: argument passing,
+return position, ~let~ and ~defvar~ with an annotation, struct field
+initialisers, ~Vec~ pushes, ~set!~, every C import's parameters. Nothing else
+had to learn about widening except the binary operators, which have no
+"wanted type" to meet.
+
+** The join rule for binary operators
+Both operands of a binary operator have one type, and the old comment said
+"there is no implicit widening, so one side has to decide it". The
+decides-rule generalises rather than disappearing:
+
+1. *An expectation still wins, and it reaches the operands.* When the site
+   wants a type — ~(defn f [] i64 (+ a b))~ — that want is threaded into both
+   operands as before, and now widens them. The addition happens at ~i64~, not
+   at ~i32~ followed by a widened result. That is the better of the two and it
+   is only reachable by programs that did not compile before.
+2. *Literals decide exactly as they did.* ~y_decides~ and ~needs_want~ are
+   untouched: a literal takes its width from the other operand, a float
+   literal outranks an integer one. ~(+ x 1)~ over a ~u64~ ~x~ still builds a
+   ~u64~ one, which is what keeps ~(let [h fnv-offset])~ with a ~u64~
+   ~defconst~ meaning exactly what it meant.
+3. *Otherwise the wider side decides* — ~Types.join~: whichever operand the
+   other widens into, with the loser wrapped in a ~Cast~ to it. ~(+ i32-var
+   i64-var)~ is ~i64~ and is newly legal. ~(min i8-var i16-var)~ is ~i16~.
+4. *Equal-width cross-sign still refuses.* ~(+ i32-var u32-var)~ has no join —
+   neither widens into the other — and the message names the cast to write.
+
+~join~ is not a real lattice and is not meant to be: ~(i32, u32)~ has no
+answer, and inventing ~i64~ for it would pick a type neither operand was
+written at.
+
+*Folds are still folds.* ~(+ a b c)~ is ~((a + b) + c)~, so the join is
+pairwise and left-to-right: the first pair settles a type and the third
+operand is checked against it. ~(+ i8 i8 i64)~ therefore still refuses, where
+~(+ i64 i8 i8)~ passes. Left to stand rather than joined across the whole
+argument list, because changing that would change what ~(- a b c)~ means, not
+only what it admits.
+
+*Shifts are carved out.* ~<<~ and ~>>~ do not take the plain join: the value
+decides, and the count widens to the value's type. Under the general rule
+~(<< u8-var i32-count)~ would widen the *value* to ~i32~ and the result type
+and the wrap width would silently follow the count's declared type — and the
+emitter's poison mask is keyed to the value's width. A count wider than the
+value is refused and says so.
+
+** Const folding is unchanged
+The ~defconst~ integer folder (lib/check.ml) folds literal arithmetic within
+one type and does not walk through a ~Cast~ node. So a widened operand is not
+a folded constant: ~(defconst n (+ small-i32-const big-i64-const))~ compiles
+and computes at run time rather than folding, and an array length written that
+way is refused as it was before. Kept as it is on purpose — the folder's job
+is array lengths and it already covers the same-type arithmetic they are
+written with.
diff --git a/lib/types.ml b/lib/types.ml
index 7c267a1..110bcaf 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -9,8 +9,11 @@
     have to have it. That rejection lives in [Check]; this module only names
     the shape. *)
 
-(* Machine integer types. Signedness and width are both part of the type —
-   there is no implicit widening anywhere, per plan.org. *)
+(* Machine integer types. Signedness and width are both part of the type, and
+   two of them are the same type only when both halves match. A value may move
+   to a type that cannot lose it — see [widens_to] at the bottom of this file,
+   FIX.org 2026-09-20 — and never the other way: narrowing is written or it
+   does not happen. *)
 type ikind = I8 | I16 | I32 | I64 | U8 | U16 | U32 | U64
 
 type fkind = F32 | F64
@@ -115,9 +118,13 @@ let ikind_name k =
 
 let fkind_name = function F32 -> "f32" | F64 -> "f64"
 
-(* Structural equality is the whole story: no subtyping, no coercion between
-   machine types, no variance. Written out rather than using [=] so that adding
-   a case with a function or a mutable field cannot silently break it. *)
+(* Structural equality is the whole story for *identity*: no subtyping, no
+   variance, and nothing here bends to admit a conversion. Implicit widening
+   (below) is deliberately not expressed as a loosening of this function or of
+   [fits] — it is a separate predicate that every caller must pair with a
+   [Cast] on the value, so a node's type never lies about the bits it holds.
+   Written out rather than using [=] so that adding a case with a function or
+   a mutable field cannot silently break it. *)
 let rec equal a b =
   match a, b with
   | Int x, Int y -> x = y
@@ -202,3 +209,53 @@ let is_equatable = function String -> true | t -> is_comparable t
    place anything resembling subtyping exists. *)
 let fits ~expected ~actual =
   match actual with Never -> true | _ -> equal expected actual
+
+(* ── Implicit widening, FIX.org 2026-09-20 ────────────────────────────
+   Which numeric types a value may move to without the program saying so.
+   One rule decides every entry: the conversion is admitted exactly when no
+   value of the source type can come out the other side as a different number.
+   Narrowing is not on this list and never will be — [(u32 x)] is how an i64
+   becomes a u32, because that one can lose.
+
+   Read out of that rule:
+
+   - Same signedness, strictly wider: i8→i16→i32→i64, u8→u16→u32→u64.
+   - Unsigned into a strictly wider signed: u8→i16, u8/u16→i32, u8/u16/u32→i64.
+     Every u32 fits in an i64, so nothing is lost. The mirror never holds:
+     signed into unsigned drops the negatives, at any width.
+   - Equal width across signedness (i32→u32, u32→i32) is refused for the same
+     reason — one of the two halves of the range has nowhere to go.
+   - f32→f64.
+   - Integer into float only where the float's significand covers the integer
+     exactly: f64 has 53 bits, so i8/i16/i32/u8/u16/u32 reach it and i64/u64 do
+     not (2^53+1 is not an f64); f32 has 24, so only i8/i16/u8/u16 reach it.
+     Odin is looser here and lets any integer into any float. This is the
+     tighter rule on purpose: a program that wants the lossy one writes (f64 x)
+     and says so, and loosening later adds programs where tightening later
+     would break them.
+
+   Nothing else participates. [Bool] is not a number, an [Enum] is its own type
+   whose whole point is that a bare integer does not fit it, [Dyn] crosses by
+   boxing and unboxing rather than by this, and a container is invariant: a
+   [Vec i32] is not a [Vec i64] and a [[i32]] is not a [[i64]], because the
+   elements would each have to be rewritten and a slice does not own its
+   bytes. *)
+let widens_to ~(from : t) ~(into : t) =
+  match from, into with
+  | Int a, Int b ->
+    if signed a = signed b then bits b > bits a
+    else (not (signed a)) && signed b && bits b > bits a
+  | Float F32, Float F64 -> true
+  | Int a, Float b -> bits a <= (match b with F64 -> 32 | F32 -> 16)
+  | _ -> false
+
+(* The type a binary operator's two operands meet at: whichever of the pair the
+   other one widens into, and nothing otherwise. That is total and it is not a
+   real lattice — (i32, u32) has no answer here, and inventing i64 for it would
+   be picking a type neither operand was written at. Equal types answer
+   themselves, so a caller can use this without checking for that first. *)
+let join a b =
+  if equal a b then Some a
+  else if widens_to ~from:a ~into:b then Some b
+  else if widens_to ~from:b ~into:a then Some a
+  else None

From 0c50f3491662d0caeb48173050b0125c6ba5da68 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:15:42 +0700
Subject: [PATCH 02/17] Widening happens at expect, and the wider operand
 decides a binary op

---
 lib/check.ml                | 141 +++++++++++++++++++++++++++++++-----
 test/programs/widening.flan | 109 ++++++++++++++++++++++++++++
 test/test_acceptance.ml     |  52 +++++++++++++
 3 files changed, 284 insertions(+), 18 deletions(-)
 create mode 100644 test/programs/widening.flan

diff --git a/lib/check.ml b/lib/check.ml
index 329b970..3cc77d2 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2192,14 +2192,43 @@ let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
     mk loc oty
       (Tast.Let ([ (s, got) ], [ mk loc oty (Tast.If (not_nil, some, none)) ]))
 
+(* What a numeric mismatch has left to say, now that widening is silent.
+   FIX.org 2026-09-20, "Implicit widening": every conversion that cannot change
+   the number happens by itself, so a numeric pair that still reaches a refusal
+   is one of exactly two things, and this tells them apart.
+
+   Either the wanted type is *narrower* — the conversion can lose, which is
+   what the language has always refused to do without being told, and the
+   sentence names the cast and points out that the other direction needed
+   nothing. Or there is no direction at all: i32 and u32 are the same width and
+   each holds values the other cannot, so neither widens and the program has to
+   say which half it means to keep.
+
+   Written once and used by both refusals that can report one — [expect]'s, and
+   the binary operators' when their two operands have no join. *)
+let numeric_note ~(want : Types.t) ~(got : Types.t) =
+  if not (Types.is_numeric want && Types.is_numeric got) then ""
+  else if Types.widens_to ~from:want ~into:got then
+    Printf.sprintf
+      " — %s into %s can lose, so it has to be written: (%s x). The other way \
+       round, %s widens into %s by itself"
+      (Types.to_string got) (Types.to_string want) (Types.to_string want)
+      (Types.to_string want) (Types.to_string got)
+  else
+    Printf.sprintf
+      " — neither widens into the other, so the conversion has to be written: \
+       (%s x)"
+      (Types.to_string want)
+
 let expect ctx loc ~want (got : Tast.expr) =
   match want with
   | None -> got
   | Some w ->
-    (* The boundary, and the only implicit conversion in the language. It runs
-       before [fits] rather than instead of it: what comes back is an ordinary
-       expression of the wanted type, and if the coercion did not produce one
-       the usual message is still the one that reports it. *)
+    (* The boundary: where a wanted type meets a produced one, and the one
+       place the language's implicit conversions live. It runs before [fits]
+       rather than instead of it: what comes back is an ordinary expression of
+       the wanted type, and if the coercion did not produce one the usual
+       message is still the one that reports it. *)
     let got =
       match w, got.Tast.ty with
       | Types.Dyn, Types.Dyn -> got
@@ -2217,6 +2246,19 @@ let expect ctx loc ~want (got : Tast.expr) =
           (Types.to_string w)
       | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
       | _, Types.Dyn -> unbox loc w got
+      (* Implicit widening, and this single arm is the whole of its surface.
+         [expect] is called by every site that annotates and by nothing else,
+         so an argument, a return, a let or defvar with a type, a struct field
+         initialiser, a push into a Vec and a C import's parameter all get it
+         here at once and none of them had to learn about it.
+
+         The conversion is performed, not waved through: [widen] emits the same
+         [Cast] node the written (i64 x) emits, so the backends sext or zext by
+         the *source* type's signedness and nothing downstream sees a node
+         whose type disagrees with its bits. [widens_to] is what keeps that
+         honest — it admits only conversions that cannot change the number, so
+         the cast this inserts is one no program can tell happened. *)
+      | _ when Types.widens_to ~from:got.Tast.ty ~into:w -> widen loc w got
       | _ -> got
     in
     if Types.fits ~expected:w ~actual:got.Tast.ty then got
@@ -2224,9 +2266,15 @@ let expect ctx loc ~want (got : Tast.expr) =
       (* Kinded so that the one caller who knows more — a call argument, which
          can name the function and the parameter — can recognise this exact
          refusal at this exact span and say the rest. Every other reader of a
-         diagnostic ignores [kind]. *)
-      Loc.failk "check/type-mismatch" loc "expected %s, found %s"
+         diagnostic ignores [kind].
+
+         [numeric_note] is the rest of the sentence when both sides are
+         numbers, and it is on this message rather than beside it because a
+         reader who has just been told i64 and i32 are different types needs
+         to be told, in the same breath, which direction needed nothing. *)
+      Loc.failk "check/type-mismatch" loc "expected %s, found %s%s"
         (Types.to_string w) (Types.to_string got.Tast.ty)
+        (numeric_note ~want:w ~got:got.Tast.ty)
 
 (* Something a [break] may not jump out of, named so the refusal can say which.
    See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@@ -5448,8 +5496,10 @@ and named_call ctx ~want loc name args =
     (* Same truthiness as [if]: a dyn argument is negated on nil/false vs.
        everything else, not narrowed to a strict bool first. *)
     prim Tast.Not Types.Bool [ check_truthy ctx (List.hd args) ]
-  (* Bitwise operators are integers-only, and the shift count has the same type
-     as the value shifted — there is no implicit widening anywhere else either. *)
+  (* Bitwise operators are integers-only. They take the ordinary join — an
+     operand that widens into the other does, so (bit-and u8-flags u32-mask) is
+     a u32 and — and the shifts below do not, which is the one carve-out
+     widening has (FIX.org 2026-09-20). *)
   | "bit-and" | "bit-or" | "bit-xor" ->
     let p = match name with
       | "bit-and" -> Tast.BitAnd | "bit-or" -> Tast.BitOr
@@ -5460,11 +5510,20 @@ and named_call ctx ~want loc name args =
       (function Types.Int _ -> true | _ -> false) "integers" args
   (* The shifts stay at two, and not only because a shift chain reads badly:
      each count would be checked against the same width below, so (<< x 30 30)
-     would pass two legal shifts and still shift the value away entirely. *)
+     would pass two legal shifts and still shift the value away entirely.
+
+     [~join:false] is the one place widening is deliberately not symmetric.
+     The count still widens *to* the value's type — (<< i64-x u8-n) is fine —
+     but the value never widens to the count's, which the general rule would do
+     for (<< u8-x i32-n). It would be the wrong answer twice over: the result's
+     type and the width the shift wraps at would be taken from a number that is
+     only saying how far, and the range check just below, along with [emit]'s
+     mask, is keyed to the *value's* width. A count wider than the value is
+     refused and is told to write the cast. *)
   | "<<" | ">>" ->
     let p = if String.equal name "<<" then Tast.Shl else Tast.Shr in
     arity ctx loc name 2 args;
-    let a, b = binary ctx name loc ~want:(numeric_want want) args in
+    let a, b = binary ctx ~join:false name loc ~want:(numeric_want want) args in
     (match a.Tast.ty with
      | Types.Int _ -> ()
      | other -> fail loc "%s takes integers, found %s" name
@@ -7434,11 +7493,48 @@ and byte_slice ctx (a : Ast.expr) =
 and numeric_want want =
   match want with Some (Types.Int _ | Types.Float _) -> want | _ -> None
 
-(* Both operands of a binary operator have one type, and there is no implicit
-   widening, so one side has to decide it. Check the side that carries the most
-   information first: a non-literal over a literal, and a float literal over an
-   integer one, since an integer constant converts to a float and not back. *)
-and binary ctx ?(dyn_ok = false) name loc ~want args =
+(* Both operands of a binary operator have one type, so one side has to decide
+   it. Check the side that carries the most information first: a non-literal
+   over a literal, and a float literal over an integer one, since an integer
+   constant converts to a float and not back.
+
+   Widening (FIX.org 2026-09-20) does not retire that rule, it finishes it.
+   Three things decide, in this order:
+
+   1. An expectation, if the site has one, and it reaches *both* operands. So
+      (defn f [] i64 (+ a b)) over two i32s widens each operand and adds at
+      i64, rather than adding at i32 and widening the sum. That is the better
+      of the two readings and it costs nothing to prefer it, because no program
+      that compiled before can reach it — the pair used to be a refusal.
+   2. A literal, exactly as before: it takes its width from the other operand,
+      so (+ x 1) over a u64 x is still u64 arithmetic and (let [h fnv-offset])
+      over a u64 defconst still means what it meant. [needs_want] is what marks
+      the forms this applies to and it is untouched.
+   3. Otherwise the *wider* side decides — [Types.join], whichever operand the
+      other widens into, with a [Cast] put on the narrower one. (+ i32-var
+      i64-var) is an i64 add. Equal width across signedness has no join, by
+      construction: neither i32 nor u32 widens into the other, and the refusal
+      says which cast to write.
+
+   [join_pair] is reached only when the *first* operand turned out to be the
+   narrower one. The other order needs nothing here: checking y against an i64
+   x already widens an i32 y inside [expect]. *)
+and join_pair ctx (a : Tast.expr) (y : Ast.expr) exn =
+  (* Asking y for [a]'s type failed. Either y is genuinely wrong, or y is
+     simply the wider operand and this is the one direction [expect] cannot
+     serve on its own. Check y on its own terms to find out; if it decides a
+     type that a widens into, a is the one that moves. Anything else re-raises
+     the original refusal, so an error inside y is still reported as itself and
+     no form that cannot check without an expectation — None, (zeroed) — loses
+     the expectation it used to get. *)
+  match check ctx y with
+  | exception _ -> raise exn
+  | b ->
+    if Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
+      widen a.Tast.loc b.Tast.ty a, b
+    else raise exn
+
+and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
   match args with
   | [ x; y ] ->
     let y_decides =
@@ -7484,12 +7580,21 @@ and binary ctx ?(dyn_ok = false) name loc ~want args =
       if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn
          || Types.equal a.Tast.ty b.Tast.ty
       then a, b
-      else a, check ctx ~want:a.Tast.ty y
+      (* Both operands are already in hand here, so the join is read off
+         directly rather than through [join_pair]'s retry. Whichever one the
+         other widens into is the pair's type; with no join, the re-check
+         produces the refusal, which names the cast at y's own line. *)
+      else
+        (match Types.join a.Tast.ty b.Tast.ty with
+         | Some t ->
+           widen a.Tast.loc t a, widen b.Tast.loc t b
+         | None -> a, check ctx ~want:a.Tast.ty y)
     end
     else begin
       let a = check ctx ?want x in
-      let b = check ctx ~want:a.Tast.ty y in
-      a, b
+      match check ctx ~want:a.Tast.ty y with
+      | b -> a, b
+      | exception e -> if join then join_pair ctx a y e else raise e
     end
   | _ -> fail loc "%s takes two arguments" name
 
diff --git a/test/programs/widening.flan b/test/programs/widening.flan
new file mode 100644
index 0000000..1062148
--- /dev/null
+++ b/test/programs/widening.flan
@@ -0,0 +1,109 @@
+;;;; Implicit widening, and the only thing worth pinning about it: the bits.
+;;;; FIX.org 2026-09-20, "Implicit widening".
+;;;;
+;;;; A widening conversion is admitted exactly when it cannot change the
+;;;; number, so every row here has an answer that is also the answer the source
+;;;; type had. Which means the test is entirely about the *emitted* cast being
+;;;; the right one: a sign-extension where the source is signed, a
+;;;; zero-extension where it is not, and the float conversions picking sitofp
+;;;; against uitofp by the same rule. Each of those is a separate instruction
+;;;; on both backends and choosing the wrong one gives a wrong number rather
+;;;; than a wrong type, which no type test would catch.
+;;;;
+;;;; The rows are picked so that a mistake is visible in the printed value:
+;;;;
+;;;;   -5 i8 to i64      sext; a zext prints 251
+;;;;   -1 i32 to i64     sext; a zext prints 4294967295
+;;;;   255 u8 to i16     zext; a sext prints -1
+;;;;   4000000000 u32    zext to i64; a sext prints -294967296
+;;;;   4294967295 u32    to f64, exact; a signed conversion prints -1
+;;;;   -2000000000 i32   to f64; a uitofp prints 2294967296
+;;;;
+;;;; Everything goes through a global rather than a literal, because a literal
+;;;; is built at the wanted width by the literal rule and would never reach a
+;;;; cast at all.
+
+(defvar i8-neg   i8   -5)
+(defvar i8-pos   i8    127)
+(defvar i16-neg  i16  -300)
+(defvar i32-neg  i32  -2000000000)
+(defvar i32-one  i32   1)
+(defvar i32-all  i32  -1)
+(defvar u8-max   u8    255)
+(defvar u16-max  u16   65535)
+(defvar u32-big  u32   4000000000)
+(defvar u32-max  u32   4294967295)
+(defvar i64-big  i64   5000000000)
+(defvar f32-half f32   0.5)
+
+;; Widening at a parameter. Each of these is a plain typed function and the
+;; call sites below hand it a narrower type with no cast written anywhere.
+(defn take-i64 [x i64] i64 x)
+(defn take-i16 [x i16] i16 x)
+(defn take-u64 [x u64] u64 x)
+(defn take-f64 [x f64] f64 x)
+(defn take-f32 [x f32] f32 x)
+
+;; Widening at a return position: the body is an i32 and the signature is i64.
+(defn ret-widened [] i64 i32-neg)
+
+;; Widening in a binary operator, both orders. The first is the direction
+;; [expect] already served; the second is the one the join rule added.
+(defn add-wide-first [] i64 (+ i64-big i32-one))
+(defn add-narrow-first [] i64 (+ i32-one i64-big))
+
+(defn main [args [string]] i32
+  ;; ── integer to integer ──────────────────────────────────────────
+  (println (take-i64 i8-neg))            ;; -5
+  (println (take-i64 i8-pos))            ;; 127
+  (println (take-i64 i16-neg))           ;; -300
+  (println (take-i64 i32-all))           ;; -1
+  (println (take-i64 i32-neg))           ;; -2000000000
+  (println (take-i16 u8-max))            ;; 255
+  (println (take-i64 u8-max))            ;; 255
+  (println (take-i64 u16-max))           ;; 65535
+  (println (take-i64 u32-big))           ;; 4000000000
+  (println (take-i64 u32-max))           ;; 4294967295
+  (println (take-u64 u32-big))           ;; 4000000000
+  (println (take-u64 u8-max))            ;; 255
+
+  ;; ── a widened return ────────────────────────────────────────────
+  (println (ret-widened))                ;; -2000000000
+
+  ;; ── integer to float, exact only ────────────────────────────────
+  (println (take-f64 i32-neg))           ;; -2000000000.0
+  (println (take-f64 u32-max))           ;; 4294967295.0
+  (println (take-f64 i8-neg))            ;; -5.0
+  (println (take-f32 i16-neg))           ;; -300.0
+  (println (take-f32 u16-max))           ;; 65535.0
+
+  ;; The printer answers %g, which rounds an f64 long before the bits it is
+  ;; carrying run out, so the exactness the int-to-float boundary is chosen for
+  ;; is asserted by subtraction rather than by reading the digits. Each of
+  ;; these is the difference between the widened value and the number it is
+  ;; supposed to be, and a conversion that lost anything answers something
+  ;; other than the last unit.
+  (println (- (take-f64 u32-max) 4294967294.0))   ;; 1
+  (println (- (take-f64 i32-neg) -1999999999.0))  ;; -1
+  (println (- (take-f32 u16-max) 65534.0))        ;; 1
+
+  ;; ── float to float ──────────────────────────────────────────────
+  (println (take-f64 f32-half))          ;; 0.5
+
+  ;; ── the binary join, both operand orders ────────────────────────
+  (println (add-wide-first))             ;; 5000000001
+  (println (add-narrow-first))           ;; 5000000001
+  ;; The narrower operand is the first one, and the sum is an i64 even though
+  ;; nothing on this line is annotated.
+  (println (+ i32-neg i64-big))          ;; 3000000000
+  ;; A comparison joins the same way, and the widened -1 must still be -1.
+  (println (< i32-all i64-big))          ;; true
+  ;; min and max over two widths answer at the wider one.
+  (println (max i8-neg i16-neg))         ;; -5
+  (println (min i8-neg i32-neg))         ;; -2000000000
+  ;; A count narrower than the value widens to it; the value's width decides.
+  (println (<< i64-big i8-pos))          ;; 0 -- masked to 127 mod 64 = 63
+  ;; An expectation reaches the operands, so this adds at i64 rather than
+  ;; wrapping at i32 and widening the sum afterwards.
+  (println (take-i64 (+ i32-neg i32-neg)))  ;; -4000000000
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index e982445..47402f4 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -542,6 +542,58 @@ let () =
     outputs "the rest of libm, both widths" "programs/math3.flan" math3_out;
     outputs ~opt:"-O0" "the rest of libm, both widths, -O0"
       "programs/math3.flan" math3_out;
+    (* Implicit widening, FIX.org 2026-09-20. The type side of it needs no
+       program — a refusal that stopped happening is a compile that succeeds —
+       so what this asserts is the *bits*: every row is a value whose printed
+       form differs depending on which extension instruction the backend chose.
+       -5 as an i8 reaching an i64 prints 251 under a zero-extension; a u8 255
+       reaching an i16 prints -1 under a sign-extension; a u32 four billion
+       reaching an i64 prints a negative number under a sign-extension. The
+       three subtraction rows are the int-to-float boundary, asserted by
+       difference because %g rounds long before an f64's bits run out.
+
+       Run on both backends and on the unoptimised build, because the choice is
+       made three separate times: emit.ml picks sext/zext/sitofp/uitofp by the
+       source type's signedness, and x86.ml gets there by a load that extends
+       by the same rule and a cvtsi2sd on the register it left behind. *)
+    let widening_out =
+      "-5\n\
+       127\n\
+       -300\n\
+       -1\n\
+       -2000000000\n\
+       255\n\
+       255\n\
+       65535\n\
+       4000000000\n\
+       4294967295\n\
+       4000000000\n\
+       255\n\
+       -2000000000\n\
+       -2e+09\n\
+       4.29497e+09\n\
+       -5\n\
+       -300\n\
+       65535\n\
+       1\n\
+       -1\n\
+       1\n\
+       0.5\n\
+       5000000001\n\
+       5000000001\n\
+       3000000000\n\
+       true\n\
+       -5\n\
+       -2000000000\n\
+       0\n\
+       -4000000000\n"
+    in
+    outputs "implicit widening, and which extension it emits"
+      "programs/widening.flan" widening_out;
+    outputs ~opt:"-O0" "implicit widening, -O0" "programs/widening.flan"
+      widening_out;
+    outputs ~x86:true "implicit widening, --x86" "programs/widening.flan"
+      widening_out;
     (* The clock and the environment. Every line of that program's output is
        an invariant — a monotonicity, a date range, a sleep that did not
        return early — and not a reading, because the same file is in the

From d0e33331b5e907bd718b6834bdc6f15991135c01 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:19:39 +0700
Subject: [PATCH 03/17] An expectation outranks the join, because an
 expectation is information

---
 lib/check.ml | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 3cc77d2..9ee4a51 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -7580,15 +7580,26 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
       if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn
          || Types.equal a.Tast.ty b.Tast.ty
       then a, b
-      (* Both operands are already in hand here, so the join is read off
-         directly rather than through [join_pair]'s retry. Whichever one the
-         other widens into is the pair's type; with no join, the re-check
-         produces the refusal, which names the cast at y's own line. *)
+      (* Asking y for [a]'s type stays the first thing tried, and not only for
+         continuity: y was checked above with no expectation at all, and an
+         expectation is information. A sum of two products handed to an f32
+         function is the case — test/programs/math.flan does it — because every
+         literal inside those products defaults to f64 on its own terms, so
+         reading the join off the two unexpected halves would answer f64 for a
+         form the site asked to be f32. The re-check builds them at f32 as it
+         always did.
+
+         [b] is only used when that re-check refuses, which is the direction
+         [expect] cannot serve: a is the narrower operand and it is the one
+         that has to move. Nothing is checked a third time — the own-terms [b]
+         already in hand is the answer. *)
       else
-        (match Types.join a.Tast.ty b.Tast.ty with
-         | Some t ->
-           widen a.Tast.loc t a, widen b.Tast.loc t b
-         | None -> a, check ctx ~want:a.Tast.ty y)
+        (match check ctx ~want:a.Tast.ty y with
+         | b' -> a, b'
+         | exception e ->
+           if join && Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
+             widen a.Tast.loc b.Tast.ty a, b
+           else raise e)
     end
     else begin
       let a = check ctx ?want x in

From 3e4267f57c6ecf29f008ed52fd0243fe081b7800 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:33:15 +0700
Subject: [PATCH 04/17] Every no-implicit-widening comment now says what is
 true instead

---
 FIX.org                  | 23 ++++++++++++-------
 docs/BUILT.md            |  8 ++++---
 lib/check.ml             | 49 +++++++++++++++++++++++++---------------
 lib/prelude.ml           | 29 ++++++++++++++----------
 test/programs/embed.flan |  5 ++--
 web-files-out.txt        |  1 +
 6 files changed, 72 insertions(+), 43 deletions(-)
 create mode 100644 web-files-out.txt

diff --git a/FIX.org b/FIX.org
index d65d942..2535e5e 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2555,11 +2555,18 @@ and the wrap width would silently follow the count's declared type — and the
 emitter's poison mask is keyed to the value's width. A count wider than the
 value is refused and says so.
 
-** Const folding is unchanged
-The ~defconst~ integer folder (lib/check.ml) folds literal arithmetic within
-one type and does not walk through a ~Cast~ node. So a widened operand is not
-a folded constant: ~(defconst n (+ small-i32-const big-i64-const))~ compiles
-and computes at run time rather than folding, and an array length written that
-way is refused as it was before. Kept as it is on purpose — the folder's job
-is array lengths and it already covers the same-type arithmetic they are
-written with.
+** Const folding is unchanged, and was never the thing it looked like
+The ~defconst~ integer folder (~const_int~, lib/check.ml) runs on the *AST*,
+before anything has a type, and carries one ~int64~ per constant with no width
+attached. So it already folded across widths and still does —
+~(defconst w i32 4)~ times ~(defconst h i64 5)~ has always been a constant 20,
+usable as an array length — and widening neither added a fold nor removed one.
+Measured, not assumed.
+
+The one thing that did change is at the edges rather than in the folder: it
+answers nothing for a ~Call~ whose operator is not one of the five arithmetic
+names, and a written cast is such a call. So ~(* w (i64 h))~ was not a
+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.
diff --git a/docs/BUILT.md b/docs/BUILT.md
index 91cffa1..ddb5897 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -806,7 +806,8 @@ fact without cutting anything in half. See "The browser is the third target" bel
 **Three edits were made to sand.flan's own text** when it was ported, and they are language decisions rather than fixes:
 
 - `(defconst gravity 0.05)` → `(defconst gravity f32 0.05)`. An untyped float constant is `f64`, `velocity` is `[f32]`,
-and there is no implicit widening.
+and `f64` into `f32` is a narrowing — still written, and still written after implicit widening landed (FIX.org
+2026-09-20), because widening is only the conversions that cannot change the number and this one can.
 - `(defvar current-color u32)` → `i32`. It is an index into `colors`, and `(len colors)` is an `i32`.
 - `(defn main [])` is unchanged — the short form, as plan.org says.
 
@@ -3934,8 +3935,9 @@ compile-time constant*. Both of emit.ml's string emitters take the bytes and ign
 constant either way and this one is a constant a global can hold.
 
 **Two spellings, not one form that changes type with its context.** Odin threads a `type_hint` everywhere and can
-afford `#load("p")` to mean a `string` here and a `[]u8` there. With structural equality, no implicit widening and no
-coercion anywhere, the same text meaning two types would be a wart, so `string` is written down when it is wanted. The
+afford `#load("p")` to mean a `string` here and a `[]u8` there. With structural equality and no conversion between one
+container and another — implicit widening is numbers only — the same text meaning two types would be a wart, so
+`string` is written down when it is wanted. The
 site's expectation is a fallback only and nothing depends on it.
 
 **The path is a literal and resolves relative to the file the form is written in.** Both are Odin's rules and for
diff --git a/lib/check.ml b/lib/check.ml
index 9ee4a51..b6d2ed6 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2026,12 +2026,19 @@ let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
        value was a bool, so what comes back is 0 or 1. *)
     widen loc Types.Bool (need "flan_dyn_need_bool" (Types.Int Types.I32))
   (* Every other width is refused rather than served by a need_i64 and a
-     truncation. This language has no implicit narrowing anywhere, and putting
-     one at the boundary where a value's type was *already* uncertain is the
-     worst place in the program to start: the annotation would read as a check
-     and would be a silent discard of the high bits. The ABI grows a per-width
-     entry point when there is a reason to; until then the spelling that works
-     is an i64 and an explicit conversion after it. *)
+     truncation. Narrowing is written or it does not happen — that survives
+     widening becoming implicit (FIX.org 2026-09-20) untouched, and this is the
+     boundary where it matters most: the value's type was *already* uncertain
+     here, so an annotation that quietly discarded the high bits would read as
+     a check and be the opposite of one.
+
+     Nor does widening reach this arm from the other side. The box carries one
+     integer width and one float width, so there is no narrower source here to
+     widen from — a u32 want is asking the i64 in the box to fit in half of
+     itself, which is the refusal above and not a conversion the lattice has.
+     The ABI grows a per-width entry point when there is a reason to; until
+     then the spelling that works is an i64 and a written conversion after
+     it. *)
   | Types.Int _ | Types.Float _ ->
     no_dyn_yet loc ~into:false want
       (Printf.sprintf
@@ -6520,9 +6527,11 @@ and named_call ctx ~want loc name args =
        let as_bytes () = mk loc (Types.Slice (Types.Int Types.U8)) (Tast.Str data) in
        (* Two spellings rather than one that changes type with its context.
           Odin threads a type_hint everywhere and can afford (embed "p") to
-          mean a string here and a []u8 there; with structural equality and no
-          implicit widening anywhere, the same text meaning two types would be
-          a wart. [want] is a fallback only, and nothing depends on it. *)
+          mean a string here and a []u8 there; with structural equality and a
+          container that never converts to another container -- implicit
+          widening is numbers only, FIX.org 2026-09-20 -- the same text meaning
+          two types would be a wart. [want] is a fallback only, and nothing
+          depends on it. *)
        (match args with
         | [ _; { Ast.e = Ast.Var "string"; _ } ] ->
           expect ctx loc ~want (as_string ())
@@ -7638,8 +7647,9 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
 let builtins : (string * string * string) list =
   [ (* arithmetic and comparison *)
     ("+", "+ [numeric? ...] numeric?",
-     "Sum, folded left over two or more operands that share one numeric \
-      type — nothing widens implicitly.");
+     "Sum, folded left over two or more operands. Two operands of different \
+      numeric types meet at the wider one when that cannot lose — i32 and i64 \
+      add at i64 — and i32 with u32 has no such type and is refused.");
     ("-", "- [numeric? ...] numeric?",
      "Difference, folded left: (- a b c) is ((a - b) - c).");
     ("*", "* [numeric? ...] numeric?",
@@ -7664,20 +7674,23 @@ let builtins : (string * string * string) list =
     ("not", "not [bool] bool",
      "Negates a bool. Nothing else in this language is a truth value.");
     ("bit-and", "bit-and [int ...] int",
-     "Bitwise and, folded left. Integers only, and every operand has the \
-      same width.");
+     "Bitwise and, folded left. Integers only; operands of different widths \
+      meet at the wider one, the way + does.");
     ("bit-or", "bit-or [int ...] int", "Bitwise or, folded left over integers.");
     ("bit-xor", "bit-xor [int ...] int",
      "Bitwise exclusive or, folded left over integers.");
     ("<<", "<< [int int] int",
-     "Left shift. The count has the shifted value's own type, and a literal \
-      count at or past its width is refused — LLVM calls that poison.");
+     "Left shift. The value's type decides — a narrower count widens to it, a \
+      wider one is refused — and a literal count at or past the value's width \
+      is refused too, because LLVM calls that poison.");
     (">>", ">> [int int] int",
-     "Right shift, by a count of the value's own type; a literal count at or \
-      past the width is refused, as it is for <<.");
+     "Right shift. The value's type decides and the count widens to it, never \
+      the reverse; a literal count at or past the width is refused, as it is \
+      for <<.");
     ("min", "min [ordered? ...] ordered?",
      "The smallest of two or more operands, each of them evaluated exactly \
-      once however many there are.");
+      once however many there are. Two widths meet at the wider: (min i8-x \
+      i16-y) is an i16.");
     ("max", "max [ordered? ...] ordered?",
      "The largest of two or more operands, each evaluated exactly once.");
     ("zeroed", "zeroed [] T",
diff --git a/lib/prelude.ml b/lib/prelude.ml
index c96d2cd..16c3062 100644
--- a/lib/prelude.ml
+++ b/lib/prelude.ml
@@ -31,12 +31,14 @@
     is strictly the better call for every one of them. [print] is the same walk
     as [println] without the trailing newline, so it covers the no-newline case
     that was the family's remaining excuse (see [show] in
-    test/programs/slices.flan). And because this language has no implicit
-    widening, [(print-i64 x)] forced an explicit [(i64 x)] at every site;
-    [(print x)] takes the value as it is. That is not only shorter: the cast
-    through the signed printer turned a [u64] above 2^63 into a negative
-    number, where [print] routes it through [flan_u64_to_bytes] and prints what
-    it actually holds. *)
+    test/programs/slices.flan). And [(print-i64 x)] forced an explicit
+    [(i64 x)] at every site, where [(print x)] takes the value as it is. That
+    is not only shorter: the cast through the signed printer turned a [u64]
+    above 2^63 into a negative number, where [print] routes it through
+    [flan_u64_to_bytes] and prints what it actually holds. Implicit widening
+    (FIX.org 2026-09-20) would have removed the cast at a [u8] or an [i32] site
+    on its own, but not at that one -- a [u64] widens into nothing at all, and
+    the printer it was being forced through was the wrong one. *)
 
 let source = {flan|
 ;; The condition every allocating operation signals when the allocator cannot
@@ -470,17 +472,20 @@ let source = {flan|
 ;; sum is the one shape a type variable cannot express, and it is worth being
 ;; precise about why rather than leaving two near-identical functions looking
 ;; like an oversight. Each of these *widens*: sum-i32 accumulates in i64 and
-;; sum-f32 in f64, with an explicit cast per element, because there is no
-;; implicit widening anywhere in the language and summing a screenful into the
-;; element's own type is how a total silently wraps or absorbs. "The wider
+;; sum-f32 in f64, because summing a screenful into the element's own type is
+;; how a total silently wraps or absorbs. The per-element casts no longer have
+;; to be written to say so — an i32 widens into an i64 by itself, FIX.org
+;; 2026-09-20 — and they stay because what these two functions exist to show is
+;; that the accumulator is a different type from the element. "The wider
 ;; type $t accumulates into" is a function from types to types — an associated
 ;; type, or a constraint system of a kind {:where} is not — and a generic sum
 ;; that took its accumulator and its + as parameters would be reduce, which is
 ;; above.
 
-;; Accumulates in i64 and each element is widened explicitly — there is no
-;; implicit widening anywhere in the language, and summing a screenful of i32
-;; into an i32 is how a total silently wraps.
+;; Accumulates in i64, because summing a screenful of i32 into an i32 is how a
+;; total silently wraps. The per-element (i64 ...) would happen on its own now;
+;; it is written to keep the accumulator's type visible at the line that feeds
+;; it.
 (defn sum-i32 [s [i32]] i64
   (let [t (i64 0)]
     (dotimes [i (len s)]
diff --git a/test/programs/embed.flan b/test/programs/embed.flan
index 4783be7..76ecdba 100644
--- a/test/programs/embed.flan
+++ b/test/programs/embed.flan
@@ -23,8 +23,9 @@
     (print (string a)))                 ; hello from a
 
   ;; `string` is the second spelling, not a different meaning for the same
-  ;; text. With structural equality and no implicit widening, one form that
-  ;; changes type with its context would be a wart.
+  ;; text. With structural equality and nothing that converts one container
+  ;; into another -- implicit widening is numbers only -- one form that changes
+  ;; type with its context would be a wart.
   (println (embed "assets/b.bin" string))          ; BBB
 
   ;; Byte-exact, including bytes no text encoding would survive: emit.ml's
diff --git a/web-files-out.txt b/web-files-out.txt
new file mode 100644
index 0000000..ff72b5c
--- /dev/null
+++ b/web-files-out.txt
@@ -0,0 +1 @@
+state

From f9ae500949c0cd3b40066d0a6241e0a8ea9530fc Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:37:55 +0700
Subject: [PATCH 05/17] The lattice pinned at its edges, and the two calls that
 could go the other way

---
 test/test_flan.ml | 82 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 82 insertions(+)

diff --git a/test/test_flan.ml b/test/test_flan.ml
index 0790e2d..5ab3e21 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -930,6 +930,88 @@ let () =
   rejects_check "float literal into an int"
     "(defn f [] i32 (+ 1 0.5))" ~needle:"expected i32";
 
+  (* ── Implicit widening, FIX.org 2026-09-20 ─────────────────────────
+     The lattice, pinned at its edges rather than row by row: what is in, what
+     is out, and the two boundaries that were a judgement call and could be
+     argued the other way — int-into-float admitting only the exact ones, and
+     equal-width cross-signedness admitting nothing.
+
+     [programs/widening.flan] is the other half and asserts the bits; these
+     assert which programs exist. *)
+  accepts "same signedness widens"
+    "(defvar a i32) (defn g [x i64] ()) (defn f [] () (g a))";
+  accepts "unsigned widens into a wider signed"
+    "(defvar a u32) (defn g [x i64] ()) (defn f [] () (g a))";
+  accepts "u8 widens into i16"
+    "(defvar a u8) (defn g [x i16] ()) (defn f [] () (g a))";
+  accepts "f32 widens into f64"
+    "(defvar a f32) (defn g [x f64] ()) (defn f [] () (g a))";
+  (* Narrowing is the thing that did not change, and the message has to say
+     narrowing rather than "these are different types" — it also names the
+     direction that needs nothing, because that is the half a reader coming
+     from the old rule will not expect. *)
+  rejects_check "narrowing is still refused, and says so"
+    "(defvar a i64) (defn g [x i32] ()) (defn f [] () (g a))"
+    ~needle:"i64 into i32 can lose";
+  rejects_check "and says the other direction is free"
+    "(defvar a i64) (defn g [x i32] ()) (defn f [] () (g a))"
+    ~needle:"i32 widens into i64 by itself";
+  rejects_check "float narrowing is refused too"
+    "(defvar a f64) (defn g [x f32] ()) (defn f [] () (g a))"
+    ~needle:"f64 into f32 can lose";
+  (* Equal width across signedness: each holds values the other cannot, so
+     there is no direction at all and the message says that instead. *)
+  rejects_check "signed does not reach the same-width unsigned"
+    "(defvar a i32) (defn g [x u32] ()) (defn f [] () (g a))"
+    ~needle:"neither widens into the other";
+  rejects_check "and a signed value never reaches an unsigned, wider or not"
+    "(defvar a i32) (defn g [x u64] ()) (defn f [] () (g a))"
+    ~needle:"neither widens into the other";
+  (* Int into float, exact only. This is where the rule is tighter than
+     Odin's, which admits any integer into any float; i64 has values no f64
+     holds, so it is out, and the cast is written. *)
+  accepts "i32 reaches f64 exactly"
+    "(defvar a i32) (defn g [x f64] ()) (defn f [] () (g a))";
+  accepts "u32 reaches f64 exactly"
+    "(defvar a u32) (defn g [x f64] ()) (defn f [] () (g a))";
+  accepts "i16 reaches f32 exactly"
+    "(defvar a i16) (defn g [x f32] ()) (defn f [] () (g a))";
+  rejects_check "i64 does not reach f64 — above 2^53 it would round"
+    "(defvar a i64) (defn g [x f64] ()) (defn f [] () (g a))"
+    ~needle:"(f64 x)";
+  rejects_check "i32 does not reach f32 — above 2^24 it would round"
+    "(defvar a i32) (defn g [x f32] ()) (defn f [] () (g a))"
+    ~needle:"(f32 x)";
+  (* Containers are invariant: widening rewrites a value with a cast, and
+     there is no value to rewrite in a slice that does not own its bytes. *)
+  rejects_check "a slice of i32 is not a slice of i64"
+    "(defn g [s [i64]] ()) (defn f [t [i32]] () (g t))"
+    ~needle:"expected [i64]";
+
+  (* The binary join. The wider operand decides, in either written order, and
+     an equal-width cross-signed pair still has nothing to decide on. *)
+  accepts "the wider operand decides, wider written first"
+    "(defvar a i64) (defvar b i32) (defn f [] i64 (+ a b))";
+  accepts "and decides when it is written second"
+    "(defvar a i64) (defvar b i32) (defn f [] i64 (+ b a))";
+  accepts "min and max join the same way"
+    "(defvar a i8) (defvar b i16) (defn f [] i16 (max a b))";
+  rejects_check "i32 and u32 have no join"
+    "(defvar a i32) (defvar b u32) (defn f [] i32 (+ a b))"
+    ~needle:"neither widens into the other";
+  (* The literal rule is untouched, which is what keeps a u64 constant's
+     arithmetic at u64 rather than defaulting the 1 to an i32. *)
+  accepts "a literal still takes the other operand's type"
+    "(defconst fnv u64 14695981039346656037) (defn f [] u64 (+ fnv 1))";
+  (* Shifts are the carve-out: the value's type decides and the count widens
+     to it, never the reverse, because the result's width and the poison check
+     both belong to the value. *)
+  accepts "a narrower count widens to the value"
+    "(defvar v i64) (defvar n u8) (defn f [] i64 (<< v n))";
+  rejects_check "a wider count does not drag the value up with it"
+    "(defvar v u8) (defvar n i32) (defn f [] u8 (<< v n))"
+    ~needle:"expected u8";
+
   (* ── Bidirectional flow ────────────────────────────────────────── *)
   accepts "return type types the literal" "(defn f [] u8 0)";
   accepts "return type types None"        "(defn f [] (Option f64) None)";

From 3b91afd47bfdef4ea6e6f77332f94036ae06c133 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:41:28 +0700
Subject: [PATCH 06/17] What the widening lane changed, kept, and measured

---
 FIX.org | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)

diff --git a/FIX.org b/FIX.org
index 2535e5e..0956983 100644
--- a/FIX.org
+++ b/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.

From b34a7bbf11c5318b98a015083220b3bd4ac6cac8 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:44:37 +0700
Subject: [PATCH 07/17] The raylib half of the sweep, and the let the note
 named

---
 FIX.org           | 6 ++++++
 test/test_flan.ml | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/FIX.org b/FIX.org
index 0956983..57a8b61 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2629,6 +2629,12 @@ what was true when they were written.
   pure addition: widening.flan's own rows. Not one existing program's
   diagnostics, output or exit status moved.
 
+  The thirteen test programs that import ~vendor:raylib~ were not run either,
+  for the same reason, and got the same treatment as examples/ below:
+  ~check~'s diagnostics are identical on both sides, LLVM ~emit~ is
+  byte-identical, and the x86 difference is the prelude-line strings and
+  nothing else.
+
   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~.
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 5ab3e21..1fea434 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1003,6 +1003,12 @@ let () =
      arithmetic at u64 rather than defaulting the 1 to an i32. *)
   accepts "a literal still takes the other operand's type"
     "(defconst fnv u64 14695981039346656037) (defn f [] u64 (+ fnv 1))";
+  (* The form DISCUSS.org's note named: an unannotated let of a u64 constant.
+     It binds a u64 and nothing about widening reaches it — a let with no type
+     has no expectation to widen against, and the constant is what it says. *)
+  accepts "an unannotated let of a u64 constant still binds a u64"
+    "(defconst fnv u64 14695981039346656037) \
+     (defn f [] u64 (let [h fnv] (* h 2)))";
   (* Shifts are the carve-out: the value's type decides and the count widens
      to it, never the reverse, because the result's width and the poison check
      both belong to the value. *)

From 13b391b7bf718f97a63d79ded25fc25f3f963521 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:45:34 +0700
Subject: [PATCH 08/17] The u64 pin is spelled the way the program that
 motivated it is

---
 test/test_flan.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/test_flan.ml b/test/test_flan.ml
index 1fea434..5f37f12 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1002,12 +1002,12 @@ let () =
   (* The literal rule is untouched, which is what keeps a u64 constant's
      arithmetic at u64 rather than defaulting the 1 to an i32. *)
   accepts "a literal still takes the other operand's type"
-    "(defconst fnv u64 14695981039346656037) (defn f [] u64 (+ fnv 1))";
+    "(defconst fnv u64 0xcbf29ce484222325) (defn f [] u64 (+ fnv 1))";
   (* The form DISCUSS.org's note named: an unannotated let of a u64 constant.
      It binds a u64 and nothing about widening reaches it — a let with no type
      has no expectation to widen against, and the constant is what it says. *)
   accepts "an unannotated let of a u64 constant still binds a u64"
-    "(defconst fnv u64 14695981039346656037) \
+    "(defconst fnv u64 0xcbf29ce484222325) \
      (defn f [] u64 (let [h fnv] (* h 2)))";
   (* Shifts are the carve-out: the value's type decides and the count widens
      to it, never the reverse, because the result's width and the poison check

From 3efa2615390db4804955e8c0785c538c8490130d Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 18:45:39 +0700
Subject: [PATCH 09/17] A build artefact does not belong in the tree

---
 web-files-out.txt | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 web-files-out.txt

diff --git a/web-files-out.txt b/web-files-out.txt
deleted file mode 100644
index ff72b5c..0000000
--- a/web-files-out.txt
+++ /dev/null
@@ -1 +0,0 @@
-state

From 657f640ec7bc47a95ab96576f3fcc23a0ea356b0 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 19:21:16 +0700
Subject: [PATCH 10/17] A reconsidered operand must leave nothing behind, and a
 literal is never reconsidered

---
 lib/check.ml                | 126 +++++++++++++++++++++++++++---------
 runtime/flan_dyn.c          |  10 +--
 runtime/flan_dyn_stub.c     |  10 +--
 test/programs/widening.flan | 100 ++++++++++++++--------------
 test/test_flan.ml           |  30 +++++++++
 5 files changed, 189 insertions(+), 87 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index b6d2ed6..503e1d2 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -20,6 +20,19 @@
 
 let fail = Loc.fail
 
+(* "A literal could not be built at the type this site asked for": 300 at a u8,
+   1.5 at an i32, 3000000000 at the i32 an unconstrained integer defaults to.
+
+   It is kinded rather than left generic because one caller has to tell this
+   refusal apart from every other one. [binary] retries a refused operand
+   against the other operand's type (FIX.org 2026-09-20, implicit widening),
+   and it must not retry *this* one: a literal takes its width from the other
+   side and always could, so a literal that does not fit is the program's
+   mistake and not a pair of types that failed to meet. Without the kind the
+   retry turns (+ u8-thing 300) into i32 arithmetic, which is a different
+   language from the one the author decided on. *)
+let literal_at_want = "check/literal-at-want"
+
 (* [List.map]'s evaluation order is unspecified, and checking allocates frame
    slots as a side effect. Left-to-right is required, not a preference: a later
    let binding sees an earlier one, and slot numbering must be reproducible. *)
@@ -2692,7 +2705,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
       match want with
       | Some (Types.Float k) -> k
       | Some other when other <> Types.Never ->
-        fail loc "expected %s, found the float literal %g"
+        Loc.failk literal_at_want loc "expected %s, found the float literal %g"
           (Types.to_string other) x
       | _ -> Types.F64
     in
@@ -3039,7 +3052,7 @@ and int_literal loc ~want ?(default = Types.I32) n =
   | Some (Types.Float k) ->
     mk loc (Types.Float k) (Tast.Float (Int64.to_float n, k))
   | Some other when other <> Types.Never ->
-    fail loc "expected %s, found the integer literal %Ld"
+    Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
       (Types.to_string other) n
   | _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default))
 
@@ -3066,7 +3079,8 @@ and in_range loc k n =
       && Int64.compare n (Int64.shift_left 1L bits) < 0
   in
   if ok then n
-  else fail loc "%Ld does not fit in %s" n (Types.ikind_name k)
+  else Loc.failk literal_at_want loc "%Ld does not fit in %s" n
+      (Types.ikind_name k)
 
 (* The arms that are names rather than calls, and the same rule holds for them:
    each is in [builtins] below, and test_flan reads this match to check it. *)
@@ -7525,23 +7539,73 @@ and numeric_want want =
       construction: neither i32 nor u32 widens into the other, and the refusal
       says which cast to write.
 
-   [join_pair] is reached only when the *first* operand turned out to be the
-   narrower one. The other order needs nothing here: checking y against an i64
-   x already widens an i32 y inside [expect]. *)
-and join_pair ctx (a : Tast.expr) (y : Ast.expr) exn =
-  (* Asking y for [a]'s type failed. Either y is genuinely wrong, or y is
-     simply the wider operand and this is the one direction [expect] cannot
-     serve on its own. Check y on its own terms to find out; if it decides a
-     type that a widens into, a is the one that moves. Anything else re-raises
-     the original refusal, so an error inside y is still reported as itself and
-     no form that cannot check without an expectation — None, (zeroed) — loses
-     the expectation it used to get. *)
-  match check ctx y with
-  | exception _ -> raise exn
-  | b ->
-    if Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
-      widen a.Tast.loc b.Tast.ty a, b
-    else raise exn
+   The mechanism for 3 is a *trial*: ask y for [a]'s type, and if that refusal
+   is the one widening was invented for, look again the other way round. Two
+   things have to be true for a trial to be honest, and both are below.
+
+   [trial] is the first. Checking is not a function of its argument — it
+   allocates frame slots and it opens scopes — so a check that is abandoned
+   has to leave no trace, and [scoped] cannot help: it restores the scope on
+   the way *out*, which an exception does not take. Without this a binding
+   from the abandoned pass outlives it, which is visible as a name that should
+   be unknown resolving anyway, and worse, as a shadow: the inner binding of
+   (let [t ...] ... (let [t ...] t) ... t) survives into the outer t's slot
+   with nothing ever stored in it. That is an uninitialised read, produced by
+   a program the compiler accepted.
+
+   [literal_at_want] is the second. A trial that refused because a *literal*
+   could not be built at the wanted type is not a pair of types that failed to
+   meet — the literal had no type of its own to bring — so looking again would
+   answer with the literal's default and quietly move (+ u8-thing 300) to i32.
+   Rule 2 above is not a description of the old language kept for continuity;
+   it is what the author decided, and the kind is how the trial obeys it. *)
+and trial ctx f =
+  (* Everything a check writes into the context that is not the expression it
+     answers. [defers] and [defer_slot] are on the list even though a [defer]
+     inside an operand is already refused — [defer_ok] is cleared on entry to
+     [check] — because "already impossible elsewhere" is the kind of reason
+     that stops being true, and putting a field back costs nothing.
+
+     Only [Loc.Error] is caught. A timeout or a stack overflow is not a
+     refusal to reconsider, and silently continuing past one would turn a
+     resource failure into a wrong answer. *)
+  let scope = ctx.scope and slots = ctx.slots in
+  let slot_tys = ctx.slot_tys and slot_names = ctx.slot_names in
+  let defers = ctx.defers and defer_slot = ctx.defer_slot in
+  match f () with
+  | r -> Ok r
+  | exception Loc.Error d ->
+    ctx.scope <- scope; ctx.slots <- slots;
+    ctx.slot_tys <- slot_tys; ctx.slot_names <- slot_names;
+    ctx.defers <- defers; ctx.defer_slot <- defer_slot;
+    Error d
+
+(* Whether the trial's refusal is one worth reconsidering. A literal that did
+   not fit is not, and neither is a refusal a program cannot make any use of
+   having a second opinion on. *)
+and reconsiderable (d : Loc.diag) = not (String.equal d.Loc.kind literal_at_want)
+
+(* [a] was checked, y refused [a]'s type, and [b] is y on its own terms — held
+   by the caller when it has one, taken here when it does not. If the pair has
+   a join it can only be [b]'s type (had it been [a]'s, the trial would have
+   passed), so [a] is the operand that moves. *)
+and join_widen (a : Tast.expr) (b : Tast.expr) =
+  match Types.join a.Tast.ty b.Tast.ty with
+  | Some t when not (Types.equal t a.Tast.ty) ->
+    Some (widen a.Tast.loc t a, widen b.Tast.loc t b)
+  | _ -> None
+
+and join_pair ctx (a : Tast.expr) (y : Ast.expr) (d : Loc.diag) =
+  (* Check y on its own terms to find out whether it was simply the wider
+     operand. This trial is guarded too: if y cannot check without an
+     expectation at all — [None], [(zeroed)] — the original refusal is the one
+     reported, so no form loses the expectation it used to get. *)
+  match trial ctx (fun () -> check ctx y) with
+  | Error _ -> raise (Loc.Error d)
+  | Ok b ->
+    (match join_widen a b with
+     | Some pair -> pair
+     | None -> raise (Loc.Error d))
 
 and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
   match args with
@@ -7603,18 +7667,22 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
          that has to move. Nothing is checked a third time — the own-terms [b]
          already in hand is the answer. *)
       else
-        (match check ctx ~want:a.Tast.ty y with
-         | b' -> a, b'
-         | exception e ->
-           if join && Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
-             widen a.Tast.loc b.Tast.ty a, b
-           else raise e)
+        (match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
+         | Ok b' -> a, b'
+         | Error d ->
+           (match
+              if join && reconsiderable d then join_widen a b else None
+            with
+            | Some pair -> pair
+            | None -> raise (Loc.Error d)))
     end
     else begin
       let a = check ctx ?want x in
-      match check ctx ~want:a.Tast.ty y with
-      | b -> a, b
-      | exception e -> if join then join_pair ctx a y e else raise e
+      match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
+      | Ok b -> a, b
+      | Error d ->
+        if join && reconsiderable d then join_pair ctx a y d
+        else raise (Loc.Error d)
     end
   | _ -> fail loc "%s takes two arguments" name
 
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index 062a821..8e9a13a 100644
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@@ -1208,10 +1208,12 @@ int64_t flan_dyn_need_i64(flan_dyn v) {
 }
 
 /* A float, and an int is not one. Refusing the widening is the decision, not
- * an omission: typed Flan has no implicit widening anywhere — [(print-i64 x)]
- * used to force an explicit [(i64 x)] at every site — and a boundary that
- * quietly turned an int into a float would be the one place in the language
- * where a *value* changed type without anybody writing it down. The dyn
+ * an omission. The typed language does widen an integer into a float, but only
+ * where the float holds every value of it exactly — an i32 into an f64, never
+ * an i64 (FIX.org 2026-09-20). This boundary has no such guarantee to offer:
+ * the box carries one integer width and it is i64, so "an int here" means the
+ * widest one, which is exactly the conversion the typed lattice refuses. The
+ * dyn
  * *operators* promote, because arithmetic between a 2 and a 2.5 has an obvious
  * answer and refusing it makes dynamic code worse; the boundary into a typed
  * f64 parameter does not, because there the annotation is somebody's stated
diff --git a/runtime/flan_dyn_stub.c b/runtime/flan_dyn_stub.c
index 617c601..41eb8b7 100644
--- a/runtime/flan_dyn_stub.c
+++ b/runtime/flan_dyn_stub.c
@@ -112,10 +112,12 @@ flan_dyn flan_dyn_vec_new(void) {
 /* ── Arithmetic ────────────────────────────────────────────────────── */
 
 /* Two numbers promote to f64 when either is one, which is the rule a reader
- * expects of a dynamic language and is not the rule the typed language uses.
- * The typed language has no implicit widening at all; here there is no
- * annotation to have been written, so refusing would leave (+ 1 2.5) with no
- * spelling that works. */
+ * expects of a dynamic language and is still not the rule the typed language
+ * uses. The typed side widens only where nothing can be lost, and an i64 into
+ * an f64 can (FIX.org 2026-09-20), so (+ i64-x 2.5) is written there and is
+ * promoted here. The difference is not an oversight on either side: here there
+ * is no annotation to have been written, so refusing would leave (+ 1 2.5)
+ * with no spelling that works. */
 static int numeric(cell *c) { return c->tag == T_I64 || c->tag == T_F64; }
 static double as_f(cell *c) { return c->tag == T_I64 ? (double)c->u.i : c->u.f; }
 
diff --git a/test/programs/widening.flan b/test/programs/widening.flan
index 1062148..6b99021 100644
--- a/test/programs/widening.flan
+++ b/test/programs/widening.flan
@@ -23,59 +23,59 @@
 ;;;; is built at the wanted width by the literal rule and would never reach a
 ;;;; cast at all.
 
-(defvar i8-neg   i8   -5)
-(defvar i8-pos   i8    127)
-(defvar i16-neg  i16  -300)
-(defvar i32-neg  i32  -2000000000)
-(defvar i32-one  i32   1)
-(defvar i32-all  i32  -1)
-(defvar u8-max   u8    255)
-(defvar u16-max  u16   65535)
-(defvar u32-big  u32   4000000000)
-(defvar u32-max  u32   4294967295)
-(defvar i64-big  i64   5000000000)
-(defvar f32-half f32   0.5)
+(defvar w-i8neg   i8   -5)
+(defvar w-i8pos   i8    127)
+(defvar w-i16neg  i16  -300)
+(defvar w-i32neg  i32  -2000000000)
+(defvar w-i32one  i32   1)
+(defvar w-i32all  i32  -1)
+(defvar w-u8max   u8    255)
+(defvar w-u16max  u16   65535)
+(defvar w-u32big  u32   4000000000)
+(defvar w-u32max  u32   4294967295)
+(defvar w-i64big  i64   5000000000)
+(defvar w-f32half f32   0.5)
 
 ;; Widening at a parameter. Each of these is a plain typed function and the
 ;; call sites below hand it a narrower type with no cast written anywhere.
-(defn take-i64 [x i64] i64 x)
-(defn take-i16 [x i16] i16 x)
-(defn take-u64 [x u64] u64 x)
-(defn take-f64 [x f64] f64 x)
-(defn take-f32 [x f32] f32 x)
+(defn w-take-i64 [x i64] i64 x)
+(defn w-take-i16 [x i16] i16 x)
+(defn w-take-u64 [x u64] u64 x)
+(defn w-take-f64 [x f64] f64 x)
+(defn w-take-f32 [x f32] f32 x)
 
 ;; Widening at a return position: the body is an i32 and the signature is i64.
-(defn ret-widened [] i64 i32-neg)
+(defn w-ret-widened [] i64 w-i32neg)
 
 ;; Widening in a binary operator, both orders. The first is the direction
 ;; [expect] already served; the second is the one the join rule added.
-(defn add-wide-first [] i64 (+ i64-big i32-one))
-(defn add-narrow-first [] i64 (+ i32-one i64-big))
+(defn w-add-wide-first [] i64 (+ w-i64big w-i32one))
+(defn w-add-narrow-first [] i64 (+ w-i32one w-i64big))
 
 (defn main [args [string]] i32
   ;; ── integer to integer ──────────────────────────────────────────
-  (println (take-i64 i8-neg))            ;; -5
-  (println (take-i64 i8-pos))            ;; 127
-  (println (take-i64 i16-neg))           ;; -300
-  (println (take-i64 i32-all))           ;; -1
-  (println (take-i64 i32-neg))           ;; -2000000000
-  (println (take-i16 u8-max))            ;; 255
-  (println (take-i64 u8-max))            ;; 255
-  (println (take-i64 u16-max))           ;; 65535
-  (println (take-i64 u32-big))           ;; 4000000000
-  (println (take-i64 u32-max))           ;; 4294967295
-  (println (take-u64 u32-big))           ;; 4000000000
-  (println (take-u64 u8-max))            ;; 255
+  (println (w-take-i64 w-i8neg))            ;; -5
+  (println (w-take-i64 w-i8pos))            ;; 127
+  (println (w-take-i64 w-i16neg))           ;; -300
+  (println (w-take-i64 w-i32all))           ;; -1
+  (println (w-take-i64 w-i32neg))           ;; -2000000000
+  (println (w-take-i16 w-u8max))            ;; 255
+  (println (w-take-i64 w-u8max))            ;; 255
+  (println (w-take-i64 w-u16max))           ;; 65535
+  (println (w-take-i64 w-u32big))           ;; 4000000000
+  (println (w-take-i64 w-u32max))           ;; 4294967295
+  (println (w-take-u64 w-u32big))           ;; 4000000000
+  (println (w-take-u64 w-u8max))            ;; 255
 
   ;; ── a widened return ────────────────────────────────────────────
-  (println (ret-widened))                ;; -2000000000
+  (println (w-ret-widened))                ;; -2000000000
 
   ;; ── integer to float, exact only ────────────────────────────────
-  (println (take-f64 i32-neg))           ;; -2000000000.0
-  (println (take-f64 u32-max))           ;; 4294967295.0
-  (println (take-f64 i8-neg))            ;; -5.0
-  (println (take-f32 i16-neg))           ;; -300.0
-  (println (take-f32 u16-max))           ;; 65535.0
+  (println (w-take-f64 w-i32neg))           ;; -2000000000.0
+  (println (w-take-f64 w-u32max))           ;; 4294967295.0
+  (println (w-take-f64 w-i8neg))            ;; -5.0
+  (println (w-take-f32 w-i16neg))           ;; -300.0
+  (println (w-take-f32 w-u16max))           ;; 65535.0
 
   ;; The printer answers %g, which rounds an f64 long before the bits it is
   ;; carrying run out, so the exactness the int-to-float boundary is chosen for
@@ -83,27 +83,27 @@
   ;; these is the difference between the widened value and the number it is
   ;; supposed to be, and a conversion that lost anything answers something
   ;; other than the last unit.
-  (println (- (take-f64 u32-max) 4294967294.0))   ;; 1
-  (println (- (take-f64 i32-neg) -1999999999.0))  ;; -1
-  (println (- (take-f32 u16-max) 65534.0))        ;; 1
+  (println (- (w-take-f64 w-u32max) 4294967294.0))   ;; 1
+  (println (- (w-take-f64 w-i32neg) -1999999999.0))  ;; -1
+  (println (- (w-take-f32 w-u16max) 65534.0))        ;; 1
 
   ;; ── float to float ──────────────────────────────────────────────
-  (println (take-f64 f32-half))          ;; 0.5
+  (println (w-take-f64 w-f32half))          ;; 0.5
 
   ;; ── the binary join, both operand orders ────────────────────────
-  (println (add-wide-first))             ;; 5000000001
-  (println (add-narrow-first))           ;; 5000000001
+  (println (w-add-wide-first))             ;; 5000000001
+  (println (w-add-narrow-first))           ;; 5000000001
   ;; The narrower operand is the first one, and the sum is an i64 even though
   ;; nothing on this line is annotated.
-  (println (+ i32-neg i64-big))          ;; 3000000000
+  (println (+ w-i32neg w-i64big))          ;; 3000000000
   ;; A comparison joins the same way, and the widened -1 must still be -1.
-  (println (< i32-all i64-big))          ;; true
+  (println (< w-i32all w-i64big))          ;; true
   ;; min and max over two widths answer at the wider one.
-  (println (max i8-neg i16-neg))         ;; -5
-  (println (min i8-neg i32-neg))         ;; -2000000000
+  (println (max w-i8neg w-i16neg))         ;; -5
+  (println (min w-i8neg w-i32neg))         ;; -2000000000
   ;; A count narrower than the value widens to it; the value's width decides.
-  (println (<< i64-big i8-pos))          ;; 0 -- masked to 127 mod 64 = 63
+  (println (<< w-i64big w-i8pos))          ;; 0 -- masked to 127 mod 64 = 63
   ;; An expectation reaches the operands, so this adds at i64 rather than
   ;; wrapping at i32 and widening the sum afterwards.
-  (println (take-i64 (+ i32-neg i32-neg)))  ;; -4000000000
+  (println (w-take-i64 (+ w-i32neg w-i32neg)))  ;; -4000000000
   0)
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 5f37f12..4d1c557 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1009,6 +1009,36 @@ let () =
   accepts "an unannotated let of a u64 constant still binds a u64"
     "(defconst fnv u64 0xcbf29ce484222325) \
      (defn f [] u64 (let [h fnv] (* h 2)))";
+  (* A literal that does not fit is the program's mistake, not a pair of types
+     that failed to meet, so the join must not reconsider it — the operand it
+     would reconsider against is the one the literal was supposed to take its
+     width *from*. Both spellings: the literal written as the operand, and the
+     literal buried in one. *)
+  rejects_check "a literal that does not fit is still refused"
+    "(defvar m u8) (defn f [] u8 (+ m 300))" ~needle:"300 does not fit in u8";
+  rejects_check "and is refused inside an operand too"
+    "(defvar m u8) (defn f [] u8 (+ m (+ 300 1)))"
+    ~needle:"300 does not fit in u8";
+  rejects_check "a float literal still cannot stand where an int is wanted"
+    "(defvar n i32) (defn f [] i32 (+ n 1.5))"
+    ~needle:"found the float literal 1.5";
+  accepts "a literal that does fit still takes the operand's type"
+    "(defvar m u8) (defn f [] u8 (+ m 200))";
+
+  (* The join reconsiders a refused operand, and a reconsidered pass must leave
+     nothing behind. [scoped] cannot see to that — it puts the scope back on
+     the way out, which an exception does not take — so [binary] snapshots and
+     restores around each trial. Both symptoms of not doing it: a binding that
+     outlives the pass that made it, and the same binding *shadowing* a live
+     one, which is an uninitialised read in a program the compiler accepted. *)
+  rejects_check "an abandoned trial leaves no binding behind"
+    "(defvar n i32) (defvar w i64) \
+     (defn f [] i32 (println (+ n (let [q w] q))) (println q) 0)"
+    ~needle:"unknown name q";
+  accepts "and does not shadow the binding it was nested in"
+    "(defvar n i32) (defvar w i64) \
+     (defn f [] i32 (let [t n] (println (+ n (let [t w] t))) (println t)) 0)";
+
   (* Shifts are the carve-out: the value's type decides and the count widens
      to it, never the reverse, because the result's width and the poison check
      both belong to the value. *)

From b4dbbb67ab97ff92b82d76eadb9e7ca0dcfa3986 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 19:25:17 +0700
Subject: [PATCH 11/17] The review's three findings, and the lanes this one
 landed on top of

---
 FIX.org           | 105 +++++++++++++++++++++++++++++++++++++++++++---
 test/test_flan.ml |  20 +++++----
 2 files changed, 112 insertions(+), 13 deletions(-)

diff --git a/FIX.org b/FIX.org
index 57a8b61..bc02ade 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2526,11 +2526,26 @@ decides-rule generalises rather than disappearing:
    operands as before, and now widens them. The addition happens at ~i64~, not
    at ~i32~ followed by a widened result. That is the better of the two and it
    is only reachable by programs that did not compile before.
-2. *Literals decide exactly as they did.* ~y_decides~ and ~needs_want~ are
-   untouched: a literal takes its width from the other operand, a float
-   literal outranks an integer one. ~(+ x 1)~ over a ~u64~ ~x~ still builds a
-   ~u64~ one, which is what keeps ~(let [h fnv-offset])~ with a ~u64~
-   ~defconst~ meaning exactly what it meant.
+2. *Literals decide exactly as they did, and this one had to be defended.*
+   ~y_decides~ and ~needs_want~ are untouched: a literal takes its width from
+   the other operand, a float literal outranks an integer one. ~(+ x 1)~ over a
+   ~u64~ ~x~ still builds a ~u64~ one, which is what keeps
+   ~(let [h fnv-offset])~ with a ~u64~ ~defconst~ meaning exactly what it
+   meant.
+
+   Saying so was not enough. The join is implemented as a *trial* — ask the
+   second operand for the first's type, and reconsider if it refuses — and the
+   first version of it reconsidered a literal too, which silently moved
+   ~(+ u8-thing 300)~ from "300 does not fit in u8" to i32 arithmetic
+   answering 555, asymmetric in the operand order, and ~(+ i32-x 1.5)~ to an
+   f64 add. That is a different language from the one decided on. A literal
+   that does not fit is the program's mistake and not a pair of types that
+   failed to meet — the literal had no type of its own to bring — so the three
+   refusals that say so (~in_range~, and the integer and float literal arms of
+   ~check~) now carry the kind ~check/literal-at-want~, and the trial re-raises
+   on sight of it rather than looking again. Pinned four ways: the literal as
+   the operand, the literal buried inside one, the float-literal spelling, and
+   a literal that *does* fit still taking the operand's type.
 3. *Otherwise the wider side decides* — ~Types.join~: whichever operand the
    other widens into, with the loser wrapped in a ~Cast~ to it. ~(+ i32-var
    i64-var)~ is ~i64~ and is newly legal. ~(min i8-var i16-var)~ is ~i16~.
@@ -2638,7 +2653,10 @@ what was true when they were written.
   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
+  LLVM output is byte-identical for all of them — after the same
+  prelude-line normalisation the x86 comparison needs, which the LLVM diff gets
+  for free because it spells those strings out as text where x86 emits them as
+  ~.byte~ data. 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
@@ -2659,3 +2677,78 @@ what was true when they were written.
   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.
+
+** Review round two: what the first version got wrong
+Three findings, all in the mechanism rather than in the lattice, and all from
+the same root — the join is implemented as a *trial* (ask the second operand
+for the first operand's type; reconsider only if that refuses), and a trial
+that catches an exception is not free the way a trial that returns an option
+is.
+
+*1. An abandoned trial left its bindings behind.* ~scoped~ restores
+~ctx.scope~ on the way out, and an exception does not take that way out — so
+every binding the abandoned pass made survived into the enclosing scope. Two
+symptoms, and the second is the serious one:
+
+- a name that should be unknown resolved anyway, and
+- the abandoned binding *shadowed* a live one. ~(let [t i32-x] (println (+
+  i32-x (let [t i64-y] t))) (println t))~ printed the sum and then ~0~ — the
+  outer ~t~ read through the dead inner binding's slot, which nothing ever
+  stored into. An uninitialised stack read, in a program the compiler
+  accepted, on both backends.
+
+Fixed with ~trial~, which snapshots ~scope~, ~slots~, ~slot_tys~,
+~slot_names~, ~defers~ and ~defer_slot~ and puts all six back when the trial
+refuses. ~scoped~ itself is untouched — it is shared by every scope-opening
+form in the file and this is not its problem to solve. ~trial~ also narrows
+the catch to ~Loc.Error~: a timeout or a stack overflow is not a refusal to
+reconsider, and continuing past one would turn a resource failure into a wrong
+answer. Both symptoms pinned.
+
+*2. The trial reconsidered literals.* Written up under the join rule above.
+The short version: ~(+ u8-thing 300)~ compiled, at i32, answering 555. The
+decision was literals-unchanged and now the code says so, by kind rather than
+by hope.
+
+*3. Three globals collided with the prelude.* The dogfood batch added
+~u8-max~, ~u16-max~ and ~u32-max~ as prelude ~defconst~s while this lane was
+open, and the acceptance program had defined its own. The textual merge was
+clean and all three acceptance rows died on "defined twice" in the merged
+tree, which is precisely the failure a per-lane ~dune test~ cannot see. Every
+global and function in test/programs/widening.flan now carries a ~w-~ prefix,
+and the rows were re-run in a trial-merged tree rather than only on the lane.
+
+** Collisions with the lanes that landed underneath
+Three, each read by hand rather than trusted to the auto-merge:
+
+- *The diagnostics lane* kinded ~expect~'s mismatch as
+  ~check/type-mismatch~ so a call-argument site can recognise it. Its wording
+  and its mechanism win; ~numeric_note~ rides on the same message, because a
+  reader who has just been told i64 and i32 are different types needs telling
+  in the same breath which direction needed nothing.
+- *The struct lane* added ~check_bare~ and ~positional_struct~. No overlap:
+  it calls ~expect~, this lane added an arm inside it. The intersection — a
+  struct literal whose field initialisers widen — was compiled and run on both
+  backends by hand.
+- *The int/float alias lane* pinned ~(+ int-var i64-var)~ as a type error,
+  with a comment saying the pin was written as identity so it would survive
+  whatever the widening table grew into. It was not written that way — it
+  pinned a refusal and a message — and it is the one refusal pin in the suite
+  this lane makes legal. Rewritten to pin identity for real: the mixed form is
+  accepted at i64 under ~int~ exactly as under ~i32~, and the narrowing back
+  into ~int~ is still refused, naming ~i32~ because that is what ~int~ erases
+  to.
+
+** Stale claims elsewhere, and one left alone
+~runtime/flan_dyn.c~'s ~flan_dyn_need_f64~ note and
+~runtime/flan_dyn_stub.c~'s arithmetic note both said the typed language has
+no implicit widening at all. Rewritten, and the rewrite is not a hedge: the
+typed language *does* widen an integer into a float now, but only the exact
+ones, and the dyn box carries integers at i64 — the one width that reaches no
+float on the lattice. So both boundaries refuse exactly what they refused, for
+a reason that is now stated correctly.
+
+~web/index.html~ (two places) makes the same stale claim. *Left alone
+deliberately*: the website has its own rewrite lane, and a marketing page is
+not the place for this lane to be making edits it cannot test. Flagged here so
+that lane picks it up.
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 4d1c557..c7545cc 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2815,13 +2815,19 @@ let () =
     "(defn f [] int 1.5)" ~needle:"expected i32";
   rejects_check "and one under float names f32"
     "(defn f [] float (f64 1.0))" ~needle:"expected f32";
-  (* Widening needs no entry for [int] because [int] *is* [i32]: the mixed
-     arithmetic that i32 refuses, int refuses identically and by the same
-     message. Pinned as identity rather than as a widening rule, so it says
-     the same thing whatever the widening table grows into. *)
-  rejects_check "int mixes with i64 exactly as i32 does"
-    "(defvar a int) (defvar b i64) (defn f [] i64 (+ a b))"
-    ~needle:"expected i64, found i32";
+  (* Widening needs no entry for [int] because [int] *is* [i32], and this pin
+     says exactly that and nothing about what the widening table holds. It used
+     to read the other way round — the mixed arithmetic that i32 *refuses*,
+     int refuses identically — which was true when it was written and stopped
+     being true when implicit widening landed (FIX.org 2026-09-20): an i32 and
+     an i64 now meet at i64, so the same form under [int] has to be accepted,
+     and accepted at i64. Kept pointing at identity by pinning both directions:
+     the one that widens, and the one that still cannot. *)
+  accepts "int mixes with i64 exactly as i32 does"
+    "(defvar a int) (defvar b i64) (defn f [] i64 (+ a b))";
+  rejects_check "and refuses the narrowing exactly as i32 does"
+    "(defvar a int) (defvar b i64) (defn f [] int (+ a b))"
+    ~needle:"expected i32, found i64";
   (* A program that declared the alias itself — which this one's author did,
      before it was builtin. True as written, it is the no-op it says it is;
      pointed anywhere else it is refused, because the alias table is never

From eb0d883e84b02187476c756a2adf84445bf9f9e5 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 19:33:32 +0700
Subject: [PATCH 12/17] The suite is green on its own merits now, and the sweep
 says so against the new tip

---
 FIX.org           | 18 ++++++++++++------
 web-files-out.txt |  1 +
 2 files changed, 13 insertions(+), 6 deletions(-)
 create mode 100644 web-files-out.txt

diff --git a/FIX.org b/FIX.org
index bc02ade..4317899 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2625,12 +2625,14 @@ 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".
+- ~dune test --root . --force~ — exit 0, 0 FAIL lines, on the lane *and* in a
+  trial-merged tree. Through most of this lane it exited 1 instead, from
+  ~test_dev.ml~'s ~trap_park~ rows racing and dying with
+  ~Fatal error: exception Flan.Wire.Closed~ at ~dev-trap-null-alloc~ — measured
+  on an untouched worktree at dev-loop's tip with nothing of this lane in it,
+  and written up above under "Found while running it". Another lane has since
+  fixed it (~trap_park stops dying on the abort race~), so the green run is a
+  real green run rather than a lucky one.
 - 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.
@@ -2639,6 +2641,10 @@ what was true when they were written.
   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.
+- *Verified in a trial-merged tree, not only on the lane.* dev-loop moved
+  five times while this was open, so the branch was rebased onto each tip and
+  the acceptance rows, the full suite and the sweep were re-run against the
+  last one. The merge into dev-loop is a fast-forward with no conflicts.
 - *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
diff --git a/web-files-out.txt b/web-files-out.txt
new file mode 100644
index 0000000..ff72b5c
--- /dev/null
+++ b/web-files-out.txt
@@ -0,0 +1 @@
+state

From 8ea1ff44811c63310a50d3ca0c4274e102ef9cd0 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 19:36:06 +0700
Subject: [PATCH 13/17] The build artefact, out of the tree for good this time

---
 web-files-out.txt | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 web-files-out.txt

diff --git a/web-files-out.txt b/web-files-out.txt
deleted file mode 100644
index ff72b5c..0000000
--- a/web-files-out.txt
+++ /dev/null
@@ -1 +0,0 @@
-state

From 114ea391aa297c5105890f2b3ac5fa3e6edfee97 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 19:38:37 +0700
Subject: [PATCH 14/17] One more dev-daemon row that raced, seen once in five

---
 FIX.org | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/FIX.org b/FIX.org
index 4317899..e9a6da5 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2633,6 +2633,14 @@ what was true when they were written.
   and written up above under "Found while running it". Another lane has since
   fixed it (~trap_park stops dying on the abort race~), so the green run is a
   real green run rather than a lucky one.
+
+  One *other* ~test_dev.ml~ row failed once across five runs of identical
+  code — "the merged program never bound ...agent.sock", a daemon that did not
+  come up in time — and was green on the four runs either side of it, on the
+  lane and in the merged tree. Recorded rather than chased: it is a socket
+  bind in the agent fixture, and this lane touches neither the agent nor the
+  dyn side. It looks like the same family as the ~trap_park~ race that was
+  just fixed, one row further along.
 - 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.

From 0d34831199927f812c955da425cd086fad345d90 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 19:51:51 +0700
Subject: [PATCH 15/17] A trial puts the whole context back, and the compiler
 now insists on it

---
 FIX.org           | 57 +++++++++++++++++++++++++++++++++++++++++------
 lib/check.ml      | 55 ++++++++++++++++++++++++++++++++++++---------
 test/test_flan.ml | 17 ++++++++++++++
 3 files changed, 112 insertions(+), 17 deletions(-)

diff --git a/FIX.org b/FIX.org
index e9a6da5..19fb1eb 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2711,13 +2711,56 @@ symptoms, and the second is the serious one:
   stored into. An uninitialised stack read, in a program the compiler
   accepted, on both backends.
 
-Fixed with ~trial~, which snapshots ~scope~, ~slots~, ~slot_tys~,
-~slot_names~, ~defers~ and ~defer_slot~ and puts all six back when the trial
-refuses. ~scoped~ itself is untouched — it is shared by every scope-opening
-form in the file and this is not its problem to solve. ~trial~ also narrows
-the catch to ~Loc.Error~: a timeout or a stack overflow is not a refusal to
-reconsider, and continuing past one would turn a resource failure into a wrong
-answer. Both symptoms pinned.
+Fixed with ~trial~, which snapshots the context and puts it back when the
+trial refuses. ~scoped~ itself is untouched — it is shared by every
+scope-opening form in the file and this is not its problem to solve. ~trial~
+also narrows the catch to ~Loc.Error~: a timeout or a stack overflow is not a
+refusal to reconsider, and continuing past one would turn a resource failure
+into a wrong answer.
+
+*The first version of that fix restored six chosen fields, and the choice was
+wrong.* Review round three found three more, and the worst of them inverts the
+symptom: where a leaked binding produces a false *accept*, a leaked window
+produces a false *refusal*.
+
+- ~in_frames~. ~check_frames~ sets it, threads the expectation into the body's
+  last form, and clears it on the way out. A trial abandoned inside that
+  window leaves the flag stuck, so
+
+    : (println (+ i32-x (handler-bind [] i64-y)))
+    : (return 0)
+
+  — which compiled before this lane and compiles again now — was refused with
+  "return is not allowed inside handler-bind yet", pointing at a line with no
+  ~handler-bind~ within sight of it. A valid program refused for a reason that
+  is not in the program.
+- ~loops~, the same window via ~loop~: a leaked ~Lrecur~ made an invalid
+  ~break~ answer "the nearest loop is a (loop ...), which answers with the
+  value of its body" instead of "break is only allowed inside a loop". No bad
+  accept, a thoroughly misleading refusal.
+- ~defer_block~, message text only, and leaked with ~loops~.
+
+*So the subset was replaced by the whole record.* ~trial~ now restores every
+mutable field of ~ctx~ — the three above, the six from round two, and
+~defer_ok~, ~tail~ and ~outer_what~, which would self-heal on their own and
+are restored anyway, because "this one cannot currently leak" is precisely the
+reasoning that produced two rounds of leaks. The destructuring is closed and
+carries ~[@warning "+9"]~, so adding a field to ~ctx~ stops ~trial~ compiling
+until somebody decides about it. *Verified that the guard guards*: removing
+one field from the pattern by hand fails the build, naming the field.
+
+One thing is deliberately not restored, and it is on ~env~ rather than ~ctx~:
+an abandoned trial that lifted a function out of an ~fn~ literal leaves it in
+~env.lifted~. That is dead and harmless — the names are ~fn/<owner>/N~ handed
+out by count, so the live pass gets fresh ones and nothing refers to the
+orphan — and it rides into the module as a function nobody calls. Left because
+~env~ is the program's table rather than this form's, and rewinding it would
+mean deciding what else on ~env~ a trial may have touched; the one piece of
+~env~ state that genuinely needs rewinding, the generic instantiation cache,
+already rewinds itself in ~instantiate~.
+
+All five symptoms pinned — the two accepts, the shadow, the unknown name, and
+the loop diagnostic.
 
 *2. The trial reconsidered literals.* Written up under the join rule above.
 The short version: ~(+ u8-thing 300)~ compiled, at i32, answering 555. The
diff --git a/lib/check.ml b/lib/check.ml
index 503e1d2..a1b721a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -7560,24 +7560,59 @@ and numeric_want want =
    Rule 2 above is not a description of the old language kept for continuity;
    it is what the author decided, and the kind is how the trial obeys it. *)
 and trial ctx f =
-  (* Everything a check writes into the context that is not the expression it
-     answers. [defers] and [defer_slot] are on the list even though a [defer]
-     inside an operand is already refused — [defer_ok] is cleared on entry to
-     [check] — because "already impossible elsewhere" is the kind of reason
-     that stops being true, and putting a field back costs nothing.
+  (* Everything a check writes into the context, put back if the check is
+     abandoned — and it is *everything* on purpose, not a chosen subset.
+
+     Picking the fields that looked like they mattered was tried twice and was
+     wrong twice. [scope] and the slot fields were the first round, found as an
+     uninitialised read. The second round was worse, because the symptom was
+     the other way up: a form that opens a window and closes it on the way out
+     — [check_frames] setting [in_frames], [loop] pushing onto [loops] — leaves
+     that window *open* when a trial inside it is abandoned, and then refuses
+     a perfectly good program.
+
+       (println (+ i32-x (handler-bind [] i64-y)))
+       (return 0)
+
+     compiled before this lane and was refused after it, with "return is not
+     allowed inside handler-bind yet" pointing at a line with no handler-bind
+     anywhere near it. A false refusal is not a lesser bug than a false accept;
+     it is just quieter about being one.
+
+     So the rule here is not judgement, it is the whole record. Three fields
+     would have self-healed anyway — [defer_ok] and [tail] are read and cleared
+     on entry to [check], [outer_what] is never written after the context is
+     built — and they are restored regardless, because "this one cannot
+     currently leak" is exactly the reasoning that produced two rounds of
+     leaks. The destructuring below is closed and warning 9 is turned on for
+     it, so a new field on [ctx] stops this function compiling until somebody
+     decides about it, rather than joining the list of things nobody noticed.
+
+     What is *not* restored, once, deliberately: [env.lifted] keeps whatever
+     function an abandoned trial lifted out of an [fn] literal. It is dead —
+     the names are [fn/<owner>/N] handed out by count, so the live pass gets
+     fresh ones and nothing refers to the orphan — and it rides along into the
+     module as a function nobody calls. Left alone because [env] is the
+     program's table and not this form's, and rewinding it would mean deciding
+     what else on [env] a trial may have touched; the generic instantiation
+     cache already rolls itself back, in [instantiate].
 
      Only [Loc.Error] is caught. A timeout or a stack overflow is not a
      refusal to reconsider, and silently continuing past one would turn a
      resource failure into a wrong answer. *)
-  let scope = ctx.scope and slots = ctx.slots in
-  let slot_tys = ctx.slot_tys and slot_names = ctx.slot_names in
-  let defers = ctx.defers and defer_slot = ctx.defer_slot in
+  let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
+                       defers; defer_slot; defer_ok; defer_block; outer = _;
+                       outer_what; in_frames; loops; tail; in_defer;
+                       owner = _ } = ctx in
   match f () with
   | r -> Ok r
   | exception Loc.Error d ->
-    ctx.scope <- scope; ctx.slots <- slots;
-    ctx.slot_tys <- slot_tys; ctx.slot_names <- slot_names;
+    ctx.slots <- slots; ctx.slot_tys <- slot_tys;
+    ctx.slot_names <- slot_names; ctx.scope <- scope;
     ctx.defers <- defers; ctx.defer_slot <- defer_slot;
+    ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
+    ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
+    ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
     Error d
 
 (* Whether the trial's refusal is one worth reconsidering. A literal that did
diff --git a/test/test_flan.ml b/test/test_flan.ml
index c7545cc..06b0698 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1031,6 +1031,23 @@ let () =
      restores around each trial. Both symptoms of not doing it: a binding that
      outlives the pass that made it, and the same binding *shadowing* a live
      one, which is an uninitialised read in a program the compiler accepted. *)
+  (* The other half, and the one that bites harder: a form that opens a window
+     and closes it on the way out leaves it *open* when a trial inside it is
+     abandoned, and then refuses a program that is fine. Both windows — the
+     frames [handler-bind] establishes, and the loop [loop] pushes — with the
+     refusal each would wrongly produce written as the second half of the
+     test, so a regression shows up as the message coming back rather than as
+     a silent accept. *)
+  accepts "an abandoned trial inside handler-bind does not leave its frames up"
+    "(defvar n i32) (defvar w i64) \
+     (defn f [] i32 (println (+ n (handler-bind [] w))) (return 0))";
+  accepts "nor does one inside a loop leave the loop up"
+    "(defvar n i32) (defvar w i64) \
+     (defn f [] i32 (println (+ n (loop [i 0] w))) (defer (println 1)) 0)";
+  rejects_check "and a break outside every loop still says so plainly"
+    "(defvar n i32) (defvar w i64) \
+     (defn f [] i32 (println (+ n (loop [i 0] w))) (break) 0)"
+    ~needle:"break is only allowed inside a loop";
   rejects_check "an abandoned trial leaves no binding behind"
     "(defvar n i32) (defvar w i64) \
      (defn f [] i32 (println (+ n (let [q w] q))) (println q) 0)"

From 765562f23eef867f3f358e035c369596a5dfbc1e Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 19:58:49 +0700
Subject: [PATCH 16/17] The racy agent row has a cause: a busy machine, not a
 wrong compiler

---
 FIX.org | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/FIX.org b/FIX.org
index 19fb1eb..bd6cf92 100644
--- a/FIX.org
+++ b/FIX.org
@@ -2634,13 +2634,17 @@ what was true when they were written.
   fixed it (~trap_park stops dying on the abort race~), so the green run is a
   real green run rather than a lucky one.
 
-  One *other* ~test_dev.ml~ row failed once across five runs of identical
+  One *other* ~test_dev.ml~ row failed twice across seven runs of identical
   code — "the merged program never bound ...agent.sock", a daemon that did not
-  come up in time — and was green on the four runs either side of it, on the
-  lane and in the merged tree. Recorded rather than chased: it is a socket
-  bind in the agent fixture, and this lane touches neither the agent nor the
-  dyn side. It looks like the same family as the ~trap_park~ race that was
-  just fixed, one row further along.
+  come up in time — and was green on every run either side, on the lane and in
+  the merged tree. The second failure named its own cause: the corpus sweep was
+  compiling in another worktree on the same machine, and the row gives the
+  daemon a fixed window to bind in. Run on an idle machine it is green.
+  Recorded rather than chased: it is a socket bind in the agent fixture, this
+  lane touches neither the agent nor the dyn side, and it looks like the same
+  family as the ~trap_park~ race that was just fixed, one row further along —
+  a timeout that is generous when nothing else is running and is not
+  otherwise.
 - 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.

From f1721e650c6e660bb07bbb8cec36a2390c0fc57c Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 20 Sep 2026 20:06:26 +0700
Subject: [PATCH 17/17] The lane caught up by merge, because every commit of it
 touches the notes

---
 FIX.org | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/FIX.org b/FIX.org
index b251e48..27e1313 100644
--- a/FIX.org
+++ b/FIX.org
@@ -3109,9 +3109,13 @@ what was true when they were written.
   operand orders, the literal rule still standing, and the shift carve-out in
   both directions.
 - *Verified in a trial-merged tree, not only on the lane.* dev-loop moved
-  five times while this was open, so the branch was rebased onto each tip and
-  the acceptance rows, the full suite and the sweep were re-run against the
-  last one. The merge into dev-loop is a fast-forward with no conflicts.
+  eight times while this was open, and the acceptance rows, the full suite and
+  the sweep were re-run against the last of them. The branch caught up by
+  rebase until the notes file made that expensive — every commit of this lane
+  touches FIX.org and so conflicted with every landing that also did — and
+  finishes with an ordinary merge of dev-loop into the lane instead, resolved
+  once. The merge back into dev-loop is clean, and was built, run and tested
+  as a merged tree rather than only on the branch.
 - *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