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