From 879a43995105c4df1fdf1d9dece4370ea29d561d Mon Sep 17 00:00:00 2001
From: Joseph Ferano <josephferano@gmail.com>
Date: Sun, 20 Sep 2026 20:21:41 +0700
Subject: [PATCH 1/6] A written zero stands where a numeric type variable
 stands

pos? over every numeric type from one definition was the motivating
example for milestone 5 and was the one thing the landed generics could
not write: (> x 0) refused with "expected t, found the integer literal
0", because int_literal had no arm for a want that is a type variable.

It has one now, and the bound is what makes it sound rather than
optimistic. Every type numeric? admits is an integer or a float, and an
untyped integer constant is usable at all of them, so there is no
instantiation of a numeric? variable at which the literal has no
meaning. Under a weaker bound there is -- ordered? admits an enum -- so
numeric? is what is asked for and the refusal names it.

The float literal is refused at a type variable even under numeric?,
and that asymmetry is the concrete arms' own: an integer constant is
usable where a float is wanted and a float literal is never usable
where an integer is wanted, so a body written with 0.5 has no meaning
at the integer half of its own bound. Refusing at the definition is
what the abstract pass is for; the alternative is a surprise at
whichever call site first asks for i32.

The node the abstract pass builds is never emitted. Each copy
re-checks the same form with the variable substituted, and that is
where the literal is built at the concrete width and range-checked --
so (+ x 300) is fine at i32 and a refusal at u8, and u8 is where it is
refused.
---
 lib/check.ml                | 60 +++++++++++++++++++++++++++++++++++--
 test/programs/generics.flan | 42 ++++++++++++++++++++++++++
 test/test_acceptance.ml     | 11 ++++++-
 test/test_flan.ml           | 33 ++++++++++++++++++++
 4 files changed, 142 insertions(+), 4 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index fcc0244..8138d16 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2701,8 +2701,10 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   let tail = ctx.tail in
   ctx.tail <- false;
   match e.Ast.e with
-  | Ast.Int n -> int_literal loc ~want n
-  | Ast.Byte b -> int_literal loc ~want ~default:Types.U8 (Int64.of_int b)
+  | Ast.Int n -> int_literal loc ~want ~preds:ctx.env.tvpreds n
+  | Ast.Byte b ->
+    int_literal loc ~want ~preds:ctx.env.tvpreds ~default:Types.U8
+      (Int64.of_int b)
   (* The float literal's own dyn case, for the reason the integer's has one:
      the ABI carries one width and the literal is built at it. f64 is already
      what an unconstrained float literal defaults to, so this only has to stop
@@ -2713,6 +2715,27 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     let k =
       match want with
       | Some (Types.Float k) -> k
+      (* A float literal at a type variable, refused even under [numeric?] —
+         the asymmetry with the integer literal above is deliberate and is the
+         same asymmetry the concrete arms already have. An untyped integer
+         constant is usable wherever a float is wanted; a float literal is
+         never usable where an integer is wanted (Odin's rule, stated at the
+         [Int] case). So [numeric?] admits integers, and a body written with a
+         float literal has no meaning at the integer half of its own bound.
+         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) ->
+        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 \
+           usable where an integer is wanted. Write the constant as an \
+           integer literal — that one is admitted under {:where (numeric? \
+           $%s)} at every numeric type — or take the value as a parameter"
+          x v
+          (if declares ctx.env.tvpreds v "numeric?" then
+             Printf.sprintf "{:where (numeric? $%s)} admits integers too, so $%s" v v
+           else Printf.sprintf "$%s" v)
+          v
       | Some other when other <> Types.Never ->
         Loc.failk literal_at_want loc "expected %s, found the float literal %g"
           (Types.to_string other) x
@@ -3043,9 +3066,29 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
         ctx.defer_block;
     register_defer ctx loc forms
 
-and int_literal loc ~want ?(default = Types.I32) n =
+and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n =
   match want with
   | Some (Types.Int k) -> mk loc (Types.Int k) (Tast.Int (in_range loc k n, k))
+  (* An integer literal where a *type variable* is wanted: the abstract pass
+     over a generic body, checking [(> x 0)] or [(+ x 1)] with [x] at [$t].
+
+     It is admitted exactly when [$t] is declared [numeric?], and that bound is
+     what makes it sound rather than optimistic: every type [numeric?] admits
+     is an integer or a float, and an untyped integer constant is usable at all
+     of them — the same rule the [Float k] arm below encodes for a concrete
+     float. So there is no instantiation of a [numeric?] variable at which this
+     literal has no meaning, which is the promise the abstract pass exists to
+     make.
+
+     The node built here is never emitted. A generic body produces no code; the
+     instantiation re-checks the same form with [$t] substituted, and then the
+     [Int k] or [Float k] arm above builds the literal at the concrete type and
+     runs the range check. [I64] is the placeholder width and is chosen only so
+     that a value too wide for [I32] survives the abstract pass to be ranged at
+     the instantiation that actually has a type — [(defn f [x $t] $t (+ x 300))]
+     is fine at [i32] and a refusal at [u8], and [u8] is where it is refused. *)
+  | Some (Types.Var v) when declares preds v "numeric?" ->
+    mk loc (Types.Var v) (Tast.Int (n, Types.I64))
   (* A literal in dyn position takes i64 and not the i32 an unconstrained one
      defaults to. This is where "dyn integers are i64" stops being a statement
      about the ABI and becomes one about the language: [(defvar x dyn 5)] holds
@@ -3060,6 +3103,17 @@ and int_literal loc ~want ?(default = Types.I32) n =
      Odin. A float literal is never usable where an integer is wanted. *)
   | Some (Types.Float k) ->
     mk loc (Types.Float k) (Tast.Float (Int64.to_float n, k))
+  (* The same position without the bound. An unconstrained variable supports
+     only what every type supports, and holding a number is not that, so the
+     refusal names the bound that would admit it rather than reporting a type
+     mismatch the programmer cannot act on. *)
+  | Some (Types.Var v) ->
+    Loc.failk literal_at_want loc
+      "the integer literal %Ld cannot stand where $%s is wanted: an \
+       unconstrained type variable may be instantiated at a type that holds \
+       no number. Declare the bound — {:where (numeric? $%s)} — and the \
+       literal is admitted at every type $%s can then be"
+      n v v v
   | Some other when other <> Types.Never ->
     Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
       (Types.to_string other) n
diff --git a/test/programs/generics.flan b/test/programs/generics.flan
index 87ed185..12ddee7 100644
--- a/test/programs/generics.flan
+++ b/test/programs/generics.flan
@@ -50,6 +50,33 @@
   {:where (ordered? $t)}
   (min (max x lo) hi))
 
+;; An integer *literal* where the type variable is wanted, which is what the
+;; author's motivating family needs: one pos? over every numeric type rather
+;; than one per width. The literal is admitted because {:where (numeric? $t)}
+;; is declared, and the bound is what makes it sound rather than optimistic —
+;; every type numeric? admits is an integer or a float, and an untyped integer
+;; constant is usable at all of them, so there is no instantiation at which
+;; this 0 has no meaning. Without the clause it is refused at the definition;
+;; see the rejects in test_flan.ml.
+;;
+;; The literal is never emitted from here. The abstract pass builds a
+;; placeholder and throws it away with the rest of the body; each copy
+;; re-checks (> x 0) with $t substituted, and *that* is where the literal is
+;; built at the concrete width and range-checked.
+(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))
+(defn neg? [x $t] bool {:where (numeric? $t)} (< x 0))
+(defn zero-p? [x $t] bool {:where (numeric? $t)} (= x 0))
+
+;; The same literal in arithmetic rather than comparison, and answering $t
+;; rather than bool, so the placeholder has to survive being the operand of a
+;; Prim and being returned.
+(defn next-after [x $t] $t {:where (numeric? $t)} (+ x 1))
+
+;; The range check is the instantiation's and not the definition's: 300 is
+;; fine at i32 and would be a refusal at u8, and u8 is where it is refused.
+;; This one is only ever asked for at i32.
+(defn plus-300 [x $t] $t {:where (numeric? $t)} (+ x 300))
+
 ;; Two variables, and the second is determined by its own argument.
 (defn fst [a $t  b $u] $t
   (do b a))
@@ -131,6 +158,21 @@
     (println (clamp-to 0.5 1.0 9.0))
     (println (fst 8 true))
 
+    ;; The literal-at-a-type-variable family, at six numeric types from three
+    ;; written bodies. i32, i64, u8, u16, f32 and f64 all reach the same 0 and
+    ;; the same 1.
+    (println (pos? 3))
+    (println (neg? (i8 -3)))
+    (println (zero-p? (u8 0)))
+    (println (zero-p? 0.0))
+    (println (pos? (u16 1)))
+    (println (neg? (f32 -0.5)))
+    (println (next-after 3))
+    (println (next-after (i64 10)))
+    (println (next-after 2.5))
+    (println (next-after (u8 254)))
+    (println (plus-300 1))
+
     (show 3)
     (show 4.5)
     (show "text")
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 542b2f9..f84c9e9 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2584,9 +2584,18 @@ let () =
        scalar types because a default that is returned and one that is
        discarded are two different lowerings, and the last pair — [2 0] — is
        the same pair at a $t that owns storage, where each answer is a header
