The review's three findings, and the lanes this one landed on top of

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
+2. *Literals decide exactly as they did, and this one had to be defended.*
-   untouched: a literal takes its width from the other operand, a float
+   ~y_decides~ and ~needs_want~ are untouched: a literal takes its width from
-   literal outranks an integer one. ~(+ x 1)~ over a ~u64~ ~x~ still builds a
+   the other operand, a float literal outranks an integer one. ~(+ x 1)~ over a
-   ~u64~ one, which is what keeps ~(let [h fnv-offset])~ with a ~u64~
+   ~u64~ ~x~ still builds a ~u64~ one, which is what keeps
-   ~defconst~ meaning exactly what it meant.
+   ~(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.

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
+  (* Widening needs no entry for [int] because [int] *is* [i32], and this pin
-     arithmetic that i32 refuses, int refuses identically and by the same
+     says exactly that and nothing about what the widening table holds. It used
-     message. Pinned as identity rather than as a widening rule, so it says
+     to read the other way round — the mixed arithmetic that i32 *refuses*,
-     the same thing whatever the widening table grows into. *)
+     int refuses identically — which was true when it was written and stopped
-  rejects_check "int mixes with i64 exactly as i32 does"
+     being true when implicit widening landed (FIX.org 2026-09-20): an i32 and
-    "(defvar a int) (defvar b i64) (defn f [] i64 (+ a b))"
+     an i64 now meet at i64, so the same form under [int] has to be accepted,
-    ~needle:"expected i64, found i32";
+     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