Merge branch 'worktree-agent-aa39c3fbfc562d62a' into dev-loop

# Conflicts:
#	FIX.org

FIX.org

@@ -3870,3 +3870,110 @@ annotated element type is reported at the generator's answer — expected u8,
 found f64, caret on the offending expression — per element, not per array.
 Named defn generators check exactly as before, arity and index types in
 array-gen's own words.
+* integer?, the collapsed abs, and the join, 2026-09-20
+The author's brief, verbatim in spirit: we want generic arithmetic as much as
+possible; we are failing if a function that can be generalized needs variants
+for different numerical types.
+
+** integer?, the fifth predicate
+~numeric?~ was one type too wide for a family of bodies. It is the only bound
+that admits a written 0, and it admits f32 and f64 too — so an integer body
+under it was instantiated at the floats, where ~(if (< x 0) (- 0 x) x)~ is
+the wrong abs (a -0.0 comes back negative) and the bitwise operators, the
+shifts and an integer-only ~%~ mean nothing at all. ~integer?~ admits every
+integer kind, signed and unsigned, at every width, and refuses floats and
+everything else: ~Types.is_integer~, wired into ~predicate_names~,
+~pred_holds~ and the entailment table.
+
+The entailments run one way. ~integer?~ entails ~numeric?~ — every integer is
+a number, so the arithmetic, the written 0 and the untyped integer literal
+all come with the one clause, through the same ~int_literal~ arm ~numeric?~
+uses — and through it ~ordered?~ and ~equal?~. The reverse does not exist,
+because it would let floats into ~bit-and~.
+
+What it unlocked in the checker: the bitwise fold asks ~unconstrained~ for
+~integer?~ now instead of ~numeric?~ (so ~(bit-and x 1)~ in a ~numeric?~ body
+is refused at the *definition*, not from inside the generic's source at
+whichever call site first instantiated at a float), and the shifts admit an
+~integer?~-bounded variable where they refused every variable before. The
+float literal in an ~integer?~-bounded body gets the bound's own sentence:
+there is no instantiation at which it means anything. ~%~ stays ~numeric?~
+deliberately — a typed float ~(% x y)~ is fmod and always was
+(test/programs/math3.flan pins the four sign cases), and tightening it would
+be a semantics change this predicate does not ask for.
+
+** abs, collapsed
+~abs-i32~ and ~abs-i64~ existed per width only because ~numeric?~ admitted
+floats. They are one ~(defn abs [x $t] $t {:where (integer? $t)} ...)~ now,
+answering at all six-and-more integer widths; the copies at i32 and i64 even
+keep the old symbols, since an instantiation mangles to ~abs-i32~ and
+~abs-i64~.
+
+The decision between "integer? plus the float overloads" and "one numeric?
+generic with a float-safe body": there is no float-safe body to write. ~(max
+x (- 0 x))~ picks whichever zero sits in the wrong slot because -0.0 and 0.0
+compare equal, and the branch spelling hands -0.0 back unchanged. The right
+float abs is a sign-bit clear, which is libm's fabs and is already declared —
+~abs-f32~/~abs-f64~ stay as the float spellings, and ~(abs 1.5)~ is refused
+naming the bound. For that refusal to be the one a float caller sees,
+~instantiate~ now checks the ~where~ clause *before* the name-collision
+check; before the reorder, ~(abs 1.5)~ computed the sym ~abs-f64~ and died on
+"already defined — rename one of them", which is the wrong sentence with no
+fix in it.
+
+Behaviour pinned identical: both signed minimums answer themselves (the
+negation wraps, as every two's-complement abs), unsigned is the identity,
+~(abs-f64 -0.0)~ is 0. test/programs/int-generic.flan, plus the math3 rows.
+
+** The survey — what else numeric?-admits-floats was keeping per-width
+The prelude's remaining per-width families, each left with its reason:
+- ~sum-i32~/~sum-f32~ — the accumulator is a *different, wider* type than the
+  element ("the type $t accumulates into" is a type-level function no
+  predicate spells); their own comment already says so.
+- ~append-i64~/~append-f64~ — two different runtime primitives.
+- ~parse-i64~/~parse-f64~ — the variable would appear only in the return
+  type, which no argument determines and no syntax names.
+- ~rand-i32-range~/~rand-f32-range~ — two different algorithms (Lemire
+  rejection vs. scale), not one body twice.
+- ~sign-f32~ — its integer twin would write -1, which has no meaning at the
+  unsigned half of ~integer?~; a bound spelling "signed" does not exist and
+  is not asked for.
+- ~min~/~max~ — builtins by decision (variadic, evaluate-once), untouched.
+- The libm pairs — declares, one C symbol each; nothing to collapse.
+So the survey's whole yield is abs, plus the *checker* generalizations above
+that let user code write generic bit/shift/mod helpers it could not write at
+all before (int-generic.flan's ~low-bits~, ~even?~, ~toggle~, ~halve~).
+
+** The join, superseding "widening does not cross a generic binding"
+The 2026-09-20 milestone-5 entry above took refusal as the walk-backable
+direction and recorded the join as the coherent alternative. The author
+walked it back the same day: *just pick the wider type for both.* The old
+entry stands as written; this one supersedes it.
+
+The rule as landed: numeric scalars bound to one ~$t~ resolve it to
+whichever written type every one of them widens into — ~Types.join~, so
+value-preserving widening only, never an invented third type... except that
+an upper bound *in the set* found through a later argument is exactly that:
+~(tri u32 i32 i64)~ has no join at the second argument and a perfectly good
+one at the third, so a joinless pair is deferred and re-asked against the
+final binding rather than refused on the spot. That is what makes acceptance
+order-independent, which is pinned two ways: both orders accept, and both
+orders of the whole program instantiate exactly one copy, at the wider type
+(the pin counts ~eq2?-i64~ in the checked program's functions).
+
+Still refused, each in its own words: a pair with no join anywhere (u64
+against i64 — no type holds every value of both), and a variable the
+signature also reaches through a container or function type (~index-of~'s
+slice binds its element exactly; elements cannot be rewritten wider). The
+arguments the final binding out-widened catch up through the same ~Cast~
+node the written conversion builds, so the emitted copy never sees the
+narrow type. Literals still decide as before — a bare literal at a bound
+~$t~ takes the binding — and spec-memory.md's Generics section now carries
+the joined rule.
+
+** Still refused, known, deferred
+A *compound constant expression* at a bounded ~$t~ — ~(+ x (+ 1 2))~ where
+~(+ x 3)~ works — is still refused: the literal arm admits a bare constant
+at a type variable, and nothing folds the compound to a bare one before the
+ask. Walk-backable (admitting more programs later invalidates nothing
+written now), so it waits until a body actually wants it.

lib/check.ml

@@ -169,6 +169,14 @@ type env = {
      chain. Odin has no cap of its own to copy, so there was nothing to
      borrow. *)
   mutable chain : (string * Types.t list * Loc.t) list;
+  (* Set while a struct, data-case or union field's type is being resolved,
+     and only then. It exists for one message: an unknown lowercase name in a
+     type slot is told to introduce a type variable with [$name] in the
+     parameter vector, and a field has no parameter vector — only a defn
+     signature binds, and a field is built at one type for every value. The
+     flag is what lets [resolve_name] say the honest thing in each place
+     instead of a suggestion that cannot be followed. *)
+  mutable in_field : bool;
 }
 
 let new_env () = {
@@ -196,6 +204,7 @@ let new_env () = {
   subst = [];
   tvpreds = [];
   chain = [];
+  in_field = false;
 }
 
 (* Where a named type was declared, and what it has, as a note.
@@ -618,10 +627,18 @@ let unimplemented loc what milestone =
 
    Odin's [where] clause is the same shape ([core/slice/slice.odin:289] is
    [where intrinsics.type_is_ordered(T)]) with forty-one predicates against
-   these four. There is no [copyable?] any more and no Odin counterpart
+   these five. There is no [copyable?] any more and no Odin counterpart
    either: Odin has no move semantics, and since the repeal neither does this
-   language, so [$T] never has to answer the question. *)
+   language, so [$T] never has to answer the question.
-let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?" ]
+
+   [integer?] is the narrowest of the five and exists because [numeric?] was
+   one type too wide for a family of bodies: an integer body under [numeric?]
+   is instantiated at f32 and f64 too, and (if (< x 0) (- 0 x) x) at -0.0 is
+   the wrong abs while %, the bitwise operators and the shifts have no float
+   meaning at all. A function that can be generalized should not need a
+   variant per numeric type, and [integer?] is what lets the integer-only
+   ones say exactly what they need. *)
+let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "integer?" ]
 
 (* ── What a type owns, transitively ────────────────────────────────────
    The one structural ownership question that survived the repeal, because it
@@ -693,6 +710,7 @@ let pred_holds p (t : Types.t) =
      [key_pair]. *)
   | "hashable?" -> Types.keyable t
   | "numeric?"  -> Types.is_numeric t