-       onto whichever of the two buffers the branch chose. *)
+       onto whichever of the two buffers the branch chose.
+
+       The six [true]s and the five numbers after the first [8] are the
+       literal-at-a-type-variable family: three written bodies — pos?/neg?/
+       zero-p?, next-after and plus-300 — reaching i8, u8, u16, i32, i64, f32
+       and f64. [255] is next-after at u8 and is the one that would say
+       whether the placeholder width the abstract pass builds had leaked into
+       a copy; [301] is plus-300 at i32, whose range check belongs to the copy
+       and not to the definition. *)
     let generics_out =
       "3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n\
+       true\ntrue\ntrue\ntrue\ntrue\ntrue\n4\n11\n3.5\n255\n301\n\
        3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n\
        0\n-1\n2.5\n0\ntrue\nfalse\ntrue\n2\n0\n\
        3\n3\n0\n21\n7\n3\n4.5\n"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 077a74b..aef9577 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4711,6 +4711,39 @@ let () =
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
 
+  (* ── A numeric literal where a type variable is wanted ──────────────
+     The author's motivating family — one pos? over every numeric type from
+     one definition — needs a written 0 to stand where $t stands. The bound
+     is what makes it sound: every type [numeric?] admits is an integer or a
+     float, and an untyped integer constant is usable at all of them, so
+     there is no instantiation of a [numeric?] variable at which the literal
+     has no meaning. That is the whole rule, and the four pins below are its
+     two halves and its one asymmetry. *)
+  accepts "an integer literal stands where a numeric? type variable is wanted"
+    "(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))";
+  accepts "and in arithmetic, answering the variable"
+    "(defn next [x $t] $t {:where (numeric? $t)} (+ x 1))";
+  (* [numeric?] is what admits it and nothing weaker does. [ordered?] admits
+     an enum, which holds no number, so a literal under it has an
+     instantiation at which it means nothing — and the refusal below is what
+     stops that reaching the call site. *)
+  rejects_check "an unconstrained type variable admits no literal"
+    ~needle:"may be instantiated at a type that holds no number"
+    "(defn f [x $t] bool (> x 0))";
+  rejects_check "and ordered? is not the bound that admits one"
+    ~needle:"Declare the bound"
+    "(defn f [x $t] bool {:where (ordered? $t)} (> x 0))";
+  (* The asymmetry, and it is the concrete arms' asymmetry rather than a new
+     one: an untyped integer constant is usable where a float is wanted, and
+     a float literal is never usable where an integer is wanted. [numeric?]
+     covers both halves of the numbers, so a body written with a float
+     literal has no meaning at the integer half of its own bound. Refused at
+     the definition, which is where the abstract pass promises refusals
+     arrive — not at whichever call site first asks for i32. *)
+  rejects_check "a float literal is refused at a type variable even under numeric?"
+    ~needle:"may be instantiated at an integer type"
+    "(defn half [x $t] $t {:where (numeric? $t)} (* x 0.5))";
+
   (* A map key that is a type variable has no hash and no equality to emit:
      they are chosen from the concrete type, which does not exist yet. So the
      map operations join print and println on the list of forms the abstract

From c91fd51ad6d5c462da2049878eba79acce4e1b4f Mon Sep 17 00:00:00 2001
From: Joseph Ferano <josephferano@gmail.com>
Date: Sun, 20 Sep 2026 20:30:36 +0700
Subject: [PATCH 2/6] Which copy a generic call gets stopped depending on
 argument order

Implicit widening landed after generics did, and the rule the two of
them left between them read off the order the arguments were written
in. (eq2? i8 i64) was refused, because $t bound to i8 and i64 into i8
can lose. (eq2? i64 i8) was accepted, because $t had already bound to
i64 and the i8 widened into the want that substitution had made
concrete. Same two values, same function, one copy at i8 refused and
one copy at i64 generated.

Neither answer was unsound -- a widen cannot change a number -- so
this is not a bug report, it is a decision that was never taken.
Taking it: implicit widening does not cross a generic binding. A
concrete argument at a variable an earlier argument already bound has
to be that type, and both orders now refuse with the same sentence,
naming the binding, the argument, and the cast to write.

Refusing is the direction that can be walked back. Letting the pair
join at the wider type is a coherent rule too, and it can be added
later without invalidating a program written under this one; the
reverse is not true.

The rule costs almost nothing because Types.widens_to admits only
numeric scalars. A variable bound inside [$t] or (Fn [$t $t] bool)
leaves a parameter no widening ever applied to, so sort-by and the
whole fn-literal path are untouched by construction. Two exceptions
keep the ergonomics: an untyped literal has no type of its own to
keep, so it still takes the variable's; and a form with no type
without a want -- (zeroed) -- is asked for its natural type through a
trial, and falls back to the want it always had when the trial
refuses.
---
 lib/check.ml      | 68 ++++++++++++++++++++++++++++++++++++++++++++---
 test/test_flan.ml | 49 ++++++++++++++++++++++++++++++++++
 2 files changed, 114 insertions(+), 3 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 8138d16..b75ec68 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -7486,9 +7486,71 @@ and generic_call ctx ~want loc name vars pats pret args =
   let subst = ref [] in
   let targs =
     map2_lr
-      (fun p a ->
-         let p = subst_ty !subst p in
-         let a = if generic_ty p then check ctx a else check ctx ~want:p a in
+      (fun pat a ->
+         let p = subst_ty !subst pat in
+         (* Which variable, if any, this parameter *is* — written as a bare
+            [$t] and already bound by an argument to the left. That is the one
+            shape implicit widening can reach, because [Types.widens_to] admits
+            only numeric scalars: a variable bound inside [[$t]] or
+            [(Fn [$t $t] bool)] leaves a parameter no widening applies to, so
+            the [sort-by] path below is untouched by construction. *)
+         let bound_scalar =
+           match pat with
+           | Types.Var v when (not (generic_ty p)) && Types.is_numeric p ->
+             Some v
+           | _ -> None
+         in
+         (* An untyped constant has no type of its own to keep, so it still
+            takes the variable's — [(clamp-to y 0 10)] with [y] an i64 means
+            three i64s and there is no conversion anywhere in it. Everything
+            else is checked on its own terms. *)
+         let untyped_literal =
+           match a.Ast.e with
+           | Ast.Int _ | Ast.Float _ | Ast.Byte _ -> true
+           | _ -> false
+         in
+         let a =
+           if generic_ty p then check ctx a
+           else if bound_scalar <> None && not untyped_literal then
+             (* On its own terms first. A form that has no type without a want
+                — [(zeroed)] is the one that matters — refuses here and is
+                checked against the parameter as it always was; the trial
+                leaves no trace of the attempt. *)
+             (match trial ctx (fun () -> check ctx a) with
+              | Ok r -> r
+              | Error _ -> check ctx ~want:p a)
+           else check ctx ~want:p a
+         in
+         (* **Implicit widening does not cross a generic binding.** A concrete
+            argument at a variable an earlier argument already bound has to be
+            the same type, not merely a type that widens into it.
+
+            This is a decision and not a consequence. Widening landed after
+            generics did, and left behind a rule that depended on argument
+            order: [(pair-eq? i64 i8)] was accepted, because [$t] bound to i64
+            first and the i8 widened into the want; [(pair-eq? i8 i64)] was
+            refused, because [$t] bound to i8 and i64 into i8 can lose. Same
+            two values, same function, two answers. Neither is unsound — a
+            widen cannot change a number — but which instantiation a program
+            gets should not depend on which argument was written first.
+
+            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". *)
+         (match bound_scalar with
+          | Some v when not (Types.equal p a.Tast.ty) ->
+            Loc.failk "check/tyvar-no-widening" a.Tast.loc
+              "%s's $%s was bound to %s by an earlier argument, and this one \
+               is %s. Implicit widening does not cross a generic binding: a \
+               written type is what a type variable takes, so the same \
+               variable is the same type at every argument. Write the \
+               conversion — (%s x) — or pass the arguments at one type"
+              name v (Types.to_string p) (Types.to_string a.Tast.ty)
+              (Types.to_string p)
+          | _ -> ());
          if 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);
diff --git a/test/test_flan.ml b/test/test_flan.ml
index aef9577..d847170 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4711,6 +4711,55 @@ let () =
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
 
+  (* ── Implicit widening does not cross a generic binding ─────────────
+     Widening landed after generics did, and the rule it left behind depended
+     on the order the arguments were written in: the i8-then-i64 call was
+     refused because i64 into i8 can lose, and the i64-then-i8 call was
+     *accepted*, because $t had already bound to i64 and the i8 widened into
+     the want. Same two values, same function, two answers.
+
+     Neither was unsound — a widen cannot change a number — but which copy a
+     program gets should not turn on which argument came first, so both are
+     refused now and both name the binding. Letting the pair join at the wider
+     type is the other coherent rule and it stays available: it can be added
+     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"
+    ~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))))";
+  (* 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"
+    "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
+     (defn main [] () (println (eq2? (i64 3) (i64 (i8 3)))))";
+  (* An untyped constant has no type of its own to keep, so it still takes the
+     variable's. Nothing is converted here — three i64s were written. *)
+  accepts "an untyped literal still takes a bound type variable's type"
+    "(defn clamp3 [x $t  lo $t  hi $t] $t {:where (ordered? $t)} \
+       (min (max x lo) hi))\n\
+     (defn main [] () (println (clamp3 (i64 12) 0 10)))";
+  (* And the shapes widening cannot reach are untouched, which is the reason
+     the rule costs so little: [Types.widens_to] admits only numeric scalars,
+     so a variable bound inside a slice or a function type leaves a parameter
+     no widening applied to in the first place. *)
+  accepts "a variable bound inside a constructor is unaffected"
+    "(defn sort2 [s [$t]  before? (Fn [$t $t] bool)] () \
+       (sort-by s before?))\n\
+     (defn main [] () (let [ns [5 3 9 1]] \
+       (sort2 (slice ns 0 4) (fn [a b] (< a b))) (println (at ns 0))))";
+  (* A form with no type of its own is still checked against the parameter:
+     the trial that asks for its natural type refuses, and the want it always
+     had is what it falls back to. *)
+  accepts "a form that needs a want still gets one at a bound type variable"
+    "(defn pick [a $t  b $t] $t (do b a))\n\
+     (defn main [] () (println (pick (i64 3) (zeroed))))";
+
   (* ── A numeric literal where a type variable is wanted ──────────────
      The author's motivating family — one pos? over every numeric type from
      one definition — needs a written 0 to stand where $t stands. The bound

From c372a98238959040ccd171bd9e5b58c36dad2351 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <josephferano@gmail.com>
Date: Sun, 20 Sep 2026 20:39:16 +0700
Subject: [PATCH 3/6] A refusal about a dyn stopped being reported against a
 prelude line

Nothing stopped a type variable being instantiated at dyn, because dyn
is an ordinary case of Types.t and substituted like any other type. The
copy was then made and walked into the dyn answers that are not all
there, and the refusal arrived from inside the generic's own source:
(or-else (Some d) e) over two dyns was reported against <prelude>:385,
a line the caller did not write and cannot act on.

Refused at the binding instead, where the call site is. The message
does not only say no: two models answer "one body, many types" here
and they are not rivals -- this one copies per written type at compile
time, defgeneric/defmethod dispatch at run time on a value that
carries its own -- so a dyn argument is asking the second question of
the first machinery, and the sentence names the other spelling.

Only the unbounded half is new. A variable carrying a {:where} clause
was already refused, because pred_holds says no to dyn for all four
predicates, and that refusal is left in front of this one on purpose:
it names the predicate the signature wrote down, which is the more
specific of the two answers.

Whether dyn should eventually flow through a generic is the author's
call and is recorded as open. Refusing now is the direction that can
be walked back: allowing it later adds programs, and nothing written
under this rule stops compiling.
---
 lib/check.ml      | 66 ++++++++++++++++++++++++++++++++++++++++++++++-
 test/test_flan.ml | 37 ++++++++++++++++++++++++++
 2 files changed, 102 insertions(+), 1 deletion(-)

diff --git a/lib/check.ml b/lib/check.ml
index b75ec68..1691019 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1374,6 +1374,19 @@ let rec generic_ty (t : Types.t) =
   | Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty r
   | _ -> false
 
+(* Does a type a call site bound a variable to reach a [dyn] anywhere? See the
+   refusal in [generic_call]: [dyn] is a concrete type and substitutes like any
+   other, so nothing stopped a copy being made at it, and the copies walked
+   straight into holes the rest of the language has no [dyn] answer for yet. *)
+let rec reaches_dyn (t : Types.t) =
+  match t with
+  | Types.Dyn -> true
+  | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+  | Types.Option e -> reaches_dyn e
+  | Types.Map (k, v) -> reaches_dyn k || reaches_dyn v
+  | Types.Fn (ps, r) -> List.exists reaches_dyn ps || reaches_dyn r
+  | _ -> false
+
 (* The refusal plan.org's Types section asks for, in one place so that every
    operator says the same thing: with no constraints a type variable supports
    only what *every* type supports, so [=], [<], [+] and [hash] over one are
@@ -7540,8 +7553,15 @@ and generic_call ctx ~want loc name vars pats pret args =
             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) ->
+          | Some v
+            when (not (Types.equal p a.Tast.ty))
+                 && Types.is_numeric a.Tast.ty ->
             Loc.failk "check/tyvar-no-widening" a.Tast.loc
               "%s's $%s was bound to %s by an earlier argument, and this one \
                is %s. Implicit widening does not cross a generic binding: a \
@@ -7569,6 +7589,50 @@ 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;
+  (* **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
+     body did with the value, and the dyn answers are not all there — [(Option
+     dyn)] has no descriptor the collector can find, [as-slice] over a
+     [(Vec dyn)] refuses. So the refusal existed, it just arrived from inside
+     the generic's own source: [(or-else (Some d) e)] over two dyns is reported
+     against [<prelude>:385], a line the caller did not write and cannot act
+     on. Every one of those is this refusal arriving late and in the wrong
+     place.
+
+     Refusing at the binding is also the honest statement of the split. Two
+     models answer "one body, many types" here and they are not rivals: this
+     one instantiates at compile time and keeps the types, and [defgeneric] /
+     [defmulti] dispatch at run time on a value that carries its own. A dyn
+     argument is asking the second question of the first machinery. The
+     message says so and names the other spelling.
+
+     Bounded variables were already refused — [pred_holds] says no to dyn for
+     all four predicates — so this closes the unbounded half, which is exactly
+     the half that reached the prelude-source diagnostics. A variable that
+     *does* carry a clause is left to that refusal deliberately: it names the
+     predicate the signature actually wrote down, which is the more specific
+     answer of the two, and the generic cast's pin depends on it. *)
+  let clause_on v =
+    match Hashtbl.find_opt ctx.env.generics name with
+    | None -> false
+    | Some gfn ->
+      List.exists
+        (fun (p : Ast.pred) -> String.equal p.Ast.pvar v) gfn.Ast.fwhere
+  in
+  List.iter
+    (fun (v, t) ->
+       if reaches_dyn t && not (clause_on v) then
+         Loc.failk "check/tyvar-at-dyn" loc
+           "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 \
+            (defmethod ...) per class dispatches on what the value turns out \
+            to be, which is the question a dyn argument is asking. Write the \
+            type the value has, or reach for the dyn side"
+           name v (Types.to_string t) name)
+    !subst;
   let cparams = List.map (subst_ty !subst) pats in
   let cret = subst_ty !subst pret in
   if List.exists generic_ty cparams || generic_ty cret then begin
diff --git a/test/test_flan.ml b/test/test_flan.ml
index d847170..57b64be 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4711,6 +4711,43 @@ let () =
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
 
+  (* ── 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 the copy was generated. What the copy
+     then ran into was the dyn answers that are not all there — (Option dyn)
+     has no descriptor the collector can find — and the refusal arrived from
+     inside the generic's own source. (or-else (Some d) e) over two dyns used
+     to be reported against <prelude>:385, a line the caller did not write.
+     The refusal is at the call site now, and it names the other model rather
+     than only saying no. *)
+  rejects_check "a type variable is not instantiated at dyn"
+    ~needle:"is not instantiated at dyn"
+    "(defn idf [x $t] $t x)\n\
+     (defvar d dyn 5)\n\
+     (defn main [] () (println (idf d)))";
+  rejects_check "and the refusal names the dyn side rather than only saying no"
+    ~needle:"defmethod"
+    "(defn idf [x $t] $t x)\n\
+     (defvar d dyn 5)\n\
+     (defn main [] () (println (idf d)))";
+  (* Nor at a type that merely *reaches* a dyn, which is the shape that used
+     to walk furthest before failing: (Option dyn) is the case the collector
+     has no descriptor for, and the refusal for it arrived from <prelude>:385.
+     It arrives here now, against the call that asked for the copy. *)
+  rejects_check "nor at a type that merely reaches a dyn"
+    ~needle:"$t = (Option dyn)"
+    "(defn maybe [] (Option dyn) None)\n\
+     (defn idf [x $t] $t x)\n\
+     (defn main [] () (println (some? (idf (maybe)))))";
+  (* A variable that carries a clause keeps the clause's refusal, which names
+     the predicate the signature actually wrote down — the more specific of
+     the two answers, and the one the generic cast's pin above depends on. *)
+  rejects_check "a bounded variable is still refused by its bound"
+    ~needle:"numeric?"
+    "(defn twice [x $t] $t {:where (numeric? $t)} (+ x x))\n\
+     (defvar d dyn 5)\n\
+     (defn main [] () (println (twice d)))";
+
   (* ── Implicit widening does not cross a generic binding ─────────────
      Widening landed after generics did, and the rule it left behind depended
      on the order the arguments were written in: the i8-then-i64 call was

From d5fed12d48349fd73f8e4051c9e5909855d8ac17 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <josephferano@gmail.com>
Date: Sun, 20 Sep 2026 20:46:35 +0700
Subject: [PATCH 4/6] Three messages about milestone 5, from a milestone that
 arrived

The refusals generics obsoleted, swept. Every message that sent
somebody to a schedule now says what is actually true of the thing in
front of them.

An unknown lowercase type name used to be reported as unimplemented
generic code over a type variable. Generics are implemented, and
resolve_name consults env.tyvars and env.subst long before anything
reaches that arm -- so a lowercase name arriving there is a typo too
far from any type to guess at, or a type variable nobody introduced.
The sentence names the sigil that would introduce it.

A capitalised name given type arguments is the other half, and it is
still genuinely unbuilt: Types.Named is a bare string with no room for
parameters, and giving it some is a change to Types.t and therefore to
the layout calculator, both backends, Render and DWARF. Both sites
that reported it -- the type resolver and the value-position fork --
now say a generic *type* is not there yet and point at the generic
function that is.

Plus the prelude's side of it. pos?, neg? and zero? are three
questions about a number's sign, one body each, answering at every
numeric type -- the family the whole feature was asked for, and the
one thing the landed generics could not write until a literal was
allowed to stand at a bounded type variable.

Two collapses examined and declined, with the real reason written
where the old one was. abs stays per width because numeric? is the
only bound that admits a written 0 and it admits floats too, and the
integer body is the wrong abs for a float: it hands back a negative
zero. It waits on an integer? predicate, which is language surface.
min and max stay builtins because they are variadic and slot each
operand so it is evaluated once; a binary prelude generic would put
the double evaluation back at the call site. Their generic half was
never missing -- ordered? already admits them in any body that
declares it.
---
 lib/check.ml                | 54 +++++++++++++++++++++++++++------
 lib/prelude.ml              | 59 +++++++++++++++++++++++++++++++++++--
 test/programs/generics.flan | 43 +++++++++++++++++----------
 test/test_acceptance.ml     |  6 +++-
 test/test_flan.ml           | 36 +++++++++++++++-------
 5 files changed, 159 insertions(+), 39 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 1691019..0e4b2f9 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -854,8 +854,19 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
      | "Map", _ -> fail loc "(Map K V) takes exactly two types"
      | "Result", _ -> unimplemented loc "(Result T E)" 6
      | _ ->
+       (* Not generics, which are here: a *function* is generic over [$t] and
+          instantiated per call site. This is a parameterised named type —
+          [(Pair i32 f64)] — and that is a different thing and is not built.
+          [Types.Named] is a bare string with no parameters, so there is
+          nowhere to put the arguments, and giving it some is a change to
+          [Types.t] and therefore to the layout calculator, both backends,
+          [Render] and the DWARF path. docs/SPIKE-GENERICS.md, question 4,
+          prices it and leaves it out. *)
        fail loc
-         "%s takes no type arguments — generics are milestone 5" name)
+         "%s takes no type arguments. A generic *function* is written with \
+          [$t] in its parameter vector and copied per call site; a generic \
+          *type* — (%s ...) — is not there yet"
+         name name)
 
 (* One edit away from a type that exists — a substitution, an insertion, a
    deletion or a transposition of neighbours. Bounded at one, because two edits
@@ -951,12 +962,26 @@ and resolve_name env ~seen loc n =
       | _ when near_miss env n <> None ->
         Loc.failk "check/unknown-type" loc "unknown type %s — did you mean %s?" n
           (Option.get (near_miss env n))
-      (* Lowercase is a type variable, Capitalized is concrete — no sigil
-         (plan.org, Types). A variable parses, but nothing at milestone 2 can
-         give a value one, so it is rejected here rather than later. *)
+      (* An unknown lowercase name, and the sentence it gets used to be that
+         generics were milestone 5 work. They are not: [$t] binds a type
+         variable and bare [t] uses one, and [resolve_name] has already
+         consulted [env.tyvars] and [env.subst] before anything reaches here.
+         So a lowercase name arriving at this arm is one of exactly two
+         things, and the message names both rather than sending somebody to a
+         schedule.
+
+         Either it is a typo too far from any type to be guessed at — the
+         near-miss arm above catches the one-edit ones — or it is a type
+         variable that was never introduced, which is the sigil's whole
+         purpose to notice: without the binding site a mistyped type name
+         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] ->
-        unimplemented loc
-          (Printf.sprintf "generic code over the type variable %s" n) 5
+        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 \
+           to introduce one, and %s reads it from there"
+          n n n
       | _ -> Loc.failk "check/unknown-type" loc "unknown type %s" n
 
 and array_len env loc = function
@@ -5651,7 +5676,17 @@ and named_call ctx ~want loc name args =
     in
     let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
     (* [min] and [max] are [<] with a pick, so [ordered?] is what they want —
-       not [numeric?]. A generic that declares [ordered?] gets both. *)
+       not [numeric?]. A generic that declares [ordered?] gets both.
+
+       They stay builtins now that generics could express them, and the reason
+       is the two lines above rather than the type system: they are variadic,
+       and each step puts both of its sides in slots so that every operand is
+       evaluated exactly once. A prelude [(defn min [a $t b $t] $t ...)] would
+       be binary and would have to be nested at the call site, which is where
+       the double evaluation this arm exists to prevent would come back. The
+       generic half is already theirs — [ordered?] admits them inside any
+       body that declares it — so collapsing them would cost the arity and
+       the evaluation rule and buy nothing. *)
     unconstrained ctx.env loc name ~needs:"ordered?" a.Tast.ty;
     if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then
       not_numeric name "numbers" a;
@@ -7409,8 +7444,9 @@ and ordinary_call ctx ~want loc name args =
                the fork the form fell down. *)
             Loc.failk "check/unknown-function" loc
               "unknown function %s. A capitalised name is a type, and a type \
-               given type arguments — (%s ...) — is generic code, which is \
-               milestone 5"
+               given type arguments — (%s ...) — is a generic type, which is \
+               not there yet. A generic *function* is: it is written with \
+               [$t] in its parameter vector and copied per call site"
               name name
           else Loc.failk "check/unknown-function" loc "unknown function %s" name
 
diff --git a/lib/prelude.ml b/lib/prelude.ml
index 16c3062..76c4cb7 100644
--- a/lib/prelude.ml
+++ b/lib/prelude.ml
@@ -467,6 +467,44 @@ let source = {flan|
         (push v (at s i))))
     v))
 
