diff --git a/NEXT.md b/NEXT.md
index b0afb1a..faca132 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -1,3 +1,88 @@
+## Decided 2026-09-13: generics by monomorphisation, checked abstractly, with `where` predicates
+
+The spike answered it (`SPIKE-GENERICS.md`, on `worktree-agent-afcd2406f3660629b`): **it runs**, the whole feature
+is `lib/check.ml` and nothing else in `lib/`, and instantiation is under the noise floor at 1.8ms whole-program
+re-check. The bill is `llc`+`ld` at **+1.7ms per extra body**, so a generic used at three types adds ~7ms to a
+redefinition. `plan.org` is updated; what follows is the decision and the reasoning that does not belong there.
+
+### The fork that turned out to be a false one
+
+`plan.org` posed a choice nobody needed to make. It said an unconstrained `=`, `<`, `+` or `hash` is *rejected*,
+and that this was "Odin's model". **Odin does not do that** — it checks a polymorphic body only per instantiation,
+so `a + b` over a `$T` compiles and fails only when someone instantiates at a type without `+`. The spike had to
+write a second pass to get plan.org's rule.
+
+Both options were bad in the way the other was good. Rejecting abstractly gives the error at the definition and
+makes every call site carry a comparison: `(sort! xs)` becomes `(sort-by! xs (fn [a b] (< a b)))` everywhere.
+Checking per instantiation keeps the call short and moves the error into code the caller did not write, which is
+worse here than in most languages because a hot-reload session may have been running for an hour before the call
+site is reached.
+
+**What dissolves it is the thing plan.org ruled out while citing Odin: Odin has constraints.**
+`core/slice/slice.odin:289` is `where intrinsics.type_is_ordered(T)`, and there are 41 such predicates. A `where`
+clause tells the abstract pass what it may assume, so the body checks at the definition *and* the call stays
+`(sort! xs)`.
+
+### What is being built
+
+- A type variable binds as `$t` in a signature and is used bare. Already decided; see the sigil entry.
+- A generic body is checked **abstractly**, once, with nothing substituted.
+- A `where` clause over **compile-time type predicates** admits the operators the body needs. Four are wanted —
+  `ordered?`, `equal?`, `hashable?`, `numeric?` — against Odin's forty-one. The prelude's nine non-collapsing
+  functions need only the first two.
+- Each instantiation checks the concrete type satisfies the predicates and refuses **that call site** if not.
+
+**This is not a type class, and the distinction is the one to keep straight.** A type class carries
+implementations, selected per instance, extensible by anyone, and needs dictionaries and coherence rules. A
+predicate carries nothing; it gates a builtin the compiler already has. The ceiling is that nobody can supply a
+user-defined `<` — and every operation the prelude and the containers need is a primitive, so the ceiling does not
+bind. The day someone asks to sort by a comparison they wrote is the day to look at type classes again, and it
+will be obvious.
+
+### What collapsing the prelude actually buys — 27 → 15, not 27 → 6
+
+Measured by the spike against the real sources, and worth knowing before the work starts:
+
+- **13 collapse into 6 with nothing but a signature change** — `swap-*!`, `reverse-*!`, `map-*!`, `reduce-*`,
+  `filter-*`, `sort-*-by!`. They move elements or already take the operation as a function value. `filter` is the
+  strongest case: it allocates, `(vec-new t)` and `push` and returns `(Vec t)`, and the type-erased container
+  runtime needed **no changes at all**, because `SizeOf`/`AlignOf` are computed where the type is concrete. That
+  is the direct confirmation that `spec-memory.md`'s type-erased containers and monomorphised functions compose.
+- **9 collapse into 4 and need a `where`** — `sort-*!`, `index-of-*`, `min-*`, `max-*`. Under the old no-constraint
+  rule these were the ones whose call sites all got longer. With predicates they do not.
+- **5 do not collapse and should not** — `sum-i32`/`sum-f32` widen to `i64`/`f64` with an explicit cast, and "the
+  wider type `t` accumulates into" is a type-level function, which is a constraint system or an associated type.
+  A generic `sum` would have to take its accumulator and its `add`, at which point it *is* `reduce`.
+  `append-i64!`/`append-f64!` are two different primitives, `I64ToBytes` and `F64ToBytes`, and choosing between
+  them per instantiation is compile-time overloading, which is what multimethods are for.
+
+The prelude keeps a per-type layer for the numeric ones. That is the honest number.
+
+### Still open, and not blocking
+
+1. **The runaway refusal.** `(defn grow [x $t] () (grow [x x]))` asks for a copy at `[2 t]`, then `[2 [2 t]]`,
+   forever. Before the spike's cap it did not fail, it **hung** — and `Session.eval` runs the same code, so what
+   hangs is `C-c C-c` with the daemon wedged behind it and nothing to show. The cap is a depth counter refusing
+   past 32, and **the number is arbitrary**. A refusal that names the chain of instantiations rather than the
+   depth it gave up at is the designed version. **Odin has no cap to copy.**
+2. **Ownership is not decidable abstractly, and plan.org does not mention it.** `Types.is_move_only (Var _)` is
+   false, but the same variable at `(Vec i32)` is move-only, so `spec-memory.md`'s dead-set analysis is sound only
+   per instantiation. Either ownership is checked per copy — a generic may then be accepted and its instantiation
+   refused — or type variables carry a move-only constraint, which is a constraint system of a different kind from
+   `where`, since it constrains what the *body* may do rather than what the type supports. Every other analysis in
+   the checker survives abstraction; this one does not.
+3. **`C-c C-c` on a generic installs nothing, silently.** `Session.eval` reports `installs=false, fns=[]` because
+   a generic name never reaches `Tast.fns` by design — only its instantiations do. The fix is expanding to
+   instantiations transitively in `session.ml`; the cells already exist. This must land before generics is usable
+   in the dev loop, which is the whole point of the project.
+4. **Deferred together: generic structs and `$n` length parameters.** `Types.Named` is a bare string and
+   `Types.Array` is `int64 * t`, so either one means `Types.t` gains a parameterised case — and `Types.t` is
+   consumed by `emit.ml`'s layout calculator, `x86.ml`, `render.ml`, the DWARF path and the map key-pair emitter.
+   Same price for both. If both are wanted they are one project; if only one is, drop `$n`.
+5. **Generics across a real compilation-unit boundary.** `Load` flattens imports before checking so it works
+   today, but a package boundary that ever becomes a real unit boundary needs the generic's *body* to cross it —
+   which separate compilation cannot do, and is why C++ puts templates in headers.
+
 ## Decided by the author, 2026-09-13: a type variable takes a `$` sigil
 
 **This overrides plan.org**, which says under Types: *"Lowercase type names are variables, Capitalized are