+  | "integer?"  -> Types.is_integer t
   | _           -> false
 
 (* What one declared predicate *also* gives you. These are entailments over
@@ -705,8 +723,14 @@ let pred_holds p (t : Types.t) =
 let pred_entails ~declared ~wanted =
   String.equal declared wanted
   || match wanted, declared with
-     | "ordered?",  "numeric?" -> true
+     | "ordered?",  ("numeric?" | "integer?") -> true
-     | "equal?",    ("numeric?" | "ordered?") -> true
+     | "equal?",    ("numeric?" | "ordered?" | "integer?") -> true
+     (* Every integer type is a number, so [integer?] gives a body everything
+        [numeric?] does — the arithmetic, the written 0, the untyped integer
+        literal — on top of the operations only it admits. The reverse is
+        never true: [numeric?] admits floats, which is exactly what a body
+        under [integer?] is promising it never meets. *)
+     | "numeric?",  "integer?" -> true
      | _ -> false
 
 let declares preds v wanted =
@@ -1027,6 +1051,20 @@ and resolve_name env ~seen loc n =
          silently became a type parameter and made the signature more
          permissive than it was written to be. *)
       | _ when n <> "" && n.[0] = Char.lowercase_ascii n.[0] ->
+        (* The parameter-vector suggestion is only followable where a
+           parameter vector exists. A field has none and never will — only a
+           defn signature binds a variable, and a field is built at one type
+           for every value — so at a field the message offers the two things
+           that can actually be written there. *)
+        if env.in_field then
+          Loc.failk "check/unknown-type" loc
+            "unknown type %s. A lowercase name is a type variable, and a \
+             field cannot hold one: only a defn signature introduces type \
+             variables, and a field is built at one type for every value — \
+             generic types are not there. Write a concrete type here, or dyn \
+             to hold any value"
+            n
+        else
           Loc.failk "check/unknown-type" loc
             "unknown type %s. A lowercase name is a type variable only where a \
              defn signature introduced it — write $%s in the parameter vector \
@@ -2813,6 +2851,17 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
          Refusing here keeps that a refusal at the definition rather than one
          that surprises whichever call site first instantiates at [i32]. *)
       | Some (Types.Var v) ->
+        (* Under {:where (integer? $t)} the sentence is simpler and its own:
+           the bound has no float half at all, so the literal has no meaning
+           at *any* type the variable can become, not merely at some. *)
+        if declares ctx.env.tvpreds v "integer?" then
+          Loc.failk literal_at_want loc
+            "the float literal %g cannot stand where $%s is wanted: \
+             {:where (integer? $%s)} admits no float type, so there is no \
+             instantiation at which this literal means anything. Write an \
+             integer literal, or take the value as a parameter"
+            x v v
+        else
           Loc.failk literal_at_want loc
             "the float literal %g cannot stand where $%s is wanted: %s may be \
              instantiated at an integer type, and a float literal is never \
@@ -5466,7 +5515,7 @@ and not_numeric name what (a : Tast.expr) =
   else
     fail where "%s takes %s, found %s" name what (Types.to_string a.Tast.ty)
 
-and fold_left_prim ctx ~want loc name p ok what args =
+and fold_left_prim ctx ~want loc name p ~needs ok what args =
   let x, y, rest =
     match args with x :: y :: rest -> x, y, rest | _ -> assert false
   in
@@ -5477,7 +5526,13 @@ and fold_left_prim ctx ~want loc name p ok what args =
   if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
     dyn_fold ctx ~want loc name [ a; b ] rest
   else begin
-  unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
+  (* [~needs] is the operator's own bound: [numeric?] for the arithmetic,
+     [integer?] for the bitwise fold. Asking the tighter question here is what
+     keeps a bitwise body's refusal at the *definition* — under [numeric?] the
+     abstract pass admitted [(bit-and x 1)] and the refusal arrived from
+     inside the generic's source at whichever call site first instantiated at
+     a float, which is the misplaced diagnostic the pass exists to avoid. *)
+  unconstrained ctx.env loc name ~needs a.Tast.ty;
   (* Past [unconstrained] a variable here is one the [where] clause admitted,
      so the concrete predicate below has nothing to say about it — it is
      answered again, per copy, at the instantiation. *)
@@ -5835,7 +5890,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
       | _ -> Tast.Div
     in
     fold_arity loc name args;
-    fold_left_prim ctx ~want loc name p Types.is_numeric "numbers" args
+    fold_left_prim ctx ~want loc name p ~needs:"numeric?" Types.is_numeric
+      "numbers" args
   (* Remainder stays at two: (% a b c) is (% (% a b) c), which is a thing
      nobody writes on purpose. *)
   | "%" ->
@@ -5936,8 +5992,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
       | _ -> Tast.BitXor
     in
     fold_arity loc name args;