+;; ── The sign questions, over every numeric type at once ───────────────
+;;
+;; The family the whole of generics was asked for. Three questions about a
+;; number's sign, one body each, answering at i8 through u64 and at both
+;; float widths — where without a type variable they would be three functions
+;; per width, which is why they were never written at all.
+;;
+;; What makes them writable is not the type variable on its own: it is that a
+;; written 0 may stand where $t stands. That needs the {:where (numeric? $t)}
+;; clause and nothing weaker, because the bound is what promises the literal
+;; has a meaning at every type the variable can become. An unconstrained
+;; variable is refused, and so is [ordered?] — it admits an enum, which holds
+;; no number.
+;;
+;; The comparison is the clause's too: [numeric?] entails [ordered?], so one
+;; predicate on the line gives the body both the < it writes and the 0 it
+;; writes it against.
+;;
+;; **The unsigned instantiations are not mistakes.** (neg? (u8 3)) is false at
+;; every u8 and the copy is a constant, which a reader may find odd in the
+;; emitted code and which is exactly right: a generic is copied per written
+;; type, and the body says what it says at each of them. Refusing the copy
+;; would mean a bound that spells "signed", and there is no such predicate.
+(defn pos? [x $t] bool
+  {:where (numeric? $t)}
+  (> x 0))
+
+(defn neg? [x $t] bool
+  {:where (numeric? $t)}
+  (< x 0))
+
+;; Named zero? rather than =0 because it reads as the question it is. The
+;; float instantiations answer true for both zeros, since -0.0 = 0.0 is what
+;; IEEE says and this does not second-guess it.
+(defn zero? [x $t] bool
+  {:where (numeric? $t)}
+  (= x 0))
+
 ;; ── The per-type layer that stays ─────────────────────────────────────
 ;;
 ;; sum is the one shape a type variable cannot express, and it is worth being
