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

@@ -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.

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.