-    fold_left_prim ctx ~want loc name p
+    fold_left_prim ctx ~want loc name p ~needs:"integer?" Types.is_integer
-      (function Types.Int _ -> true | _ -> false) "integers" args
+      "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.
@@ -5956,6 +6012,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     let a, b = binary ctx ~join:false name loc ~want:(numeric_want want) args in
     (match a.Tast.ty with
      | Types.Int _ -> ()
+     (* A type variable under {:where (integer? $t)}: every type the bound
+        admits has a width to shift within, so the abstract pass lets the
+        body through and each instantiation meets the concrete checks below
+        at its own width. Anything weaker — [numeric?] included — is refused
+        here, at the definition, because a shift at f32 means nothing. *)
+     | t when generic_ty t ->
+       unconstrained ctx.env loc name ~needs:"integer?" t
      | other -> fail loc "%s takes integers, found %s" name
                   (Types.to_string other));
     (* A shift by the operand's own width or more is poison in LLVM, which at
@@ -7845,6 +7908,33 @@ and generic_call ctx ~want loc name vars pats pret args =
      take its types from. Left to right, which is the order Odin's operands
      are gathered in and the order [map2_lr] already guarantees. *)
   let subst = ref [] in
+  (* Does the signature bind [v] anywhere *inside* a type — [[$t]],
+     [(Fn [$t $t] bool)], [(Vec $t)]? A bare [$t] parameter is a scalar the
+     join below may move; a variable reached through a constructor is bound
+     exactly, because a container's elements cannot be rewritten and a
+     function value's type is its own. One scan, answered per variable. *)
+  let rec mentions v (t : Types.t) =
+    match t with
+    | Types.Var u -> String.equal u v
+    | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+    | Types.Option e -> mentions v e
+    | Types.Map (k, w) -> mentions v k || mentions v w
+    | Types.Fn (ps, r) -> List.exists (mentions v) ps || mentions v r
+    | _ -> false
+  in
+  let bound_exactly v =
+    List.exists
+      (fun (p : Types.t) ->
+         match p with Types.Var _ -> false | t -> mentions v t)
+      pats
+  in
+  (* Pairs that met no join while the arguments were walked. They are not
+     refused on the spot because a *later* argument can still settle them:
+     (f u32-x i32-y i64-z) has no join at the second argument and a perfectly
+     good one — i64, which both widen into — at the third. Each entry is
+     re-asked against the final binding below, so acceptance cannot depend on
+     the order the arguments were written in. *)
+  let pending = ref [] in
   let targs =
     map2_lr
       (fun pat a ->
@@ -7882,44 +7972,55 @@ and generic_call ctx ~want loc name vars pats pret args =
               | Error _ -> check ctx ~want:p a)
            else check ctx ~want:p a
          in
-         (* **Implicit widening does not cross a generic binding.** A concrete
+         (* **Mixed widths at one variable join at the wider type.** The rule
-            argument at a variable an earlier argument already bound has to be
+            used to refuse the pair both ways — FIX.org, "Generics and
-            the same type, not merely a type that widens into it.
+            implicit widening", recorded the join as the coherent alternative
+            and refusing as the direction that could be walked back. It was
+            walked back on 2026-09-20, by the author: a numeric argument at a
+            variable an earlier argument already bound resolves the variable
+            to whichever of the pair the other widens into, value-preserving
+            widening only, so [(eq2? (i8 3) (i64 3))] and its reverse are one
+            copy at i64. A pair with no join — u64 against i64 — is still
+            refused: there is no type that holds every value of both, and
+            inventing one would be picking a type neither argument was
+            written at.
 
-            This is a decision and not a consequence. Widening landed after
+            Only where the variable is bound by bare scalars. A variable the
-            generics did, and left behind a rule that depended on argument
+            signature also reaches through a container is bound exactly —
-            order: [(pair-eq? i64 i8)] was accepted, because [$t] bound to i64
+            a slice's elements cannot be rewritten to a wider width — so
-            first and the i8 widened into the want; [(pair-eq? i8 i64)] was
+            those keep the refusal, in their own words. And only where the
-            refused, because [$t] bound to i8 and i64 into i8 can lose. Same
+            pair is one widening has an opinion about: a string where $t was
-            two values, same function, two answers. Neither is unsound — a
+            bound to i64 is an ordinary mismatch and gets the ordinary
-            widen cannot change a number — but which instantiation a program
+            refusal below. *)
-            gets should not depend on which argument was written first.
+         let handled =
-
+           match bound_scalar with
-            Refusing both is the direction that can be walked back. Allowing
-            the pair to join at the wider type is a coherent rule too, and it
-            is the one to reach for if the ergonomics turn out to want it; it
-            can be added later without invalidating a program that was written
-            under this rule, and the reverse is not true. FIX.org, "Generics
-            and implicit widening". *)
-         (* Only where the pair is one widening had an opinion about. A string
-            passed where $t was bound to i64 is an ordinary mismatch and gets
-            the ordinary refusal; the sentence below is about the conversion
-            that no longer happens, and it would read as a non-sequitur over a
-            pair that never had one available. *)
-         (match bound_scalar with
            | Some v
              when (not (Types.equal p a.Tast.ty))
                   && Types.is_numeric a.Tast.ty ->
+             (match Types.join p a.Tast.ty with
+              | Some j when Types.equal j p ->
+                (* This argument widens into the binding; the wrap happens
+                   with the others, once the binding is final. *)
+                true
+              | Some j when not (bound_exactly v) ->
+                subst := (v, j) :: List.remove_assoc v !subst;
+                true
+              | Some _ ->
                 Loc.failk "check/tyvar-no-widening" a.Tast.loc
-              "%s's $%s was bound to %s by an earlier argument, and this one \
+                  "%s's $%s was bound to %s by an earlier argument, and this \
-               is %s. Implicit widening does not cross a generic binding: a \
+                   one is %s. The signature also binds $%s inside a \
-               written type is what a type variable takes, so the same \
+                   container or function type, which binds its element \
-               variable is the same type at every argument. Write the \
+                   exactly — the pair cannot join at the wider type there. \
-               conversion — (%s x) — or pass the arguments at one type"
+                   Write the conversion — (%s x) — or pass the arguments at \
-              name v (Types.to_string p) (Types.to_string a.Tast.ty)
+                   one type"
+                  name v (Types.to_string p) (Types.to_string a.Tast.ty) v
                   (Types.to_string p)
-          | _ -> ());
+              | None ->
-         if not (bind_ty subst p a.Tast.ty) then
+                pending := (v, p, a.Tast.ty, a.Tast.loc) :: !pending;
+                true)
+           | _ -> false
+         in
+         if (not handled) && not (bind_ty subst p a.Tast.ty) then
            fail a.Tast.loc "%s expects %s here, found %s" name
              (Types.to_string p) (Types.to_string a.Tast.ty);
          a)
@@ -7937,6 +8038,44 @@ and generic_call ctx ~want loc name vars pats pret args =
             generic function is instantiated from its call site, and there is \
             no syntax for naming the type" name v)
     vars;
+  (* The pairs that met no join, re-asked now that every argument has spoken.
+     A later, wider argument dissolves one — u32 and i32 both widen into an
+     i64 that arrived third — and one still standing is the real refusal:
+     these two widths meet at no type. *)
+  List.iter
+    (fun (v, t1, t2, ploc) ->
+       let final = List.assoc v !subst in
+       let fits t =
+         Types.equal t final || Types.widens_to ~from:t ~into:final
+       in
+       if not (fits t1 && fits t2) then
+         Loc.failk "check/tyvar-no-join" ploc
+           "this call binds %s's $%s to both %s and %s, and the two meet at \
+            no type: implicit widening only ever widens — every value kept, \
+            no sign lost — and neither of these holds every value of the \
+            other. Write the conversion you mean at one of the arguments, or \
+            pass them at one type"
+           name v (Types.to_string t1) (Types.to_string t2))
+    !pending;
+  (* The binding is final; the arguments it out-widened catch up. Only a bare
+     [$t] parameter can be here — [bound_exactly] kept every container-bound
+     variable at one exact type — and the cast is the same node the written
+     conversion would have built. *)
+  let targs =
+    map2_lr
+      (fun (pat : Types.t) a ->
+         match pat with
+         | Types.Var v ->
+           (match List.assoc_opt v !subst with
+            | Some f
+              when (not (Types.equal f a.Tast.ty))
+                   && Types.is_numeric a.Tast.ty
+                   && Types.widens_to ~from:a.Tast.ty ~into:f ->
+              widen a.Tast.loc f a
+            | _ -> a)
+         | _ -> a)
+      pats targs
+  in
   (* **A type variable is not instantiated at dyn.** Nothing stopped it before:
      [dyn] is an ordinary case of [Types.t], so it substituted like any other
      type and a copy was generated at it. The copy then reached whatever the
@@ -7975,11 +8114,11 @@ and generic_call ctx ~want loc name vars pats pret args =
            "this call would instantiate %s at $%s = %s, and a type variable \
             is not instantiated at dyn: a copy is made per *written* type, \
             and dyn is the one type whose own type is not known until it \
-            runs. One value, two models — (defgeneric %s [...]) with a \
+            runs. One value, two models — a defgeneric with a defmethod per \
-            (defmethod ...) per class dispatches on what the value turns out \
+            class dispatches on what the value turns out to be, which is the \
-            to be, which is the question a dyn argument is asking. Write the \
+            question a dyn argument is asking. Write the type the value has, \
-            type the value has, or reach for the dyn side"
+            or reach for the dyn side"
-           name v (Types.to_string t) name)
+           name v (Types.to_string t))
     !subst;
   let cparams = List.map (subst_ty !subst) pats in
   let cret = subst_ty !subst pret in