@@ -947,9 +985,24 @@ let source = {flan|
 (declare cbrt-f32 [x f32] f32 "cbrtf")
 (declare cbrt-f64 [x f64] f64 "cbrt")
 
-;; Integer magnitude, one per width because there are no generics over the
-;; numeric types and min and max are builtins rather than functions, so a
-;; single abs is not expressible today.
+;; Integer magnitude, one per width, and the reason it stays that way changed
+;; when generics landed. The old one — no generics over the numeric types —
+;; is not true any more: (defn abs [x $t] $t {:where (numeric? $t)} (if (< x
+;; 0) (- 0 x) x)) checks and runs at every integer width, and the literal 0
+;; stands there because the clause admits it.
+;;
+;; **What stops it is the float half of its own bound.** numeric? is the only
+;; predicate that admits a written 0, and it admits f32 and f64 too — so a
+;; generic abs would be instantiated at them, and the body above is the wrong
+;; abs for a float: (< -0.0 0) is false, so it hands back a negative zero
+;; from a function named abs. The float pair below is libm's for exactly that
+;; reason, a sign-bit clear rather than a negation, and a generic that shadows
+;; it at f32 would be a quiet wrong answer rather than a tidier prelude.
+;;
+;; So the collapse waits on a bound that spells "an integer type" — an
+;; integer? predicate, which is language surface and not this file's call.
+;; FIX.org, "Generics and implicit widening", records it as the candidate.
+;; 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
diff --git a/test/programs/generics.flan b/test/programs/generics.flan
index 12ddee7..78944a8 100644
--- a/test/programs/generics.flan
+++ b/test/programs/generics.flan
@@ -51,21 +51,25 @@
   (min (max x lo) hi))
 
 ;; An integer *literal* where the type variable is wanted, which is what the
