diff --git a/FIX.org b/FIX.org
index d9a0b9c..de939ef 100644
--- a/FIX.org
+++ b/FIX.org
@@ -3229,9 +3229,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.
@@ -3558,3 +3562,230 @@ them exactly as it skips the shadowing guard; nothing in that test changed.
 and ~@sanitize~ sweeps were not run here — the new corpus row is registered
 for the x86 survey through the existing ~programs/*.flan~ glob and will be
 compared on the next sweep.
+* 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.
+
+** 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/lib/check.ml b/lib/check.ml
index 0a2f854..bebe66f 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -904,8 +904,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
@@ -1001,12 +1012,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
@@ -1424,6 +1449,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
@@ -2751,8 +2789,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
@@ -2763,6 +2803,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
@@ -3093,9 +3154,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
@@ -3110,6 +3191,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
@@ -5678,7 +5770,17 @@ and named_call ?(qualified = false) 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;
@@ -7436,8 +7538,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
 
@@ -7526,9 +7629,78 @@ 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". *)
+         (* 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 ->
+            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);
@@ -7547,6 +7719,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
@@ -7760,8 +7976,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/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/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.
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/generics.flan b/test/programs/generics.flan
index 87ed185..78944a8 100644
--- a/test/programs/generics.flan
+++ b/test/programs/generics.flan
@@ -50,6 +50,37 @@
   {:where (ordered? $t)}
   (min (max x lo) hi))
 
+;; An integer *literal* where the type variable is wanted, which is what the
+;; 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.
+;;
+;; 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
+;; 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 +162,28 @@
     (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-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/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 e9b671d..bea8d35 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
@@ -2598,9 +2622,22 @@ 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. 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"
@@ -2661,6 +2698,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 e03034d..7b21077 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"
@@ -4815,6 +4825,172 @@ 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
+     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
+     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
+     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 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
+     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