diff --git a/plan.org b/plan.org
index 85b579e..1837d33 100644
--- a/plan.org
+++ b/plan.org
@@ -210,14 +210,33 @@ and on a managed ~class~ instance. An ordinary ~struct~ never carries one.
 - ~i8..i64~, ~u8..u64~, ~f32~, ~f64~ as real machine types; wrapping arithmetic.
 - Vector width 128-bit. Fixed arrays with component-wise ops and swizzles.
 - Parametric polymorphism by monomorphisation (Odin's model, no type classes, no
-  HKTs). Lowercase type names are variables, Capitalized are concrete — no sigil.
-  This is what makes ~map~/~filter~/~reduce~ and the monomorphic containers work.
-  The price, made explicit in spec-memory.md: with no constraints, a type variable
-  supports only what every type supports. ~=~, ~<~, ~+~ and ~hash~ over an
-  unconstrained ~a~ are rejected, not silently instantiated — they are passed in as
-  function values. ~println~ is the one compiler-provided exception: it selects a
-  structural printer at each concrete instantiation. Compile-time interfaces, if
-  they are ever wanted, come after the base checker is stable.
+  HKTs). A type variable is written ~$t~ at its binding site in a signature and
+  bare ~t~ at a use. This is what makes ~map~/~filter~/~reduce~ and the monomorphic
+  containers work.
+  A generic body is checked *abstractly*, with nothing substituted, so ~=~, ~<~,
+  ~+~ and ~hash~ over an unconstrained variable are rejected at the definition
+  rather than at whichever call site first instantiates it. **This is not Odin's
+  rule** — Odin checks a polymorphic body only per instantiation — and the two
+  decisions are independent even though this line once bundled them.
+  What makes the rejection liveable is a ~where~ clause over compile-time type
+  predicates, which is Odin's (~core/slice/slice.odin:289~,
+  ~where intrinsics.type_is_ordered(T)~). ~(sort! xs)~ declares ~ordered?~ of its
+  variable, the abstract pass then allows ~<~ in the body, and each instantiation
+  checks the concrete type satisfies the predicate and refuses the call site if it
+  does not. Roughly four predicates are wanted here — ~ordered?~, ~equal?~,
+  ~hashable?~, ~numeric?~ — against Odin's forty-one.
+  This is not a type class and the difference is worth keeping straight: a type
+  class carries *implementations* selected per instance and extensible by anyone,
+  and needs dictionaries and coherence rules. A predicate carries nothing — it
+  gates a builtin the compiler already has. The ceiling is that no one can supply
+  a user-defined ~<~; every operation the prelude and the containers need is a
+  primitive, so it does not bind. Compile-time interfaces, if they are ever
+  wanted, come after the base checker is stable.
+  ~println~ is a compiler-provided exception and needs an explicit allow-list of
+  forms the abstract pass defers to instantiation: whether a printer exists for a
+  variable is only decidable once it is substituted. Keep the list short — every
+  member moves a refusal from the definition to a call site, which is what the
+  abstract rule exists to avoid.
 - Function values split three ways (spec-memory.md): ~(Fn [T1 T2] R)~ is a plain
   pointer with no environment — the only kind that crosses FFI or sits in a reload
   cell; a *non-escaping* ~fn~ captures enclosing locals by value into a stack
@@ -833,8 +852,9 @@ marked.
 - ~set~ on places → a fixed list of assignable forms, not ~setf~.
 - Loop story → imperative ~while~/~for~ with ~break~/~continue~ and ~return~;
   ~loop~/~recur~ only if it later earns its place. sand.flan is ported.
-- Generic parameters → inferred at call sites, no explicit instantiation; and no
-  type classes, so unconstrained operators over a type variable are rejected.
+- Generic parameters → inferred at call sites, no explicit instantiation. No type
+  classes. An operator over a variable with no ~where~ clause asserting it is
+  rejected at the definition; a ~where~ predicate is what admits it.
 
 * Unverified claims in this plan
 - *Scope is the biggest risk, not any single feature.* A language, inference,