-;; author's motivating family needs: one pos? over every numeric type rather
-;; than one per width. The literal is admitted because {:where (numeric? $t)}
-;; is declared, and the bound is what makes it sound rather than optimistic —
-;; every type numeric? admits is an integer or a float, and an untyped integer
-;; constant is usable at all of them, so there is no instantiation at which
-;; this 0 has no meaning. Without the clause it is refused at the definition;
-;; see the rejects in test_flan.ml.
+;; sign family needs: one pos? over every numeric type rather than one per
+;; width. The literal is admitted because {:where (numeric? $t)} is declared,
+;; and the bound is what makes it sound rather than optimistic — every type
+;; numeric? admits is an integer or a float, and an untyped integer constant
+;; is usable at all of them, so there is no instantiation at which this 0 has
+;; no meaning. Without the clause it is refused at the definition; see the
+;; rejects in test_flan.ml.
 ;;
 ;; The literal is never emitted from here. The abstract pass builds a
 ;; placeholder and throws it away with the rest of the body; each copy
 ;; re-checks (> x 0) with $t substituted, and *that* is where the literal is
 ;; built at the concrete width and range-checked.
-(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))
-(defn neg? [x $t] bool {:where (numeric? $t)} (< x 0))
-(defn zero-p? [x $t] bool {:where (numeric? $t)} (= x 0))
+;;
+;; The -t? suffix is because the prelude now carries pos?/neg?/zero? itself.
+;; These are the same three bodies written in an ordinary program, which is
+;; what says the machinery belongs to the language and not to the prelude.
+(defn pos-t? [x $t] bool {:where (numeric? $t)} (> x 0))
+(defn neg-t? [x $t] bool {:where (numeric? $t)} (< x 0))
+(defn zero-t? [x $t] bool {:where (numeric? $t)} (= x 0))
 
 ;; The same literal in arithmetic rather than comparison, and answering $t
 ;; rather than bool, so the placeholder has to survive being the operand of a
@@ -161,18 +165,25 @@
     ;; The literal-at-a-type-variable family, at six numeric types from three
     ;; written bodies. i32, i64, u8, u16, f32 and f64 all reach the same 0 and
     ;; the same 1.
-    (println (pos? 3))
-    (println (neg? (i8 -3)))
-    (println (zero-p? (u8 0)))
-    (println (zero-p? 0.0))
-    (println (pos? (u16 1)))
-    (println (neg? (f32 -0.5)))
+    (println (pos-t? 3))
+    (println (neg-t? (i8 -3)))
+    (println (zero-t? (u8 0)))
+    (println (zero-t? 0.0))
+    (println (pos-t? (u16 1)))
+    (println (neg-t? (f32 -0.5)))
     (println (next-after 3))
     (println (next-after (i64 10)))
     (println (next-after 2.5))
     (println (next-after (u8 254)))
     (println (plus-300 1))
 
+    ;; And the prelude's own three, which are these bodies under their real
+    ;; names. The -0.0 is the one worth asserting: IEEE says -0.0 = 0.0 and
+    ;; zero? does not second-guess it.
+    (println (pos? (i64 3)))
+    (println (zero? -0.0))
+    (println (neg? (u8 3)))
+
     (show 3)
     (show 4.5)
     (show "text")
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index f84c9e9..1a2dbc0 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2592,10 +2592,14 @@ let () =
        and f64. [255] is next-after at u8 and is the one that would say
        whether the placeholder width the abstract pass builds had leaked into
        a copy; [301] is plus-300 at i32, whose range check belongs to the copy
-       and not to the definition. *)
+       and not to the definition. The [true true false] after them is the
+       prelude's own pos?/zero?/neg? — the same three bodies under their real
+       names — and the middle one is zero? at -0.0, which IEEE says is zero
+       and which this does not second-guess. *)
     let generics_out =
       "3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n\
        true\ntrue\ntrue\ntrue\ntrue\ntrue\n4\n11\n3.5\n255\n301\n\
+       true\ntrue\nfalse\n\
        3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n\
        0\n-1\n2.5\n0\ntrue\nfalse\ntrue\n2\n0\n\
        3\n3\n0\n21\n7\n3\n4.5\n"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 57b64be..9965aca 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1161,12 +1161,15 @@ let () =
       | Some { Tast.params = [ Types.Dyn; Types.Dyn ]; _ } -> ()
       | _ -> check "an unannotated pair is two dyn parameters" false)
    | exception _ -> check "an unannotated pair is two dyn parameters" false);
-  (* A bare lowercase name is still an unimplemented type variable everywhere a
-     type is the only thing a slot can hold. A defn's parameter vector stopped
-     being such a place — a slot there may be a parameter instead — so the rule
-     is exercised where it still decides, at a field. *)
+  (* A bare lowercase name where a type is the only thing a slot can hold. It
+     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
+     sigil rather than a milestone. A defn's parameter vector stopped being a
+     type-only slot, which is why the rule is exercised at a field. *)
   rejects_check "a real type variable" "(defstruct Holder [x elem])"
-    ~needle:"milestone 5";
+    ~needle:"write $elem in the parameter vector";
   rejects_check "an unknown concrete type" "(defn f [x Widget] ())"
     ~needle:"unknown type Widget";
 
@@ -2073,9 +2076,16 @@ let () =
   (* [(Pair i32)] in a defvar falls down the value fork now that the third
      element takes either reading, and the generics answer the type fork gave
      it has to be reachable from here too. *)
-  rejects_check "a capitalised call with arguments is generics"
+  (* A capitalised head with arguments is a *type* given type arguments, and
+     that is the half of generics that is not built — Types.Named is a bare
+     string with no room for parameters. The sentence says which half, since
+     generic functions are here and pointing at them is the useful part. *)
+  rejects_check "a capitalised call with arguments is a generic type"
     "(defvar x (Pair i32)) (defn f [] i32 0)"
-    ~needle:"is generic code, which is milestone 5";
+    ~needle:"is a generic type, which is not there yet";
+  accepts "and the generic function it points at is"
+    "(defn pair-fst [a $t  b $u] $t (do b a))\n\
+     (defn main [] () (println (pair-fst 1 true)))";
   rejects_check "defined twice" "(defn f [] ()) (defn f [] ())"
     ~needle:"defined twice";
   accepts "main with no parameters and no return" "(defn main [] ())";
@@ -2895,8 +2905,8 @@ let () =
      defn's body that just answers one says nothing about them. *)
   rejects_check "an fn with nothing to say what it takes"
     "(defn f [] () (fn [x] x))" ~needle:"nothing here says what this fn";
-  rejects_check "type variables are milestone 5" "(defn f [] a 0)"
-    ~needle:"milestone 5";
+  rejects_check "a lowercase return type no signature introduced"
+    "(defn f [] a 0)" ~needle:"write $a in the parameter vector";
   (* The other half: a name in value position now *works*, and the arity is
      checked against the function it names. *)
   rejects_check "a function value at the wrong arity"
@@ -4806,9 +4816,15 @@ let () =
      has no meaning. That is the whole rule, and the four pins below are its
      two halves and its one asymmetry. *)
   accepts "an integer literal stands where a numeric? type variable is wanted"
-    "(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))";
+    "(defn above-zero? [x $t] bool {:where (numeric? $t)} (> x 0))";
   accepts "and in arithmetic, answering the variable"
     "(defn next [x $t] $t {:where (numeric? $t)} (+ x 1))";