@@ -8047,15 +8186,18 @@ and instantiate env loc gname vars subst cparams cret =
       gname ^ "-"
       ^ String.concat "-" (List.map (fun v -> mangle_ty (List.assoc v subst)) vars)
     in
-    if Hashtbl.mem env.fns sym then
-      fail loc
-        "%s at these types is called %s, and %s is already defined — rename \
-         one of them" gname sym sym;
-    runaway env loc gname cparams;
     (* Each instantiation checks the concrete types answer the [where] clause.
        This is the half of the feature that only exists per copy: the abstract
        pass took the predicates on trust, and here is where the trust is
-       settled, at the call site that asked, naming it. *)
+       settled, at the call site that asked, naming it.
+
+       Before the name-collision check, on purpose. The prelude keeps a
+       per-width family beside a generic where the generic's bound refuses
+       some widths — [abs] under [integer?] beside the declared [abs-f32] and
+       [abs-f64] — so a float caller of [abs] computes the sym [abs-f64], and
+       "abs-f64 is already defined, rename one of them" is the wrong sentence
+       for what went wrong: the bound refused the type, and that is the
+       message with the fix in it. *)
     let fn = Hashtbl.find env.generics gname in
     List.iter
       (fun (p : Ast.pred) ->
@@ -8072,6 +8214,11 @@ and instantiate env loc gname vars subst cparams cret =
                gname p.Ast.pvar (Types.to_string t) (Types.to_string t)
                p.Ast.pname gname p.Ast.pname p.Ast.pvar)
       fn.Ast.fwhere;
+    if Hashtbl.mem env.fns sym then
+      fail loc
+        "%s at these types is called %s, and %s is already defined — rename \
+         one of them" gname sym sym;
+    runaway env loc gname cparams;
     (* The entry goes in *before* the body is checked, which is what makes a
        recursive generic function terminate: the call to itself at the same
        types finds this and does not generate a second copy. *)
@@ -8855,7 +9002,14 @@ let collect env (decls : Ast.decl list) =
   in
   while fold_consts () do () done;
   let field (f : Ast.field) : Tast.field =
-    let fty = resolve env f.Ast.fty in
+    (* The flag is reset through [Fun.protect] because a refusal here does not
+       end the run: [program_all] carries on collecting diagnostics, and a
+       flag left set would misword every later unknown-type message. *)
+    env.in_field <- true;
+    let fty =
+      Fun.protect ~finally:(fun () -> env.in_field <- false)
+        (fun () -> resolve env f.Ast.fty)
+    in
     no_zeroed_fn f.Ast.fty.Ast.tloc
       (Printf.sprintf "the field %s" f.Ast.fname) fty;
     { Tast.fname = f.Ast.fname; fty }

lib/prelude.ml

