diff --git a/spec-conditions.md b/spec-conditions.md
index 5e20abb..8b0e45a 100644
--- a/spec-conditions.md
+++ b/spec-conditions.md
@@ -139,6 +139,31 @@ non-idempotent mutation bites. §3's rule that every clause body and the body
 share a type places the restart syntactically; nothing places it *semantically*,
 and that choice is the author's.
 
+**Which of the runtime's own conditions establish a restart, and why only some
+do.** Four are signalled from below the program with `error`: `StorageExhausted`
+when an allocator cannot satisfy a request, `FileError` when a file operation
+fails, `BoundsError` for an index or a slice outside its container, and
+`ArithError` for an arithmetic operation that has no answer — a divide or
+remainder by zero, `INT64_MIN / -1`, and a float-to-integer cast whose value does
+not fit, each of which was a raw `SIGFPE` or an undefined result before it was a
+condition. The first two establish a `retry` restart at the failing site, because
+their attempt is repeatable: a handler frees something or supplies another path
+and the same operation then succeeds. The last two establish **nothing**, and
+that is a decision rather than an omission. Nothing a handler can do makes index
+51 valid for a length-50 array or makes a division by zero have a quotient, so
+there is no attempt to resume into. A site restart would also have to be
+allocated by the `restart-case` that offers it, on its own stack (§3), which
+means an `alloca` and a push/pop pair emitted at every indexing and every
+division in every checked build — and what it would buy is a *different* answer,
+silently.
+
+So the rule this section describes is unchanged by them: the restarts that matter
+for a bad index or a bad division are the ones the program already established —
+a frame loop's `continue` — and those are on the restart stack and reachable from
+a handler or from the break loop without anything being pushed at the failing
+site. Allocation and file failure are the named exceptions, and spec-memory.md's
+"Allocation failure" says why they have to be.
+
 ## 6. Crossing compiler-generated frames
 
 Transfer is lowered **explicitly** — result propagation plus branch targets — not
diff --git a/spec-memory.md b/spec-memory.md
index dec8722..f13eb43 100644
--- a/spec-memory.md
+++ b/spec-memory.md
@@ -38,12 +38,16 @@ enums, strings, fixed arrays, and value structs composed recursively from those
 types. Tuples and triples join that set when they are introduced. `Ptr`, slices,
 `Vec`, and `Map` are not map keys yet.
 
-Equality and hashing for those keys are compiler-provided structural operations,
-not type classes and not operations available to an unconstrained type variable.
-An empty map takes its type from its context:
+Equality and hashing for those keys are compiler-provided structural operations
+and not type classes. They are not available to an unconstrained type variable
+either; a variable that means to key a map declares `hashable?` in the signature
+that binds it, and the refusal then lands at the call site that names an
+unhashable key. An empty map names its key and value types, because a global
+cannot hold one and there is therefore no declaration for it to take a type from:
 
 ```
-(defvar enemies (Map string Enemy) (map-new))
+(let [enemies (map-new string Enemy)]
+  ...)
 ```
 
 `(get m k)` returns `(Option V)`: absence is `None`, not an untyped `nil`.
@@ -128,26 +132,48 @@ visible in the type:
 
 ## Generics
 
-Parametric polymorphism is monomorphisation, with **no type classes and no
-constraints**. The consequence is a hard rule:
+Parametric polymorphism is monomorphisation, with **no type classes**. A type
+variable is written `$t` wherever a *type* goes — a parameter, the return type,
+or nested as `[$t]` or `(Vec $t)` — and bare `t` where a type's *name* is an
+argument in expression position, as in `(vec-new t)` and the cast `(t x)`. A
+generic body is checked **abstractly**, with nothing substituted, so the rule
+below bites at the definition rather than at whichever call site first
+instantiates it:
 
-> A type variable `a` supports only what every type supports: move, `clone`,
+> A type variable `$t` supports only what every type supports: move, `clone`,
 > field-free storage. It does **not** support `=`, `<`, `+`, or `hash`.
 
-Anything else is passed in explicitly as a function value:
+What makes that liveable is a `where` clause of compile-time type predicates,
+written as a map at the head of the body. There are five — `ordered?`, `equal?`,
+`hashable?`, `numeric?`, `copyable?` — they are not type classes because a
+predicate carries no implementations and merely gates a builtin the compiler
+already has, and they entail one another in one direction, so one clause usually
+does. A variable is move-only by default and `copyable?` is the opt-out, because
+whether a variable moves is not decidable abstractly. plan.org's Types section
+has the full account.
 
 ```
-(defn largest [xs [a]  gt (Fn [a a] bool)] (Option a) ...)
+(defn sort! [s [$t]] ()
+  {:where (ordered? $t)}
+  ...)
 ```
 
-Ordered/arithmetic operators over `a` are therefore rejected, not silently
-instantiated. The alternatives — compile-time interfaces, or intrinsics
-restricted to primitives — are deliberately deferred until the base checker is
-stable (build sequence milestone 4).
+Without such a clause the operator is rejected where it is written, not silently
+instantiated, and the operation is passed in explicitly as a function value
+instead:
+
+```
+(defn largest [xs [$t]  gt (Fn [$t $t] bool)] (Option $t) ...)
+```
+
+The alternatives to predicates — compile-time interfaces, or intrinsics
+restricted to primitives — remain deliberately deferred until the base checker is
+stable (build sequence milestone 4). The ceiling is that nobody can supply a
+user-defined `<`.
 
 `println` is the deliberate exception. It is a compiler-provided,
 type-directed intrinsic: monomorphisation selects or emits a structural printer
-for each concrete instantiation, so `(println x)` is legal for `x : a` without
+for each concrete instantiation, so `(println x)` is legal for `x : $t` without
 introducing a `Printable` type class. Structs, fixed arrays, options and,
 eventually, Vecs and Maps print structurally. `Ptr` and `Handle` print their
 address or identity rather than recursively dereferencing, and collection