+  (* And the prelude's own three, which are that body under its real name at
+     every numeric type from one definition. *)
+  accepts "the prelude's sign family answers at six numeric types"
+    "(defn main [] () (println (pos? 3) ) (println (neg? (i8 -1))) \
+       (println (zero? (u8 0))) (println (zero? 0.0)) \
+       (println (pos? (u64 1))) (println (neg? (f32 -0.5))))";
   (* [numeric?] is what admits it and nothing weaker does. [ordered?] admits
      an enum, which holds no number, so a literal under it has an
      instantiation at which it means nothing — and the refusal below is what

From b64770feb79e93155f8d0152e83fc71d5b4fd992 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <josephferano@gmail.com>
Date: Sun, 20 Sep 2026 21:00:22 +0700
Subject: [PATCH 5/6] A generic crosses a package boundary, and a trial leaves
 one copy

The two compositions the milestone owed, pinned, and the record of the
whole lane.

A package whose exports are generic: pkgs/gen, imported by
pkg-generic.flan at three shapes. One generic at two element types.
One that calls another in its own package at its own variable, so the
transitive copy is generated from a call site two files away. And a
generic written in the program calling one written in the package at
its own $t, which only resolves once Load has flattened both bodies
into one namespace -- the thing that has to change the day a package
becomes a real compilation unit, because a copy is made from a body
and a body that did not cross cannot be copied. Plus the call-site
half of a bound written in another file, quoted here rather than
pointed at in a file the caller cannot change.

And the composition with the widening trial. A binary operator
re-checks its right operand at its left one's type inside a trial, so
a generic call written there is checked twice and once thrown away.
The discarded pass's instantiation does not go back out: instantiate
rewinds a copy whose *body* refused, which is a different event. It
does not have to, and the reason is this lane's own rule rather than
luck -- a generic call's instantiation is read off its arguments and
never off the ambient want, so both passes ask for the same types and
the second ask is a cache hit. Pinned by counting the copies in the
checked program.

The widening lane's note said that cache already rewinds itself. It
does not. Corrected in the comment and in FIX.org, in place.
---
 FIX.org                               | 224 +++++++++++++++++++++++++-
 lib/check.ml                          |  14 +-
 test/dune                             |  13 +-
 test/programs/pkg-generic-reject.flan |  12 ++
 test/programs/pkg-generic.flan        |  35 ++++
 test/programs/pkgs/gen/gen.flan       |  33 ++++
 test/test_acceptance.ml               |  36 +++++
 test/test_flan.ml                     |  41 +++++
 8 files changed, 400 insertions(+), 8 deletions(-)
 create mode 100644 test/programs/pkg-generic-reject.flan
 create mode 100644 test/programs/pkg-generic.flan
 create mode 100644 test/programs/pkgs/gen/gen.flan

diff --git a/FIX.org b/FIX.org
index 27e1313..aafb23f 100644
--- a/FIX.org
+++ b/FIX.org
@@ -3218,9 +3218,13 @@ an abandoned trial that lifted a function out of an ~fn~ literal leaves it in
 out by count, so the live pass gets fresh ones and nothing refers to the
 orphan — and it rides into the module as a function nobody calls. Left because
 ~env~ is the program's table rather than this form's, and rewinding it would
-mean deciding what else on ~env~ a trial may have touched; the one piece of
-~env~ state that genuinely needs rewinding, the generic instantiation cache,
-already rewinds itself in ~instantiate~.
+mean deciding what else on ~env~ a trial may have touched.
+
+[Corrected by the milestone-5 lane, below: the generic instantiation cache
+does not rewind itself either, and does not need to. ~instantiate~ rewinds a
+copy whose *body* refused, which is a different event from a copy the caller
+abandoned. The abandoned one is harmless because the trial and the live pass
+cannot disagree about which copy to make.]
 
 All five symptoms pinned — the two accepts, the shadow, the unknown name, and
 the loop diagnostic.
@@ -3272,3 +3276,217 @@ a reason that is now stated correctly.
 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.
+
+* Milestone 5, and the sweep behind it, 2026-09-20
+
+** What was already there
+Almost all of it, and the first finding of this lane is that finding.
+docs/SPIKE-GENERICS.md carries a banner saying so — "it stopped being current
+when generics landed for real, on 2026-09-13" — and the code agrees:
+~$t~ binds and bare ~t~ reads; ~collect~ puts a generic signature in ~gsigs~
+and keeps it out of ~env.fns~; ~generic_call~ binds left to right,
+substituting each binding into the parameters still to come; ~instantiate~
+caches by ~Types.equal~ on the concrete parameter list; the body is checked
+once abstractly so a refusal lands at the definition; ~{:where~ carries four
+predicates with an entailment table; ~runaway~ caps the depth; a copy is an
+ordinary ~Tast.fn~ with a cell, so both backends were untouched then and are
+untouched now; and ~Check.instantiations~ expands a redefined generic's name
+for ~Session.eval~, which test_session pins at four shapes including a copy
+the running process was never built with.
+
+So this lane is not "start M5". It is the four things M5 did not reach, and
+the sweep the author asked for.
+
+** 1. A written zero may stand where a numeric type variable stands
+The one thing the landed generics could not express was the family the whole
+feature was asked for:
+
+#+begin_src lisp
+(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))
+#+end_src
+
+~(> x 0)~ was refused with "expected t, found the integer literal 0", because
+~int_literal~ had no arm for a want that is a type variable. It has one now,
+and *the bound is what makes it sound rather than optimistic*: every type
+~numeric?~ admits is an integer or a float, and an untyped integer constant is
+usable at all of them, so there is no instantiation of a ~numeric?~ variable
+at which the literal has no meaning. Under anything weaker there is —
+~ordered?~ admits an enum, which holds no number — so ~numeric?~ is what is
+asked for and the refusal names it.
+
+*The float literal is refused at a type variable even under ~numeric?~*, and
+that asymmetry is the concrete arms' own rather than a new rule: an integer
+constant is usable where a float is wanted, and a float literal is never
+usable where an integer is wanted. ~numeric?~ covers both halves of the
+numbers, so a body written with ~0.5~ has no meaning at the integer half of
+its own bound, and refusing at the definition is what the abstract pass is
+for.
+
+Nothing built here is emitted. The abstract pass builds a placeholder at i64
+and throws it away with the rest of the body; each copy re-checks the same
+form with the variable substituted, and that is where the literal is built at
+the concrete width and range-checked — so ~(+ x 300)~ is fine at i32 and a
+refusal at u8, and u8 is where it is refused.
+
+** 2. Generics and implicit widening
+*Decided: implicit widening does not cross a generic binding.*
+
+Widening landed days after generics did, and the rule the two of them left
+between them read off the order the arguments were written in:
+
+#+begin_src lisp
+(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))
+(eq2? (i8 3) (i64 3))   ; refused — i64 into i8 can lose
+(eq2? (i64 3) (i8 3))   ; accepted — $t was i64 already, the i8 widened in
+#+end_src
+
+Same two values, same function, one copy at i8 refused and one copy at i64
+generated. Neither answer is unsound — a widen cannot change a number — so
+this is not a bug report; it is a decision nobody had taken, because the two
+features had never been in the tree at the same time.
+
+Taken: a concrete argument at a variable an earlier argument already bound has
+to be that type. Both orders refuse now, with one sentence naming the binding,
+the argument and the cast to write.
+
+*Why refuse rather than join.* Letting the pair meet at the wider type is the
+other coherent rule, and it is the better one if the ergonomics ask for it.
+It can be added later without invalidating a single program written under this
+rule. The reverse is not true. Refusing is the direction that can be walked
+back, and with two features that had never met, that is the direction to be
+wrong in.
+
+The rule costs almost nothing, because ~Types.widens_to~ admits only numeric
+scalars: a variable bound inside ~[$t]~ or ~(Fn [$t $t] bool)~ leaves a
+parameter no widening ever applied to, so ~sort-by~ and the whole fn-literal
+path are untouched by construction. Two exceptions keep the ergonomics —
+an untyped literal has no type of its own to keep, so it still takes the
+variable's; and a form with no type without a want (~(zeroed)~) is asked for
+its natural type through a ~trial~ and falls back to the want when that
+refuses.
+
+*** And the composition with the trial machinery, which is the reason to care
+A binary operator whose operands disagree re-checks the right one at the left
+one's type inside a ~trial~, so a generic call written there is checked twice,
+once in a pass that is thrown away. An instantiation made during the discarded
+pass does *not* go back out: ~instantiate~ rewinds a copy whose body refused,
+which is a different event.
+
+It does not have to, and the reason is this lane's own rule rather than luck.
+*A generic call's instantiation is read off its arguments and never off the
+ambient want* — an unbound variable is checked with no expectation at all, and
+a bound one no longer widens — so the trial and the live pass ask
+~instantiate~ for the same types, the second ask is a cache hit on the first,
+and exactly one copy exists either way. Pinned by counting copies in the
+checked program, not by reading the comment.
+
+The widening lane's own note said the instantiation cache "already rewinds
+itself"; it does not, and the entry above has been corrected in place.
+
+** 3. A type variable is not instantiated at dyn
+*Decided: refused, at the binding.*
+
+Nothing stopped it before, because ~dyn~ is an ordinary case of ~Types.t~ and
+substituted like any other type. The copy was then made and walked into the
+dyn answers that are not all there, and the refusal arrived from inside the
+generic's own source: ~(or-else (Some d) e)~ over two dyns was reported
+against ~<prelude>:385~, about a descriptor the collector cannot build for
+~(Option dyn)~ — a line the caller did not write and cannot act on. Every
+such case is this refusal arriving late and in the wrong place.
+
+The message does not only say no. Two models answer "one body, many types"
+here and they are not rivals: this one copies per written type at compile
+time, ~defgeneric~/~defmethod~ dispatch at run time on a value that carries
+its own. A dyn argument is asking the second question of the first machinery,
+so the sentence names the other spelling.
+
+Only the unbounded half is new — a variable carrying a ~{:where}~ clause was
+already refused by ~pred_holds~, and that refusal is left in front of this one
+deliberately, because it names the predicate the signature wrote down.
+
+*Open, and the author's:* whether dyn should eventually flow through a
+generic at all. Refusing now is the walk-backable direction for the same
+reason as the widening decision.
+
+** 4. Three messages about milestone 5, from a milestone that arrived
+Swept, and they were not all the same kind of stale.
+
+- ~check.ml~'s unknown-lowercase-type arm reported "generic code over the
+  type variable X is not implemented yet — milestone 5 work". Generics are
+  implemented, and ~resolve_name~ consults ~env.tyvars~ and ~env.subst~ long
+  before anything reaches that arm, so a lowercase name arriving there is a
+  typo too far from any type to guess at, or a type variable nobody
+  introduced. It names the sigil that would introduce it.
+- The type resolver's "X takes no type arguments — generics are milestone 5"
+  and the value-position fork's "a type given type arguments is generic code,
+  which is milestone 5" are about the *other* half, which is genuinely
+  unbuilt: ~Types.Named~ is a bare string with no room for parameters, and
+  giving it some is a change to ~Types.t~ and therefore to the layout
+  calculator, both backends, ~Render~ and DWARF. Both now say a generic
+  *type* is not there yet and point at the generic function that is. Nothing
+  was built for them.
+
+Three test needles moved with them.
+
+** 5. The prelude sweep — what collapsed, what did not
+*Added:* ~pos?~, ~neg?~, ~zero?~. Three questions about a number's sign, one
+body each, answering at i8 through u64 and at both float widths. They were
+never written before because without a type variable they are three functions
+per width; they are writable now because of item 1 above and not because of
+the type variable alone.
+
+*Declined, with the real reason written where the old one was:*
+
+- ~abs-i32~/~abs-i64~ stay two functions. The comment's old reason — "there
+  are no generics over the numeric types" — is false now, and the generic
+  body checks and runs at every integer width. What stops it is the float
+  half of its own bound: ~numeric?~ is the only predicate that admits a
+  written ~0~ and it admits f32/f64 too, and ~(if (< x 0) (- 0 x) x)~ is the
+  wrong abs for a float — it hands back a negative zero. The float pair is
+  libm's ~fabs~ for exactly that reason. *The collapse waits on a bound that
+  spells "an integer type".*
+- ~min~/~max~ stay builtins. Not a type-system limit: they are variadic, and
+  each step slots both of its sides so every operand is evaluated exactly
+  once. A binary prelude generic would have to be nested at the call site,
+  which puts the double evaluation back. Their generic half was never missing
+  — ~ordered?~ already admits them in any body that declares it.
+
+*** An ~integer?~ predicate — recorded, not built
+It would collapse ~abs~, and it would let ~%~, the bitwise operators and the
+shifts be written over a variable. It is four lines in ~pred_holds~,
+~predicate_names~ and ~pred_entails~ (declared ~integer?~ gives ~numeric?~,
+~ordered?~ and ~equal?~). It is not built here because adding a predicate is
+language surface — the vocabulary a programmer writes — and that is the
+author's call, not a lane's.
+
+** What this lane did not build, deliberately
+- *Generic types.* ~(defstruct Pair [a $t b $t])~ cannot be spelled, and
+  the price is in the spike: ~Types.t~ and every backend. Out of scope, and
+  the two messages above now say so accurately.
+- *"In instantiation of" notes.* A refusal inside a copy points at the
+  generic's source with no note saying which call site asked for that type.
+  ~Check.instantiation_origin~ exists and ~session.ml~ already uses it for
+  compatibility reports, so the data is there; wiring it into every ~fail~
+  under an instantiation is the spike's "bulky, not hard" bucket and is a
+  lane of its own. Two of the three places it mattered most are closed by
+  items 2 and 3 above, which move those refusals to the call site outright.
+- *~$n~ in length position.* Same price as generic types, smaller prize.
+
+** Pins added
+Cross-package generics (~programs/pkg-generic.flan~ and a new
+~pkgs/gen~ package — one generic at two element types, one calling another in
+its own package at its own variable so the transitive copy is generated from a
+call site two files away, and a local generic calling across the boundary at
+its own ~$t~), both backends and -O0; the package bound refused at the call
+with the clause quoted; the literal family at six numeric types in the
+generics corpus row; the prelude's three under their real names including
+~zero?~ at ~-0.0~; both widening orders refusing; the written conversion and
+the untyped literal still accepted; the fn-literal path unaffected; ~(zeroed)~
+still getting its want; ~$t~ at dyn and at ~(Option dyn)~; a bounded variable
+still refused by its bound; the abandoned-trial copy count; and the three
+reworded messages.
+
+Dev-loop reload needed nothing: test_session already pins ~C-c C-c~ on a
+generic installing its copies, the callee side, the absence of a stale cache
+across two evaluations, and a redefinition that needs a copy the process was
+never built with.
diff --git a/lib/check.ml b/lib/check.ml
index 0e4b2f9..a3dffc2 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -7882,8 +7882,18 @@ and trial ctx f =
      fresh ones and nothing refers to the orphan — and it rides along into the
      module as a function nobody calls. Left alone because [env] is the
      program's table and not this form's, and rewinding it would mean deciding
