The lattice of conversions that cannot change the number

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.

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