@@ -985,34 +985,32 @@ let source = {flan|
 (declare cbrt-f32 [x f32] f32 "cbrtf")
 (declare cbrt-f64 [x f64] f64 "cbrt")
 
-;; Integer magnitude, one per width, and the reason it stays that way changed
+;; Integer magnitude, one body for every integer width. The per-width pair —
-;; when generics landed. The old one — no generics over the numeric types —
+;; abs-i32 and abs-i64 — waited here on a bound that spells "an integer
-;; is not true any more: (defn abs [x $t] $t {:where (numeric? $t)} (if (< x
+;; type", and integer? is that bound, so they collapsed into this on
-;; 0) (- 0 x) x)) checks and runs at every integer width, and the literal 0
+;; 2026-09-20 (FIX.org).
-;; stands there because the clause admits it.
 ;;
-;; **What stops it is the float half of its own bound.** numeric? is the only
+;; **The bound is integer? and not numeric?, and that is the whole design.**
-;; predicate that admits a written 0, and it admits f32 and f64 too — so a
+;; numeric? admits f32 and f64, and this body is the wrong abs for a float:
-;; generic abs would be instantiated at them, and the body above is the wrong
+;; (< -0.0 0) is false, so it hands back a negative zero from a function
-;; abs for a float: (< -0.0 0) is false, so it hands back a negative zero
+;; named abs. There is no float-safe spelling of the body either — (max x
-;; from a function named abs. The float pair below is libm's for exactly that
+;; (- 0 x)) picks whichever zero sits in the wrong slot, since -0.0 and 0.0
-;; reason, a sign-bit clear rather than a negation, and a generic that shadows
+;; compare equal. The right float abs is a sign-bit clear, which is libm's
-;; it at f32 would be a quiet wrong answer rather than a tidier prelude.
+;; fabs, declared above as abs-f32 and abs-f64; a caller with a float writes
-;;
+;; those, and (abs 1.5) is refused with the bound named rather than shadowing
-;; So the collapse waits on a bound that spells "an integer type" — an
+;; them with a quiet wrong answer. One capability, one spelling per side of
-;; integer? predicate, which is language surface and not this file's call.
+;; the integer/float line — not one per width, which is what this collapse
-;; FIX.org, "Generics and implicit widening", records it as the candidate.
+;; ends.
-;; Two functions is the honest price until then.
 ;;
 ;; The most negative value of each width has no positive counterpart, and this
 ;; does not special-case it: the subtraction is the same subtraction written
 ;; anywhere else and meets whatever the build's overflow rule is. Saturating
 ;; to the maximum would be a wrong answer returned quietly, which is the one
-;; thing this file does not do.
+;; thing this file does not do. The unsigned instantiations are the identity,
-(defn abs-i32 [x i32] i32
+;; for the reason pos? gives about its own: a generic is copied per written
-  (if (< x 0) (- 0 x) x))
+;; type, and at a u32 the body says what it says.
-
+(defn abs [x $t] $t
-(defn abs-i64 [x i64] i64
+  {:where (integer? $t)}
   (if (< x 0) (- 0 x) x))
 
 ;; pi and tau at both widths, because a defconst has a type and a cast between

lib/types.ml

@@ -172,6 +172,13 @@ let rec to_string = function
 
 let is_numeric = function Int _ | Float _ -> true | _ -> false
 
+(* Every integer kind, signed and unsigned, at every width — and nothing
+   else. This is [integer?]'s question: the bound that admits a body written
+   with %, the bitwise operators or the shifts, and that keeps the same body
+   from ever being instantiated at a float, where those operations either do
+   not exist or mean something different. *)
+let is_integer = function Int _ -> true | _ -> false
+
 (* The key types the first Map implementation admits (spec-memory.md, "Maps —
    first implementation"): integers, enums, strings, fixed arrays, and value
    structs composed recursively from those. Equality and hashing for them are

spec-memory.md

@@ -254,13 +254,17 @@ instantiates it:
 > field-free storage. It does **not** support `=`, `<`, `+`, or `hash`.
 
 What makes that liveable is a `where` clause of compile-time type predicates,
-written as a map at the head of the body. There are four — `ordered?`,
+written as a map at the head of the body. There are five — `ordered?`,
-`equal?`, `hashable?`, `numeric?` — they are not type classes because a
+`equal?`, `hashable?`, `numeric?`, `integer?` — they are not type classes
-predicate carries no implementations and merely gates a builtin the compiler
+because a predicate carries no implementations and merely gates a builtin the
-already has, and they entail one another in one direction, so one clause
+compiler already has, and they entail one another in one direction, so one
-usually does. (`copyable?` was the fifth until the second repeal removed the
+clause usually does: `integer?` admits every integer kind and no float, and
-move concept it opted out of.) plan.org's Types section has the full
+entails `numeric?`, which entails `ordered?`, which entails `equal?`.
-account.
+`integer?` is what admits the bitwise operators, the shifts and an
+integer-only body like `abs`'s — under `numeric?` those bodies would be
+instantiated at the floats too (FIX.org 2026-09-20). (`copyable?` was once a
+sixth until the second repeal removed the move concept it opted out of.)
+plan.org's Types section has the full account.
 
 ```
 (defn sort [s [$t]] ()
@@ -314,12 +318,16 @@ at a type variable even under `numeric?`, because `numeric?` covers the
 integers too and a float literal is never usable where an integer is wanted.
 The range check belongs to each copy, not to the definition.
 
-**Implicit widening does not cross a generic binding.** A concrete argument at
+**Mixed widths at one type variable join at the wider type.** The first rule
-a variable an earlier argument already bound has to be that type, not merely
+here refused the pair both ways and recorded the join as the loosening that
-one that widens into it — otherwise which copy a call gets depends on which
+could be added later; the author added it on 2026-09-20 (FIX.org, the
-argument was written first. Letting the pair meet at the wider type stays
+integer? entry). Numeric scalars bound to one `$t` resolve it to whichever
-available as a later loosening; nothing written under this rule would stop
+type every one of them widens into — value-preserving widening only, and in
-compiling. An untyped literal is unaffected: it has no type of its own to keep.
+any argument order, so both orders produce the identical copy. A pair with no
+join (u64 against i64) is still refused, and a variable the signature also
+reaches through a container or function type is still bound exactly, because
+a slice's elements cannot be rewritten. An untyped literal is unaffected: it
+has no type of its own to keep.
 
 **A type variable is not instantiated at `dyn`.** Two models answer "one body,
 many types" and they are not rivals: this one copies per written type at

test/programs/int-generic.flan

@@ -0,0 +1,112 @@
+;;;; integer?, end to end: the bound numeric? was one type too wide for.
+;;;;
+;;;; Three families in here, in order. The collapsed abs — one written body
+;;;; under {:where (integer? $t)} where abs-i32 and abs-i64 used to be, pinned
+;;;; at six widths, at both signed minimums (the answer is itself, because the
+;;;; negation wraps — what every two's-complement abs does), and beside the
+;;;; libm float pair it deliberately does not shadow: (abs-f64 -0.0) is 0
+;;;; because fabs clears the sign bit, which no integer body spells. Then the
+;;;; operations only integer? admits in a generic body — bit-and, bit-or,
+;;;; bit-xor, the shifts, and % — at several widths each. Then the join:
+;;;; mixed widths at one $t resolve to the wider type in either argument
+;;;; order (FIX.org 2026-09-20), so both orders print the same number from
+;;;; the same copy.
+
+(defvar i32min i32 -2147483648)
+(defvar i64min i64 -9223372036854775808)
+
+;; The low n bits, which needs a shift, a bit-and and the literal 1 — every
+;; one of them admitted by integer? and none by anything weaker.
+(defn low-bits [x $t  n $t] $t
+  {:where (integer? $t)}
+  (bit-and x (- (<< 1 n) 1)))
+
+;; Truncated %, the semantics everywhere in the language, in a generic body.
+(defn even? [x $t] bool
+  {:where (integer? $t)}
+  (= (% x 2) 0))
+
+;; xor and or, and the shift right.
+(defn toggle [x $t  m $t] $t
+  {:where (integer? $t)}
+  (bit-xor x m))
+
+(defn with-flag [x $t  f $t] $t
+  {:where (integer? $t)}
+  (bit-or x f))
+
+(defn halve [x $t] $t
+  {:where (integer? $t)}
+  (>> x 1))
+
+;; The untyped literal at a bounded variable: admitted under integer? by the
+;; same arm that admits it under numeric?, ranged per copy.
+(defn plus-300 [x $t] $t
+  {:where (integer? $t)}
+  (+ x 300))
+
+;; The join family. eq2? is the pair the refusal used to be pinned on.
+(defn eq2? [a $t  b $t] bool
+  {:where (equal? $t)}
+  (= a b))
+
+(defn tri [a $t  b $t  c $t] $t
+  {:where (numeric? $t)}
+  (+ a (+ b c)))
+
+(defn main [] ()
+  ;; abs, one body, six widths.
+  (println (abs (i8 -7)))
+  (println (abs -7))
+  (println (abs (i64 -7)))
+  (println (abs (u8 7)))
+  (println (abs (u32 7)))
+  (println (abs (u64 7)))
+  ;; The signed minimums answer themselves: the negation wraps, and saturating
+  ;; quietly would be the wrong answer this file exists to refuse.
+  (println (abs i32min))
+  (println (abs i64min))
+  ;; The float abs stays libm's: a sign-bit clear, so -0.0 comes back 0.
+  (println (abs-f64 -0.0))
+  (println (abs-f32 -0.0))
+  (println (abs-f64 -1.5))
+  (println (abs-f32 -2.5))
+
+  ;; The integer?-only operations, per width.
+  (println (low-bits 255 3))
+  (println (low-bits (u16 65535) (u16 4)))
+  (println (low-bits (i64 1023) (i64 5)))
+  (println (even? 4))
+  (println (even? (u8 3)))
+  (println (even? (i64 -2)))
+  (println (toggle (u8 255) (u8 15)))
+  (println (with-flag 8 1))
+  (println (halve (u64 10)))
+  (println (halve (i64 -4)))
+  (println (plus-300 1))
+  (println (plus-300 (i64 1)))
+
+  ;; The join: both orders, one copy, one answer.
+  (let [a (i8 3)
+        b (i64 3)]
+    (println (eq2? a b))
+    (println (eq2? b a)))
+  (let [x (u32 1)
+        y (i32 2)
+        z (i64 3)]
+    ;; u32 and i32 meet at no type of their own; all three meet at the i64,
+    ;; wherever it stands in the argument list.
+    (println (tri x y z))
+    (println (tri z y x)))
+  ;; A literal beside a wider variable joins too: 4 arrives as an i32 and the
+  ;; copy is i64's.
+  (let [w (i64 38)]
+    (println (tri w 3 1)))
+  ;; And the one direction a container-bound variable does admit: the slice
+  ;; fixed $t at i32 exactly, and a narrower scalar widens *into* that — the
+  ;; same conversion a monomorphic i32 parameter would apply. (The reverse,
+  ;; an i64 scalar against this slice, stays refused; the checker pins it.)
+  (let [ns [5 3 9 1]]
+    (match (index-of (slice ns 0 4) (i16 9))
+      (Some i) (println i)
+      _ (println -1))))

test/programs/math3.flan

@@ -89,10 +89,11 @@
   (show64 (round-f64 2.5))              ; 3
   (println "")
 
-  ;; Integer magnitude, one per width.
+  ;; Integer magnitude, one generic under integer? — the per-width pair
-  (print (abs-i32 -7)) (print " ")      ; 7
+  ;; collapsed into it (FIX.org 2026-09-20). Two widths, two copies.
-  (print (abs-i64 (i64 -7))) (print " ") ; 7
+  (print (abs -7)) (print " ")          ; 7
-  (print (abs-i32 7)) (print " ")       ; 7
+  (print (abs (i64 -7))) (print " ")    ; 7
+  (print (abs 7)) (print " ")           ; 7
   ;; tau is 2pi at both widths. Pinning the relation rather than the digits is
   ;; what catches a constant written to too few of them.
   (print (= tau-f32 (* 2.0 pi-f32))) (print " ")

test/test_acceptance.ml

@@ -2671,6 +2671,27 @@ let () =
     outputs "generics" "programs/generics.flan" generics_out;
     outputs ~opt:"-O0" "generics, -O0" "programs/generics.flan" generics_out;
 
+    (* integer?, end to end — see the program's own header. The first eight
+       lines are the collapsed abs at six widths and both signed minimums
+       (which answer themselves; the negation wraps). The [0 0] after them is
+       the libm float pair at -0.0, the sign-bit clear no integer body
+       spells. Then the integer?-only operations at several widths, and last
+       the join family: [true true], [6 6] and [42] are mixed widths at one
+       $t answering identically in both argument orders, from one copy at
+       the wider type (FIX.org 2026-09-20). The closing [2] is an i16 scalar
+       widening into the i32 a slice fixed index-of's $t at — the one
+       direction a container-bound variable admits. *)
+    let int_generic_out =
+      "7\n7\n7\n7\n7\n7\n-2147483648\n-9223372036854775808\n\
+       0\n0\n1.5\n2.5\n\
+       7\n15\n31\ntrue\nfalse\ntrue\n240\n9\n5\n-2\n301\n301\n\
+       true\ntrue\n6\n6\n42\n2\n"
+    in
+    outputs "integer? and the collapsed abs" "programs/int-generic.flan"
+      int_generic_out;
+    outputs ~opt:"-O0" "integer? and the collapsed abs, -O0"
+      "programs/int-generic.flan" int_generic_out;
+
     (* Reach's walk, edge by edge. Pruning is what makes the link follow the
        program, and the cost of getting it wrong is not a wrong answer: a
        function the walk fails to reach is not emitted, and the build dies in

test/test_flan.ml

@@ -1195,11 +1195,17 @@ let () =
      used to be reported as unimplemented generics; generics are implemented,
      and a lowercase name is a type variable only where a defn signature
      introduced one with the sigil — a struct field is not such a place and
-     never will be, since only a signature binds. So the sentence names the
+     never will be, since only a signature binds. The message used to tell a
-     sigil rather than a milestone. A defn's parameter vector stopped being a
+     field to "write $elem in the parameter vector", and a field has no
-     type-only slot, which is why the rule is exercised at a field. *)
+     parameter vector — the suggestion could not be followed where it was
-  rejects_check "a real type variable" "(defstruct Holder [x elem])"
+     printed. A field now gets its own sentence, naming the two things that
-    ~needle:"write $elem in the parameter vector";
+     can actually be written there; the parameter-vector suggestion survives
+     where it works, which the return-type pin further down exercises. *)
+  rejects_check "a real type variable at a field" "(defstruct Holder [x elem])"
+    ~needle:"a field is built at one type for every value";
+  rejects_check "and the field message offers what a field can hold"
+    "(defstruct Holder [x elem])"
+    ~needle:"Write a concrete type here, or dyn to hold any value";
   rejects_check "an unknown concrete type" "(defn f [x Widget] ())"
     ~needle:"unknown type Widget";
 
@@ -4909,6 +4915,61 @@ let () =
     "(defn same [a $t b $t] bool {:where (ordered? $t)} (= a b))";
   accepts "numeric? entails ordered?"
     "(defn less [a $t b $t] bool {:where (numeric? $t)} (< a b))";
+
+  (* ── integer? — the bound numeric? was one type too wide for ─────────
+     It admits every integer kind, signed and unsigned, at every width, and
+     refuses floats and everything else. It exists so a function that can be
+     generalized does not need a variant per numeric type: an integer body
+     under numeric? was instantiated at f32 and f64 too, which is why abs
+     stayed per-width for a milestone. It entails numeric? — every integer
+     is a number — so the arithmetic, the written 0 and the untyped integer
+     literal all come with it; the reverse entailment would let floats into
+     bit-and and does not exist. *)
+  accepts "integer? admits +, via the entailment"
+    "(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))";
+  accepts "integer? admits <, via the entailment"
+    "(defn small? [x $t] bool {:where (integer? $t)} (< x 10))";
+  accepts "integer? admits bit-and"
+    "(defn low? [x $t] bool {:where (integer? $t)} (= (bit-and x 1) 1))";
+  accepts "integer? admits the shifts"
+    "(defn dbl [x $t] $t {:where (integer? $t)} (<< x 1))";
+  rejects_check "numeric? does not admit bit-and"
+    ~needle:"nothing here says t is integer?"
+    "(defn low? [x $t] bool {:where (numeric? $t)} (= (bit-and x 1) 1))";
+  rejects_check "nor the shifts"
+    ~needle:"nothing here says t is integer?"
+    "(defn dbl [x $t] $t {:where (numeric? $t)} (<< x 1))";
+  (* An integer?-bounded caller satisfies a numeric?-bounded callee: the
+     entailment carries across generic calls exactly as ordered?-over-equal?
+     does. *)
+  accepts "integer? carries a numeric? callee"
+    "(defn z? [x $t] bool {:where (numeric? $t)} (= x 0))\n\
+     (defn odd-z? [x $t] bool {:where (integer? $t)} (z? (bit-and x 1)))";
+  (* The integer literal is admitted at a bounded variable by the same arm
+     under both bounds — the bound promises the literal a meaning at every
+     type the variable can become, and integer?'s types are a subset of
+     numeric?'s. *)
+  accepts "an integer literal stands where an integer?-bounded $t is wanted"
+    "(defn bump [x $t] $t {:where (integer? $t)} (+ x 300))";
+  (* A float at integer?, refused at the call that asked, naming the bound. *)
+  rejects_check "a float does not instantiate an integer?-bounded variable"
+    ~needle:"f64 does not answer integer?"
+    "(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))\n\
+     (defn main [] () (println (bump 1.5)))";
+  (* And dyn is refused by the bound too — the clause's own refusal, the more
+     specific of the two answers, exactly as at numeric?. *)
+  rejects_check "dyn does not instantiate an integer?-bounded variable"
+    ~needle:"dyn does not answer integer?"
+    "(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))\n\
+     (defvar d dyn 5)\n\
+     (defn main [] () (println (bump d)))";
+  (* A float literal inside an integer?-bounded body is refused at the
+     definition, in the bound's own words: there is no instantiation at which
+     it means anything. *)
+  rejects_check "a float literal has no meaning under integer?"
+    ~needle:"admits no float type"
+    "(defn h [x $t] $t {:where (integer? $t)} (+ x 1.5))";
+
   accepts "a variable read twice under one predicate"
     "(defn twice [a $t] bool {:where (ordered? $t)} (< a a))";
   rejects_check "a predicate nobody has heard of"
@@ -5041,28 +5102,80 @@ let () =
      (defvar d dyn 5)\n\
      (defn main [] () (println (twice d)))";
 
-  (* ── Implicit widening does not cross a generic binding ─────────────
+  (* ── Mixed widths at one type variable join at the wider type ───────
-     Widening landed after generics did, and the rule it left behind depended
+     The rule used to refuse the pair both ways, with the join recorded as
-     on the order the arguments were written in: the i8-then-i64 call was
+     the coherent alternative that could be added without invalidating
-     refused because i64 into i8 can lose, and the i64-then-i8 call was
+     anything — the walk-backable direction. The author walked it back on
-     *accepted*, because $t had already bound to i64 and the i8 widened into
+     2026-09-20: a scalar pair at one $t resolves to whichever of the two
-     the want. Same two values, same function, two answers.
+     the other widens into, value-preserving widening only, and both
-
+     argument orders produce the identical copy. A pair with no join — u64
-     Neither was unsound — a widen cannot change a number — but which copy a
+     against i64 — keeps a refusal, because there is no type that holds
-     program gets should not turn on which argument came first, so both are
+     every value of both. FIX.org, "Generics and implicit widening", and the
-     refused now and both name the binding. Letting the pair join at the wider
+     2026-09-20 entry that supersedes it. *)
-     type is the other coherent rule and it stays available: it can be added
+  accepts "a scalar pair at one $t joins at the wider type"
-     without invalidating anything written under this one, which is why this
-     is the direction to be wrong in. FIX.org, "Generics and implicit
-     widening". *)
-  rejects_check "a narrower argument does not widen into a bound type variable"
-    ~needle:"was bound to i64 by an earlier argument"
     "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
      (defn main [] () (println (eq2? (i64 3) (i8 3))))";
-  rejects_check "and the other argument order refuses identically"
+  accepts "and the other argument order joins identically"
-    ~needle:"was bound to i8 by an earlier argument"
     "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
      (defn main [] () (println (eq2? (i8 3) (i64 3))))";
+  (* Order-independence, pinned on the copies and not only on acceptance:
+     both orders in one program make exactly one instantiation, at i64, and
+     none at i8. *)
+  (let syms order_a order_b =
+     match
+       checked
+         ("(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
+           (defn main [] () (do (println (eq2? " ^ order_a ^ "))\
+           (println (eq2? " ^ order_b ^ "))))")
+     with
+     | p ->
+       List.filter_map
+         (fun (f : Tast.fn) ->
+            if String.length f.Tast.name >= 4
+               && String.sub f.Tast.name 0 4 = "eq2?" then Some f.Tast.name
+            else None)
+         p.Tast.fns
+     | exception _ -> [ "did not check" ]
+   in
+   check "both orders share one copy, at the wider type"
+     (syms "(i8 3) (i64 4)" "(i64 5) (i8 6)" = [ "eq2?-i64" ]);
+   check "and the reversed program instantiates the same one copy"
+     (syms "(i64 5) (i8 6)" "(i8 3) (i64 4)" = [ "eq2?-i64" ]));
+  (* The pair that meets at no type is the refusal that stays: neither u64
+     nor i64 holds every value of the other, and inventing a third type
+     would be picking one neither argument was written at. *)
+  rejects_check "u64 and i64 meet at no type"
+    ~needle:"the two meet at no type"
+    "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
+     (defvar u u64 3)\n(defvar i i64 3)\n\
+     (defn main [] () (println (eq2? u i)))";
+  (* And a later, wider argument settles a pair that had no join of its own:
+     u32 and i32 meet nowhere, but all three meet at the i64 that arrives
+     third — in either order, which is what the deferred re-ask is for. *)
+  accepts "a later argument settles a joinless pair"
+    "(defn tri [a $t  b $t  c $t] $t {:where (numeric? $t)} (+ a (+ b c)))\n\
+     (defvar x3 u32 1)\n(defvar y3 i32 2)\n(defvar z3 i64 3)\n\
+     (defn main [] () (println (tri x3 y3 z3)))";
+  accepts "and the same trio in the other order"
+    "(defn tri [a $t  b $t  c $t] $t {:where (numeric? $t)} (+ a (+ b c)))\n\
+     (defvar x3 u32 1)\n(defvar y3 i32 2)\n(defvar z3 i64 3)\n\
+     (defn main [] () (println (tri z3 y3 x3)))";
+  (* A variable the signature also reaches through a container is bound
+     exactly — a slice's elements cannot be rewritten to a wider width — so
+     the join never moves one, in either direction of the mismatch. *)
+  rejects_check "a container-bound variable does not join wider"
+    ~needle:"binds its element exactly"
+    "(defn main [] () (let [ns [5 3 9 1]] \
+       (match (index-of (slice ns 0 4) (i64 9)) \
+         (Some i) (println i) _ (println -1))))";
+  (* The one direction a container-fixed binding does admit, and it is new
+     with the join: a *narrower* scalar widens into the type the container
+     fixed, through the same cast a monomorphic i32 parameter applies. This
+     used to refuse with the same both-ways sentence as everything else. *)
+  accepts "a narrower scalar widens into a container-fixed binding"
+    "(defn main [] () (let [ns [5 3 9 1]] \
+       (match (index-of (slice ns 0 4) (i16 9)) \
+         (Some i) (println i) _ (println -1))))";
   (* The written conversion is what the message asks for, and it is accepted:
      the refusal is about the *implicit* step, not about reaching i64. *)
   accepts "the written conversion is accepted"

web/index.html

@@ -927,11 +927,12 @@ $t)} at the head of the body, or take the operation as a parameter — a
 <p>What makes that liveable is a <code>where</code> clause, written as a Clojure-style
 map at the head of the body — <code>{:where (ordered? $t)}</code>, or a vector when
 there is more than one: <code>{:where [(ordered? $t) (hashable? $u)]}</code>. There
-are four predicates, and each gates builtins the compiler already has:</p>
+are five predicates, and each gates builtins the compiler already has:</p>
 
 <div class="scroll">
 <table>
 <tr><th>Predicate</th><th>What it admits</th></tr>
+<tr><td><code>integer?</code></td><td><code>bit-and</code> <code>bit-or</code> <code>bit-xor</code> <code>&lt;&lt;</code> <code>&gt;&gt;</code> — every integer type, no float</td></tr>
 <tr><td><code>numeric?</code></td><td><code>+</code> <code>-</code> <code>*</code> <code>/</code> <code>%</code>, and a cast <code>(t x)</code></td></tr>
 <tr><td><code>ordered?</code></td><td><code>&lt;</code> <code>&lt;=</code> <code>&gt;</code> <code>&gt;=</code> <code>min</code> <code>max</code></td></tr>
 <tr><td><code>equal?</code></td><td><code>=</code> and <code>!=</code></td></tr>
@@ -940,9 +941,12 @@ are four predicates, and each gates builtins the compiler already has:</p>
 </div>
 
 <p>They entail each other in one direction, so one clause usually does:
-<code>numeric?</code> gives <code>ordered?</code>, and <code>ordered?</code> gives
+<code>integer?</code> gives <code>numeric?</code>, <code>numeric?</code> gives
-<code>equal?</code>. A <code>sort</code> that compares its elements declares
+<code>ordered?</code>, and <code>ordered?</code> gives <code>equal?</code>. A
-<code>ordered?</code> and nothing else.</p>
+<code>sort</code> that compares its elements declares <code>ordered?</code> and
+nothing else, and the prelude's <code>abs</code> declares <code>integer?</code>
+alone — the bound is what keeps its integer body away from the floats, whose
+<code>abs-f32</code>/<code>abs-f64</code> are libm's sign-bit clear.</p>
 
 <p><strong>Every value copies.</strong> There used to be a fifth predicate,
 <code>copyable?</code>, gating a second read of a move-only variable; the move
@@ -1051,7 +1055,7 @@ over.</p>
 <tr><td>text</td><td><code>split-on-byte</code>, <code>split-next</code>, <code>split</code>, <code>lower-ascii</code>, <code>upper-ascii</code>, <code>to-lower</code>, <code>to-upper</code></td></tr>
 <tr><td>building bytes</td><td><code>append</code>, <code>append-i64</code>, <code>append-f64</code>, <code>concat</code>, <code>join</code>, <code>repeat-bytes</code>, <code>replace-bytes</code>, <code>slices-new</code>, <code>format-f64</code></td></tr>
 <tr><td>UTF-8</td><td><code>decode-rune</code>, <code>rune-at</code>, <code>rune-count</code>, <code>rune-size</code>, <code>rune-start?</code>, <code>valid-utf8?</code>, <code>encode-rune</code></td></tr>
-<tr><td>numbers</td><td><code>sign-f32</code>, <code>lerp</code>, <code>clamp</code>, <code>floor-f32</code>, <code>ceil-f32</code>, <code>round-f32</code>, <code>abs-i32</code>, <code>abs-i64</code>, the constants <code>pi-f32</code>, <code>pi-f64</code>, <code>tau-f32</code>, <code>tau-f64</code>, and libm through a <code>declare</code> at both widths: <code>sqrt</code>, <code>abs</code>, <code>floor</code>, <code>ceil</code>, <code>round</code>, <code>fmod</code>, <code>sin</code>, <code>cos</code>, <code>tan</code>, <code>asin</code>, <code>acos</code>, <code>atan</code>, <code>atan2</code>, <code>log</code>, <code>log2</code>, <code>log10</code>, <code>exp</code>, <code>pow</code>, <code>hypot</code>, <code>cbrt</code> — each spelled <code>-f32</code> or <code>-f64</code></td></tr>
+<tr><td>numbers</td><td><code>sign-f32</code>, <code>lerp</code>, <code>clamp</code>, <code>floor-f32</code>, <code>ceil-f32</code>, <code>round-f32</code>, <code>abs</code> (generic over every integer width), the constants <code>pi-f32</code>, <code>pi-f64</code>, <code>tau-f32</code>, <code>tau-f64</code>, and libm through a <code>declare</code> at both widths: <code>sqrt</code>, <code>abs</code>, <code>floor</code>, <code>ceil</code>, <code>round</code>, <code>fmod</code>, <code>sin</code>, <code>cos</code>, <code>tan</code>, <code>asin</code>, <code>acos</code>, <code>atan</code>, <code>atan2</code>, <code>log</code>, <code>log2</code>, <code>log10</code>, <code>exp</code>, <code>pow</code>, <code>hypot</code>, <code>cbrt</code> — each spelled <code>-f32</code> or <code>-f64</code></td></tr>
 <tr><td>time</td><td><code>monotonic-ns</code>, <code>monotonic-seconds</code>, <code>unix-ns</code>, <code>unix-seconds</code>, <code>sleep-ns</code>, <code>sleep-seconds</code>, and <code>ns-per-second</code> and its two smaller siblings</td></tr>
 <tr><td>files</td><td><code>file-exists?</code> and <code>file-size</code>, which answer a value; <code>slurp</code>, <code>barf</code>, <code>delete-file</code>, <code>rename-file</code> and <code>make-directory</code>, which signal <code>FileError</code> under <code>retry</code> and <code>use-value</code></td></tr>
 <tr><td>the operating system</td><td><code>getenv</code>, which answers an <code>(Option [u8])</code> viewing the process environment</td></tr>