-     what else on [env] a trial may have touched; the generic instantiation
-     cache already rolls itself back, in [instantiate].
+     what else on [env] a trial may have touched.
+
+     The generic instantiation cache is the other table a trial reaches, and
+     it does not rewind either. [instantiate] rewinds a copy whose *body*
+     refused, which is a different event from a copy the caller abandoned —
+     and the abandoned one does not need rewinding. A generic call's
+     instantiation is read off its arguments and never off the ambient want:
+     an unbound variable is checked with no expectation at all, and a bound
+     one does not widen. So the trial and the live pass ask [instantiate] for
+     the same types, the second ask is a cache hit on the first, and exactly
+     one copy exists either way. Pinned in test_flan, "a generic inside an
+     abandoned trial".
 
      Only [Loc.Error] is caught. A timeout or a stack overflow is not a
      refusal to reconsider, and silently continuing past one would turn a
diff --git a/test/dune b/test/dune
index fe33b84..62338d6 100644
--- a/test/dune
+++ b/test/dune
@@ -60,6 +60,10 @@
   ; it defines a get of its own — shadow-builtin.flan, which is the pin that
   ; a shadow stops at the file that declared it.
   (glob_files programs/pkgs/shadowed/*)
+  ; The package whose exports are generic, which pkg-generic.flan and
+  ; pkg-generic-reject.flan import: the body has to be present where the copy
+  ; is made, so the directory comes whole like every other package.
+  (glob_files programs/pkgs/gen/*)
   ; The synthetic C header the importer's table reads. Committed rather than
   ; reached for on the machine: the raylib case needs raylib installed, at the
   ; right version, with a variable set, so it skips everywhere and covers
@@ -221,7 +225,8 @@
   (glob_files programs/pkgs/macring/*)
   (glob_files programs/pkgs/macspin/*)
   ; And the package shadow-builtin.flan imports.
-  (glob_files programs/pkgs/shadowed/*))
+  (glob_files programs/pkgs/shadowed/*)
+  (glob_files programs/pkgs/gen/*))
  (action (run ./test_valgrind.exe)))
 
 ; The corpus a fourth time, through the hand-written x86-64 backend, compared
@@ -280,7 +285,8 @@
   (glob_files programs/pkgs/macring/*)
   (glob_files programs/pkgs/macspin/*)
   ; And the package shadow-builtin.flan imports.
-  (glob_files programs/pkgs/shadowed/*))
+  (glob_files programs/pkgs/shadowed/*)
+  (glob_files programs/pkgs/gen/*))
  (action
   (setenv SURVEY_STRICT 1
    (setenv SURVEY_QUIET 1
@@ -445,7 +451,8 @@
   (glob_files programs/pkgs/macring/*)
   (glob_files programs/pkgs/macspin/*)
   ; And the package shadow-builtin.flan imports.
-  (glob_files programs/pkgs/shadowed/*))
+  (glob_files programs/pkgs/shadowed/*)
+  (glob_files programs/pkgs/gen/*))
  (action
   (setenv SURVEY_STRICT 1
    (setenv SURVEY_QUIET 1
diff --git a/test/programs/pkg-generic-reject.flan b/test/programs/pkg-generic-reject.flan
new file mode 100644
index 0000000..29d36b7
--- /dev/null
+++ b/test/programs/pkg-generic-reject.flan
@@ -0,0 +1,12 @@
+;;;; The call-site half of a bound written in another file.
+;;;;
+;;;; gen/largest is {:where (ordered? $t)}, and a [string] is not ordered. The
+;;;; refusal has to arrive here, against the call that asked for the copy, and
+;;;; it has to quote the clause — a message pointing into pkgs/gen/gen.flan
+;;;; would be naming a line the caller did not write and cannot change.
+(import gen "pkgs/gen")
+
+(defn main [] i32
+  (let [ss ["a" "b"]]
+    (println (gen/largest (slice ss 0 2))))
+  0)
diff --git a/test/programs/pkg-generic.flan b/test/programs/pkg-generic.flan
new file mode 100644
index 0000000..58a7289
--- /dev/null
+++ b/test/programs/pkg-generic.flan
@@ -0,0 +1,35 @@
+;;;; A generic defined in a package, instantiated by the program.
+;;;;
+;;;; The copies are made here, from a body written there. Three things are
+;;;; being asserted and only the first is obvious: that the call works at all;
+;;;; that instantiation is still transitive across the boundary, so gen/ends
+;;;; asking for gen/last-of at its own variable generates that copy from this
+;;;; file's call site; and that a {:where} clause written in the package is
+;;;; what a caller here is judged against.
+;;;;
+;;;; And one thing in the other direction: a generic written *here* calling a
+;;;; generic written *there* at its own variable, which is the shape that only
+;;;; resolves once both bodies are in one namespace.
+
+(import gen "pkgs/gen")
+
+;;; Local generic over the imported one, at this file's variable.
+(defn tail-twice [s [$t]] $t
+  {:where (numeric? $t)}
+  (+ (gen/ends s) (gen/ends s)))
+
+(defn main [] i32
+  (let [ns [5 3 9 1]
+        fs [2.5 0.5 1.5]]
+    ;; One package generic at two element types: two copies, one body.
+    (println (gen/last-of (slice ns 0 4)))
+    (println (gen/last-of (slice fs 0 3)))
+    ;; The transitive one, also at two.
+    (println (gen/ends (slice ns 0 4)))
+    (println (gen/ends (slice fs 0 3)))
+    ;; The bounded one.
+    (println (gen/largest (slice ns 0 4)))
+    ;; And the local generic that calls across the boundary at its own $t.
+    (println (tail-twice (slice ns 0 4)))
+    (println (tail-twice (slice fs 0 3))))
+  0)
diff --git a/test/programs/pkgs/gen/gen.flan b/test/programs/pkgs/gen/gen.flan
new file mode 100644
index 0000000..24146a0
--- /dev/null
+++ b/test/programs/pkgs/gen/gen.flan
@@ -0,0 +1,33 @@
+;;;; A package whose exports are generic.
+;;;;
+;;;; The spike's "no plan" bucket named this one, and named what makes it
+;;;; work: Load flattens every import into one namespace *before* the checker
+;;;; runs, so the generic's body is present at the call site the way a C++
+;;;; template's is because it sits in a header. Nothing here crosses a real
+;;;; compilation-unit boundary, and the day a package becomes one, this is the
+;;;; thing that has to change — a copy is made from a body, and a body that
+;;;; did not cross cannot be copied.
+;;;;
+;;;; What this package is for: a generic called from the program at two types,
+;;;; a bounded generic whose {:where} has to be readable from outside the
+;;;; file that wrote it, and a generic that calls another generic in its own
+;;;; package at its own variable, so the transitive copy is generated from a
+;;;; call site two files away.
+
+(defn last-of [s [$t]] $t
+  (at s (- (len s) 1)))
+
+;;; Calls last-of at its own variable: the copy of last-of is generated when
+;;; this is instantiated, and this is instantiated from the program.
+(defn ends [s [$t]] $t
+  (last-of s))
+
+;;; The bound travels with the signature. A caller that passes a type the
+;;; clause refuses is refused at the call, against a requirement written in
+;;; another file.
+(defn largest [s [$t]] $t
+  {:where (ordered? $t)}
+  (let [m (at s 0)]
+    (dotimes [i (len s)]
+      (set m (max m (at s i))))
+    m))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 1a2dbc0..7bbbe26 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2513,6 +2513,30 @@ let () =
        raylib itself. Loading it twice would declare every binding twice. *)
     outputs "a package reached along two routes" "programs/pkg-shared.flan"
       "ok\n";
+    (* A generic defined in a package and instantiated by the program. The
+       spike's "no plan" bucket named this and named what makes it work: Load
+       flattens every import into one namespace before the checker runs, so
+       the generic's *body* is present where the copy is made, the way a C++
+       template's is because it sits in a header. It is also the thing that
+       has to change the day a package becomes a real compilation unit — a
+       copy is made from a body, and a body that did not cross cannot be
+       copied.
+
+       Three shapes, because only the first is obvious. gen/last-of at two
+       element types is one body and two copies. gen/ends calls gen/last-of at
+       its *own* variable, so that copy is generated from this file's call
+       site and instantiation is still transitive across the boundary. And
+       tail-twice is a generic written here calling one written there at its
+       own $t, which only resolves once both bodies are in the one namespace.
+
+       The numbers are: last-of at i32 and f64, ends at the same two, largest
+       at i32, and tail-twice at both. *)
+    outputs "a generic defined in a package" "programs/pkg-generic.flan"
+      "1\n1.5\n1\n1.5\n9\n2\n3\n";
+    outputs ~opt:"-O0" "a generic defined in a package, -O0"
+      "programs/pkg-generic.flan" "1\n1.5\n1\n1.5\n9\n2\n3\n";
+    (* The call-site half of a bound written in another file is pinned with
+       the other refusals, further down — see "a package generic's bound". *)
     (* And the diamond with a type crossing it, which is the case the dedupe
        exists for rather than a restatement of the one above. pkg-diamond
        imports area and draw; both import shape; a shape/Box is built inside
@@ -2660,6 +2684,18 @@ let () =
        beneath it, naming rl/with-mode-2d at the call site rather than
        pointing into the package — that half is rendering and is not asserted
        here. *)
+    (* A {:where} clause travels with the signature across a package
+       boundary, and the refusal it produces lands at the call. Both halves
+       are asserted because only together are they the Elm-grade answer: the
+       type that failed and the clause it failed against, quoted here rather
+       than pointed at in pkgs/gen/gen.flan — a line the caller did not write
+       and cannot change. *)
+    refuses "a package generic's bound, refused at the call"
+      "programs/pkg-generic-reject.flan"
+      "string does not answer ordered?";
+    refuses "and the refusal quotes the clause the package wrote"
+      "programs/pkg-generic-reject.flan" "{:where (ordered? $t)}";
+
     refuses "with-mode-2d written without a camera"
       "programs/rl-with-reject.flan"
       "with-mode-2d-takes-a-camera-and-a-body";
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 9965aca..cd985b9 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4721,6 +4721,47 @@ let () =
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
 
+  (* ── A generic call inside an abandoned widening trial ──────────────
+     The two features land days apart and meet here. A binary operator whose
+     operands disagree re-checks the right one at the left one's type inside a
+     [trial], and on a refusal reconsiders with the join — so a generic call
+     written on the right is checked twice, once in a pass that is thrown
+     away. What the discarded pass leaves behind in [env] is the question, and
+     [env] is the program's table, not the form's: an instantiation made
+     during it does not go back out, because [instantiate] rewinds only a copy
+     whose *body* refused.
+
+     It does not have to. The answer is that the two passes cannot disagree
+     about which copy to make, and that is a consequence of the rule above
+     rather than luck: a generic call's instantiation is read off its
+     arguments and never off the ambient want — an unbound variable is checked
+     with no expectation at all, and a bound one no longer widens — so the
+     trial and the live pass ask [instantiate] for the same types, and the
+     second ask is a cache hit on the first. One copy is emitted, at the type
+     the arguments chose, and the widening happens around the call.
+
+     (twoq 2 3) is i32 both times; the i8 on the left is what moves. *)
+  (let p =
+     checked
+       "(defn twoq [a $t  b $t] $t {:where (numeric? $t)} (+ a b))\n\
+        (defn main [] () (let [small (i8 1)] \
+          (println (+ small (twoq 2 3)))))"
+   in
+   let copies =
+     List.filter
+       (fun (f : Tast.fn) ->
+          String.length f.Tast.name >= 5 && String.sub f.Tast.name 0 5 = "twoq-")
+       p.Tast.fns
+   in
+   match copies with
+   | [ { Tast.name = "twoq-i32"; _ } ] -> ()
+   | l ->
+     check
+       (Printf.sprintf
+          "a generic inside an abandoned trial is instantiated once: %s"
+          (String.concat " " (List.map (fun (f : Tast.fn) -> f.Tast.name) l)))
+       false);
+
   (* ── 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 the copy was generated. What the copy

From 56040ec6bdc09276360d43227f28f60d54e90dac Mon Sep 17 00:00:00 2001
From: Joseph Ferano <josephferano@gmail.com>
Date: Sun, 20 Sep 2026 21:04:37 +0700
Subject: [PATCH 6/6] The account of generics catches up with the three rules
 it gained

The spike banner names plan.org's Types section and spec-memory.md's
Generics section as the current account. Neither said anything about a
literal at a type variable, about widening meeting a generic binding,
or about dyn, and all three are now observable from a program -- so
the account had a hole rather than an error. Filled, in
spec-memory.md, in the terms a programmer meets them in.

And one stale claim found and deliberately left: plan.org still lists
five predicates and describes copyable? and move-only-by-default at
length. spec-memory.md already records that copyable? went with the
second repeal and check.ml has four. That sentence belongs to the
ownership-repeal lane, so it is flagged in FIX.org rather than
rewritten here.
---
 FIX.org        | 14 ++++++++++++++
 spec-memory.md | 27 +++++++++++++++++++++++++++
 2 files changed, 41 insertions(+)

diff --git a/FIX.org b/FIX.org
index aafb23f..6b8c2f1 100644
--- a/FIX.org
+++ b/FIX.org
@@ -3490,3 +3490,17 @@ Dev-loop reload needed nothing: test_session already pins ~C-c C-c~ on a
 generic installing its copies, the callee side, the absence of a stale cache
 across two evaluations, and a redefinition that needs a copy the process was
 never built with.
+
+** One stale claim flagged, not touched
+plan.org's Types section still lists *five* predicates and describes
+~copyable?~ and "a type variable is move-only by default" at length.
+spec-memory.md's Generics section already records that ~copyable?~ went with
+the second repeal, and ~predicate_names~ in check.ml has four. plan.org is the
+one that is behind. Left alone deliberately: it is the ownership-repeal lane's
+sentence to retire, not this one's, and it is flagged here so that lane picks
+it up.
+
+spec-memory.md's Generics section gained the three rules this lane decided —
+the literal under ~numeric?~, the widening boundary, and dyn — because the
+spike banner names that section and plan.org's Types as the current account,
+and all three are observable from a program.
diff --git a/spec-memory.md b/spec-memory.md
index 5345170..3430b07 100644
--- a/spec-memory.md
+++ b/spec-memory.md
@@ -301,6 +301,33 @@ Type arguments are **inferred at call sites** from the argument types; there is
 no explicit instantiation syntax in the first implementation. A type variable
 that appears only in the return type is therefore an error.
 
+Three further rules about what a call site may pass, all decided 2026-09-20 and
+written up in FIX.org, "Milestone 5, and the sweep behind it":
+
+**A written number may stand where a type variable stands, under `numeric?`.**
+`(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))` is the family the
+feature was asked for, and the bound is what makes the `0` sound rather than
+optimistic: every type `numeric?` admits is an integer or a float, and an
+untyped integer constant is usable at all of them. Nothing weaker admits it —
+`ordered?` admits an enum, which holds no number. A *float* literal is refused
+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
+a variable an earlier argument already bound has to be that type, not merely
+one that widens into it — otherwise which copy a call gets depends on which
+argument was written first. Letting the pair meet at the wider type stays
+available as a later loosening; nothing written under this rule would stop
+compiling. 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
+compile time, `defgeneric`/`defmethod` dispatch at run time on a value that
+carries its own. A dyn argument asks the second question of the first
+machinery, and the refusal says so. Whether dyn should ever flow through a
+generic is open.
+
 ## Function values
 
 Three cases, split by whether the value escapes the frame that made it.