From cb56fc14b16a7201f3d4e33c66268ef060bb8b1e Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 13:13:10 +0700
Subject: [PATCH 01/11] Generic functions instantiated at their call sites,
 spiked

---
 lib/check.ml           | 341 ++++++++++++++++++++++++++++++++++++++++-
 spike/generics/id.flan |   7 +
 2 files changed, 346 insertions(+), 2 deletions(-)
 create mode 100644 spike/generics/id.flan

diff --git a/lib/check.ml b/lib/check.ml
index 30b2326..ff22475 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -73,6 +73,35 @@ type env = {
      because a handler is called from wherever the signal was and cannot be a
      branch in the function that established it. *)
   mutable lifted : Tast.fn list;
+
+  (* ── Generics by monomorphisation (spike, milestone 5) ────────────────
+     A generic [defn] is *not* in [fns]: its signature mentions type variables
+     and nothing can be called at it. It lives here, as the AST it was written
+     as, and every call site turns it into an ordinary function with concrete
+     types. Odin's model exactly — [find_or_generate_polymorphic_procedure]
+     keeps the source [Entity] and hangs generated ones off it. *)
+  generics : (string, Ast.fn) Hashtbl.t;
+  (* Its signature as *written*: parameter and return types with [Types.Var]
+     in them. This is the pattern a call site matches its argument types
+     against to bind the variables. *)
+  gsigs   : (string, string list * Types.t list * Types.t) Hashtbl.t;
+  (* The instantiation cache. Odin's [gen_procs] list, keyed the way Odin keys
+     it: a linear scan comparing whole concrete signatures with
+     [are_types_identical] — here [Types.equal] pairwise. Same types twice
+     means one copy. *)
+  insts   : (string, (Types.t list * Types.t * string) list ref) Hashtbl.t;
+  (* The copies themselves, in the order they were generated. They are
+     ordinary [Tast.fn]s from here down; nothing in a backend knows they were
+     ever generic. *)
+  mutable instances : Tast.fn list;
+  (* The type variables in scope while a generic signature is being resolved.
+     Empty everywhere else, which is what keeps the lowercase rejection at
+     [resolve_name] the default. *)
+  mutable tyvars : string list;
+  (* What each of them is bound to while one instantiation's body is checked.
+     [resolve_name] consults it before anything else, so the body resolves
+     [t] to [i32] and every node under it is concrete. *)
+  mutable subst : (string * Types.t) list;
 }
 
 let new_env () = {
@@ -87,6 +116,12 @@ let new_env () = {
   fns     = Hashtbl.create 32;
   globals = Hashtbl.create 16;
   lifted = [];
+  generics = Hashtbl.create 8;
+  gsigs = Hashtbl.create 8;
+  insts = Hashtbl.create 8;
+  instances = [];
+  tyvars = [];
+  subst = [];
 }
 
 (* Where a named type was declared, and what it has, as a note.
@@ -520,6 +555,33 @@ and near_miss env n =
   List.find_opt (fun c -> c <> n && one_edit n c) candidates
 
 and resolve_name env ~seen loc n =
+  (* ── Type variables, with a sigil at the binding site ─────────────────
+     [$t] *introduces* a variable and bare [t] uses it, which is Odin's
+     spelling ([$T] in the signature, [T] in the body). The sigil is read as
+     an ordinary symbol character, so the whole decision lives here: nothing
+     in the reader, the parser or the AST knows the character means anything.
+
+     Which names are variables is decided before this is ever called —
+     [signature_tyvars] scans the signature for the sigil and puts the bare
+     names in [env.tyvars] — so an unknown lowercase name is still the
+     unknown-type error it always was. That is the point of the sigil: without
+     one, a mistyped type name silently became a type parameter and made the
+     function more permissive than it was written to be. *)
+  let bare = if n <> "" && n.[0] = '$' then String.sub n 1 (String.length n - 1) else n in
+  match List.assoc_opt bare env.subst with
+  (* Inside an instantiation: the variable is this concrete type, and every
+     node checked under it is as concrete as if it had been written out. *)
+  | Some t -> t
+  | None ->
+  if List.mem bare env.tyvars then Types.Var bare
+  else if n <> bare then
+    (* A sigil somewhere that is not a [defn] signature: a struct field, a
+       global, a [let] annotation. There is nowhere for it to bind, so it is
+       the error rather than a variable with no scope. *)
+    Loc.failk "check/unbound-type-variable" loc
+      "%s introduces a type variable, and only a defn signature can — write \
+       the concrete type here" n
+  else
   match Types.ikind_of_name n with
   | Some k -> Types.Int k
   | None ->
@@ -570,6 +632,123 @@ and array_len env loc = function
        fail loc "%s is not a compile-time integer constant, so it cannot be \
                  an array length" n)
 
+(* ── Generics: the four operations monomorphisation needs ───────────────
+   Naming a variable, binding one from an argument, substituting the binding
+   back in, and spelling the result as a symbol. Everything else about the
+   feature is where these are called from. *)
+
+(* The variables a signature introduces: every [$t] written in it, in the
+   order written, once each. Only a [defn] signature is scanned, which is what
+   makes the binding site a *place* and not merely a spelling. *)
+let signature_tyvars (fn : Ast.fn) =
+  let acc = ref [] in
+  let name loc n =
+    if n <> "" && n.[0] = '$' then begin
+      let bare = String.sub n 1 (String.length n - 1) in
+      if bare = "" then fail loc "$ on its own does not name a type variable";
+      (* [$i32] would shadow a machine type inside the body and read as one
+         everywhere else. There is no reason to want it. *)
+      if List.mem bare Types.primitive_names
+         || Types.ikind_of_name bare <> None
+         || Types.fkind_of_name bare <> None then
+        fail loc "%s is a type, so $%s cannot be a type variable" bare bare;
+      if not (List.mem bare !acc) then acc := bare :: !acc
+    end
+  in
+  let rec ty (t : Ast.texpr) =
+    match t.Ast.t with
+    | Ast.Tname n -> name t.Ast.tloc n
+    | Ast.Tslice e -> ty e
+    | Ast.Tarray (_, e) -> ty e
+    | Ast.Tmap (k, v) -> ty k; ty v
+    (* The head of an application is a constructor — [Ptr], [Option], [Vec] —
+       and a variable cannot stand there: this spike is generic over types,
+       not over type constructors. A [$t] inside the arguments is ordinary. *)
+    | Ast.Tapp (_, args) -> List.iter ty args
+    | Ast.Tfn (ps, r) -> List.iter ty ps; ty r
+  in
+  List.iter (fun (p : Ast.field) -> ty p.Ast.fty) fn.Ast.params;
+  (match fn.Ast.ret with Some r -> ty r | None -> ());
+  List.rev !acc
+
+(* Bind the variables in a parameter's written type from the type an argument
+   turned out to have. Odin's [is_polymorphic_type_assignable], structurally
+   and with the same rule: a variable already bound must match what it is
+   bound to, so [(pair 1 2.0)] over [a $t b $t] is a refusal and not a
+   second instantiation. *)
+let rec bind_ty subst (pat : Types.t) (arg : Types.t) =
+  match pat, arg with
+  | Types.Var v, a ->
+    (match List.assoc_opt v !subst with
+     | None -> subst := (v, a) :: !subst; true
+     | Some b -> Types.equal a b)
+  | Types.Slice p, Types.Slice a
+  | Types.Ptr p, Types.Ptr a
+  | Types.Vec p, Types.Vec a
+  | Types.Pool p, Types.Pool a
+  | Types.Handle p, Types.Handle a
+  | Types.Option p, Types.Option a -> bind_ty subst p a
+  | Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && bind_ty subst p a
+  | Types.Map (k, v), Types.Map (k', v') ->
+    bind_ty subst k k' && bind_ty subst v v'
+  | Types.Fn (ps, r), Types.Fn (ps', r') ->
+    List.length ps = List.length ps'
+    && List.for_all2 (bind_ty subst) ps ps' && bind_ty subst r r'
+  (* Nothing generic left on the pattern side: this is ordinary type
+     equality, and [Never] fits anywhere exactly as it does elsewhere. *)
+  | p, a -> Types.fits ~expected:p ~actual:a
+
+let rec subst_ty subst (t : Types.t) =
+  match t with
+  | Types.Var v -> (match List.assoc_opt v subst with Some c -> c | None -> t)
+  | Types.Slice e -> Types.Slice (subst_ty subst e)
+  | Types.Array (n, e) -> Types.Array (n, subst_ty subst e)
+  | Types.Map (k, v) -> Types.Map (subst_ty subst k, subst_ty subst v)
+  | Types.Ptr e -> Types.Ptr (subst_ty subst e)
+  | Types.Vec e -> Types.Vec (subst_ty subst e)
+  | Types.Pool e -> Types.Pool (subst_ty subst e)
+  | Types.Handle e -> Types.Handle (subst_ty subst e)
+  | Types.Option e -> Types.Option (subst_ty subst e)
+  | Types.Fn (ps, r) -> Types.Fn (List.map (subst_ty subst) ps, subst_ty subst r)
+  | t -> t
+
+(* Does this resolved type still mention a variable? *)
+let rec generic_ty (t : Types.t) =
+  match t with
+  | Types.Var _ -> true
+  | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+  | Types.Pool e | Types.Handle e | Types.Option e -> generic_ty e
+  | Types.Map (k, v) -> generic_ty k || generic_ty v
+  | Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty r
+  | _ -> false
+
+(* How a concrete type is spelled inside an instantiation's name. The prelude
+   already writes this by hand — [filter-i32], [sum-f32], [append-i64] — so a
+   generated name reads like the handwritten one it replaces, which is what a
+   backtrace, a [Reach] edge and a dev-build cell all end up showing.
+   [Types.to_string] cannot serve: [[i32]] and [(Vec i32)] are not symbols. *)
+let rec mangle_ty (t : Types.t) =
+  match t with
+  | Types.Unit -> "unit"
+  | Types.Slice e -> "slice-" ^ mangle_ty e
+  | Types.Array (n, e) -> Printf.sprintf "arr%Ld-%s" n (mangle_ty e)
+  | Types.Map (k, v) -> Printf.sprintf "map-%s-%s" (mangle_ty k) (mangle_ty v)
+  | Types.Ptr e -> "ptr-" ^ mangle_ty e
+  | Types.Vec e -> "vec-" ^ mangle_ty e
+  | Types.Pool e -> "pool-" ^ mangle_ty e
+  | Types.Handle e -> "handle-" ^ mangle_ty e
+  | Types.Option e -> "opt-" ^ mangle_ty e
+  | Types.Fn (ps, r) ->
+    Printf.sprintf "fn-%s-to-%s"
+      (String.concat "-" (List.map mangle_ty ps)) (mangle_ty r)
+  | t -> Types.to_string t
+
+(* [check_fn] is defined after the expression checker and an instantiation is
+   made from inside it, so the knot is tied here and closed at the bottom of
+   the file. One forward reference rather than moving a 90-line function. *)
+let check_fn_ref : (env -> Ast.fn -> Tast.fn) ref =
+  ref (fun _ _ -> assert false)
+
 (* ── Small helpers over the AST ────────────────────────────────────── *)
 
 (* Untyped literals: their machine type comes from context, so when one is an
@@ -4225,6 +4404,9 @@ and named_call ctx ~want loc name args =
     (match lookup ctx name with
      | Some b -> call_value ctx ~want loc (mk loc b.bty (Tast.Local b.slot)) args
      | None -> assert false)
+  | _ when Hashtbl.mem ctx.env.gsigs name ->
+    let vars, params, ret = Hashtbl.find ctx.env.gsigs name in
+    generic_call ctx ~want loc name vars params ret args
   | _ ->
     match Hashtbl.find_opt ctx.env.fns name with
     | Some (params, ret) ->
@@ -4257,6 +4439,97 @@ and named_call ctx ~want loc name args =
           (Printf.sprintf "the call %s into an imported package" name) 4
       else Loc.failk "check/unknown-function" loc "unknown function %s" name
 
+(* ── A call to a generic function ───────────────────────────────────────
+   The whole of instantiation, and it is at the call site because the call
+   site is the only place the concrete types exist. Odin does the same thing
+   in the same place: [check_expr.cpp]'s
+   [find_or_generate_polymorphic_procedure] runs from call checking, builds
+   the concrete proc type from the operands, scans the base entity's
+   [gen_procs] for an [are_types_identical] match, and generates a new
+   [Entity] only on a miss. *)
+and generic_call ctx ~want loc name vars pats pret args =
+  if List.length args <> List.length pats then
+    fail loc "%s takes %d argument%s, given %d" name (List.length pats)
+      (if List.length pats = 1 then "" else "s") (List.length args);
+  (* Arguments first, and with no expectation where the parameter's type still
+     mentions a variable — there is nothing to expect until the argument has
+     said what it is. So an untyped literal falls to its own default and
+     [(id 3)] instantiates at i32, which is the one place inference at a
+     generic call site is weaker than at a monomorphic one. *)
+  let targs =
+    map2_lr
+      (fun p a -> if generic_ty p then check ctx a else check ctx ~want:p a)
+      pats args
+  in
+  let subst = ref [] in
+  List.iter2
+    (fun p (a : Tast.expr) ->
+       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))
+    pats targs;
+  (* Every variable has to be determined by an argument. A return-only
+     variable has nothing to bind it — there is no explicit instantiation
+     syntax by design (plan.org) — so it is refused here, where the signature
+     can be named, rather than producing a copy with a hole in it. *)
+  List.iter
+    (fun v ->
+       if not (List.mem_assoc v !subst) then
+         fail loc
+           "%s's type variable $%s is not determined by any argument — a \
+            generic function is instantiated from its call site, and there is \
+            no syntax for naming the type" name v)
+    vars;
+  let cparams = List.map (subst_ty !subst) pats in
+  let cret = subst_ty !subst pret in
+  let sym = instantiate ctx.env loc name vars !subst cparams cret in
+  expect loc ~want (mk loc cret (Tast.Call (sym, targs)))
+
+(* Cache or generate, Odin's loop. The key is the whole concrete signature
+   compared pairwise with [Types.equal] — [are_types_identical] — so calling
+   at the same type twice makes one copy. *)
+and instantiate env loc gname vars subst cparams cret =
+  let cache =
+    match Hashtbl.find_opt env.insts gname with
+    | Some r -> r
+    | None -> let r = ref [] in Hashtbl.replace env.insts gname r; r
+  in
+  let same (ps, r, _) =
+    List.length ps = List.length cparams
+    && List.for_all2 Types.equal ps cparams && Types.equal r cret
+  in
+  match List.find_opt same !cache with
+  | Some (_, _, sym) -> sym
+  | None ->
+    let sym =
+      gname ^ "-"
+      ^ String.concat "-" (List.map (fun v -> mangle_ty (List.assoc v subst)) vars)
+    in
+    if Hashtbl.mem env.fns sym then
+      fail loc
+        "%s at these types is called %s, and %s is already defined — rename \
+         one of them" gname sym sym;
+    (* The entry goes in *before* the body is checked, which is what makes a
+       recursive generic function terminate: the call to itself at the same
+       types finds this and does not generate a second copy. *)
+    cache := (cparams, cret, sym) :: !cache;
+    Hashtbl.replace env.fns sym (cparams, cret);
+    let fn = Hashtbl.find env.generics gname in
+    let saved_subst = env.subst and saved_vars = env.tyvars in
+    (* Inside the copy there are no variables left: [resolve_name] answers
+       [t] with the concrete type, so every node the body produces is as
+       concrete as one written out by hand. *)
+    env.subst <- List.map (fun v -> (v, List.assoc v subst)) vars;
+    env.tyvars <- [];
+    let restore () = env.subst <- saved_subst; env.tyvars <- saved_vars in
+    let tfn =
+      match !check_fn_ref env { fn with Ast.name = sym } with
+      | tfn -> restore (); tfn
+      | exception e -> restore (); raise e
+    in
+    env.instances <- tfn :: env.instances;
+    sym
+
 and is_cast name =
   Types.ikind_of_name name <> None || Types.fkind_of_name name <> None
 
@@ -4524,13 +4797,24 @@ let collect env (decls : Ast.decl list) =
               Hashtbl.replace env.cases c.Tast.vname (n, c))
            cases
        | Ast.Defn fn ->
+         (* A signature that introduces a type variable is a *pattern*, not a
+            signature: it goes in [gsigs] and the function goes nowhere near
+            [fns], because nothing can be called at [t]. Every call site turns
+            it into an ordinary entry. *)
+         let vars = signature_tyvars fn in
+         env.tyvars <- vars;
          let params =
            List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
          in
          let ret =
            match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t
          in
-         Hashtbl.replace env.fns fn.Ast.name (params, ret)
+         env.tyvars <- [];
+         if vars = [] then Hashtbl.replace env.fns fn.Ast.name (params, ret)
+         else begin
+           Hashtbl.replace env.generics fn.Ast.name fn;
+           Hashtbl.replace env.gsigs fn.Ast.name (vars, params, ret)
+         end
        | Ast.Defvar (n, t, _) ->
          let ty = match t with
            | Some t -> resolve env t
@@ -4597,7 +4881,7 @@ let check_finite env =
 
 (* ── Declarations: pass 2, check bodies ────────────────────────────── *)
 
-let check_fn env (fn : Ast.fn) : Tast.fn =
+let rec check_fn env (fn : Ast.fn) : Tast.fn =
   let params, ret = Hashtbl.find env.fns fn.Ast.name in
   let ctx = { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
                 outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false;
@@ -4684,6 +4968,35 @@ let check_fn env (fn : Ast.fn) : Tast.fn =
        normal path has them spliced into [body] above. *)
     ret; body; fdefers = ctx.defers; fparent = None; floc = fn.Ast.nloc }
 
+(* The generic body, checked once with its variables abstract. Nothing is kept
+   — the [Tast.fn] it produces is thrown away, and so is anything it lifted —
+   because a generic function has no code: only its instantiations do. What is
+   kept is the *refusal*: an operator an unconstrained variable does not
+   support fails here, at the definition, naming the variable, rather than at
+   whichever call site happened to instantiate it at a type that worked.
+
+   The holes in it are real and are the report's business: [println] is
+   plan.org's one compiler-provided exception and this pass rejects it, and
+   move-only-ness is not decidable abstractly at all — [Types.is_move_only
+   (Var _)] is false, but the same variable at [(Vec i32)] is move-only. *)
+and check_generic env (fn : Ast.fn) =
+  let vars, params, ret = Hashtbl.find env.gsigs fn.Ast.name in
+  let saved_lifted = env.lifted and saved_vars = env.tyvars in
+  env.tyvars <- vars;
+  Hashtbl.replace env.fns fn.Ast.name (params, ret);
+  let finish () =
+    Hashtbl.remove env.fns fn.Ast.name;
+    env.lifted <- saved_lifted;
+    env.tyvars <- saved_vars
+  in
+  (match check_fn env fn with
+   | _ -> finish ()
+   | exception e -> finish (); raise e)
+
+(* The knot from [instantiate]: a call site makes a copy, and making one is
+   checking a function. *)
+let () = check_fn_ref := check_fn
+
 (* A global of move-only type is refused. The dead set is per function, so two
    functions each freeing the same global is a double free nothing here could
    see; and within one function a global read does not go through [var]'s move
@@ -4809,6 +5122,22 @@ let build_program ~keep_going (decls : Ast.decl list) : Tast.program * env =
   check_finite env;
   let s = Loc.sink ~on:keep_going in
   ignore (Loc.caught s (fun () -> check_main env));
+  (* Every generic body, checked once with its variables left abstract, and
+     the result thrown away. This is the pass plan.org's rule needs and Odin
+     has no equivalent of: Odin checks a polymorphic body only per
+     instantiation, so [a + b] over a [$T] compiles there and fails only if
+     nobody ever calls it at a numeric type. plan.org says the opposite — an
+     unconstrained variable supports only what every type supports, and [=],
+     [<], [+] and [hash] over one are *rejected, not silently instantiated*.
+     Rejecting them means type-checking the body with nothing substituted,
+     which is this, and it is a second pass over the same source. *)
+  List.iter
+    (fun (d : Ast.decl) ->
+       match d.Ast.d with
+       | Ast.Defn fn when Hashtbl.mem env.gsigs fn.Ast.name ->
+         ignore (Loc.caught s (fun () -> check_generic env fn))
+       | _ -> ())
+    decls;
   let globals =
     List.filter_map
       (fun d -> Option.join (Loc.caught s (fun () -> check_global env d)))
@@ -4818,6 +5147,9 @@ let build_program ~keep_going (decls : Ast.decl list) : Tast.program * env =
     List.filter_map
       (fun (d : Ast.decl) ->
          match d.Ast.d with
+         (* A generic [defn] does not reach the typed IR at all. Only its
+            instantiations do, and they are collected below. *)
+         | Ast.Defn fn when Hashtbl.mem env.gsigs fn.Ast.name -> None
          | Ast.Defn fn -> Loc.caught s (fun () -> check_fn env fn)
          | _ -> None)
       decls
@@ -4827,6 +5159,11 @@ let build_program ~keep_going (decls : Ast.decl list) : Tast.program * env =
      from here down; nothing in the backend knows they were written inside
      something else. *)
   let fns = fns @ List.rev env.lifted in
+  (* The copies generics turned into, in the order they were generated. Like a
+     lifted clause they are ordinary functions from here down — but unlike one
+     they are reached *by name* from arbitrary call sites, so they carry no
+     [fparent] and a dev build gives each its own cell. *)
+  let fns = fns @ List.rev env.instances in
   (* Sorted, so the emitted IR is reproducible build to build: a Hashtbl's
      fold order is not. *)
   let values name tbl =
diff --git a/spike/generics/id.flan b/spike/generics/id.flan
new file mode 100644
index 0000000..4e02968
--- /dev/null
+++ b/spike/generics/id.flan
@@ -0,0 +1,7 @@
+(defn id [x $t] t x)
+
+(defn main [] ()
+  (println (id 3))
+  (println (id 4.5))
+  (println (id 7))
+  (println (id true)))

From 50798aac8982f5b85af289b1464fa8830c3595b7 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 13:20:12 +0700
Subject: [PATCH 02/11] A generic sort takes its comparison as a value, and an
 operator over a variable is refused

---
 lib/check.ml               | 57 ++++++++++++++++++++++++++++++--------
 spike/generics/reject.flan |  4 +++
 spike/generics/sort.flan   | 25 +++++++++++++++++
 spike/generics/swap.flan   | 19 +++++++++++++
 4 files changed, 94 insertions(+), 11 deletions(-)
 create mode 100644 spike/generics/reject.flan
 create mode 100644 spike/generics/sort.flan
 create mode 100644 spike/generics/swap.flan

diff --git a/lib/check.ml b/lib/check.ml
index ff22475..2842d2a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -722,6 +722,22 @@ let rec generic_ty (t : Types.t) =
   | Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty 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
+   rejected rather than silently instantiated at whatever type the first call
+   site happened to use. The way out is the one plan.org names — pass the
+   operation in as a function value, which is what [sort-i32-by!] already
+   does with [(Fn [i32 i32] bool)]. *)
+let unconstrained loc op (t : Types.t) =
+  if generic_ty t then
+    Loc.failk "check/unconstrained-type-variable" loc
+      "%s over the type variable %s is refused: an unconstrained type \
+       variable supports only what every type supports, and %s is not that \
+       (plan.org, Types). Take the operation as a parameter — a (Fn [%s %s] \
+       ...) — and call it here"
+      op (Types.to_string t) op (Types.to_string t) (Types.to_string t)
+
 (* How a concrete type is spelled inside an instantiation's name. The prelude
    already writes this by hand — [filter-i32], [sum-f32], [append-i64] — so a
    generated name reads like the handwritten one it replaces, which is what a
@@ -2691,6 +2707,7 @@ and fold_left_prim ctx ~want loc name p ok what args =
     match args with x :: y :: rest -> x, y, rest | _ -> assert false
   in
   let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
+  unconstrained loc name a.Tast.ty;
   if not (ok a.Tast.ty) then
     fail loc "%s takes %s, found %s" name what (Types.to_string a.Tast.ty);
   let ty = a.Tast.ty in
@@ -3011,6 +3028,7 @@ and named_call ctx ~want loc name args =
   | "%" ->
     arity loc name 2 args;
     let a, b = binary ctx name loc ~want:(numeric_want want) args in
+    unconstrained loc name a.Tast.ty;
     if not (Types.is_numeric a.Tast.ty) then
       fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
     prim Tast.Rem a.Tast.ty [ a; b ]
@@ -3030,6 +3048,7 @@ and named_call ctx ~want loc name args =
       | "=" | "!=" -> Types.is_equatable a.Tast.ty
       | _ -> Types.is_comparable a.Tast.ty
     in
+    unconstrained loc name a.Tast.ty;
     if not ok then
       fail loc
         "%s compares machine numbers; %s has no built-in comparison \
@@ -4455,19 +4474,26 @@ and generic_call ctx ~want loc name vars pats pret args =
      mentions a variable — there is nothing to expect until the argument has
      said what it is. So an untyped literal falls to its own default and
      [(id 3)] instantiates at i32, which is the one place inference at a
-     generic call site is weaker than at a monomorphic one. *)
+     generic call site is weaker than at a monomorphic one.
+
+     A variable already bound by an earlier argument is substituted back into
+     the parameters still to come, so [(sort-by! (slice ns 0 4) (fn [a b] (< a
+     b)))] works: by the time the [fn] is reached, [(Fn [$t $t] bool)] has
+     become [(Fn [i32 i32] bool)] and the literal has the position it needs to
+     take its types from. Left to right, which is the order Odin's operands
+     are gathered in and the order [map2_lr] already guarantees. *)
+  let subst = ref [] in
   let targs =
     map2_lr
-      (fun p a -> if generic_ty p then check ctx a else check ctx ~want:p a)
+      (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
+         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);
+         a)
       pats args
   in
-  let subst = ref [] in
-  List.iter2
-    (fun p (a : Tast.expr) ->
-       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))
-    pats targs;
   (* Every variable has to be determined by an argument. A return-only
      variable has nothing to bind it — there is no explicit instantiation
      syntax by design (plan.org) — so it is refused here, where the signature
@@ -4482,8 +4508,17 @@ and generic_call ctx ~want loc name vars pats pret args =
     vars;
   let cparams = List.map (subst_ty !subst) pats in
   let cret = subst_ty !subst pret in
-  let sym = instantiate ctx.env loc name vars !subst cparams cret in
-  expect loc ~want (mk loc cret (Tast.Call (sym, targs)))
+  if List.exists generic_ty cparams || generic_ty cret then
+    (* One generic function calling another at its *own* variable, seen from
+       the abstract pass over the caller's body — [sort-by!] calling [swap!]
+       at [t]. There is no copy to make yet: [t] is not a type. The node is
+       built so the call still type-checks and is thrown away with the rest of
+       the abstract pass; the real copy is generated when the caller is
+       instantiated and the same call site resolves [t] to a concrete type. *)
+    expect loc ~want (mk loc cret (Tast.Call (name, targs)))
+  else
+    let sym = instantiate ctx.env loc name vars !subst cparams cret in
+    expect loc ~want (mk loc cret (Tast.Call (sym, targs)))
 
 (* Cache or generate, Odin's loop. The key is the whole concrete signature
    compared pairwise with [Types.equal] — [are_types_identical] — so calling
diff --git a/spike/generics/reject.flan b/spike/generics/reject.flan
new file mode 100644
index 0000000..8aeb7f9
--- /dev/null
+++ b/spike/generics/reject.flan
@@ -0,0 +1,4 @@
+(defn add2 [a $t b $t] t (+ a b))
+
+(defn main [] ()
+  (println (add2 1 2)))
diff --git a/spike/generics/sort.flan b/spike/generics/sort.flan
new file mode 100644
index 0000000..444e852
--- /dev/null
+++ b/spike/generics/sort.flan
@@ -0,0 +1,25 @@
+;; The shape prelude.ml's sort-i32-by! / sort-f32-by! pair would collapse into:
+;; one generic body, the comparison passed in as a function value because an
+;; unconstrained type variable has no < of its own.
+
+(defn swap! [xs [$t] i i32 j i32] ()
+  (let [tmp (at xs i)]
+    (set (at xs i) (at xs j))
+    (set (at xs j) tmp)))
+
+(defn sort-by! [s [$t] before? (Fn [$t $t] bool)] ()
+  (let [i 1]
+    (while (< i (len s))
+      (let [j i]
+        (while (and (> j 0) (before? (at s j) (at s (- j 1))))
+          (swap! s (- j 1) j)
+          (set j (- j 1))))
+      (set i (+ i 1)))))
+
+(defn main [] ()
+  (let [ns [5 3 9 1]
+        fs [2.5 0.5 1.5]]
+    (sort-by! (slice ns 0 4) (fn [a b] (< a b)))
+    (sort-by! (slice fs 0 3) (fn [a b] (> a b)))
+    (dotimes [i 4] (println (at ns i)))
+    (dotimes [i 3] (println (at fs i)))))
diff --git a/spike/generics/swap.flan b/spike/generics/swap.flan
new file mode 100644
index 0000000..8d69ae4
--- /dev/null
+++ b/spike/generics/swap.flan
@@ -0,0 +1,19 @@
+;; One generic function over one type variable, called at two concrete types
+;; in one program. The sigil binds ($t), a bare use reads it (t).
+
+(defn swap! [xs [$t] i i32 j i32] ()
+  (let [tmp (at xs i)]
+    (set (at xs i) (at xs j))
+    (set (at xs j) tmp)))
+
+(defn main [] ()
+  (let [ns [10 20 30]
+        fs [1.5 2.5 3.5]]
+    (swap! (slice ns 0 3) 0 2)
+    (swap! (slice fs 0 3) 0 1)
+    (swap! (slice ns 0 3) 1 2)
+    (println (at ns 0))
+    (println (at ns 1))
+    (println (at ns 2))
+    (println (at fs 0))
+    (println (at fs 1))))

From 074991342009a19ae43e5c430c0deb35aa0fd27b Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 13:24:45 +0700
Subject: [PATCH 03/11] A generic filter allocates its Vec, and the sweep says
 what a rebuild costs

---
 lib/check.ml                       |   9 +-
 spike/generics/measure.ml          | 171 +++++++++++++++++++++++++++++
 spike/generics/prelude-shapes.flan |  51 +++++++++
 spike/generics/run.sh              |  28 +++++
 4 files changed, 258 insertions(+), 1 deletion(-)
 create mode 100644 spike/generics/measure.ml
 create mode 100644 spike/generics/prelude-shapes.flan
 create mode 100644 spike/generics/run.sh

diff --git a/lib/check.ml b/lib/check.ml
index 2842d2a..a15b3ae 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2884,7 +2884,14 @@ and file_guard ctx loc ~path_slot ~op mk_steps =
    both callers, so the next kind of type added cannot be added to one of
    them. *)
 and type_named ctx n =
-  List.mem n Types.primitive_names
+  (* A type variable names a type here too, which is what lets [(vec-new t)]
+     be written in a generic body: inside an instantiation [resolve_name]
+     answers with the concrete element type, and during the abstract pass it
+     answers [Var t] and the [Vec] that comes back is a [(Vec t)] — generic,
+     and refused by anything that needs a size. *)
+  List.mem n ctx.env.tyvars
+  || List.mem_assoc n ctx.env.subst
+  || List.mem n Types.primitive_names
   || Hashtbl.mem ctx.env.structs n
   || Hashtbl.mem ctx.env.unions n
   || Hashtbl.mem ctx.env.enums n
diff --git a/spike/generics/measure.ml b/spike/generics/measure.ml
new file mode 100644
index 0000000..229c395
--- /dev/null
+++ b/spike/generics/measure.ml
@@ -0,0 +1,171 @@
+(* What redefining a generic function costs the dev loop, measured.
+
+   The question the spike exists to answer: C-c C-c on a concrete function is
+   about 35 ms today, and a generic function that is redefined has to rebuild
+   *every* instantiation. So the sweep is one generic called at N concrete
+   types, N = 1..8, against the handwritten N-copies program it replaces, and
+   the three things a C-c C-c actually pays for are timed separately:
+
+     check   Check.program_with_env over the whole accumulated program —
+             which is what Session.eval does on every evaluation, so this is
+             paid whether the redefined function is generic or not.
+     emit    Emit.redefinition for the fns being installed.
+     build   llc + ld -shared, from Build.shared — the dominant term.
+
+   Nothing here modifies the session or the dev loop; it drives the real ones. *)
+
+let tys = [| "i8"; "i16"; "i32"; "i64"; "u8"; "u16"; "u32"; "f32" |]
+
+let time f =
+  let t0 = Unix.gettimeofday () in
+  let x = f () in
+  (x, (Unix.gettimeofday () -. t0) *. 1000.)
+
+(* Best of k, because llc and the linker are processes and the machine is
+   noisy; a median would hide a systematic cost and a mean would report the
+   scheduler. *)
+let best k f =
+  let rec go i acc = if i = 0 then acc else
+      let _, ms = time f in go (i - 1) (min acc ms) in
+  go k infinity
+
+let generic_src n =
+  let b = Buffer.create 1024 in
+  Buffer.add_string b
+    "(defn gswap [xs [$t] i i32 j i32] ()\n\
+    \  (let [tmp (at xs i)]\n\
+    \    (set (at xs i) (at xs j))\n\
+    \    (set (at xs j) tmp)))\n\n\
+     (defn gsort [s [$t] before? (Fn [$t $t] bool)] ()\n\
+    \  (let [i 1]\n\
+    \    (while (< i (len s))\n\
+    \      (let [j i]\n\
+    \        (while (and (> j 0) (before? (at s j) (at s (- j 1))))\n\
+    \          (gswap s (- j 1) j)\n\
+    \          (set j (- j 1))))\n\
+    \      (set i (+ i 1)))))\n\n";
+  for i = 0 to n - 1 do
+    Buffer.add_string b (Printf.sprintf "(defvar xs-%s [8 %s])\n" tys.(i) tys.(i))
+  done;
+  Buffer.add_string b "\n(defn main [] ()\n";
+  for i = 0 to n - 1 do
+    Buffer.add_string b
+      (Printf.sprintf "  (gsort (slice xs-%s 0 8) (fn [a b] (< a b)))\n" tys.(i))
+  done;
+  Buffer.add_string b "  )\n";
+  Buffer.contents b
+
+(* The same program as it is written today: one copy of each function per
+   element type, by hand. This is prelude.ml's shape. *)
+let mono_src n =
+  let b = Buffer.create 1024 in
+  for i = 0 to n - 1 do
+    let t = tys.(i) in
+    Buffer.add_string b
+      (Printf.sprintf
+         "(defn mswap-%s [xs [%s] i i32 j i32] ()\n\
+         \  (let [tmp (at xs i)]\n\
+         \    (set (at xs i) (at xs j))\n\
+         \    (set (at xs j) tmp)))\n\n\
+          (defn msort-%s [s [%s] before? (Fn [%s %s] bool)] ()\n\
+         \  (let [i 1]\n\
+         \    (while (< i (len s))\n\
+         \      (let [j i]\n\
+         \        (while (and (> j 0) (before? (at s j) (at s (- j 1))))\n\
+         \          (mswap-%s s (- j 1) j)\n\
+         \          (set j (- j 1))))\n\
+         \      (set i (+ i 1)))))\n\n"
+         t t t t t t t);
+    Buffer.add_string b (Printf.sprintf "(defvar xs-%s [8 %s])\n\n" t t)
+  done;
+  Buffer.add_string b "(defn main [] ()\n";
+  for i = 0 to n - 1 do
+    Buffer.add_string b
+      (Printf.sprintf "  (msort-%s (slice xs-%s 0 8) (fn [a b] (< a b)))\n"
+         tys.(i) tys.(i))
+  done;
+  Buffer.add_string b "  )\n";
+  Buffer.contents b
+
+let write path s =
+  let oc = open_out path in output_string oc s; close_out oc
+
+let dir =
+  let d = Filename.concat (Filename.get_temp_dir_name ()) "flan-generics-spike" in
+  (try Unix.mkdir d 0o700 with Unix.Unix_error (Unix.EEXIST, _, _) -> ());
+  d
+
+let decls_of path =
+  (Flan.Load.program ~file:path
+     (Flan.Parse.program (Flan.Reader.read_file path))).Flan.Load.decls
+
+(* Every function the program ended up with whose name starts with one of the
+   generic names — the instantiations, which is exactly what a redefinition of
+   the generic would have to rebuild. *)
+let instantiations (p : Flan.Tast.program) =
+  List.filter_map
+    (fun (f : Flan.Tast.fn) ->
+       let n = f.Flan.Tast.name in
+       if String.length n > 6 && String.sub n 0 6 = "gswap-" then Some n
+       else if String.length n > 6 && String.sub n 0 6 = "gsort-" then Some n
+       else None)
+    p.Flan.Tast.fns
+
+let build_ms ir =
+  let out = Filename.concat dir "redef.so" in
+  best 3 (fun () ->
+    ignore
+      (Flan.Build.shared
+         ~opts:{ Flan.Build.default with dev = true } ~ir ~out ()))
+
+let () =
+  Printf.printf
+    "n   check-gen  check-mono   emit-1  emit-N   build-1  build-N   fns\n";
+  (try
+  for n = 1 to 8 do
+    let gpath = Filename.concat dir (Printf.sprintf "gen%d.flan" n) in
+    let mpath = Filename.concat dir (Printf.sprintf "mono%d.flan" n) in
+    write gpath (generic_src n);
+    write mpath (mono_src n);
+    let gd = decls_of gpath and md = decls_of mpath in
+    let check_gen = best 3 (fun () -> ignore (Flan.Check.program_with_env gd)) in
+    let check_mono = best 3 (fun () -> ignore (Flan.Check.program_with_env md)) in
+    let p, _ = Flan.Check.program_with_env gd in
+    let insts = instantiations p in
+    let one = [ List.hd insts ] in
+    let ir_one =
+      Flan.Emit.redefinition ~dev:true ~known:(fun _ -> true) p ~fns:one
+    in
+    let ir_all =
+      Flan.Emit.redefinition ~dev:true ~known:(fun _ -> true) p ~fns:insts
+    in
+    let emit1 =
+      best 3 (fun () ->
+        ignore (Flan.Emit.redefinition ~dev:true ~known:(fun _ -> true) p ~fns:one))
+    and emitn =
+      best 3 (fun () ->
+        ignore (Flan.Emit.redefinition ~dev:true ~known:(fun _ -> true) p ~fns:insts))
+    in
+    let b1 = build_ms ir_one and bn = build_ms ir_all in
+    Printf.printf "%d   %8.1f  %10.1f  %7.1f %7.1f  %8.1f %8.1f   %d\n%!"
+      n check_gen check_mono emit1 emitn b1 bn (List.length insts)
+  done
+   with Flan.Loc.Error d -> prerr_endline (Flan.Loc.report d); exit 1);
+  (* And what the session actually does when the generic itself is redefined.
+     This is the real C-c C-c path — Session.eval on the form the editor sent
+     — and what it reports is the finding, not the timing. *)
+  let gpath = Filename.concat dir "gen4.flan" in
+  let t, _ = Flan.Session.create ~file:gpath () in
+  let form =
+    "(defn gswap [xs [$t] i i32 j i32] ()\n\
+    \  (let [tmp (at xs i)]\n\
+    \    (set (at xs i) (at xs j))\n\
+    \    (set (at xs j) tmp)))\n"
+  in
+  let c, ms = time (fun () -> Flan.Session.eval ~origin:gpath t form) in
+  Printf.printf
+    "\nSession.eval on the generic gswap itself: %.1f ms, installs=%b, \
+     fns=[%s], names=[%s]\n"
+    ms c.Flan.Session.installs
+    (String.concat " " c.Flan.Session.fns)
+    (String.concat " " c.Flan.Session.names)
diff --git a/spike/generics/prelude-shapes.flan b/spike/generics/prelude-shapes.flan
new file mode 100644
index 0000000..b17b777
--- /dev/null
+++ b/spike/generics/prelude-shapes.flan
@@ -0,0 +1,51 @@
+;; Which of prelude.ml's per-type families collapse as they are written, and
+;; which need their signature changed. Nothing here is installed in the
+;; prelude; it is the same bodies, over $t, checked and run.
+
+(defn keep [s [$t] keep? (Fn [$t] bool)] (Vec $t)
+  (let [v (vec-new t)]
+    (dotimes [i (len s)]
+      (when (keep? (at s i))
+        (push v (at s i))))
+    v))
+
+(defn apply! [s [$t] f (Fn [$t] $t)] ()
+  (dotimes [i (len s)]
+    (set (at s i) (f (at s i)))))
+
+(defn fold [s [$t] init $t f (Fn [$t $t] $t)] t
+  (let [acc init]
+    (dotimes [i (len s)]
+      (set acc (f acc (at s i))))
+    acc))
+
+(defn flip! [s [$t]] ()
+  (let [i 0
+        j (- (len s) 1)]
+    (while (< i j)
+      (let [tmp (at s i)]
+        (set (at s i) (at s j))
+        (set (at s j) tmp))
+      (set i (+ i 1))
+      (set j (- j 1)))))
+
+(defvar ns [5 i32])
+(defvar fs [5 f32])
+
+(defn main [] ()
+  (let [xs (slice ns 0 5)
+        ys (slice fs 0 5)]
+    (dotimes [i 5]
+      (set (at xs i) (+ i 1))
+      (set (at ys i) (f32 (* 2 (+ i 1)))))
+    (apply! xs (fn [x] (* x 10)))
+    (apply! ys (fn [x] (* x (f32 2))))
+    (flip! xs)
+    (flip! ys)
+    (println (fold xs 0 (fn [a b] (+ a b))))
+    (println (fold ys (f32 0) (fn [a b] (+ a b))))
+    (let [evens (keep xs (fn [x] (= (% x 20) 0)))]
+      (println (len evens))
+      (free evens))
+    (println (at xs 0))
+    (println (at ys 0))))
diff --git a/spike/generics/run.sh b/spike/generics/run.sh
new file mode 100644
index 0000000..7771e36
--- /dev/null
+++ b/spike/generics/run.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+# The generics spike's measurement, driven by hand with ocamlfind against the
+# flan.cmxa dune already builds — the same arrangement spike/backend uses, and
+# for the same reason: nothing under spike/ is wired into the build, there is
+# no dune file here, and `dune test --root .` cannot see any of it.
+#
+# The three .flan programs beside this file are run with the ordinary driver:
+#   dune exec --root . bin/main.exe -- run spike/generics/sort.flan
+set -u
+here=$(cd "$(dirname "$0")" && pwd)
+root=$(cd "$here/../.." && pwd)
+cd "$root" || exit 1
+
+dune build --root . lib/flan.cmxa 2>&1 | head -20
+
+out=$(mktemp -d); trap 'rm -rf "$out"' EXIT
+
+ocamlfind ocamlopt -thread -package unix,threads.posix -linkpkg \
+  -I "$root/_build/default/lib/.flan.objs/byte" \
+  -I "$root/_build/default/lib/.flan.objs/native" \
+  -I "$out" -I "$here" \
+  -o "$out/measure" \
+  "$root/_build/default/lib/flan.cmxa" \
+  -cclib -rdynamic -ccopt -L"$root/_build/default/lib" \
+  "$here/measure.ml" 2>&1 | head -40
+
+test -x "$out/measure" || { echo "build failed"; exit 1; }
+"$out/measure"

From 75c630ada9937e92ad79ac35e5f24096fa8b8b79 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 13:29:21 +0700
Subject: [PATCH 04/11] The generics spike, answered

---
 SPIKE-GENERICS.md            | 322 +++++++++++++++++++++++++++++++++++
 spike/generics/two-vars.flan |   5 +
 2 files changed, 327 insertions(+)
 create mode 100644 SPIKE-GENERICS.md
 create mode 100644 spike/generics/two-vars.flan

diff --git a/SPIKE-GENERICS.md b/SPIKE-GENERICS.md
new file mode 100644
index 0000000..9b10b37
--- /dev/null
+++ b/SPIKE-GENERICS.md
@@ -0,0 +1,322 @@
+# The generics spike, answered: it runs, and the bill lands on the dev loop rather than on the checker
+
+Milestone 5's parametric polymorphism, run early and deliberately out of order, as a spike rather than as a
+decision. **Feasible, and smaller than expected.** A generic function written in Flan goes through the ordinary
+frontend, is instantiated at each concrete type its call sites ask for, is emitted as real functions and runs,
+answering correctly at every one of them. The whole of it is `lib/check.ml`; `lib/types.ml`, `lib/tast.ml`,
+`lib/emit.ml` and every backend are untouched, and `dune test --root .` is green (203 checks, 0 failures) either
+side of it.
+
+The demonstrations are `spike/generics/*.flan` and are run with the ordinary driver —
+`dune exec --root . bin/main.exe -- run spike/generics/sort.flan`. The measurement is `spike/generics/measure.ml`,
+driven by `bash spike/generics/run.sh` with ocamlfind against the `flan.cmxa` dune already builds, exactly as
+`spike/backend` is and for the same reason: nothing under `spike/` is wired into the build.
+
+**The headline is not that it works.** It is that the two costs everyone expects to be the problem — checking and
+instantiating — are under the noise floor, and the cost that is real is one nobody named: `C-c C-c` on a generic
+function today **silently installs nothing**, and making it install something multiplies the part of the dev loop
+that was already the slowest. Measured below.
+
+## The sigil, since it changed under the spike
+
+plan.org says lowercase is a type variable and there is no sigil. That was revised while this was being built, and
+this is built against the revision: **`$t` at the binding site, bare `t` at every use**, which is Odin's spelling
+(`$T` in the signature, `T` in the body).
+
+```lisp
+(defn swap! [xs [$t] i i32 j i32] () ...)   ; $t binds
+(defn fold [s [$t] init $t f (Fn [$t $t] $t)] t ...)   ; later $t are the same variable; t reads it
+```
+
+Both spellings are accepted at a use — `resolve_name` strips the sigil before it looks anything up — because that
+is one `String.sub` and refusing the sigil at a use would be a second rule to explain. The binding rule is the one
+that is enforced: **only a `defn` signature introduces a variable**, and `$t` anywhere else (a struct field, a
+global, a `let` annotation) is a refusal that says so.
+
+The decision costs one function and one `match` arm, both in `check.ml`. The reader already treats `$` as an
+ordinary symbol character, so `$t` arrives as `Ast.Tname "$t"` with no change to `reader.ml`, `parse.ml` or
+`ast.ml`, and changing the sigil to anything else is changing one character in `resolve_name` and one in
+`signature_tyvars`. Nothing else in the compiler knows the character means anything.
+
+The revision's reasoning holds up in the code. `signature_tyvars` scans for the sigil and puts the bare names in
+`env.tyvars`; `resolve_name` consults that list and nothing else. So an unknown lowercase type name is still the
+unknown-type error it always was, and the old rule's failure mode — a mistyped type name silently becoming a type
+parameter, making the function *more* permissive than it was written to be — cannot happen. The near-miss guard at
+`check.ml:553` stays where it is and keeps `f65` a typo.
+
+## Question 1 — does it work end to end
+
+Yes, at four shapes, all of them run and checked against their output.
+
+**One variable, one function, two types** (`spike/generics/id.flan`):
+
+```lisp
+(defn id [x $t] t x)
+(defn main [] ()
+  (println (id 3))  (println (id 4.5))  (println (id 7))  (println (id true)))
+```
+
+prints `3 / 4.5 / 7 / true`, and emits exactly three bodies — `flan.id-i32`, `flan.id-f64`, `flan.id-bool`. Four
+calls, three copies: `(id 3)` and `(id 7)` share one, which is the instantiation cache doing its job.
+
+**Through a slice, mutating in place** (`spike/generics/swap.flan`): `(defn swap! [xs [$t] i i32 j i32] () ...)`
+called at `[i32]` and `[f64]`, correct both times. The variable is bound *inside* a type constructor here, which
+is the `is_polymorphic_type_assignable` walk rather than a name match.
+
+**The one that matters — a generic calling a generic, with the operator passed in** (`spike/generics/sort.flan`):
+
+```lisp
+(defn swap! [xs [$t] i i32 j i32] () ...)
+
+(defn sort-by! [s [$t] before? (Fn [$t $t] bool)] ()
+  (let [i 1]
+    (while (< i (len s))
+      (let [j i]
+        (while (and (> j 0) (before? (at s j) (at s (- j 1))))
+          (swap! s (- j 1) j)
+          (set j (- j 1))))
+      (set i (+ i 1)))))
+
+(defn main [] ()
+  (let [ns [5 3 9 1]  fs [2.5 0.5 1.5]]
+    (sort-by! (slice ns 0 4) (fn [a b] (< a b)))
+    (sort-by! (slice fs 0 3) (fn [a b] (> a b)))
+    ...))
+```
+
+prints `1 3 5 9` then `2.5 1.5 0.5`, and emits four bodies: `sort-by!-i32`, `sort-by!-f64`, `swap!-i32`,
+`swap!-f64`. This is prelude.ml's `sort-i32-by!`/`sort-f32-by!` pair, collapsed, running. Note what had to work
+for it: `sort-by!` calls `swap!` at its *own* variable `t`, so the copy of `swap!` is generated when `sort-by!`
+is instantiated and not before — instantiation is transitive.
+
+It also forced the one piece of real inference in the spike. Arguments are checked left to right and **each
+binding is substituted back into the parameters still to come**, so by the time `(fn [a b] (< a b))` is reached,
+`(Fn [$t $t] bool)` has already become `(Fn [i32 i32] bool)` and the literal has the position it needs to take
+its types from. Without that the `fn` literal has no types and the call does not check. This is the same
+left-to-right operand order Odin gathers its operands in.
+
+**Two variables** (`spike/generics/two-vars.flan`) was out of scope and fell out for free: `(defn fst [a $t b $u]
+t a)` at three combinations works, because the substitution is a list and was never written as a single binding.
+
+**The refusal.** `(defn add2 [a $t b $t] t (+ a b))` is rejected *at the definition*, before any call site:
+
+```
+spike/generics/reject.flan:1:26: + over the type variable t is refused: an unconstrained type variable supports
+only what every type supports, and + is not that (plan.org, Types). Take the operation as a parameter — a
+(Fn [t t] ...) — and call it here
+  1 | (defn add2 [a $t b $t] t (+ a b))
+    |                          ^^^^^^^
+```
+
+`=` and `<` get the same refusal from the same place. This is what `sort-by!` above is the positive case of: the
+comparison it cannot have is the comparison it is given.
+
+## Question 2 — where instantiation belongs in this pipeline
+
+**In the checker, at the call site, which is where Odin puts it.** `check_expr.cpp`'s
+`find_or_generate_polymorphic_procedure` runs from call checking: it builds the concrete proc type from the
+operands, scans the base entity's `gen_procs` for an `are_types_identical` match, and generates a new `Entity`
+only on a miss. `check.ml`'s `generic_call` and `instantiate` are that loop, with `Types.equal` pairwise standing
+in for `are_types_identical`.
+
+It belongs there and nowhere else for a reason specific to this pipeline: the call site is the only place the
+concrete types exist, and it is the same argument `check.ml` already makes for `SizeOf`/`AlignOf` ("the checker
+builds these at the site where the concrete element type is known"). A pass after checking would have to re-derive
+every argument type it had just thrown away; a pass before it has nothing to work with.
+
+**What that means for `Tast`: a generic `defn` does not reach the typed IR at all.** Only its instantiations do.
+Concretely:
+
+- `collect` puts a generic signature in a new `gsigs` table and **not** in `env.fns`. Nothing can be called at
+  `t`, so nothing may find it by the ordinary path.
+- `build_program`'s pass-two fold skips generic `defn`s. They produce no `Tast.fn`.
+- Each instantiation is an ordinary `Tast.fn` appended to the program next to the handler clauses `env.lifted`
+  already collects, with `fparent = None` — unlike a lifted clause it is reached *by name* from arbitrary call
+  sites, so it needs a cell, and it gets one automatically: `flan.cell.sort-by!-i32` is in the `--dev` output with
+  no change to `emit.ml`.
+- `Tast` is unchanged. `Types.Var` already existed, and after instantiation no node carries one.
+
+The naming convention is the prelude's own: `id-i32`, `sort-by!-f64`, `keep-i32`, and for constructed types
+`slice-i32`, `vec-f32`, `opt-i64`, `arr8-u8`. A generated name reads like the handwritten one it replaces, which
+is what a backtrace, a `Reach` edge and a dev-build cell all end up showing. `Types.to_string` cannot serve —
+`[i32]` and `(Vec i32)` are not symbols — so there is a second spelling function, `mangle_ty`, and it is a
+namespace hazard: see the "no plan" bucket.
+
+## Question 3 — the cost to the dev loop, measured
+
+This is the question the spike exists for, and the answer has two halves: the half that is free, and the half
+that is not implemented and will not be free.
+
+`spike/generics/run.sh` sweeps one generic pair (`gswap` + `gsort`, the insertion sort above) called at N distinct
+element types, N = 1..8, against the handwritten N-copies program it would replace. Best of three per cell, on an
+otherwise idle machine:
+
+```
+n   check-gen  check-mono   emit-1  emit-N   build-1  build-N   fns
+1        1.8         1.8      0.1     0.1      19.0     21.3   2
+2        1.8         1.8      0.1     0.3      19.6     24.7   4
+3        1.9         1.6      0.1     0.4      19.2     28.1   6
+4        1.9         1.9      0.1     0.4      18.5     31.9   8
+5        2.1         2.1      0.1     0.6      19.3     35.9   10
+6        1.8         1.9      0.1     0.7      18.8     39.1   12
+7        2.0         1.8      0.1     0.8      18.6     41.9   14
+8        1.8         2.0      0.1     0.8      19.0     45.1   16
+```
+
+`check-*` is `Check.program_with_env` over the whole accumulated program, which is what `Session.eval` does on
+**every** evaluation. `emit-*` is `Emit.redefinition`. `build-*` is `Build.shared` — llc + `ld -shared` — with the
+same options `dev.ml` passes (`dev = true`, `-O2`). Under load every column scales by about 3×; the ratios hold.
+
+Read off it:
+
+1. **Checking a generic program costs what checking the handwritten one costs.** 1.8 ms either way, flat in N.
+   Instantiation — matching, substituting, cache scan, and checking each copy's body — does not show above the
+   noise, because whole-program checking is dominated by the 1665-line prelude. The instantiation cache is rebuilt
+   from scratch on every `C-c C-c`, since `Check.program_with_env` makes a fresh `env`, and that is affordable:
+   there is no persistent cache to invalidate and therefore no staleness to get wrong.
+2. **Emitting is free.** 0.1 ms for one body, 0.8 ms for sixteen.
+3. **`llc` + `ld` is the whole bill, and it is per body.** 19 ms for one, 45 ms for sixteen — about **+1.7 ms per
+   extra body**, roughly linear. A redefinition module with one function is ~19 ms; the same redefinition of a
+   generic used at 8 element types is ~45 ms.
+
+So: **redefining a generic function used at N element types costs the dev loop about `19 + 1.7 × (bodies − 1)` ms
+against a 19 ms baseline.** For the realistic case — a generic used at two or three types — that is 21–28 ms, a
+10–50% increase on the slowest part of the loop. For a `map` used at eight types it is 2.4×. It stays under the
+"redefine a whole file" cost, and it is proportional to what changed rather than to the program.
+
+**And the half that is not implemented.** The last line of the sweep is the finding:
+
+```
+Session.eval on the generic gswap itself: 2.5 ms, installs=false, fns=[], names=[gswap]
+```
+
+`session.ml:eval` computes `fns` as the names in the incoming form that appear in `program.Tast.fns`. A generic
+`defn` is not in `Tast.fns` — by design, per question 2 — so `fns` is empty, `installs` is false, and the editor
+is told nothing was installed. **Today, `C-c C-c` on a generic function is a no-op that does not lie about it but
+does not do anything either.** The fix is not in this lane (`session.ml` is held elsewhere) and is small in
+principle: expand a redefined generic name to its instantiations, transitively through generics that call it, and
+pass *those* to `Emit.redefinition`. The cells already exist. The cost of doing so is the table above.
+
+Two things that cost nothing and are worth having in writing: the compatibility check (`Session.compatible`) sees
+instantiations as ordinary functions and compares their signatures as it always did; and a generic whose
+*signature* changes produces differently-named instantiations, so the old ones stay in the process with nothing
+calling them — dead, not stale.
+
+## Question 4 — what the whole feature would have to lower
+
+Against what a generic function has to survive, in DISCUSS.md item 15's buckets:
+
+| | |
+|---|---|
+| **Done in the spike** | one or more type variables in a signature; binding through `[t]`, `(Ptr t)`, `(Option t)`, `(Fn [t] t)` and nesting; return types mentioning a variable; left-to-right binding with substitution into later parameters so an `fn` literal gets its types; the Odin-keyed instantiation cache; generic calling generic, transitively; `(vec-new t)`; the abstract refusal pass for `+`, `-`, `*`, `/`, `%`, `=`, `!=`, `<`, `<=`, `>`, `>=`, the bitwise operators and the shifts; instantiations as ordinary `Tast.fn`s with dev cells and `Reach` edges for free |
+| **Mechanical** | the remaining builtins that take a *type name* as an argument — `pool-new`, `map-new`, `zeroed`, `uninit`, the casts — each of which reaches `type_named`/`resolve_name` by its own path, exactly as `vec-new` did (one line there fixed `vec-new`; the others are one line each); `hash` and the map key-pair path, which must refuse a `Var` rather than assume; the `fns` expansion in `session.ml` described above |
+| **Bulky, not hard** | error messages that say *where* an instantiation came from — Odin's "in instantiation of" note. Today a refusal inside an instantiated body points at the generic's source with no indication which call site asked for that type, and with three or four instantiations that is the difference between a readable refusal and a puzzle. It is a context stack in `ctx` and a `Loc.note` per frame, and it touches every `fail` under an instantiation |
+| **Fiddly** | move-only and ownership. `Types.is_move_only (Var _)` is false, but the same variable at `(Vec i32)` is move-only — so the abstract pass **cannot decide ownership at all**, and the dead-set analysis is only sound per instantiation. Today that means a generic body that moves its parameter type-checks abstractly and is caught, if at all, at one instantiation and not another. The rule has to be stated: either ownership is checked only per copy (and the abstract pass skips it, so a generic may be accepted and its instantiation refused), or type variables carry a move-only constraint, which is a constraint system and plan.org says not yet |
+| **No plan** | (1) **Unbounded instantiation.** `(defn grow [x $t] () (grow [x x]))` hangs the checker: each copy asks for a copy at `[2 t]`, forever. There is no depth cap, no size cap, and no cycle detection — and **Odin has none either**, so there is no implementation to copy. It needs a designed limit with a refusal that names the chain. (2) **Generic structs and containers.** `Types.Named` is a bare string with no parameters, so `(defstruct Pair [a $t b $t])` cannot be spelled at all — a parameterised named type is a change to `Types.t` and therefore to every backend, `Render`, DWARF and the layout calculator. (3) **`println` over a type variable.** plan.org's one compiler-provided exception; the abstract pass rejects it (`no printer for t`), see question 6. (4) **Generics across packages.** `Load` flattens imports into one namespace before checking, so it happens to work here, but a package boundary that is ever a real compilation-unit boundary would need the generic's *body* to cross it — the thing separate compilation cannot do and the reason C++ puts templates in headers |
+
+The "no plan" row's first entry is the one to take seriously: it is not a missing feature, it is a hang, and it is
+reachable from three lines of ordinary-looking Flan.
+
+## Question 5 — what collapsing prelude.ml's 34 functions would actually require
+
+Bucketed by what the body needs from the element type, which is readable straight off the sources. `spike/generics/prelude-shapes.flan` is the experiment: the same bodies over `$t`, checked, instantiated and run at `i32`
+and `f32`, printing the right answers and emitting `keep-i32`, `fold-i32`, `fold-f32`, `apply!-i32`, `apply!-f32`,
+`flip!-i32`, `flip!-f32`.
+
+**Collapse as they are written — nothing but the signature changes.** `swap-i32!`/`swap-f32!`/`swap-bytes!`,
+`reverse-i32!`/`reverse-f32!`, `map-i32!`/`map-f32!`, `reduce-i32`/`reduce-f32`, `filter-i32`/`filter-f32`,
+`sort-i32-by!`/`sort-f32-by!`. They only move elements, or they already take the operation as a function value.
+`filter` is the strongest case and the one that surprised: it allocates — `(vec-new t)`, `push`, returns
+`(Vec t)` — and the type-erased container runtime made that work with no changes at all, because `SizeOf`/`AlignOf`
+are computed at the instantiation site where the type is concrete. **That is the direct confirmation that
+spec-memory.md's type-erased `Vec`/`Map` and monomorphised functions compose**, which is the thing to check before
+building either.
+
+**Do not collapse without a signature change.** `sort-i32!`/`sort-f32!`/`sort-bytes!` need `<`;
+`index-of-i32`/`index-of-byte` need `=`; `min-i32`/`min-f32`/`max-i32`/`max-f32` need `<`. Under plan.org's
+rejection rule every one of them must take the comparison as a `(Fn [t t] bool)` — which means `(sort! xs)`
+becomes `(sort-by! xs (fn [a b] (< a b)))` at every call site in the corpus. The functions collapse; the *calls*
+get longer. That is the visible cost of "no constraints", and it is a language-ergonomics decision rather than a
+compiler one.
+
+**Do not collapse at all, as written.** `sum-i32` returns `i64` and `sum-f32` returns `f64`: each widens its
+element with an explicit cast, because there is no implicit widening anywhere in the language. "The wider type
+that `t` accumulates into" is not expressible over an unconstrained variable — it is a type-level function, which
+is a constraint system or an associated type, and plan.org rules both out for now. A generic `sum` would have to
+be `(defn sum [s [$t] init $u add (Fn [$u $t] $u)] u ...)`, at which point it is `reduce` and should just be
+`reduce`. Likewise `append-i64!`/`append-f64!`: their bodies are `I64ToBytes` and `F64ToBytes`, two different
+primitives, and picking between them per instantiation is exactly the compile-time overloading plan.org says
+multimethods are for.
+
+Counted by name, the 27 of the family I could account for split **13 / 9 / 5**:
+
+- 13 collapse cleanly into 6 generics — `swap-i32!` `swap-f32!` `swap-bytes!`, `reverse-i32!` `reverse-f32!`,
+  `map-i32!` `map-f32!`, `reduce-i32` `reduce-f32`, `filter-i32` `filter-f32`, `sort-i32-by!` `sort-f32-by!`.
+- 9 collapse into 4 but change their signatures and every call site — `sort-i32!` `sort-f32!` `sort-bytes!`,
+  `index-of-i32` `index-of-byte`, `min-i32` `min-f32` `max-i32` `max-f32`.
+- 5 do not collapse — `sum-i32` `sum-f32`, `append!` `append-i64!` `append-f64!` — because they are not one
+  function written twice; they are functions that happen to rhyme.
+
+So the net is on the order of **27 → 15**, not 27 → 6, and the prelude keeps a per-type layer for the numeric
+ones.
+
+## Question 6 — what contradicts plan.org
+
+**1. plan.org bundles two decisions that are independent, and the spike had to implement both separately.** It
+says parametric polymorphism is "Odin's model", and it says an unconstrained variable's `=`, `<`, `+` and `hash`
+are "rejected, not silently instantiated". **Odin does not do the second.** Odin checks a polymorphic body only
+per instantiation, so `a + b` over a `$T` compiles there and fails only when — and if — someone instantiates it at
+a type without `+`. Getting plan.org's rule instead requires a second pass that type-checks the body with nothing
+substituted, which is `check_generic` in this spike: one extra whole-body check per generic `defn`, discarded.
+It is cheap and it is worth it, but it is *not* Odin's model and the plan should stop saying it is.
+
+**2. The abstract pass rejects `println` over a type variable**, and plan.org names `println` as "the one
+compiler-provided exception: it selects a structural printer at each concrete instantiation". Those two statements
+cannot both hold as written: a pass that decides an operator's legality without substituting cannot make an
+exception for the one operator whose legality is only decidable after substituting. `(defn show [x $t] () (println
+x))` gets `no printer for t` today. The resolution is small but it is a decision, not an oversight: the abstract
+pass needs an explicit allow-list of forms it defers to instantiation, `println` being the first member. Every
+member of that list is a place where a refusal moves from the definition to a call site, which is exactly what
+plan.org's rule was trying to avoid — so the list should stay short and be written down.
+
+**3. The sigil.** Already superseded by the author's revision, and the spike is built to the revision. Recorded
+here because plan.org still says "no sigil" and the correction belongs in the record rather than being patched
+over: without a binding site there is no way to tell introduction from use, and `check.ml:563` already had the
+contradiction in miniature — an unknown *length* name in `[n t]` is an error while an unknown *type* name in the
+same brackets became a type parameter.
+
+**4. Ownership is not decidable without the type.** Not contradicted by plan.org, because plan.org does not
+mention it; stated here because it is the interaction that will bite. `Types.is_move_only` is a property of the
+concrete type, and spec-memory.md's whole dead-set analysis is downstream of it. Every other analysis in the
+checker survives abstraction; that one does not.
+
+## `$n` in length position, as asked
+
+Not built, and it does not fall out for free. `(defn rotate [xs [$n i32]] ...)` would let a function be generic
+over array length the way Odin's `$N: int` does. The cost, specifically:
+
+- `Ast.len` is `Lint of int64 | Lname of string`, so `$n` parses today as `Lname "$n"` and needs no reader or
+  parser change — the same free ride the type sigil got.
+- But `Types.Array` is `int64 * t`. A length that is a *variable* means either a third case or a `len` type
+  inside `Types.t`, and `Types.t` is consumed by `emit.ml`'s layout calculator, `x86.ml`, `render.ml`, the DWARF
+  path and the map key-pair emitter. That is the same "change `Types.t` and every backend" price generic structs
+  pay, for a smaller prize.
+- `bind_ty` gains a length-binding case (`Array (n, p)` against `Array (m, a)` binds `n := m`), `mangle_ty` gains
+  a number, and `array_len` has to answer "a variable" rather than failing — which means the checker's
+  compile-time constant folding has to know a length can be symbolic until instantiation.
+
+Everything after the second bullet is the expensive part, and it is expensive for the same reason generic structs
+are. If both are wanted, they are one project and should be sequenced together; if only one is, this is the one
+to drop.
+
+## Reproducing
+
+```
+dune exec --root . bin/main.exe -- run spike/generics/id.flan
+dune exec --root . bin/main.exe -- run spike/generics/swap.flan
+dune exec --root . bin/main.exe -- run spike/generics/sort.flan
+dune exec --root . bin/main.exe -- run spike/generics/two-vars.flan
+dune exec --root . bin/main.exe -- run spike/generics/prelude-shapes.flan
+dune exec --root . bin/main.exe -- check spike/generics/reject.flan     # the refusal
+bash spike/generics/run.sh                                              # the sweep
+```
diff --git a/spike/generics/two-vars.flan b/spike/generics/two-vars.flan
new file mode 100644
index 0000000..fe3b300
--- /dev/null
+++ b/spike/generics/two-vars.flan
@@ -0,0 +1,5 @@
+(defn fst [a $t b $u] t a)
+(defn main [] ()
+  (println (fst 1 2.5))
+  (println (fst true (i64 9)))
+  (println (fst 3 false)))

From eec0dfd1c391e1015fce0415ac4987494ff0530b Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 13:32:33 +0700
Subject: [PATCH 05/11] A runaway instantiation refuses instead of hanging the
 editor

---
 SPIKE-GENERICS.md           | 26 +++++++++++++++++++-------
 lib/check.ml                | 31 +++++++++++++++++++++++++++++--
 spike/generics/runaway.flan |  3 +++
 3 files changed, 51 insertions(+), 9 deletions(-)
 create mode 100644 spike/generics/runaway.flan

diff --git a/SPIKE-GENERICS.md b/SPIKE-GENERICS.md
index 9b10b37..8c04be8 100644
--- a/SPIKE-GENERICS.md
+++ b/SPIKE-GENERICS.md
@@ -179,10 +179,17 @@ Read off it:
    extra body**, roughly linear. A redefinition module with one function is ~19 ms; the same redefinition of a
    generic used at 8 element types is ~45 ms.
 
-So: **redefining a generic function used at N element types costs the dev loop about `19 + 1.7 × (bodies − 1)` ms
-against a 19 ms baseline.** For the realistic case — a generic used at two or three types — that is 21–28 ms, a
-10–50% increase on the slowest part of the loop. For a `map` used at eight types it is 2.4×. It stays under the
-"redefine a whole file" cost, and it is proportional to what changed rather than to the program.
+**What the 19 ms is and is not.** It is `Build.shared` alone: `llc` plus `ld -shared`. The ~35 ms the brief
+quotes for `C-c C-c` is the whole round trip, and `dev.ml:446` pays several things around this call that are not
+in it — `Session.eval`'s read/parse/Load/check (the 1.8 ms column), writing the `.ll` and the `.o`, `deliver` and
+the `dlopen` at a frame boundary, and the wire exchange with the editor. So the two numbers are not in conflict;
+they are measuring different brackets, and the ~16 ms between them is the part this spike does not change.
+
+**The marginal number is the one that transfers, and it is invariant to which baseline it is added to: +1.7 ms
+per extra body.** In the terms the brief asks for: a generic used at two element types adds about 3.5 ms to a
+~35 ms loop (one generic that calls another, so four bodies rather than two — 10%); at three types, ~7 ms; at
+eight types, ~26 ms, which is a loop of ~61 ms rather than ~35. It stays well under the "redefine a whole file"
+cost and is proportional to what changed rather than to the size of the program.
 
 **And the half that is not implemented.** The last line of the sweep is the finding:
 
@@ -208,11 +215,11 @@ Against what a generic function has to survive, in DISCUSS.md item 15's buckets:
 
 | | |
 |---|---|
-| **Done in the spike** | one or more type variables in a signature; binding through `[t]`, `(Ptr t)`, `(Option t)`, `(Fn [t] t)` and nesting; return types mentioning a variable; left-to-right binding with substitution into later parameters so an `fn` literal gets its types; the Odin-keyed instantiation cache; generic calling generic, transitively; `(vec-new t)`; the abstract refusal pass for `+`, `-`, `*`, `/`, `%`, `=`, `!=`, `<`, `<=`, `>`, `>=`, the bitwise operators and the shifts; instantiations as ordinary `Tast.fn`s with dev cells and `Reach` edges for free |
+| **Done in the spike** | one or more type variables in a signature; binding through `[t]`, `(Ptr t)`, `(Option t)`, `(Fn [t] t)` and nesting; return types mentioning a variable; left-to-right binding with substitution into later parameters so an `fn` literal gets its types; the Odin-keyed instantiation cache; generic calling generic, transitively; `(vec-new t)`; the abstract refusal pass for `+`, `-`, `*`, `/`, `%`, `=`, `!=`, `<`, `<=`, `>`, `>=`, the bitwise operators and the shifts; instantiations as ordinary `Tast.fn`s with dev cells and `Reach` edges for free; a depth cap so runaway instantiation refuses instead of hanging |
 | **Mechanical** | the remaining builtins that take a *type name* as an argument — `pool-new`, `map-new`, `zeroed`, `uninit`, the casts — each of which reaches `type_named`/`resolve_name` by its own path, exactly as `vec-new` did (one line there fixed `vec-new`; the others are one line each); `hash` and the map key-pair path, which must refuse a `Var` rather than assume; the `fns` expansion in `session.ml` described above |
 | **Bulky, not hard** | error messages that say *where* an instantiation came from — Odin's "in instantiation of" note. Today a refusal inside an instantiated body points at the generic's source with no indication which call site asked for that type, and with three or four instantiations that is the difference between a readable refusal and a puzzle. It is a context stack in `ctx` and a `Loc.note` per frame, and it touches every `fail` under an instantiation |
-| **Fiddly** | move-only and ownership. `Types.is_move_only (Var _)` is false, but the same variable at `(Vec i32)` is move-only — so the abstract pass **cannot decide ownership at all**, and the dead-set analysis is only sound per instantiation. Today that means a generic body that moves its parameter type-checks abstractly and is caught, if at all, at one instantiation and not another. The rule has to be stated: either ownership is checked only per copy (and the abstract pass skips it, so a generic may be accepted and its instantiation refused), or type variables carry a move-only constraint, which is a constraint system and plan.org says not yet |
-| **No plan** | (1) **Unbounded instantiation.** `(defn grow [x $t] () (grow [x x]))` hangs the checker: each copy asks for a copy at `[2 t]`, forever. There is no depth cap, no size cap, and no cycle detection — and **Odin has none either**, so there is no implementation to copy. It needs a designed limit with a refusal that names the chain. (2) **Generic structs and containers.** `Types.Named` is a bare string with no parameters, so `(defstruct Pair [a $t b $t])` cannot be spelled at all — a parameterised named type is a change to `Types.t` and therefore to every backend, `Render`, DWARF and the layout calculator. (3) **`println` over a type variable.** plan.org's one compiler-provided exception; the abstract pass rejects it (`no printer for t`), see question 6. (4) **Generics across packages.** `Load` flattens imports into one namespace before checking, so it happens to work here, but a package boundary that is ever a real compilation-unit boundary would need the generic's *body* to cross it — the thing separate compilation cannot do and the reason C++ puts templates in headers |
+| **Fiddly** | move-only and ownership. `Types.is_move_only (Var _)` is false, but the same variable at `(Vec i32)` is move-only — so the abstract pass **cannot decide ownership at all**, and the dead-set analysis is only sound per instantiation. Today that means a generic body that moves its parameter type-checks abstractly and is caught, if at all, at one instantiation and not another. The rule has to be stated: either ownership is checked only per copy (and the abstract pass skips it, so a generic may be accepted and its instantiation refused), or type variables carry a move-only constraint, which is a constraint system and plan.org says not yet. One smaller thing in the same bucket, found and left alone: the abstract pass over a generic body that calls *another* generic at a concrete type generates that copy and keeps it, so plain `flan emit` can carry a body no call site asked for. It is a valid instantiation and `Reach.link` drops it, so `flan build` and `flan run` are unaffected — but the abstract pass is meant to leave nothing behind and this is the one thing it does |
+| **No plan** | (1) **Unbounded instantiation.** `(defn grow [x $t] () (grow [x x]))` asks for a copy at `[2 t]`, which asks for one at `[2 [2 t]]`, forever. Before the cap it did not fail, it *hung* — and since `Session.eval` runs this same code, the thing that hangs is `C-c C-c`, with the dev daemon wedged behind it and no error to show. That is the project's stated priority hanging on three lines of ordinary-looking Flan, so the spike stops it: a depth counter in `env`, refusing past 32 and naming the type it had reached (`spike/generics/runaway.flan`). **The number is arbitrary and the designed refusal — one that names the chain of instantiations rather than the depth it gave up at — is still open.** **Odin has no cap of its own**, so there is no implementation to copy. (2) **Generic structs and containers.** `Types.Named` is a bare string with no parameters, so `(defstruct Pair [a $t b $t])` cannot be spelled at all — a parameterised named type is a change to `Types.t` and therefore to every backend, `Render`, DWARF and the layout calculator. (3) **`println` over a type variable.** plan.org's one compiler-provided exception; the abstract pass rejects it (`no printer for t`), see question 6. (4) **Generics across packages.** `Load` flattens imports into one namespace before checking, so it happens to work here, but a package boundary that is ever a real compilation-unit boundary would need the generic's *body* to cross it — the thing separate compilation cannot do and the reason C++ puts templates in headers |
 
 The "no plan" row's first entry is the one to take seriously: it is not a missing feature, it is a hang, and it is
 reachable from three lines of ordinary-looking Flan.
@@ -311,6 +318,10 @@ to drop.
 
 ## Reproducing
 
+`dune test --root .` is green either side of this work. One caveat for anyone reproducing under load:
+`test_dev`'s `the daemon never listened` check is timing-sensitive and fails identically at `97cb77d` with
+`lib/check.ml` restored from that commit — it is not this lane's. On an idle machine it passes.
+
 ```
 dune exec --root . bin/main.exe -- run spike/generics/id.flan
 dune exec --root . bin/main.exe -- run spike/generics/swap.flan
@@ -318,5 +329,6 @@ dune exec --root . bin/main.exe -- run spike/generics/sort.flan
 dune exec --root . bin/main.exe -- run spike/generics/two-vars.flan
 dune exec --root . bin/main.exe -- run spike/generics/prelude-shapes.flan
 dune exec --root . bin/main.exe -- check spike/generics/reject.flan     # the refusal
+dune exec --root . bin/main.exe -- check spike/generics/runaway.flan    # the depth cap
 bash spike/generics/run.sh                                              # the sweep
 ```
diff --git a/lib/check.ml b/lib/check.ml
index a15b3ae..00a4c1a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -102,6 +102,14 @@ type env = {
      [resolve_name] consults it before anything else, so the body resolves
      [t] to [i32] and every node under it is concrete. *)
   mutable subst : (string * Types.t) list;
+  (* How many instantiations deep the checker is. A generic that calls itself
+     at a *larger* type — [(defn grow [x $t] () (grow [x x]))] — asks for a
+     copy at [[2 t]], which asks for one at [[2 [2 t]]], forever. Without this
+     the checker does not fail, it hangs, and since [Session.eval] runs the
+     same code that is the editor hanging with the daemon wedged behind it.
+     Odin has no cap of its own to copy; the number is arbitrary and the
+     refusal that names the chain is still to design. *)
+  mutable depth : int;
 }
 
 let new_env () = {
@@ -122,6 +130,7 @@ let new_env () = {
   instances = [];
   tyvars = [];
   subst = [];
+  depth = 0;
 }
 
 (* Where a named type was declared, and what it has, as a note.
@@ -4554,6 +4563,13 @@ and instantiate env loc gname vars subst cparams cret =
     (* The entry goes in *before* the body is checked, which is what makes a
        recursive generic function terminate: the call to itself at the same
        types finds this and does not generate a second copy. *)
+    if env.depth >= 32 then
+      fail loc
+        "%s instantiates itself without end — the copy at (%s) asks for \
+         another at a larger type, 32 deep and still growing. A generic \
+         function may call itself, but not at a type built out of its own \
+         type variable" gname
+        (String.concat " " (List.map Types.to_string cparams));
     cache := (cparams, cret, sym) :: !cache;
     Hashtbl.replace env.fns sym (cparams, cret);
     let fn = Hashtbl.find env.generics gname in
@@ -4563,11 +4579,22 @@ and instantiate env loc gname vars subst cparams cret =
        concrete as one written out by hand. *)
     env.subst <- List.map (fun v -> (v, List.assoc v subst)) vars;
     env.tyvars <- [];
-    let restore () = env.subst <- saved_subst; env.tyvars <- saved_vars in
+    env.depth <- env.depth + 1;
+    let restore () =
+      env.subst <- saved_subst; env.tyvars <- saved_vars;
+      env.depth <- env.depth - 1
+    in
     let tfn =
       match !check_fn_ref env { fn with Ast.name = sym } with
       | tfn -> restore (); tfn
-      | exception e -> restore (); raise e
+      | exception e ->
+        restore ();
+        (* A copy whose body did not check is not a copy. Both entries go back
+           out, so a second call at the same types is the same refusal again
+           rather than a cache hit on a function that does not exist. *)
+        cache := List.filter (fun (_, _, s) -> s <> sym) !cache;
+        Hashtbl.remove env.fns sym;
+        raise e
     in
     env.instances <- tfn :: env.instances;
     sym
diff --git a/spike/generics/runaway.flan b/spike/generics/runaway.flan
new file mode 100644
index 0000000..9423840
--- /dev/null
+++ b/spike/generics/runaway.flan
@@ -0,0 +1,3 @@
+(defn grow [x $t] ()
+  (grow [x x]))
+(defn main [] () (grow 1))

From 7f86f32699c9f24efd2bfe33ca65335bb49cf174 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 14:33:45 +0700
Subject: [PATCH 06/11] where predicates admit operators, and a type variable
 is move-only until it says otherwise

The spike proved the shape; this makes it the feature. A generic body is
still checked abstractly once, but now it may be told what to assume:
{:where (ordered? $t)} at the head of the body, Clojure's {:pre [...]}
spelling, with five predicates - ordered?, equal?, hashable?, numeric?
and copyable?.

The syntax catch settled structurally: {K V} is still a legal return
type, and a constraint map is told from one by its leading keyword. A
keyword is not a type anywhere in the language, so the slot after the
return type is unambiguous and {K V} did not have to go.

A type variable is move-only by default, with copyable? the opt-out.
Move is the stricter rule, so assuming it can only refuse a valid
program, never admit a bad one. That is Rust's T: Copy and not Odin's
anything - Odin has no move semantics at all.

The runaway refusal no longer names a depth. It names the chain: a
generic already on the instantiation stack, asked for again at a type
built around the one it had before, is growing and will not stop.
---
 lib/ast.ml                         |  11 +
 lib/check.ml                       | 374 +++++++++++++++++++++++++----
 lib/cimport.ml                     |   2 +-
 lib/parse.ml                       |  81 ++++++-
 spike/generics/prelude-shapes.flan |   2 +
 5 files changed, 415 insertions(+), 55 deletions(-)

diff --git a/lib/ast.ml b/lib/ast.ml
index e90b2d3..4359b7f 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -126,10 +126,21 @@ and pattern =
 
 (* ── Declarations ──────────────────────────────────────────────────── *)
 
+(* One [where] predicate: [(ordered? $t)] is [{ pname = "ordered?"; pvar = "t" }].
+   A predicate is a *compile-time question about a type*, not a type class: it
+   carries no implementation and selects no instance, it only tells the
+   abstract pass which builtin operators the variable may be used with, and
+   makes each instantiation check the concrete type answers yes. *)
+type pred = { pname : string; pvar : string; ploc : Loc.t }
+
 type fn = {
   name    : string;
   params  : field list;
   ret     : texpr option;             (* None means (); only declare omits it *)
+  (* The [{:where ...}] map at the head of the body, already unpacked. Empty
+     for every function that has none, which is every function that is not
+     generic and most that are. *)
+  fwhere  : pred list;
   fbody   : expr list;
   nloc    : Loc.t;
 }
diff --git a/lib/check.ml b/lib/check.ml
index 00a4c1a..305b1d8 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -102,14 +102,24 @@ type env = {
      [resolve_name] consults it before anything else, so the body resolves
      [t] to [i32] and every node under it is concrete. *)
   mutable subst : (string * Types.t) list;
-  (* How many instantiations deep the checker is. A generic that calls itself
-     at a *larger* type — [(defn grow [x $t] () (grow [x x]))] — asks for a
-     copy at [[2 t]], which asks for one at [[2 [2 t]]], forever. Without this
-     the checker does not fail, it hangs, and since [Session.eval] runs the
-     same code that is the editor hanging with the daemon wedged behind it.
-     Odin has no cap of its own to copy; the number is arbitrary and the
-     refusal that names the chain is still to design. *)
-  mutable depth : int;
+  (* The [where] predicates in scope: what the abstract pass may assume about
+     the variables, and what each instantiation checks its concrete types
+     answer yes to. Empty everywhere a generic signature or body is not being
+     resolved, which is what keeps every refusal below the default. *)
+  mutable tvpreds : Ast.pred list;
+  (* The chain of instantiations currently being generated, innermost last:
+     the generic's name and the concrete parameter types each copy was asked
+     for. It is the refusal for a generic that instantiates itself without
+     end — [(defn grow [x $t] () (grow [x x]))] asks for a copy at [[2 t]],
+     which asks for one at [[2 [2 t]]], forever — and without it the checker
+     does not fail, it *hangs*, which through [Session.eval] is [C-c C-c]
+     hanging with the dev daemon wedged behind it.
+
+     The test is structural rather than a depth count. A depth count names a
+     number the programmer did not write and cannot act on; this names the
+     chain. Odin has no cap of its own to copy, so there was nothing to
+     borrow. *)
+  mutable chain : (string * Types.t list * Loc.t) list;
 }
 
 let new_env () = {
@@ -130,7 +140,8 @@ let new_env () = {
   instances = [];
   tyvars = [];
   subst = [];
-  depth = 0;
+  tvpreds = [];
+  chain = [];
 }
 
 (* Where a named type was declared, and what it has, as a note.
@@ -388,6 +399,87 @@ let unimplemented loc what milestone =
   fail loc "%s is not implemented yet — milestone %d (see plan.org)"
     what milestone
 
+(* ── where predicates ──────────────────────────────────────────────────
+   A predicate is a compile-time question about a type, and that is the whole
+   of it. It carries no implementation, selects no instance, and is not
+   extensible: it gates a builtin the compiler already has. So there are no
+   dictionaries, no coherence rules and no run-time cost — and the ceiling is
+   that nobody can supply a [<] of their own, which does not bind because
+   every operation the prelude and the containers need is a primitive.
+
+   Odin's [where] clause is the same shape ([core/slice/slice.odin:289] is
+   [where intrinsics.type_is_ordered(T)]) with forty-one predicates against
+   these five. The fifth, [copyable?], has no Odin counterpart at all: Odin
+   has no move semantics, so [$T] never has to answer the question. The prior
+   art there is Rust's [T: Copy], with the difference that [copyable?] is a
+   question the compiler answers rather than a trait a user implements. *)
+let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable?" ]
+
+(* Does a concrete type answer yes? Checked at every instantiation, against
+   the type the call site asked for. *)
+let pred_holds p (t : Types.t) =
+  match p with
+  | "ordered?"  -> Types.is_comparable t
+  | "equal?"    -> Types.is_equatable t
+  (* [Types.keyable] says yes to a struct and leaves its fields to [key_pair],
+     which walks them at the operation. That split is the existing one and is
+     kept: a generic declared [hashable?] and instantiated at a struct whose
+     fields are not keyable is refused where every other program is, by
+     [key_pair]. *)
+  | "hashable?" -> Types.keyable t
+  | "numeric?"  -> Types.is_numeric t
+  | "copyable?" -> not (Types.is_move_only t)
+  | _           -> false
+
+(* What one declared predicate *also* gives you. These are entailments over
+   the type system as it stands, not conveniences: every type [is_comparable]
+   admits is a number or an enum, so it is equatable and it is not move-only.
+   The table is only sound while that is true — an ordered move-only type, or
+   an ordered type with no [=], would make it wrong — so it lives in one place
+   and says so. The gain is real ergonomics: [{:where (ordered? $t)}] is
+   enough for a [sort!] that also compares and reads its elements twice,
+   rather than three predicates on one line. *)
+let pred_entails ~declared ~wanted =
+  String.equal declared wanted
+  || match wanted, declared with
+     | "ordered?",  "numeric?" -> true
+     | "equal?",    ("numeric?" | "ordered?") -> true
+     | "copyable?", ("numeric?" | "ordered?" | "equal?" | "hashable?") -> true
+     | _ -> false
+
+let declares preds v wanted =
+  List.exists
+    (fun (p : Ast.pred) ->
+       String.equal p.Ast.pvar v && pred_entails ~declared:p.Ast.pname ~wanted)
+    preds
+
+(* Which variable, if any, a type bottoms out at. Only a bare variable can
+   carry a predicate: [(Vec t)] is a Vec whatever [t] is, and its own
+   properties are the Vec's. *)
+let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None
+
+(* ── Move-only, with a type variable defaulting to move ────────────────
+   [Types.is_move_only (Var _)] is [false] and cannot be anything else: the
+   same variable is [i32] at one instantiation and [(Vec i32)] at the next, so
+   the property is not decidable abstractly. The author's decision is to
+   default to **move**, because move is the *stricter* rule: assuming it can
+   only refuse a program that would have been fine, never admit one that
+   double-frees. [copyable?] is the opt-out, exactly as Rust's [T: Copy] is.
+
+   In the body this means a generic may not use a parameter twice without
+   declaring [copyable?]: [(defn twice [x $t] $t (+ x x))] is refused, which
+   is right — correct at [i32], a double read of a moved value at [(Vec i32)],
+   and the checker cannot tell which until it substitutes.
+
+   A [Var] only ever survives the abstract pass. Inside an instantiation
+   [env.subst] has made everything concrete, so this is [Types.is_move_only]
+   there and the strictness costs nothing at a call site. *)
+let rec move_only preds (t : Types.t) =
+  match t with
+  | Types.Var v -> not (declares preds v "copyable?")
+  | Types.Option e | Types.Array (_, e) -> move_only preds e
+  | t -> Types.is_move_only t
+
 (* ── (Map K V), spec-memory.md ──────────────────────────────────────────
    Both halves are checked where the type is written, not where an operation
    is, so that a map nothing ever uses is still refused if it cannot work.
@@ -395,12 +487,12 @@ let unimplemented loc what milestone =
    and repeats these refusals rather than assuming: the two are reached by
    different paths and a silent disagreement between them would be worse than
    saying the same thing twice. *)
-let map_type loc (k : Types.t) (v : Types.t) =
+let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
   (* The value. The restriction is the one [(Vec (Vec T))] already carries,
      for the identical reason: the runtime copies and releases entries
      bytewise, so an owning value would have its header duplicated by clone
      and its buffer dropped on the floor by free. *)
-  if Types.is_move_only v then
+  if move_only preds v then
     fail loc
       "(Map %s %s) holds a move-only value, and the type-erased runtime \
        copies entries bytewise — so clone would duplicate headers instead of \
@@ -423,7 +515,13 @@ let map_type loc (k : Types.t) (v : Types.t) =
      struct table is not necessarily complete while a type is being resolved,
      and every map that exists reaches an operation anyway, because a global of
      move-only type is refused and a local needs (map-new). *)
-  if not (Types.keyable k) then
+  (* A type variable is a map key exactly when the [where] clause says it is
+     hashable. Nothing else about it is knowable here, and falling through to
+     [Types.keyable] would answer no for a variable that is about to be
+     instantiated at [string]. *)
+  if not (match k with
+          | Types.Var v -> declares preds v "hashable?"
+          | k -> Types.keyable k) then
     fail loc
       "%s is not a map key. The first implementation takes integers, enums, \
        bools, strings, fixed arrays of those, and value structs composed of \
@@ -471,7 +569,8 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
      braces two meanings is what the colon-to-dot change was for. A map is
      built with (map-new) and filled with (put). *)
   | Ast.Tmap (k, v) ->
-    map_type loc (resolve env ~seen k) (resolve env ~seen v)
+    map_type ~preds:env.tvpreds loc (resolve env ~seen k)
+      (resolve env ~seen v)
   (* (Fn [T ...] R): a function value, which is one code address and no
      environment beside it. There is no capture — [check_fn] refuses a
      reference to an enclosing local by name — so this is a pointer with a
@@ -497,7 +596,7 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
           buffers on the floor. Recursive teardown is what step 5's [drop]
           brings, and this is refused until it does rather than shipping the
           shallow answer under the deep name. *)
-       if Types.is_move_only e then
+       if move_only env.tvpreds e then
          fail loc
            "(Vec %s) holds a move-only element, and the type-erased runtime \
             copies and releases elements bytewise — so clone would duplicate \
@@ -507,7 +606,8 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
        Types.Vec e
      | "Vec", _ -> fail loc "(Vec T) takes exactly one type"
      | "Map", [ k; v ] ->
-       map_type loc (resolve env ~seen k) (resolve env ~seen v)
+       map_type ~preds:env.tvpreds loc (resolve env ~seen k)
+         (resolve env ~seen v)
      | "Map", _ -> fail loc "(Map K V) takes exactly two types"
      | "Result", _ -> unimplemented loc "(Result T E)" 6
      | "Pool", [ a ] ->
@@ -516,7 +616,7 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
           runtime is type-erased and copies and releases slots bytewise, so a
           release would drop what an owning element owns. Recursive teardown
           arrives with drop. *)
-       if Types.is_move_only e then
+       if move_only env.tvpreds e then
          fail loc
            "(Pool %s) holds a move-only element, and the type-erased runtime \
             copies and releases slots bytewise — so releasing a slot would \
@@ -735,17 +835,27 @@ let rec generic_ty (t : Types.t) =
    operator says the same thing: with no constraints a type variable supports
    only what *every* type supports, so [=], [<], [+] and [hash] over one are
    rejected rather than silently instantiated at whatever type the first call
-   site happened to use. The way out is the one plan.org names — pass the
-   operation in as a function value, which is what [sort-i32-by!] already
-   does with [(Fn [i32 i32] bool)]. *)
-let unconstrained loc op (t : Types.t) =
+   site happened to use.
+
+   With [where] there are now two ways out and the message names both: declare
+   the predicate, or take the operation as a function value the way
+   [sort-by!] does. Declaring it is the one that keeps the call site short,
+   which is the whole reason predicates exist — under the no-constraint rule
+   [(sort! xs)] had to become [(sort-by! xs (fn [a b] (< a b)))] at every call
+   site in the corpus. *)
+let unconstrained env loc op ~needs (t : Types.t) =
   if generic_ty t then
-    Loc.failk "check/unconstrained-type-variable" loc
-      "%s over the type variable %s is refused: an unconstrained type \
-       variable supports only what every type supports, and %s is not that \
-       (plan.org, Types). Take the operation as a parameter — a (Fn [%s %s] \
-       ...) — and call it here"
-      op (Types.to_string t) op (Types.to_string t) (Types.to_string t)
+    match tyvar_of t with
+    | Some v when declares env.tvpreds v needs -> ()
+    | _ ->
+      Loc.failk "check/unconstrained-type-variable" loc
+        "%s over the type variable %s is refused: a type variable supports \
+         only what it is declared to support, and nothing here says %s is \
+         %s. Write {:where (%s $%s)} at the head of the body, or take the \
+         operation as a parameter — a (Fn [%s %s] ...) — and call it here"
+        op (Types.to_string t) (Types.to_string t) needs needs
+        (Types.to_string t) (Types.to_string t) (Types.to_string t)
+
 
 (* How a concrete type is spelled inside an instantiation's name. The prelude
    already writes this by hand — [filter-i32], [sum-f32], [append-i64] — so a
@@ -768,6 +878,82 @@ let rec mangle_ty (t : Types.t) =
       (String.concat "-" (List.map mangle_ty ps)) (mangle_ty r)
   | t -> Types.to_string t
 
+(* ── The runaway instantiation, refused by name rather than by depth ────
+   [(defn grow [x $t] () (grow [x x]))] asks for a copy at [[t]], which asks
+   for one at [[[t]]], forever. Before this the checker did not fail, it
+   *hung*, and [Session.eval] runs the same code — so what hung was [C-c C-c],
+   with the dev daemon wedged behind it and nothing to show the editor. That
+   is the project's stated priority stopped by three lines of ordinary-looking
+   Flan, which is why this is a refusal and not a cap.
+
+   The spike stopped it with a depth counter refusing past 32. A number is the
+   wrong thing to say: 32 is not in the program, the programmer cannot act on
+   it, and a legitimate deep instantiation and a runaway one look identical in
+   the message. **The structural test is exact.** A generic that is already on
+   the chain and is being asked for again at a type that *contains* the type
+   it was asked for before is growing, and growing without a smaller case is
+   not going to stop. A generic that recurses at the *same* types never
+   reaches here — the cache entry goes in before the body is checked — and one
+   that recurses at a *smaller* or unrelated type is fine and stays fine.
+
+   The message prints the chain, which is what the programmer can act on: each
+   link is a call site and a type, and the place the type started growing is
+   visible in the list.
+
+   Odin has no cap of its own to copy, so there was nothing to borrow and this
+   is the whole design. The depth backstop below stays as a backstop only: it
+   catches a growth this test does not recognise, and it is never the thing
+   the message is about. *)
+let rec occurs_in ~needle (t : Types.t) =
+  Types.equal needle t
+  ||
+  match t with
+  | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+  | Types.Pool e | Types.Handle e | Types.Option e -> occurs_in ~needle e
+  | Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
+  | Types.Fn (ps, r) ->
+    List.exists (occurs_in ~needle) ps || occurs_in ~needle r
+  | _ -> false
+
+(* [b] is [a] with something built around it: same shape, strictly bigger. *)
+let grows ~from_:a ~to_:b =
+  List.length a = List.length b
+  && List.for_all2 (fun x y -> occurs_in ~needle:x y) a b
+  && not (List.for_all2 Types.equal a b)
+
+let runaway env loc gname cparams =
+  let chain_text () =
+    String.concat "\n  "
+      (List.map
+         (fun (g, ps, l) ->
+            Printf.sprintf "%s at (%s), asked for at %s" g
+              (String.concat " " (List.map Types.to_string ps))
+              (Loc.to_string l))
+         (env.chain @ [ (gname, cparams, loc) ]))
+  in
+  let earlier =
+    List.find_opt
+      (fun (g, ps, _) -> String.equal g gname && grows ~from_:ps ~to_:cparams)
+      env.chain
+  in
+  (match earlier with
+   | Some _ ->
+     Loc.failk "check/runaway-instantiation" loc
+       "%s instantiates itself without end. Each copy asks for another at a \
+        type built around the one before, so there is no last copy to \
+        generate:\n  %s\nA generic function may call itself, but not at a \
+        type built out of its own type variable — the argument has to get \
+        smaller, or stay the same"
+       gname (chain_text ())
+   | None -> ());
+  (* The backstop. Nothing known reaches it; it exists so that a growth the
+     test above does not recognise is still a refusal with the chain in it
+     rather than a hang. *)
+  if List.length env.chain >= 64 then
+    Loc.failk "check/runaway-instantiation" loc
+      "%s has been instantiated 64 deep and is still going:\n  %s"
+      gname (chain_text ())
+
 (* [check_fn] is defined after the expression checker and an instantiation is
    made from inside it, so the knot is tied here and closed at the bottom of
    the file. One forward reference rather than moving a 90-line function. *)
@@ -1035,6 +1221,19 @@ let direct = function
    two maps with the same key type share one pair. *)
 let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
   match k with
+  (* A hash and an equality for a type variable would have to be *chosen*,
+     and nothing here can choose: the pair is emitted as concrete symbols and
+     the concrete type does not exist until the instantiation. Refused rather
+     than assumed — falling through to [bytewise_key] would hash whatever
+     bytes the variable turned out to have, which is the wrong answer for a
+     [string] and for any struct with padding. Inside an instantiation this
+     arm is unreachable: [env.subst] has already made [k] concrete. *)
+  | Types.Var v ->
+    Loc.failk "check/generic-map-key" loc
+      "a map keyed by the type variable %s cannot have its hash and equality \
+       emitted here — they are chosen from the concrete type, which does not \
+       exist until this generic is instantiated. The key pair is emitted per \
+       copy, so this operation belongs in a body the checker has substituted" v
   | Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str"
   | t when bytewise_key t ->
     Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"
@@ -1510,7 +1709,8 @@ and var ctx loc ~want name =
   | _ ->
     match lookup ctx name with
     | Some b ->
-      if Types.is_move_only b.bty then moved ~ty:b.bty ctx loc name b.slot;
+      if move_only ctx.env.tvpreds b.bty then
+        moved ~ty:b.bty ctx loc name b.slot;
       expect loc ~want (mk loc b.bty (Tast.Local b.slot))
     | None ->
       match Hashtbl.find_opt ctx.env.globals name with
@@ -2716,8 +2916,11 @@ and fold_left_prim ctx ~want loc name p ok what args =
     match args with x :: y :: rest -> x, y, rest | _ -> assert false
   in
   let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
-  unconstrained loc name a.Tast.ty;
-  if not (ok a.Tast.ty) then
+  unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
+  (* Past [unconstrained] a variable here is one the [where] clause admitted,
+     so the concrete predicate below has nothing to say about it — it is
+     answered again, per copy, at the instantiation. *)
+  if not (ok a.Tast.ty || generic_ty a.Tast.ty) then
     fail loc "%s takes %s, found %s" name what (Types.to_string a.Tast.ty);
   let ty = a.Tast.ty in
   let acc =
@@ -2977,7 +3180,7 @@ and pool_new_elem ctx ~want loc args =
   in
   match named with
   | Some (t, rest) ->
-    if Types.is_move_only t then
+    if move_only ctx.env.tvpreds t then
       fail loc
         "(Pool %s) holds a move-only element, and the type-erased runtime \
          copies and releases slots bytewise. Recursive teardown arrives with \
@@ -3044,8 +3247,8 @@ and named_call ctx ~want loc name args =
   | "%" ->
     arity loc name 2 args;
     let a, b = binary ctx name loc ~want:(numeric_want want) args in
-    unconstrained loc name a.Tast.ty;
-    if not (Types.is_numeric a.Tast.ty) then
+    unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
+    if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then
       fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
     prim Tast.Rem a.Tast.ty [ a; b ]
   | "=" | "!=" | "<" | "<=" | ">" | ">=" ->
@@ -3064,8 +3267,10 @@ and named_call ctx ~want loc name args =
       | "=" | "!=" -> Types.is_equatable a.Tast.ty
       | _ -> Types.is_comparable a.Tast.ty
     in
-    unconstrained loc name a.Tast.ty;
-    if not ok then
+    unconstrained ctx.env loc name
+      ~needs:(match name with "=" | "!=" -> "equal?" | _ -> "ordered?")
+      a.Tast.ty;
+    if not (ok || generic_ty a.Tast.ty) then
       fail loc
         "%s compares machine numbers; %s has no built-in comparison \
          (plan.org, Types)" name (Types.to_string a.Tast.ty);
@@ -3123,7 +3328,10 @@ and named_call ctx ~want loc name args =
       match args with x :: y :: rest -> x, y, rest | _ -> assert false
     in
     let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
-    if not (Types.is_numeric a.Tast.ty) then
+    (* [min] and [max] are [<] with a pick, so [ordered?] is what they want —
+       not [numeric?]. A generic that declares [ordered?] gets both. *)
+    unconstrained ctx.env loc name ~needs:"ordered?" a.Tast.ty;
+    if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then
       fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
     let ty = a.Tast.ty in
     let cmp = if String.equal name "min" then Tast.Lt else Tast.Gt in
@@ -3796,7 +4004,7 @@ and named_call ctx ~want loc name args =
   | "map-new" ->
     let k, v, args = map_new_types ctx ~want loc args in
     let a = allocator_arg ctx loc args in
-    let mty = map_type loc k v in
+    let mty = map_type ~preds:ctx.env.tvpreds loc k v in
     let m = fresh_slot ctx mty in
     let attempt =
       rt loc (Types.Int Types.I8) "flan_map_init"
@@ -4318,6 +4526,30 @@ and named_call ctx ~want loc name args =
        printing of one would be its last. *)
     let target = List.hd args in
     let a = borrowed ctx target (fun () -> check ctx target) in
+    (* ── The allow-list, and it has exactly two members: [print] and
+       [println]. ──────────────────────────────────────────────────────
+       plan.org names [println] as the one compiler-provided exception — it
+       "selects a structural printer at each concrete instantiation" — and
+       that cannot be reconciled with an abstract pass as written: a pass that
+       decides an operator's legality *without* substituting cannot make an
+       exception for the one operator whose legality is only decidable after
+       substituting. So the exception is made explicit: these two forms are
+       *deferred* to instantiation, and every other operator is answered where
+       it is written.
+
+       Every member of this list is a place where a refusal moves from the
+       definition to a call site, which is the thing the abstract pass exists
+       to prevent. That is the whole cost of the exception and the reason the
+       list stays two long and is written down here. There is no [where]
+       predicate for printability on purpose: every type prints, so the
+       predicate would always hold and would only be noise on a signature.
+
+       The node produced here is a unit no-op, thrown away with the rest of
+       the abstract pass. The real printer is selected when the copy is
+       checked with [t] concrete. *)
+    if generic_ty a.Tast.ty then
+      mk loc Types.Unit Tast.Unit
+    else
     let bslice = Types.Slice (Types.Int Types.U8) in
     let write x = mk loc Types.Unit (Tast.Prim (Tast.WriteStdout, [ x ])) in
     let conv pr x = mk loc bslice (Tast.Prim (pr, [ x ])) in
@@ -4560,29 +4792,43 @@ and instantiate env loc gname vars subst cparams cret =
       fail loc
         "%s at these types is called %s, and %s is already defined — rename \
          one of them" gname sym sym;
+    runaway env loc gname cparams;
+    (* Each instantiation checks the concrete types answer the [where] clause.
+       This is the half of the feature that only exists per copy: the abstract
+       pass took the predicates on trust, and here is where the trust is
+       settled, at the call site that asked, naming it. *)
+    let fn = Hashtbl.find env.generics gname in
+    List.iter
+      (fun (p : Ast.pred) ->
+         match List.assoc_opt p.Ast.pvar subst with
+         | None -> ()
+         | Some t ->
+           if not (pred_holds p.Ast.pname t) then
+             Loc.failk "check/predicate-unsatisfied" loc
+               "%s here would instantiate %s at $%s = %s, and %s is not %s — \
+                the body of %s is written against {:where (%s $%s)}"
+               gname gname p.Ast.pvar (Types.to_string t) (Types.to_string t)
+               p.Ast.pname gname p.Ast.pname p.Ast.pvar)
+      fn.Ast.fwhere;
     (* The entry goes in *before* the body is checked, which is what makes a
        recursive generic function terminate: the call to itself at the same
        types finds this and does not generate a second copy. *)
-    if env.depth >= 32 then
-      fail loc
-        "%s instantiates itself without end — the copy at (%s) asks for \
-         another at a larger type, 32 deep and still growing. A generic \
-         function may call itself, but not at a type built out of its own \
-         type variable" gname
-        (String.concat " " (List.map Types.to_string cparams));
     cache := (cparams, cret, sym) :: !cache;
     Hashtbl.replace env.fns sym (cparams, cret);
-    let fn = Hashtbl.find env.generics gname in
-    let saved_subst = env.subst and saved_vars = env.tyvars in
+    let saved_subst = env.subst and saved_vars = env.tyvars
+    and saved_preds = env.tvpreds and saved_chain = env.chain in
     (* Inside the copy there are no variables left: [resolve_name] answers
        [t] with the concrete type, so every node the body produces is as
-       concrete as one written out by hand. *)
+       concrete as one written out by hand. The [where] clause goes out of
+       scope with them — there is nothing abstract left for it to permit, and
+       every operator is answered by the concrete type it now has. *)
     env.subst <- List.map (fun v -> (v, List.assoc v subst)) vars;
     env.tyvars <- [];
-    env.depth <- env.depth + 1;
+    env.tvpreds <- [];
+    env.chain <- env.chain @ [ (gname, cparams, loc) ];
     let restore () =
       env.subst <- saved_subst; env.tyvars <- saved_vars;
-      env.depth <- env.depth - 1
+      env.tvpreds <- saved_preds; env.chain <- saved_chain
     in
     let tfn =
       match !check_fn_ref env { fn with Ast.name = sym } with
@@ -4871,7 +5117,28 @@ let collect env (decls : Ast.decl list) =
             [fns], because nothing can be called at [t]. Every call site turns
             it into an ordinary entry. *)
          let vars = signature_tyvars fn in
+         (* The [where] clause is checked against the signature here, once,
+            rather than at every use of it: a predicate nobody has heard of,
+            or one about a variable the signature never bound, is a mistake
+            about this definition and is refused at this definition. *)
+         List.iter
+           (fun (p : Ast.pred) ->
+              if not (List.mem p.Ast.pname predicate_names) then
+                Loc.failk "check/unknown-predicate" p.Ast.ploc
+                  "%s is not a type predicate. The ones there are: %s"
+                  p.Ast.pname (String.concat ", " predicate_names);
+              if not (List.mem p.Ast.pvar vars) then
+                Loc.failk "check/unbound-predicate-variable" p.Ast.ploc
+                  "$%s is not a type variable of %s — a where clause \
+                   constrains the variables the signature binds%s"
+                  p.Ast.pvar fn.Ast.name
+                  (if vars = [] then ", and this signature binds none"
+                   else
+                     ", which here are "
+                     ^ String.concat ", " (List.map (fun v -> "$" ^ v) vars)))
+           fn.Ast.fwhere;
          env.tyvars <- vars;
+         env.tvpreds <- fn.Ast.fwhere;
          let params =
            List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
          in
@@ -4879,6 +5146,7 @@ let collect env (decls : Ast.decl list) =
            match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t
          in
          env.tyvars <- [];
+         env.tvpreds <- [];
          if vars = [] then Hashtbl.replace env.fns fn.Ast.name (params, ret)
          else begin
            Hashtbl.replace env.generics fn.Ast.name fn;
@@ -5050,13 +5318,19 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
    (Var _)] is false, but the same variable at [(Vec i32)] is move-only. *)
 and check_generic env (fn : Ast.fn) =
   let vars, params, ret = Hashtbl.find env.gsigs fn.Ast.name in
-  let saved_lifted = env.lifted and saved_vars = env.tyvars in
+  let saved_lifted = env.lifted and saved_vars = env.tyvars
+  and saved_preds = env.tvpreds in
   env.tyvars <- vars;
+  (* What the abstract pass may assume. Every operator the body reaches asks
+     [env.tvpreds] whether the variable was declared to support it, and every
+     instantiation asks the concrete type the same question again. *)
+  env.tvpreds <- fn.Ast.fwhere;
   Hashtbl.replace env.fns fn.Ast.name (params, ret);
   let finish () =
     Hashtbl.remove env.fns fn.Ast.name;
     env.lifted <- saved_lifted;
-    env.tyvars <- saved_vars
+    env.tyvars <- saved_vars;
+    env.tvpreds <- saved_preds
   in
   (match check_fn env fn with
    | _ -> finish ()
diff --git a/lib/cimport.ml b/lib/cimport.ml
index faee6fd..a3fede3 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -788,7 +788,7 @@ let of_dump ~env ~taken ~bound_syms ~config (d : dump) : imported =
            decls :=
              { Ast.d =
                  Ast.DeclareC
-                   ({ Ast.name = flan; params; ret; fbody = []; nloc = f.cloc },
+                   ({ Ast.name = flan; params; ret; fwhere = []; fbody = []; nloc = f.cloc },
                     f.csym);
                dloc = f.cloc }
              :: !decls)
diff --git a/lib/parse.ml b/lib/parse.ml
index 6530821..44020fb 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -93,6 +93,76 @@ let rec fields (f : Form.t) (items : Form.t list) : Ast.field list =
     Loc.fail odd.loc "field %s has no type — these come in name/type pairs"
       (Form.to_string odd)
 
+(* ── The constraint map at the head of a defn body ──────────────────────
+   [(defn sort! [s [$t]] () {:where (ordered? $t)} body ...)]. Clojure's
+   [{:pre [...] :post [...]}] is the precedent and the reason it is a map
+   rather than a bare keyword: it leaves room for further keys without new
+   syntax.
+
+   **The disambiguation, since it is the one syntax question the feature had
+   to settle.** [{K V}] is a legal *return type* spelling for [(Map K V)], so
+   [(defn f [xs [$t]] {string i32} {:where ...} body)] puts two braces in a
+   row meaning different things. They are told apart structurally, by the
+   first form inside: a constraint map leads with a *keyword*, and a map type
+   leads with a type — [{string i32}], [{K V}] — and a keyword is not a type
+   anywhere in the language. So [Map ({v = Kw _} :: _)] in the slot after the
+   return type is a constraint map and nothing else can be. The return-type
+   slot itself is never ambiguous: [Parse] takes it unconditionally, before
+   this is consulted. [{K V}] stays exactly as it was — whether it survives is
+   a separate open question, and this feature does not force it.
+
+   A bare [{}] in *expression* position is already refused ([expr] below), so
+   there is also nothing for a constraint map to be confused with once past
+   the return type. *)
+let constraints (body : Form.t list) : Ast.pred list * Form.t list =
+  match body with
+  | ({ Form.v = Form.Map (({ Form.v = Form.Kw _; _ } :: _ as kvs)); _ } as m)
+    :: rest ->
+    let pred (p : Form.t) =
+      match p.Form.v with
+      (* [$t] at a predicate, not bare [t]: the clause talks about the
+         variable the signature *bound*, and writing it the way the signature
+         wrote it is the one spelling that cannot be read as a concrete type
+         that happens to share the name. *)
+      | Form.List [ { Form.v = Form.Sym name; _ };
+                    { Form.v = Form.Sym v; loc = vloc } ]
+        when String.length v > 1 && v.[0] = '$' ->
+        ignore vloc;
+        { Ast.pname = name; pvar = String.sub v 1 (String.length v - 1);
+          ploc = p.Form.loc }
+      | _ ->
+        Loc.fail p.Form.loc
+          "a where predicate is (name? $t), one predicate about one type \
+           variable — found %s" (Form.to_string p)
+    in
+    let rec keys = function
+      | [] -> []
+      | { Form.v = Form.Kw "where"; _ } :: v :: rest ->
+        (match v.Form.v with
+         (* A vector, because two predicates on one variable is the ordinary
+            case — [{:where [(ordered? $t) (copyable? $t)]}] is what a
+            comparing generic that also reads its parameter twice needs. One
+            predicate on its own is accepted unwrapped, which is the same
+            sugar [:pre] does not have and is worth the line it costs. *)
+         | Form.Vec ps -> List.map pred ps
+         | _ -> [ pred v ])
+        @ keys rest
+      | { Form.v = Form.Kw k; loc } :: _ :: rest ->
+        Loc.fail loc
+          "%s is not a key a defn's constraint map takes; :where is the only \
+           one" (":" ^ k)
+        |> fun () -> keys rest
+      | odd :: _ ->
+        Loc.fail odd.Form.loc
+          "a constraint map is keyword/value pairs — found %s"
+          (Form.to_string odd)
+    in
+    if List.length kvs mod 2 <> 0 then
+      Loc.fail m.Form.loc "a constraint map is keyword/value pairs, and this \
+                           one has an odd number of forms";
+    (keys kvs, rest)
+  | _ -> ([], body)
+
 (* ── Expressions ───────────────────────────────────────────────────── *)
 
 let rec expr (f : Form.t) : Ast.expr =
@@ -782,8 +852,9 @@ let rec decl (f : Form.t) : Ast.decl =
              "%s. This is the return type, which every defn states -- a \
               function that returns nothing writes ()" msg
        in
+       let fwhere, body = constraints body in
        mk (Ast.Defn { Ast.name = sym n; params = fields f ps;
-                      ret = Some rty; fbody = body_of body;
+                      ret = Some rty; fwhere; fbody = body_of body;
                       nloc = n.loc })
      | _ ->
        fail f
@@ -814,10 +885,11 @@ let rec decl (f : Form.t) : Ast.decl =
        (match List.rev rest with
         | [ n; { v = Form.Vec ps; _ } ] ->
           mk (mkd { Ast.name = sym n; params = fields f ps;
-                    ret = None; fbody = []; nloc = n.loc } csym)
+                    ret = None; fwhere = []; fbody = []; nloc = n.loc } csym)
         | [ n; { v = Form.Vec ps; _ }; r ] ->
           mk (mkd { Ast.name = sym n; params = fields f ps;
-                    ret = Some (texpr r); fbody = []; nloc = n.loc } csym)
+                    ret = Some (texpr r); fwhere = []; fbody = [];
+                    nloc = n.loc } csym)
         | _ -> fail f "%s" usage)
      | _ -> fail f "%s" usage)
 
@@ -873,7 +945,8 @@ let rec decl (f : Form.t) : Ast.decl =
                params = [ { Ast.fname = sym p;
                             fty = { Ast.t = Ast.Tslice form_t; tloc = p.loc };
                             floc = p.loc } ];
-               ret = Some form_t; fbody = body_of body; nloc = n.loc })
+               ret = Some form_t; fwhere = []; fbody = body_of body;
+               nloc = n.loc })
      | _ :: { v = Form.Vec ps; _ } :: body when body <> [] ->
        List.iter (fun (p : Form.t) -> ignore (sym p)) ps;
        fail f
diff --git a/spike/generics/prelude-shapes.flan b/spike/generics/prelude-shapes.flan
index b17b777..a53425e 100644
--- a/spike/generics/prelude-shapes.flan
+++ b/spike/generics/prelude-shapes.flan
@@ -3,6 +3,7 @@
 ;; prelude; it is the same bodies, over $t, checked and run.
 
 (defn keep [s [$t] keep? (Fn [$t] bool)] (Vec $t)
+  {:where (copyable? $t)}
   (let [v (vec-new t)]
     (dotimes [i (len s)]
       (when (keep? (at s i))
@@ -14,6 +15,7 @@
     (set (at s i) (f (at s i)))))
 
 (defn fold [s [$t] init $t f (Fn [$t $t] $t)] t
+  {:where (copyable? $t)}
   (let [acc init]
     (dotimes [i (len s)]
       (set acc (f acc (at s i))))

From b438a71031d0805d495ca121fb65a9a0406fc552 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 14:37:55 +0700
Subject: [PATCH 07/11] C-c C-c on a generic installs its copies, and a refusal
 about one says where it came from

A generic defn produces no Tast.fn, so the editor was told nothing had
been installed and nothing had gone wrong. eval now expands a redefined
generic name to its copies, and picks up any copy the running process
was never built with - which is how a redefined caller reaching a
generic at a new element type gets that copy built and loaded.

C-x C-e is the path that could really go stale, and did: it checks
against the live environment, so an expression naming a generic at an
unused type generated a copy that existed in no program and the thunk
called a symbol nothing defined. Marked and spliced.

There was no cache to invalidate. program_with_env builds a fresh env
every evaluation, so the instantiation cache cannot survive one; the
test pins that rather than inventing machinery for it.

A signature change reaches the session as a refusal about put!-i32, a
name the source does not contain. It now says which generic it is a
copy of, at which types, and that every copy changed together.
---
 lib/check.ml                      |  48 ++++++++++
 lib/session.ml                    | 102 +++++++++++++++++++--
 test/programs/reload-generic.flan |  39 +++++++++
 test/test_session.ml              | 141 ++++++++++++++++++++++++++++++
 4 files changed, 322 insertions(+), 8 deletions(-)
 create mode 100644 test/programs/reload-generic.flan

diff --git a/lib/check.ml b/lib/check.ml
index 305b1d8..6bd480e 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -5540,6 +5540,54 @@ let program (decls : Ast.decl list) : Tast.program =
 let program_all (decls : Ast.decl list) : Tast.program =
   fst (build_program ~keep_going:true decls)
 
+(* ── What a session needs to know about instantiations ──────────────────
+   A generic [defn] never reaches [Tast.fns] — only its copies do — so the
+   editor's [C-c C-c], which installs the bodies named by the form it was
+   sent, would install nothing at all for a generic. These are what
+   [Session.eval] expands the name with. They are here rather than there
+   because [env]'s tables are the only record that a symbol was ever generic:
+   past this module an instantiation is an ordinary function and nothing knows
+   it was written once. *)
+
+(* Is this name a generic definition rather than an ordinary one? *)
+let is_generic env n = Hashtbl.mem env.gsigs n
+
+(* Every copy of [gname] this check produced, by symbol. Transitivity needs no
+   walk: a whole-program check has already generated every copy every call
+   site asked for, including the ones a generic pulled in by calling another
+   generic at its own variable. *)
+let instantiations env gname =
+  match Hashtbl.find_opt env.insts gname with
+  | None -> []
+  | Some l -> List.rev_map (fun (_, _, sym) -> sym) !l
+
+(* The generic a symbol came from, and the types it was asked for — [None] for
+   an ordinary function. What a refusal about [sort!-i32] needs in order to
+   say which line the programmer should look at, since [sort!-i32] appears
+   nowhere in the source. *)
+let instantiation_origin env sym =
+  Hashtbl.fold
+    (fun gname l acc ->
+       match acc with
+       | Some _ -> acc
+       | None ->
+         (match List.find_opt (fun (_, _, s) -> String.equal s sym) !l with
+          | Some (ps, _, _) -> Some (gname, ps)
+          | None -> None))
+    env.insts None
+
+(* Checking one expression against a live session can *generate* a copy: the
+   first [C-x C-e] of [(id 3)] instantiates [id] at [i32] and the copy is in
+   [env.instances] and in no program anywhere. Without these two the module
+   that gets built calls a symbol it never defined. A mark before and the
+   difference after is the whole protocol. *)
+let instance_mark env = List.length env.instances
+
+let instances_since env mark =
+  let fresh = List.length env.instances - mark in
+  List.rev
+    (List.filteri (fun i _ -> i < fresh) env.instances)
+
 (* One expression, checked against a program that is already running. The
    frame is empty — a REPL expression has no parameters and no enclosing
    function — so the slots it needs are whatever its own [let]s allocate. *)
diff --git a/lib/session.ml b/lib/session.ml
index 3218d1e..1fe1103 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -128,7 +128,8 @@ let known t n =
 (* Everything here is a change that would load cleanly and then be wrong. The
    house rule (NEXT.md, Watch for) says recognise it and refuse with the
    reason, so each one names what it would have broken. *)
-let compatible ~loc (old_ : Tast.program) (new_ : Tast.program) =
+let compatible ?(origin = fun _ -> None) ~loc (old_ : Tast.program)
+    (new_ : Tast.program) =
   let find_fn p n =
     List.find_opt (fun (f : Tast.fn) -> String.equal f.Tast.name n) p.Tast.fns
   in
@@ -154,15 +155,46 @@ let compatible ~loc (old_ : Tast.program) (new_ : Tast.program) =
             until they do, rather than becoming a silent mismatch. See
             plan.org, Hot reload, and open decision #6. *)
          if not same then
+           (* ── When the name is not one the programmer wrote ──────────────
+              A generic's instantiations are named [sort!-i32], [sort!-f32]
+              and so on, and the mangling carries only the *type variables*
+              — so editing the generic's other parameters changes every copy's
+              signature at once, under the same names. The refusal then
+              arrives about [sort!-i32], which appears nowhere in the file
+              being edited, for a reason invisible at the edited line.
+
+              So the refusal says where the name came from: which generic, at
+              which types, and that every copy changed together. The
+              programmer's next move is a restart either way — the point is
+              that they can tell *why* without going looking for a function
+              that does not exist in the source.
+
+              Note what does *not* come through here: adding or removing a
+              [where] clause changes no signature at all. It changes which
+              call sites are legal, and those refusals land at the call sites,
+              in the checker, before this is ever reached. *)
+           let what, note =
+             match origin f.Tast.name with
+             | None -> f.Tast.name, ""
+             | Some (gname, tys) ->
+               ( Printf.sprintf "%s, the copy of the generic %s at %s"
+                   f.Tast.name gname
+                   (String.concat ", " (List.map Types.to_string tys)),
+                 Printf.sprintf
+                   " Editing %s changed every copy of it at once, so this \
+                    refusal is about a function the source does not name."
+                   gname )
+           in
            fail loc
              "%s changes signature, from (Fn [%s] %s) to (Fn [%s] %s); \
               the calls already compiled into the running program pass the old \
-              one. Restart to change it."
-             f.Tast.name
+              one.%s Restart to change it."
+             what
              (String.concat " " (List.map Types.to_string g.Tast.params))
              (Types.to_string g.Tast.ret)
              (String.concat " " (List.map Types.to_string f.Tast.params))
-             (Types.to_string f.Tast.ret))
+             (Types.to_string f.Tast.ret)
+             note)
     new_.Tast.fns;
   List.iter
     (fun (g : Tast.global) ->
@@ -354,9 +386,29 @@ let eval ?(origin = "<eval>") ?pause t src : change =
   (* Nothing above this line has changed the session. A [Loc.Error] from here
      leaves it exactly as it was. *)
   let program, env = Check.program_with_env decls in
-  compatible ~loc t.program program;
+  compatible ~origin:(Check.instantiation_origin env) ~loc t.program program;
   compatible_enums ~loc t.decls decls;
-  let fns =
+  (* ── The bodies to install ────────────────────────────────────────────
+     The names the form declared that have a body in the checked program —
+     and, for a generic, the bodies its *copies* have, because a generic
+     [defn] never reaches [Tast.fns] at all. Without the second clause
+     [C-c C-c] on a generic reports [installs=false, fns=[]]: it installs
+     nothing and says nothing went wrong, which is the feature being unusable
+     in the loop the project exists for.
+
+     Transitivity is free. The check above was a whole-program check, so
+     [env.insts] already holds every copy every call site asked for, including
+     the ones a redefined generic pulled in by calling another generic at its
+     own variable.
+
+     The third clause is the one that makes a redefinition reach a type the
+     process was never built with. Redefining a *caller* so that it uses a
+     generic at a new element type generates a brand-new symbol the host has
+     never had — it is not [known t] and no name in [names] mentions it — so
+     it has to be found by being an instantiation that the running process
+     lacks. [Emit.redefinition] then writes it as a new by-name cell, which is
+     the same path a [defn] the process was never built with already takes. *)
+  let declared_fns =
     List.filter
       (fun n ->
          List.exists
@@ -364,6 +416,26 @@ let eval ?(origin = "<eval>") ?pause t src : change =
            program.Tast.fns)
       names
   in
+  let from_generics =
+    List.concat_map
+      (fun n ->
+         if Check.is_generic env n then Check.instantiations env n else [])
+      names
+  in
+  let new_instances =
+    List.filter_map
+      (fun (f : Tast.fn) ->
+         if known t f.Tast.name then None
+         else
+           match Check.instantiation_origin env f.Tast.name with
+           | Some _ -> Some f.Tast.name
+           | None -> None)
+      program.Tast.fns
+  in
+  let fns =
+    List.sort_uniq String.compare
+      (declared_fns @ from_generics @ new_instances)
+  in
   (* A constant that changed and can be published: known to the host, not
      consumed by the checker. The module stores its new value at the frame
      boundary, exactly as it stores a new function body. *)
@@ -1010,7 +1082,15 @@ let eval_expr ?(origin = "<eval>") ?(pause = false) t src : change =
         Ast.loc = parsed.Ast.loc }
     else parsed
   in
+  (* Checking against the live environment can *generate* code: the first
+     [C-x C-e] of a call to a generic at a type nothing has used yet
+     instantiates it here, and the copy lands in [t.env] and in no program
+     anywhere. Marked before and collected after, and spliced into the module
+     below — without this the thunk calls a symbol the module never defines
+     and the host has no cell for. *)
+  let mark = Check.instance_mark t.env in
   let checked, base, bnames = Check.expression t.env parsed in
+  let fresh = Check.instances_since t.env mark in
   (* The thunk's frame starts at whatever [Check.expression] needed and grows
      as the walk finds slices in it, so the slots the renderer asks for are
      appended past [base] and collected here to size the frame below. *)
@@ -1047,15 +1127,21 @@ let eval_expr ?(origin = "<eval>") ?(pause = false) t src : change =
      for every expression ever typed. *)
   let program =
     { t.program with
-      Tast.fns = t.program.Tast.fns @ [ thunk ];
+      Tast.fns = t.program.Tast.fns @ fresh @ [ thunk ];
       externs = t.program.Tast.externs @ externs }
   in
+  (* The copies stay in the session's program, unlike the thunk: the thunk is
+     not a declaration and there is nothing to keep, but a copy that has been
+     built and loaded *is* part of the running process from here on, and
+     forgetting it would generate a second one under the same name at the next
+     evaluation. *)
+  t.program <- { t.program with Tast.fns = t.program.Tast.fns @ fresh };
   let ir =
     (* The thunk gets debug info on the same flag as everything else. It is a
        function nobody sets a breakpoint on by name, but it is a frame on the
        stack when the expression signals, and a frame the debugger cannot name
        is the thing the conditions buffer is trying to stop showing. *)
     Emit.redefinition ~dev:true ~debug:t.debug ~known:(known t) ~call:name
-      program ~fns:[ name ]
+      program ~fns:(List.map (fun (f : Tast.fn) -> f.Tast.name) fresh @ [ name ])
   in
   { ir; names = []; fns = []; installs = true }
diff --git a/test/programs/reload-generic.flan b/test/programs/reload-generic.flan
new file mode 100644
index 0000000..3e7db4a
--- /dev/null
+++ b/test/programs/reload-generic.flan
@@ -0,0 +1,39 @@
+;;;; The session's fixture for generics in the dev loop.
+;;;;
+;;;; A generic [defn] never reaches [Tast.fns] — only its copies do — so every
+;;;; question the editor asks about one has to be answered by expanding the
+;;;; name. This file is the smallest program that makes each of those
+;;;; questions concrete: one generic used at two element types, one generic
+;;;; that calls another so that instantiation has to be transitive, and one
+;;;; call site whose element type is *not* used anywhere else, so that a
+;;;; redefinition can reach a copy the process was never built with.
+
+(defvar counter i64)
+
+(defn put! [xs [$t] i i32 v $t] ()
+  {:where (copyable? $t)}
+  (set (at xs i) v))
+
+;;; Calls [put!] at its own variable, so the copy of [put!] is generated when
+;;; [hold!] is instantiated and not before.
+(defn hold! [xs [$t] v $t] ()
+  {:where (copyable? $t)}
+  (put! xs 0 v))
+
+(defn pick [xs [$t]] $t
+  {:where (ordered? $t)}
+  (let [m (at xs 0)]
+    (dotimes [i (len xs)]
+      (set m (min m (at xs i))))
+    m))
+
+(defn step [] ()
+  (let [ns [5 3 9 1]
+        fs [2.5 0.5 1.5]]
+    (hold! (slice ns 0 4) 7)
+    (hold! (slice fs 0 3) 0.25)
+    (set counter (+ counter (i64 (pick (slice ns 0 4)))))))
+
+(defn main [] ()
+  (step)
+  (println counter))
diff --git a/test/test_session.ml b/test/test_session.ml
index 2bce7b3..413bd0b 100644
--- a/test/test_session.ml
+++ b/test/test_session.ml
@@ -265,6 +265,147 @@ let () =
   if has str.Session.ir "@flan_reload_transient" then
     fail "an expression holding a string claimed to be unloadable";
 
+  (* ── Generics in the dev loop ─────────────────────────────────────────
+     A generic [defn] produces no [Tast.fn] of its own — only its copies do —
+     so every one of these is a question the editor asks that the ordinary
+     name-to-body path cannot answer. *)
+  let gen () = fst (Session.create ~file:"programs/reload-generic.flan" ()) in
+
+  (* 1. [C-c C-c] on a generic used to report [installs=false, fns=[]]: it
+     installed nothing and did not say anything had gone wrong. Both copies
+     have to be named, and the copy of [put!] that [hold!] pulls in has to be
+     there too, which is transitivity. *)
+  (match Session.eval (gen ()) "(defn hold! [xs [$t] v $t] () {:where (copyable? $t)} (put! xs 0 v) (put! xs 0 v))" with
+   | c ->
+     if not c.Session.installs then
+       fail "redefining a generic installed nothing";
+     List.iter
+       (fun want ->
+          if not (List.mem want c.Session.fns) then
+            fail "redefining a generic did not install %s; it installed %s"
+              want (String.concat " " c.Session.fns))
+       [ "hold!-i32"; "hold!-f64" ];
+     (* And only its own copies: [put!] did not change, and its copies are
+        reached through their cells, so reinstalling them would be work with
+        no effect. *)
+     if List.mem "put!-i32" c.Session.fns then
+       fail "redefining a generic reinstalled an unchanged generic's copies"
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     fail "redefining a generic: %s" m);
+
+  (* The callee side of the same rule: redefining [put!] reinstalls the copies
+     of [put!], which exist only because [hold!] asked for them — the
+     instantiation that generated them was transitive, and finding them again
+     is one table lookup rather than a walk, because a whole-program check has
+     already regenerated all of them. *)
+  (match Session.eval (gen ()) "(defn put! [xs [$t] i i32 v $t] () {:where (copyable? $t)} (set (at xs i) v))" with
+   | c ->
+     List.iter
+       (fun want ->
+          if not (List.mem want c.Session.fns) then
+            fail "redefining a called generic did not install %s; it \
+                  installed %s" want (String.concat " " c.Session.fns))
+       [ "put!-i32"; "put!-f64" ]
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     fail "redefining a generic: %s" m);
+
+  (* 2. Staleness, and the answer is that there is none to have. The
+     instantiation cache lives in the [Check.env] that [Check.program_with_env]
+     builds *fresh* on every evaluation, so a redefined generic's copies are
+     regenerated from the new body and there is no cached copy of the old one
+     anywhere to invalidate. Pinned here because the alternative — a cache that
+     survived between evaluations — would make [C-c C-c] appear to succeed
+     while the program kept running the old body, which is the quiet version
+     of failure (1). *)
+  (let t = gen () in
+   let c =
+     Session.eval t
+       "(defn pick [xs [$t]] $t {:where (ordered? $t)} (let [m (at xs 0)] \
+        (dotimes [i (len xs)] (set m (max m (at xs i)))) m))"
+   in
+   if not (List.mem "pick-i32" c.Session.fns) then
+     fail "redefining a generic did not reinstall pick-i32";
+   (* The new body is the one that got emitted, not a cached copy of the old:
+      [max] lowers to a [>] where [min] lowered to a [<]. *)
+   if not (has c.Session.ir "icmp sgt") then
+     fail "the reinstalled copy carried the old body";
+   (* And again, to show the second evaluation is not served from a cache the
+      first one left behind. *)
+   let c2 = Session.eval t "(defn pick [xs [$t]] $t {:where (ordered? $t)} (at xs 0))" in
+   if not (List.mem "pick-i32" c2.Session.fns) then
+     fail "a second redefinition of a generic installed nothing");
+
+  (* 3. A redefinition that needs a copy the process was never built with. The
+     fixture never calls [pick] at f64, so [pick-f64] exists in no program
+     anywhere; redefining the *caller* to ask for it has to build and install
+     it. Nothing in the form names [pick-f64] — it is found by being an
+     instantiation the host lacks. *)
+  (match
+     Session.eval (gen ())
+       "(defn step [] () (let [ns [5 3 9 1] fs [2.5 0.5 1.5]] \
+        (set counter (+ counter (i64 (pick (slice ns 0 4)))) ) \
+        (set counter (+ counter (i64 (pick (slice fs 0 3)))))))"
+   with
+   | c ->
+     if not (List.mem "pick-f64" c.Session.fns) then
+       fail "a redefinition needing a new instantiation did not install \
+             pick-f64; it installed %s" (String.concat " " c.Session.fns)
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     fail "a redefinition needing a new instantiation: %s" m);
+
+  (* 4. A signature change on a generic is refused, and the refusal is about a
+     name the source does not contain: the mangling carries only the type
+     variables, so every copy changes signature at once and under the same
+     name. It has to say where that name came from. *)
+  (* The change has to be one the *checker* accepts, which is the narrow case
+     and worth saying why. A generic whose arity or variable positions move is
+     refused at its call sites, in the checker, with the call site's own
+     location — a better error than this one and the reason this path is
+     reached less often than it looks. What reaches here is a change every
+     call site still accepts and every *copy* does not: widening the index
+     from i32 to i64 leaves [(put! xs 0 v)] checking, because the literal
+     adapts, and changes [put!-i32]'s signature underneath every compiled
+     caller. *)
+  (match
+     Session.eval (gen ())
+       "(defn put! [xs [$t] i i64 v $t] () {:where (copyable? $t)} \
+        (set (at xs (i32 i)) v))"
+   with
+   | _ -> fail "a generic's changed parameter type was accepted"
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     if not (has m "changes signature") then
+       fail "a generic's changed parameter type: %S" m;
+     if not (has m "the copy of the generic put!") then
+       fail "the refusal did not say the name came from put!: %S" m;
+     if not (has m "every copy of it at once") then
+       fail "the refusal did not say every copy changed together: %S" m);
+
+  (* And what is *not* refused, which the notes expected to be: adding a
+     [where] clause changes no signature at all. What it changes is which call
+     sites are legal, and an illegal one is a checker refusal at the call site
+     long before the session is asked anything. *)
+  (match
+     Session.eval (gen ())
+       "(defn pick [xs [$t]] $t {:where [(ordered? $t) (copyable? $t)]} (at xs 0))"
+   with
+   | c ->
+     if not (List.mem "pick-i32" c.Session.fns) then
+       fail "adding a where predicate did not reinstall the copies"
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     fail "adding a where predicate was refused: %s" m);
+
+  (* [C-x C-e] checks against the *live* environment rather than re-checking
+     the program, so an expression that instantiates a generic at a type
+     nothing has used generates a copy that exists in no program. The module
+     has to carry it, or the thunk calls a symbol nothing defines. *)
+  (let t = gen () in
+   match Session.eval_expr t "(println (pick (slice [1.5 0.5] 0 2)))" with
+   | e ->
+     if not (has e.Session.ir "pick-f64") then
+       fail "an expression that instantiated a generic did not carry the copy"
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     fail "an expression that instantiates a generic: %s" m);
+
   if !failures = 0 then print_endline "session: all tests passed"
   else begin
     Printf.printf "\n%d failure(s)\n" !failures;

From dad725afe477747a5768ae9e35e199cff1b0614c Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 14:49:11 +0700
Subject: [PATCH 08/11] The prelude's per-type families collapse: 22 functions
 become 10, 27 become 16

swap!, reverse!, sort!, sort-by!, index-of, min-of, max-of, map!,
reduce and filter, each written once over $t. Every call site in the
corpus moves with them.

min-of and max-of are not min and max because min and max are builtins
over two or more numbers and nothing shadows a builtin. These reduce a
slice, which is a different operation at a different arity.

sort-bytes! did not collapse into sort!, and the reason is the point of
the predicates: a [u8] is not ordered? and cannot be, because < is an
instruction and comparing two slices lexicographically is a loop. It is
sort-by! with bytes<? written in, one line, keeping its name and its
stability note. sum-i32/sum-f32 and append-i64!/append-f64! stay for the
reasons the spike gave.

Not what the notes predicted: none of the ten collapses on a signature
change alone. filter and reduce need copyable? because the checker
demands it - reduce's accumulator at (Vec i32) is a double move - and
the rest declare it because a slice of owning elements would have them
duplicating headers.
---
 lib/check.ml                       |  36 ++-
 lib/prelude.ml                     | 349 +++++++++++++----------------
 test/programs/algorithms.flan      |  26 +--
 test/programs/fn-values.flan       |  10 +-
 test/programs/generic-reject.flan  |  15 ++
 test/programs/generic-runaway.flan |  10 +
 test/programs/generics.flan        | 105 +++++++++
 test/programs/higher-order.flan    |  20 +-
 test/programs/reach-walk.flan      |   6 +-
 test/programs/slices.flan          |  28 +--
 test/programs/text.flan            |   6 +-
 test/test_acceptance.ml            |  25 +++
 test/test_flan.ml                  |  80 +++++++
 vendor/edn/edn.flan                |   2 +-
 web/examples/option.flan           |   4 +-
 15 files changed, 480 insertions(+), 242 deletions(-)
 create mode 100644 test/programs/generic-reject.flan
 create mode 100644 test/programs/generic-runaway.flan
 create mode 100644 test/programs/generics.flan

diff --git a/lib/check.ml b/lib/check.ml
index 6bd480e..99b8955 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -4756,14 +4756,46 @@ and generic_call ctx ~want loc name vars pats pret args =
     vars;
   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
+  if List.exists generic_ty cparams || generic_ty cret then begin
     (* One generic function calling another at its *own* variable, seen from
        the abstract pass over the caller's body — [sort-by!] calling [swap!]
        at [t]. There is no copy to make yet: [t] is not a type. The node is
        built so the call still type-checks and is thrown away with the rest of
        the abstract pass; the real copy is generated when the caller is
-       instantiated and the same call site resolves [t] to a concrete type. *)
+       instantiated and the same call site resolves [t] to a concrete type.
+
+       But the callee's [where] clause is answerable here, and has to be. The
+       whole promise of the abstract pass is that a generic's refusals arrive
+       at its definition; if the predicate were left to the instantiation,
+       [(defn f [x $t] () (sort! [x]))] would be accepted at its definition
+       and refused at whichever call site first instantiated it — a refusal in
+       code the caller did not write, which is the thing the pass exists to
+       avoid. So the caller has to declare at least what the callee asks for,
+       and [pred_entails] means [ordered?] covers a callee wanting
+       [copyable?] without anyone writing both. *)
+    (match Hashtbl.find_opt ctx.env.generics name with
+     | None -> ()
+     | Some gfn ->
+       List.iter
+         (fun (p : Ast.pred) ->
+            match List.assoc_opt p.Ast.pvar !subst with
+            | Some (Types.Var v) when not (declares ctx.env.tvpreds v p.Ast.pname) ->
+              Loc.failk "check/predicate-not-carried" loc
+                "%s is written {:where (%s $%s)}, and this call passes the \
+                 type variable %s, which nothing here declares %s. Add \
+                 {:where (%s $%s)} to this function's own clause — a \
+                 predicate a body relies on has to be carried by every \
+                 signature between it and the call site"
+                name p.Ast.pname p.Ast.pvar v p.Ast.pname p.Ast.pname v
+            | Some t when not (generic_ty t) && not (pred_holds p.Ast.pname t) ->
+              Loc.failk "check/predicate-unsatisfied" loc
+                "%s is written {:where (%s $%s)}, and this call passes %s, \
+                 which is not %s"
+                name p.Ast.pname p.Ast.pvar (Types.to_string t) p.Ast.pname
+            | _ -> ())
+         gfn.Ast.fwhere);
     expect loc ~want (mk loc cret (Tast.Call (name, targs)))
+  end
   else
     let sym = instantiate ctx.env loc name vars !subst cparams cret in
     expect loc ~want (mk loc cret (Tast.Call (sym, targs)))
diff --git a/lib/prelude.ml b/lib/prelude.ml
index 4184cb5..553014f 100644
--- a/lib/prelude.ml
+++ b/lib/prelude.ml
@@ -145,37 +145,109 @@ let source = {flan|
 ;; shape and the same argument — so the set is the same i32 and f32 the rest of
 ;; this family covers.
 
-(defn swap-i32! [s [i32]  i i32  j i32] ()
+;; ── One family, over one type variable ────────────────────────────────
+;;
+;; What used to be a copy per element type. A [$t] binds a type variable in
+;; the signature and every call site instantiates the body at the types it
+;; passes, so [(sort! xs)] over a [i32] and over a [f32] are two emitted
+;; bodies from one written one.
+;;
+;; **Two things in the signatures are not decoration.**
+;;
+;; [{:where (ordered? $t)}] is what lets the body write [<] at all. A type
+;; variable supports only what it is declared to support — an unconstrained
+;; one is refused at the *definition*, not at some later call site — and
+;; [ordered?] is the predicate that admits [<], [<=], [>], [>=], [min] and
+;; [max]. It admits [=] and [copyable?] too: every type the language orders is
+;; a number or an enum, so it is equatable and it is not move-only.
+;;
+;; [{:where (copyable? $t)}] is the opt-out from the other default. A type
+;; variable is **move-only** until it says otherwise, because move is the
+;; stricter rule and assuming it can only refuse a valid program rather than
+;; admit a broken one: [reduce]'s accumulator is read into [f] and then
+;; assigned again, which is correct at [i32] and a double move at [(Vec i32)],
+;; and the checker cannot tell which until it substitutes. So the ones that
+;; hold an element in a local say [copyable?] and the ones that only move
+;; elements between slots do not.
+;;
+;; **What did not collapse, and why it should not.** [sum-i32] and [sum-f32]
+;; widen their element into [i64] and [f64]; "the wider type $t accumulates
+;; into" is a type-level function, which is a constraint system of a different
+;; kind, and a generic [sum] that took its accumulator and its [+] would just
+;; be [reduce]. [append-i64!] and [append-f64!] are two different primitives.
+;; [sort-bytes!] needs [bytes<?] rather than [<] — a [[u8]] is not [ordered?]
+;; and cannot be — so it is [sort-by!] with the comparison written in, and it
+;; keeps its name because the stability contract in its comment is worth
+;; keeping attached to something.
+
+(defn swap! [s [$t]  i i32  j i32] ()
+  {:where (copyable? $t)}
   (let [t (at s i)]
     (set (at s i) (at s j))
     (set (at s j) t)))
 
-(defn reverse-i32! [s [i32]] ()
+(defn reverse! [s [$t]] ()
+  {:where (copyable? $t)}
   (let [i 0
         j (- (len s) 1)]
     (while (< i j)
-      (swap-i32! s i j)
+      (swap! s i j)
       (set i (+ i 1))
       (set j (- j 1)))))
 
-;; Insertion sort: in place, no recursion, no auxiliary array and no
-;; comparison function — quicksort would want a stack and mergesort a buffer,
-;; and neither exists. Ascending, and stable, though with no payload type to
-;; carry that is not yet observable.
-(defn sort-i32! [s [i32]] ()
+;; Insertion sort: in place, no recursion, no auxiliary array — quicksort
+;; would want a stack and mergesort a buffer, and neither exists. Ascending,
+;; and stable, though with no payload type to carry that is not yet
+;; observable.
+;;
+;; One caveat that only arises at f32: **a NaN in the input makes the order
+;; undefined.** Every comparison against a NaN is false, so the insertion loop
+;; never moves one and never moves anything past one; what comes out is sorted
+;; within each run between NaNs and not sorted across them. That is what C's
+;; qsort with a naive comparator does too, and the only fix is not to have
+;; NaNs in the array — there is no ordering of the reals a NaN sits anywhere
+;; in.
+(defn sort! [s [$t]] ()
+  {:where (ordered? $t)}
   (let [i 1]
     (while (< i (len s))
       (let [j i]
         ;; `and` short-circuits, which is load-bearing: at j = 0 the left test
         ;; fails and (at s -1) is never evaluated, so this does not trap.
         (while (and (> j 0) (> (at s (- j 1)) (at s j)))
-          (swap-i32! s (- j 1) j)
+          (swap! s (- j 1) j)
+          (set j (- j 1))))
+      (set i (+ i 1)))))
+
+;; The same insertion sort, with the one comparison it had written in replaced
+;; by the one it is told. before? answers "does a come before b", so passing
+;; (fn [a b] (< a b)) is ascending and reversing it is descending — and a
+;; caller wanting a key rather than an order writes the comparison.
+;;
+;; It is stable exactly as sort! is: the loop stops the moment before? says
+;; no, so equal elements never swap past each other. A before? that is not a
+;; strict weak ordering — one answering true for both (a b) and (b a) — is the
+;; caller's mistake and shows up as an order, not as a loop: the inner while
+;; is bounded by j reaching 0 whatever the comparison says.
+;;
+;; This one needs no [ordered?]: the comparison it cannot have is the
+;; comparison it is given. It is the shape every generic had to take before
+;; predicates existed, and it stays because passing a comparison is a real
+;; thing to want and not only a workaround.
+(defn sort-by! [s [$t]  before? (Fn [$t $t] bool)] ()
+  {:where (copyable? $t)}
+  (let [i 1]
+    (while (< i (len s))
+      (let [j i]
+        (while (and (> j 0) (before? (at s j) (at s (- j 1))))
+          (swap! s (- j 1) j)
           (set j (- j 1))))
       (set i (+ i 1)))))
 
 ;; The first index holding x. None rather than -1, because Option is what the
 ;; language has and a sentinel index is the bug this avoids.
-(defn index-of-i32 [s [i32]  x i32] (Option i32)
+(defn index-of [s [$t]  x $t] (Option i32)
+  {:where (equal? $t)}
   (dotimes [i (len s)]
     (when (= (at s i) x)
       (return (Some i))))
@@ -183,8 +255,16 @@ let source = {flan|
 
 ;; None for an empty slice: there is no least i32 that is also an honest
 ;; answer, and returning one would be a value the caller cannot tell from a
-;; real element.
-(defn min-i32 [s [i32]] (Option i32)
+;; real element. A NaN in the input is not special-cased and propagates the
+;; way it does through the builtins — the comparison fails, so the running
+;; value simply does not change.
+;;
+;; Named min-of rather than min because [min] and [max] are builtins over two
+;; or more numbers, and a defn cannot shadow a builtin: nothing shadows [+]
+;; either. These reduce a slice, which is a different operation with a
+;; different arity, so the different name is honest rather than a workaround.
+(defn min-of [s [$t]] (Option $t)
+  {:where (ordered? $t)}
   (if (= (len s) 0)
     None
     (let [m (at s 0)]
@@ -192,7 +272,8 @@ let source = {flan|
         (set m (min m (at s i))))
       (Some m))))
 
-(defn max-i32 [s [i32]] (Option i32)
+(defn max-of [s [$t]] (Option $t)
+  {:where (ordered? $t)}
   (if (= (len s) 0)
     None
     (let [m (at s 0)]
@@ -200,6 +281,54 @@ let source = {flan|
         (set m (max m (at s i))))
       (Some m))))
 
+;; map! writes back into the slice it was handed, for the same reason sort!
+;; does — a slice is non-owning, and transforming a thing you already own
+;; should not allocate. A map that produces a *different* element type is not
+;; here: it is two type variables and a second signature, and nothing has
+;; wanted it.
+(defn map! [s [$t]  f (Fn [$t] $t)] ()
+  {:where (copyable? $t)}
+  (dotimes [i (len s)]
+    (set (at s i) (f (at s i)))))
+
+;; The general fold, of which sum-i32 is the special case with the + written
+;; in. The accumulator comes first in the step, which is the order that reads
+;; as (f acc x) and the order Odin's slice.reduce uses.
+(defn reduce [s [$t]  init $t  f (Fn [$t $t] $t)] $t
+  {:where (copyable? $t)}
+  (let [acc init]
+    (dotimes [i (len s)]
+      (set acc (f acc (at s i))))
+    acc))
+
+;; A new Vec holding the elements the predicate kept, in the order they were
+;; in. Owned by the caller: (free v), or let a (free-all a) take the region.
+;;
+;; This is the one that proves the containers and the generics compose. It
+;; allocates — (vec-new t), push, returns (Vec t) — and the type-erased Vec
+;; runtime needed no change at all, because SizeOf and AlignOf are computed at
+;; the instantiation site, where the element type is concrete.
+(defn filter [s [$t]  keep? (Fn [$t] bool)] (Vec $t)
+  {:where (copyable? $t)}
+  (let [v (vec-new t)]
+    (dotimes [i (len s)]
+      (when (keep? (at s i))
+        (push v (at s i))))
+    v))
+
+;; ── The per-type layer that stays ─────────────────────────────────────
+;;
+;; sum is the one shape a type variable cannot express, and it is worth being
+;; precise about why rather than leaving two near-identical functions looking
+;; like an oversight. Each of these *widens*: sum-i32 accumulates in i64 and
+;; sum-f32 in f64, with an explicit cast per element, because there is no
+;; implicit widening anywhere in the language and summing a screenful into the
+;; element's own type is how a total silently wraps or absorbs. "The wider
+;; type $t accumulates into" is a function from types to types — an associated
+;; type, or a constraint system of a kind {:where} is not — and a generic sum
+;; that took its accumulator and its + as parameters would be reduce, which is
+;; above.
+
 ;; Accumulates in i64 and each element is widened explicitly — there is no
 ;; implicit widening anywhere in the language, and summing a screenful of i32
 ;; into an i32 is how a total silently wraps.
@@ -209,167 +338,19 @@ let source = {flan|
       (set t (+ t (i64 (at s i)))))
     t))
 
-;; ── The same family over f32 ──────────────────────────────────────────
-;;
-;; sort-i32! was the only sort in the language, which is what NEXT.md's second
-;; tier means by "a sort that is not integers-only". This is the second, and it
-;; is a copy and not an abstraction — see the note above on why.
-;;
-;; One caveat that has no counterpart in the i32 family, because it cannot
-;; arise there: **a NaN in the input makes the order undefined.** Every
-;; comparison against a NaN is false, so the insertion loop never moves one and
-;; never moves anything past one; what comes out is sorted within each run
-;; between NaNs and not sorted across them. That is what C's qsort with a naive
-;; comparator does too. The fix is not to have NaNs in the array — which is
-;; also the only fix, since there is no ordering of the reals that a NaN sits
-;; anywhere in.
-
-(defn swap-f32! [s [f32]  i i32  j i32] ()
-  (let [t (at s i)]
-    (set (at s i) (at s j))
-    (set (at s j) t)))
-
-(defn reverse-f32! [s [f32]] ()
-  (let [i 0
-        j (- (len s) 1)]
-    (while (< i j)
-      (swap-f32! s i j)
-      (set i (+ i 1))
-      (set j (- j 1)))))
-
-(defn sort-f32! [s [f32]] ()
-  (let [i 1]
-    (while (< i (len s))
-      (let [j i]
-        (while (and (> j 0) (> (at s (- j 1)) (at s j)))
-          (swap-f32! s (- j 1) j)
-          (set j (- j 1))))
-      (set i (+ i 1)))))
-
-;; None for an empty slice, exactly as min-i32 does. A NaN in the input is not
-;; special-cased and propagates the same way it does through the builtins: the
-;; comparison fails, so the running value simply does not change.
-(defn min-f32 [s [f32]] (Option f32)
-  (if (= (len s) 0)
-    None
-    (let [m (at s 0)]
-      (dotimes [i (len s)]
-        (set m (min m (at s i))))
-      (Some m))))
-
-(defn max-f32 [s [f32]] (Option f32)
-  (if (= (len s) 0)
-    None
-    (let [m (at s 0)]
-      (dotimes [i (len s)]
-        (set m (max m (at s i))))
-      (Some m))))
-
 ;; Accumulates in f64 and widens each element explicitly, which is sum-i32's
-;; argument in its floating form and a stronger one: summing a screenful of f32
-;; in f32 does not wrap, it *absorbs* — once the running total is large enough,
-;; adding a small element rounds to no change at all, and the answer is silently
-;; short rather than obviously wrong. An f64 accumulator has 29 more bits of
-;; mantissa and pushes that failure out of reach of any array a game holds.
+;; argument in its floating form and a stronger one: summing a screenful of
+;; f32 in f32 does not wrap, it *absorbs* — once the running total is large
+;; enough, adding a small element rounds to no change at all, and the answer
+;; is silently short rather than obviously wrong. An f64 accumulator has 29
+;; more bits of mantissa and pushes that failure out of reach of any array a
+;; game holds.
 (defn sum-f32 [s [f32]] f64
   (let [t 0.0]
     (dotimes [i (len s)]
       (set t (+ t (f64 (at s i)))))
     t))
 
-;; ── The ones that take a function ─────────────────────────────────────
-;;
-;; map, filter, reduce and a comparator sort, which were the four the previous
-;; tier could not write. The blocker was function values and not generics, and
-;; the difference shows in what arrived and what did not: these take a
-;; (Fn [T ...] R) as an ordinary parameter and needed nothing else, and they
-;; are still one copy per element type because *that* is the generics half.
-;;
-;; Two rules, both inherited rather than invented here:
-;;
-;; 1. **The in-place ones stay in place.** map! writes back into the slice it
-;;    was handed, for the same reason sort-i32! does — a slice is non-owning,
-;;    and transforming a thing you already own should not allocate. A map that
-;;    produces a *different* element type is not here: it would be one copy per
-;;    ordered pair of types, which is the point at which a per-type family
-;;    stops being honest.
-;; 2. **filter allocates and the caller frees**, like everything in the
-;;    building tier: (free v), or let a (free-all a) take the region.
-;;
-;; The function is passed by name — this is a Lisp-1, so a bare defn name is
-;; the function — or written inline as an (fn [x] ...), whose parameter types
-;; come from the parameter it is being passed to. It may not capture: an fn is
-;; lifted into a function of its own and sees its parameters and the globals
-;; and nothing else.
-
-(defn map-i32! [s [i32]  f (Fn [i32] i32)] ()
-  (dotimes [i (len s)]
-    (set (at s i) (f (at s i)))))
-
-(defn map-f32! [s [f32]  f (Fn [f32] f32)] ()
-  (dotimes [i (len s)]
-    (set (at s i) (f (at s i)))))
-
-;; The general fold, of which sum-i32 is the special case with the + written
-;; in. The accumulator comes first in the step, which is the order that reads
-;; as (f acc x) and the order Odin's slice.reduce uses.
-(defn reduce-i32 [s [i32]  init i32  f (Fn [i32 i32] i32)] i32
-  (let [acc init]
-    (dotimes [i (len s)]
-      (set acc (f acc (at s i))))
-    acc))
-
-(defn reduce-f32 [s [f32]  init f32  f (Fn [f32 f32] f32)] f32
-  (let [acc init]
-    (dotimes [i (len s)]
-      (set acc (f acc (at s i))))
-    acc))
-
-;; A new Vec holding the elements the predicate kept, in the order they were
-;; in. Owned by the caller.
-(defn filter-i32 [s [i32]  keep? (Fn [i32] bool)] (Vec i32)
-  (let [v (vec-new i32)]
-    (dotimes [i (len s)]
-      (when (keep? (at s i))
-        (push v (at s i))))
-    v))
-
-(defn filter-f32 [s [f32]  keep? (Fn [f32] bool)] (Vec f32)
-  (let [v (vec-new f32)]
-    (dotimes [i (len s)]
-      (when (keep? (at s i))
-        (push v (at s i))))
-    v))
-
-;; The same insertion sort sort-i32! is, with the one comparison it had written
-;; in replaced by the one it is told. before? answers "does a come before b",
-;; so passing (fn [a b] (< a b)) is ascending and reversing it is descending —
-;; and a caller wanting a key rather than an order writes the comparison.
-;;
-;; It is stable exactly as sort-i32! is: the loop stops the moment before? says
-;; no, so equal elements never swap past each other. A before? that is not a
-;; strict weak ordering — one answering true for both (a b) and (b a) — is the
-;; caller's mistake and shows up as an order, not as a loop: the inner while is
-;; bounded by j reaching 0 whatever the comparison says.
-(defn sort-i32-by! [s [i32]  before? (Fn [i32 i32] bool)] ()
-  (let [i 1]
-    (while (< i (len s))
-      (let [j i]
-        ;; `and` short-circuits, so (at s -1) is never evaluated at j = 0.
-        (while (and (> j 0) (before? (at s j) (at s (- j 1))))
-          (swap-i32! s (- j 1) j)
-          (set j (- j 1))))
-      (set i (+ i 1)))))
-
-(defn sort-f32-by! [s [f32]  before? (Fn [f32 f32] bool)] ()
-  (let [i 1]
-    (while (< i (len s))
-      (let [j i]
-        (while (and (> j 0) (before? (at s j) (at s (- j 1))))
-          (swap-f32! s (- j 1) j)
-          (set j (- j 1))))
-      (set i (+ i 1)))))
-
 ;; ── Bytes ─────────────────────────────────────────────────────────────
 ;;
 ;; Over [u8] and not over string, so (bytes s) is what a caller writes and one
@@ -397,12 +378,6 @@ let source = {flan|
   (and (<= (len p) (len s))
        (bytes=? (slice s (- (len s) (len p)) (len s)) p)))
 
-(defn index-of-byte [s [u8]  b u8] (Option i32)
-  (dotimes [i (len s)]
-    (when (= (at s i) b)
-      (return (Some i))))
-  None)
-
 ;; The whole slice is an integer, or it is None. bytes->i64 is strtoll, which
 ;; answers 0 for "" and for "abc" and stops at the first junk byte in "12x" —
 ;; three wrong answers a caller cannot tell from a real 12. This is also the
@@ -868,7 +843,7 @@ let source = {flan|
 
 ;; How many bytes this code point encodes to, or None if it is not a scalar
 ;; value. Odin's rune_size answers -1 for the refusals; a sentinel index is
-;; exactly what index-of-i32 avoids above, so this is an Option like the rest
+;; exactly what index-of avoids above, so this is an Option like the rest
 ;; of the file.
 (defn rune-size [code i32] (Option i32)
   (cond
@@ -944,7 +919,7 @@ let source = {flan|
 (defn split-next! [it (Ptr Split)] (Option [u8])
   (when (not (.more it))
     (return None))
-  (match (index-of-byte (.rest it) (.sep it))
+  (match (index-of (.rest it) (.sep it))
     (Some i)
     (let [field (slice (.rest it) 0 i)]
       (set (.rest it) (slice (.rest it) (+ i 1) (len (.rest it))))
@@ -1030,24 +1005,20 @@ let source = {flan|
         (return (< (at a i) (at b i)))))
     (< (len a) (len b))))
 
-(defn swap-bytes! [s [[u8]]  i i32  j i32] ()
-  (let [t (at s i)]
-    (set (at s i) (at s j))
-    (set (at s j) t)))
-
-;; The same insertion sort as sort-i32!, over the same in-place contract: the
-;; *slices* move, never the bytes they point at, so this sorts a [[u8]] of
+;; sort-by! with the comparison written in, over the same in-place contract:
+;; the *slices* move, never the bytes they point at, so this sorts a [[u8]] of
 ;; fields borrowed from one buffer without touching the buffer. Stable, and
 ;; here that is observable — two equal fields are two distinct slices of
 ;; different parts of the input, and a caller can see which one came first.
+;;
+;; It keeps a name of its own rather than collapsing into sort!, and the
+;; reason is the point of the predicates: a [u8] is not ordered? and cannot
+;; be, because < is defined on machine numbers and comparing two slices
+;; lexicographically is a loop and not an instruction. bytes<? is that loop.
+;; So this is the shape a generic takes when the operation it needs is not a
+;; primitive: pass it in.
 (defn sort-bytes! [s [[u8]]] ()
-  (let [i 1]
-    (while (< i (len s))
-      (let [j i]
-        (while (and (> j 0) (bytes<? (at s j) (at s (- j 1))))
-          (swap-bytes! s (- j 1) j)
-          (set j (- j 1))))
-      (set i (+ i 1)))))
+  (sort-by! s (fn [a b] (bytes<? a b))))
 
 ;; ── Building bytes, which is the tier that needed an allocator ────────
 ;;
diff --git a/test/programs/algorithms.flan b/test/programs/algorithms.flan
index 04f3072..847a055 100644
--- a/test/programs/algorithms.flan
+++ b/test/programs/algorithms.flan
@@ -1,6 +1,6 @@
 ;;;; The slice family at its second and third element types.
 ;;;;
-;;;; sort-i32! was the only sort in the language. These are the other two, and
+;;;; sort! was the only sort in the language. These are the other two, and
 ;;;; they are copies rather than an abstraction: map, filter, reduce and a sort
 ;;;; taking a comparator all need a *function value*, which check.ml refuses
 ;;;; with "a function type is not implemented yet -- milestone 5". So the
@@ -22,55 +22,55 @@
 (defn main [] i32
   ;; Every float literal is cast. A literal defaults to f64 and an array
   ;; literal has no context to say otherwise -- a let has no type annotation --
-  ;; so [3.5 -1.0] is an [f64] and (sort-f32!) refuses it by type. The cast is
+  ;; so [3.5 -1.0] is an [f64] and (sort!) refuses it by type. The cast is
   ;; the only spelling available today.
   ;;
-  ;; sort-f32!: duplicates, negatives, a zero and an odd length, which is the
+  ;; sort!: duplicates, negatives, a zero and an odd length, which is the
   ;; input shape the i32 sort is tested on for the same reasons.
   (let [xs [(f32 3.5) (f32 -1.0) (f32 0.0) (f32 3.5) (f32 -2.25) (f32 10.0) (f32 0.5)]]
-    (sort-f32! (slice xs 0 7))
+    (sort! (slice xs 0 7))
     (show-f32 (slice xs 0 7)))          ; -2.25 -1 0 0.5 3.5 3.5 10
 
   ;; In place and ptr+len: sorting a subslice leaves its neighbours alone. That
   ;; is the whole content of the in-place claim, and a version that copied
   ;; would pass every test above and fail this one.
   (let [xs [(f32 9.0) (f32 4.0) (f32 3.0) (f32 2.0) (f32 1.0) (f32 9.0)]]
-    (sort-f32! (slice xs 1 5))
+    (sort! (slice xs 1 5))
     (show-f32 (slice xs 0 6)))          ; 9 1 2 3 4 9
 
   ;; Already sorted, reverse sorted, and a single element -- the three inputs
   ;; where an insertion loop with the comparison the wrong way round still
   ;; looks plausible.
   (let [xs [(f32 1.0) (f32 2.0) (f32 3.0)]]
-    (sort-f32! (slice xs 0 3))
+    (sort! (slice xs 0 3))
     (show-f32 (slice xs 0 3)))          ; 1 2 3
   (let [xs [(f32 3.0) (f32 2.0) (f32 1.0)]]
-    (sort-f32! (slice xs 0 3))
+    (sort! (slice xs 0 3))
     (show-f32 (slice xs 0 3)))          ; 1 2 3
   (let [xs [(f32 7.0)]]
-    (sort-f32! (slice xs 0 1))
+    (sort! (slice xs 0 1))
     (show-f32 (slice xs 0 1)))          ; 7
   ;; The empty slice must not read (at s -1).
   (let [xs [(f32 7.0)]]
-    (sort-f32! (slice xs 0 0))
+    (sort! (slice xs 0 0))
     (show-f32 (slice xs 0 0)))          ;
 
   (let [xs [(f32 1.0) (f32 2.0) (f32 3.0) (f32 4.0)]]
-    (reverse-f32! (slice xs 0 4))
+    (reverse! (slice xs 0 4))
     (show-f32 (slice xs 0 4)))          ; 4 3 2 1
 
   ;; min, max and sum. The empty slice is None for the first two -- there is no
   ;; least f32 that is also an honest answer -- and the sum accumulates in f64,
   ;; which is why 16777216 + 1 does not absorb here the way it would in f32.
   (let [xs [(f32 3.5) (f32 -1.0) (f32 10.0)]]
-    (match (min-f32 (slice xs 0 3)) (Some m) (print m) None (print "none"))
+    (match (min-of (slice xs 0 3)) (Some m) (print m) None (print "none"))
     (print " ")
-    (match (max-f32 (slice xs 0 3)) (Some m) (print m) None (print "none"))
+    (match (max-of (slice xs 0 3)) (Some m) (print m) None (print "none"))
     (print " ")
     (print (sum-f32 (slice xs 0 3)))
     (println ""))                       ; -1 10 12.5
   (let [xs [(f32 1.0)]]
-    (match (min-f32 (slice xs 0 0)) (Some m) (print m) None (print "none"))
+    (match (min-of (slice xs 0 0)) (Some m) (print m) None (print "none"))
     (print " ")
     (print (sum-f32 (slice xs 0 0)))
     (println ""))                       ; none 0
diff --git a/test/programs/fn-values.flan b/test/programs/fn-values.flan
index fc001a6..c2d872a 100644
--- a/test/programs/fn-values.flan
+++ b/test/programs/fn-values.flan
@@ -23,11 +23,11 @@
 ;; A comparator, which is the other half of what was blocked: a sort that is
 ;; told the order rather than having it written in. Insertion sort, because the
 ;; point here is the parameter and not the algorithm.
-(defn sort-by! [xs [i32]  before? (Fn [i32 i32] bool)] ()
+(defn insertion-by! [xs [i32]  before? (Fn [i32 i32] bool)] ()
   (dotimes [i (len xs)]
     (let [j i]
       (while (and (> j 0) (before? (at xs j) (at xs (- j 1))))
-        (swap-i32! xs j (- j 1))
+        (swap! xs j (- j 1))
         (set j (- j 1))))))
 
 (defn ascending [a i32  b i32] bool (< a b))
@@ -75,12 +75,12 @@
   ;; A comparator, and the same slice sorted both ways.
   (let [ys [3 1 4 1 5 9 2 6]
         s (slice ys 0 8)]
-    (sort-by! s ascending)
+    (insertion-by! s ascending)
     (print (at s 0)) (print " ") (print (at s 7)) (println "")
-    (sort-by! s descending)
+    (insertion-by! s descending)
     (print (at s 0)) (print " ") (print (at s 7)) (println "")
     ;; A returned function value, and a computed head calling it.
-    (sort-by! s (pick true))
+    (insertion-by! s (pick true))
     (print (at s 0)) (println "")
     (println ((pick false) 1 2)))
 
diff --git a/test/programs/generic-reject.flan b/test/programs/generic-reject.flan
new file mode 100644
index 0000000..82d848e
--- /dev/null
+++ b/test/programs/generic-reject.flan
@@ -0,0 +1,15 @@
+;;;; The refusal, at the definition and not at a call site.
+;;;;
+;;;; A generic body is checked once with its type variables abstract, so an
+;;;; operator the variable is not declared to support is refused here, naming
+;;;; the variable — rather than at whichever call site first instantiated it
+;;;; at a type that did not work. That is not Odin's model: Odin checks a
+;;;; polymorphic body only per instantiation, so (+ a b) over a $T compiles
+;;;; there and fails only if someone reaches it at a type without +.
+;;;;
+;;;; The way out is either predicate — {:where (numeric? $t)} — or the
+;;;; parameter, a (Fn [$t $t] $t) the caller supplies. Neither is written
+;;;; here, which is the point.
+(defn add2 [a $t  b $t] $t (+ a b))
+
+(defn main [] () (println (add2 1 2)))
diff --git a/test/programs/generic-runaway.flan b/test/programs/generic-runaway.flan
new file mode 100644
index 0000000..a124b36
--- /dev/null
+++ b/test/programs/generic-runaway.flan
@@ -0,0 +1,10 @@
+;;;; A generic that instantiates itself at a larger type every time.
+;;;;
+;;;; (grow [x x]) asks for a copy at [t], which asks for one at [[t]],
+;;;; forever. Before the refusal this did not fail, it *hung*, and since
+;;;; Session.eval runs the same code the thing that hung was C-c C-c with the
+;;;; dev daemon wedged behind it. The refusal names the chain of
+;;;; instantiations rather than a depth it gave up at.
+(defn grow [x $t] () {:where (copyable? $t)} (grow [x x]))
+
+(defn main [] () (grow 1))
diff --git a/test/programs/generics.flan b/test/programs/generics.flan
new file mode 100644
index 0000000..44d4220
--- /dev/null
+++ b/test/programs/generics.flan
@@ -0,0 +1,105 @@
+;;;; Generics by monomorphisation, end to end.
+;;;;
+;;;; A [$t] binds a type variable in a defn signature and every call site
+;;;; instantiates the body at the types it passes. The body is checked once
+;;;; *abstractly*, with nothing substituted, so an operator the variable is
+;;;; not declared to support is refused at the definition and not at whichever
+;;;; call site happened to reach a type that worked — see generic-reject.flan
+;;;; and generic-runaway.flan for that half.
+;;;;
+;;;; What this program is asserting, in order: one variable at several types,
+;;;; a variable bound inside a slice, a generic calling a generic at its own
+;;;; variable so that instantiation has to be transitive, the four where
+;;;; predicates, two variables at once, println deferred to the instantiation,
+;;;; and the collapsed prelude family the whole feature was for.
+
+;; One variable, several types, and (ident 3) and (ident 7) share one copy.
+;; The identity needs its parameter once, so it needs nothing declared: a type
+;; variable is move-only by default and one move is what this is.
+(defn ident [x $t] $t x)
+
+;; The variable is bound *inside* a type constructor, which is a structural
+;; walk rather than a name match.
+(defn first-or [s [$t]  d $t] $t
+  {:where (copyable? $t)}
+  (if (= (len s) 0) d (at s 0)))
+
+;; A generic calling a generic at its own variable: the copy of [swap!] is
+;; generated when [rotate!] is instantiated and not before.
+(defn rotate! [s [$t]] ()
+  {:where (copyable? $t)}
+  (dotimes [i (- (len s) 1)]
+    (swap! s i (+ i 1))))
+
+;; numeric? admits + - * / %.
+(defn twice [x $t] $t
+  {:where (numeric? $t)}
+  (+ x x))
+
+;; equal? admits = and !=; ordered? admits < <= > >= min max, and entails
+;; equal? and copyable?.
+(defn count-of [s [$t]  x $t] i32
+  {:where (equal? $t)}
+  (let [n 0]
+    (dotimes [i (len s)]
+      (when (= (at s i) x)
+        (set n (+ n 1))))
+    n))
+
+(defn clamp-to [x $t  lo $t  hi $t] $t
+  {:where (ordered? $t)}
+  (min (max x lo) hi))
+
+;; Two variables, and the second is determined by its own argument.
+(defn fst [a $t  b $u] $t
+  {:where [(copyable? $t) (copyable? $u)]}
+  (do b a))
+
+;; println over a type variable is the one form the abstract pass defers to
+;; the instantiation, because its legality is only decidable after
+;; substituting. The structural printer is selected per copy.
+(defn show [x $t] ()
+  {:where (copyable? $t)}
+  (println x))
+
+(defn main [] ()
+  (println (ident 3))
+  (println (ident 4.5))
+  (println (ident true))
+  (println (ident 7))
+
+  (let [ns [5 3 9 1]
+        fs [2.5 0.5 1.5]]
+    (println (first-or (slice ns 0 4) -1))
+    (println (first-or (slice ns 0 0) -1))
+    (rotate! (slice ns 0 4))
+    (println (at ns 3))
+
+    (println (twice 21))
+    (println (twice 1.5))
+    (println (count-of (slice ns 0 4) 9))
+    (println (clamp-to 12 0 10))
+    (println (clamp-to 0.5 1.0 9.0))
+    (println (fst 8 true))
+
+    (show 3)
+    (show 4.5)
+    (show "text")
+
+    ;; The collapsed prelude family, at both element types.
+    (sort! (slice ns 0 4))
+    (println (at ns 0))
+    (sort-by! (slice fs 0 3) (fn [a b] (> a b)))
+    (println (at fs 0))
+    (reverse! (slice ns 0 4))
+    (println (at ns 0))
+    (map! (slice ns 0 4) (fn [x] (* x 2)))
+    (println (reduce (slice ns 0 4) 0 (fn [a b] (+ a b))))
+    (match (min-of (slice ns 0 4)) (Some m) (println m) _ (println -1))
+    (match (max-of (slice fs 0 3)) (Some m) (println m) _ (println -1.0))
+    (match (index-of (slice ns 0 4) 18) (Some i) (println i) _ (println -1))
+    (let [a (arena-new 4096)
+          keep (filter (slice ns 0 4) (fn [x] (> x 5)))]
+      (println (len (as-slice keep)))
+      (free keep)
+      (free-all a))))
diff --git a/test/programs/higher-order.flan b/test/programs/higher-order.flan
index 08db084..e0cea10 100644
--- a/test/programs/higher-order.flan
+++ b/test/programs/higher-order.flan
@@ -15,36 +15,36 @@
   ;; map! writes back into the slice it was handed.
   (let [xs [1 2 3 4]
         s (slice xs 0 4)]
-    (map-i32! s triple)
+    (map! s triple)
     (print (at s 0)) (print " ") (print (at s 3)) (println "")
 
     ;; reduce, with the accumulator first in the step. The prelude's own
     ;; sum-i32 is this with the + written in.
-    (print (reduce-i32 s 0 adds)) (println "")
+    (print (reduce s 0 adds)) (println "")
     ;; ... and an fn literal, whose parameter types come from the parameter.
-    (print (reduce-i32 s 1 (fn [a b] (* a b)))) (println "")
+    (print (reduce s 1 (fn [a b] (* a b)))) (println "")
 
     ;; filter allocates and the caller frees.
-    (let [v (filter-i32 s odd?)]
+    (let [v (filter s odd?)]
       (print (len v)) (print " ") (print (at v 0)) (println "")
       (free v))
 
     ;; A comparator sort, both directions off the same slice.
-    (sort-i32-by! s longer-first)
+    (sort-by! s longer-first)
     (print (at s 0)) (print " ") (print (at s 3)) (println "")
-    (sort-i32-by! s (fn [a b] (< a b)))
+    (sort-by! s (fn [a b] (< a b)))
     (print (at s 0)) (print " ") (print (at s 3)) (println ""))
 
   ;; The f32 half of the family, which is the same code at the other element
   ;; type — the copy that generics would remove.
   (let [ys [(f32 4.0) (f32 1.0) (f32 8.0) (f32 2.0)]
         t (slice ys 0 4)]
-    (map-f32! t halve)
+    (map! t halve)
     (print (at t 0)) (print " ") (print (at t 2)) (println "")
-    (print (reduce-f32 t 0.0 (fn [a b] (+ a b)))) (println "")
-    (let [w (filter-f32 t big?)]
+    (print (reduce t 0.0 (fn [a b] (+ a b)))) (println "")
+    (let [w (filter t big?)]
       (print (len w)) (println "")
       (free w))
-    (sort-f32-by! t (fn [a b] (> a b)))
+    (sort-by! t (fn [a b] (> a b)))
     (print (at t 0)) (print " ") (print (at t 3)) (println ""))
   0)
diff --git a/test/programs/reach-walk.flan b/test/programs/reach-walk.flan
index 0a35f50..3561167 100644
--- a/test/programs/reach-walk.flan
+++ b/test/programs/reach-walk.flan
@@ -7,7 +7,7 @@
 ;;;; functions below is called from exactly one place, and that place is an
 ;;;; edge no other program in the corpus exercises:
 ;;;;
-;;;;   index-of    the index expression of a place, (set (at a (f)) v)
+;;;;   index-expr    the index expression of a place, (set (at a (f)) v)
 ;;;;   through     a place under (addr ...), here a (deref ...) so that it is
 ;;;;               the addr edge and not the index one again
 ;;;;   placeholder a restart-case clause body, which is reached by a transfer
@@ -21,7 +21,7 @@
 
 (defstruct Nope [id i32])
 
-(defn index-of [] i32 2)
+(defn index-expr [] i32 2)
 
 (defn through [] (Ptr i32) (addr slot))
 
@@ -37,7 +37,7 @@
 
 (defn main [] i32
   ;; The index of a place is an expression, and it can call.
-  (set (at cells (index-of)) 10)
+  (set (at cells (index-expr)) 10)
   (print (at cells 2)) (println "")
 
   ;; (addr (deref p)) is p, so this is the addr edge over a place whose own
diff --git a/test/programs/slices.flan b/test/programs/slices.flan
index ad66103..f96ada3 100644
--- a/test/programs/slices.flan
+++ b/test/programs/slices.flan
@@ -36,47 +36,47 @@
 
   ;; Reading the whole slice, before anything reorders it.
   (print (sum-i32 (slice xs 0 (len xs)))) (println "")            ; 23
-  (print (match (min-i32 (slice xs 0 (len xs))) (Some v) v None 99))
+  (print (match (min-of (slice xs 0 (len xs))) (Some v) v None 99))
   (println "")                                    ; -3
-  (print (match (max-i32 (slice xs 0 (len xs))) (Some v) v None 99))
+  (print (match (max-of (slice xs 0 (len xs))) (Some v) v None 99))
   (println "")                                    ; 12
   ;; First index, not the last: 5 appears at 0 and at 2.
-  (print (match (index-of-i32 (slice xs 0 (len xs)) 5) (Some v) v None -1))
+  (print (match (index-of (slice xs 0 (len xs)) 5) (Some v) v None -1))
   (println "")                                    ; 0
-  (print (match (index-of-i32 (slice xs 0 (len xs)) 4) (Some v) v None -1))
+  (print (match (index-of (slice xs 0 (len xs)) 4) (Some v) v None -1))
   (println "")                                    ; -1
   ;; An empty slice has no least element, and None is the answer.
-  (print (match (min-i32 (slice xs 3 3)) (Some v) v None 99))
+  (print (match (min-of (slice xs 3 3)) (Some v) v None 99))
   (println "")                                    ; 99
 
   ;; Reverse of an odd-length slice: the middle element stays put.
-  (reverse-i32! (slice xs 0 (len xs)))
+  (reverse! (slice xs 0 (len xs)))
   (show (slice xs 0 (len xs)))                    ; 7 -3 12 0 5 -3 5
   ;; And of a two-element one, the smallest case that can actually move.
-  (reverse-i32! (slice xs 0 2))
+  (reverse! (slice xs 0 2))
   (show (slice xs 0 (len xs)))                    ; -3 7 12 0 5 -3 5
 
   (load-xs)
-  (sort-i32! (slice xs 0 (len xs)))
+  (sort! (slice xs 0 (len xs)))
   (show (slice xs 0 (len xs)))                    ; -3 -3 0 5 5 7 12
 
   ;; Reverse-sorted: the case a comparison that never fires would pass.
   (set (at ys 0) 5) (set (at ys 1) 4) (set (at ys 2) 3)
   (set (at ys 3) 2) (set (at ys 4) 1)
-  (sort-i32! (slice ys 0 (len ys)))
+  (sort! (slice ys 0 (len ys)))
   (show (slice ys 0 (len ys)))                    ; 1 2 3 4 5
 
   ;; A subslice, with the elements on both sides left alone.
   (set (at zs 0) 100) (set (at zs 1) 9) (set (at zs 2) -1)
   (set (at zs 3) 9) (set (at zs 4) 4) (set (at zs 5) 0)
   (set (at zs 6) 200) (set (at zs 7) 300)
-  (sort-i32! (slice zs 1 6))
+  (sort! (slice zs 1 6))
   (show (slice zs 0 (len zs)))                    ; 100 -1 0 4 9 9 200 300
 
   ;; Degenerate lengths must do nothing rather than run off an end.
-  (sort-i32! (slice zs 0 0))
-  (reverse-i32! (slice zs 0 0))
-  (sort-i32! (slice zs 2 3))
-  (reverse-i32! (slice zs 2 3))
+  (sort! (slice zs 0 0))
+  (reverse! (slice zs 0 0))
+  (sort! (slice zs 2 3))
+  (reverse! (slice zs 2 3))
   (show (slice zs 0 (len zs)))                    ; 100 -1 0 4 9 9 200 300
   0)
diff --git a/test/programs/text.flan b/test/programs/text.flan
index 5ca88ec..1c93790 100644
--- a/test/programs/text.flan
+++ b/test/programs/text.flan
@@ -31,11 +31,11 @@
   (println "")
 
   ;; First occurrence, and None for a byte that is not there.
-  (print (match (index-of-byte (bytes "banana") \a) (Some i) i None -1))
+  (print (match (index-of (bytes "banana") \a) (Some i) i None -1))
   (print " ")
-  (print (match (index-of-byte (bytes "banana") \z) (Some i) i None -1))
+  (print (match (index-of (bytes "banana") \z) (Some i) i None -1))
   (print " ")
-  (print (match (index-of-byte (bytes "") \a) (Some i) i None -1))
+  (print (match (index-of (bytes "") \a) (Some i) i None -1))
   (println "")
 
   ;; Accepted.
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 3d7e17e..7351bce 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1320,6 +1320,13 @@ let () =
     outputs "a local shadows an imported name" "programs/pkg-shadow.flan"
       "7\n20\n0\n5\n";
 
+    (* Generics end to end: one written body per family, several emitted, and
+       the collapsed prelude running underneath it. Every line of the expected
+       output is an answer a per-type copy used to give. *)
+    let generics_out = "3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n3\n" in
+    outputs "generics" "programs/generics.flan" generics_out;
+    outputs ~opt:"-O0" "generics, -O0" "programs/generics.flan" generics_out;
+
     (* Reach's walk, edge by edge. Pruning is what makes the link follow the
        program, and the cost of getting it wrong is not a wrong answer: a
        function the walk fails to reach is not emitted, and the build dies in
@@ -1368,6 +1375,24 @@ let () =
     in
     (* Visibility: main is not a name a package offers, and saying so is the
        point — "unknown name sand/main" would be true and useless. *)
+    (* Generics, at the definition rather than at a call site. Both of these
+       are refusals the abstract pass exists for: the body is checked once
+       with its type variables left abstract, so an operator the variable was
+       not declared to support, and an instantiation that grows without end,
+       are both answered where they are written. The second one used to *hang*
+       rather than fail, which through Session.eval is C-c C-c hanging with
+       the dev daemon behind it — so what is asserted is that it names the
+       chain of instantiations and not a depth it gave up at. *)
+    refuses "an unconstrained operator in a generic body"
+      "programs/generic-reject.flan"
+      "only what it is declared to support";
+    refuses "an unconstrained operator names the way out"
+      "programs/generic-reject.flan" "{:where (numeric? $t)}";
+    refuses "a runaway instantiation" "programs/generic-runaway.flan"
+      "instantiates itself without end";
+    refuses "a runaway instantiation names the chain"
+      "programs/generic-runaway.flan" "grow at ([2 i32])";
+
     refuses "a package's main is not visible" "programs/pkg-hidden-main.flan"
       "sand/main is not a name";
     refuses "one directory under two aliases" "programs/pkg-two-aliases.flan"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 1cff6c9..679b673 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2118,6 +2118,86 @@ let () =
       | [] -> check "a report has a first line" false)
    | None -> check "a report needs a diagnostic" false);
 
+  (* ── Generics: the syntax, the predicates, and the two defaults ──
+     The syntax question the feature had to settle first: [{K V}] is a legal
+     *return type*, so a defn with a map return type and a constraint map puts
+     two braces in a row meaning different things. They are told apart
+     structurally, by the first form inside — a constraint map leads with a
+     keyword and a map type leads with a type — so [{K V}] did not have to go
+     and is still exactly what it was. *)
+  accepts "a map return type is still a map return type"
+    "(defn f [] {string i32} (map-new string i32))";
+  accepts "a map return type followed by a constraint map"
+    "(defn f [x $t] {string i32} {:where (copyable? $t)} \
+     (do x (map-new string i32)))";
+  rejects_check "a map return type is not read as a constraint map"
+    ~needle:"is not a type variable of f"
+    "(defn f [] {string i32} {:where (ordered? $t)} (map-new string i32))";
+
+  (* The predicates, and each one gating the operator it is for. *)
+  accepts "ordered? admits <"
+    "(defn less [a $t b $t] bool {:where (ordered? $t)} (< a b))";
+  accepts "equal? admits ="
+    "(defn same [a $t b $t] bool {:where (equal? $t)} (= a b))";
+  accepts "numeric? admits +"
+    "(defn add [a $t b $t] $t {:where (numeric? $t)} (+ a b))";
+  rejects_check "equal? does not admit <"
+    ~needle:"nothing here says t is ordered?"
+    "(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))";
+  (* The entailments, which are the reason a signature is one predicate long
+     rather than three. Every type the language orders is a number or an enum,
+     so it is equatable and it is not move-only. *)
+  accepts "ordered? entails equal?"
+    "(defn same [a $t b $t] bool {:where (ordered? $t)} (= a b))";
+  accepts "numeric? entails ordered?"
+    "(defn less [a $t b $t] bool {:where (numeric? $t)} (< a b))";
+  accepts "ordered? entails copyable?"
+    "(defn twice [a $t] bool {:where (ordered? $t)} (< a a))";
+  rejects_check "a predicate nobody has heard of"
+    ~needle:"is not a type predicate"
+    "(defn f [a $t] $t {:where (sortable? $t)} a)";
+  rejects_check "a predicate about a variable the signature never bound"
+    ~needle:"is not a type variable of f"
+    "(defn f [a i32] i32 {:where (ordered? $t)} a)";
+
+  (* Move-only by default, which is the other half of the where clause and the
+     one with no Odin counterpart: Odin has no move semantics, so its $T never
+     has to answer. The prior art is Rust's T: Copy, and the difference is
+     that copyable? is a question the compiler answers rather than a trait a
+     user implements. Conservative in the safe direction — move is the
+     stricter rule, so assuming it can only refuse a valid program. *)
+  rejects_check "a type variable is move-only until it says otherwise"
+    ~needle:"cannot be used again"
+    "(defn twice [a $t b (Fn [$t $t] $t)] $t (b a a))";
+  accepts "and copyable? is the opt-out"
+    "(defn twice [a $t b (Fn [$t $t] $t)] $t {:where (copyable? $t)} (b a a))";
+
+  (* The allow-list, and it has two members. println over a type variable is
+     deferred to the instantiation, because its legality is only decidable
+     after substituting — which is the one thing the abstract pass otherwise
+     refuses to do. *)
+  accepts "println over a type variable is deferred"
+    "(defn show [x $t] () {:where (copyable? $t)} (println x))";
+  accepts "and so is print"
+    "(defn show [x $t] () {:where (copyable? $t)} (print x))";
+
+  (* A predicate a body relies on has to be carried by every signature between
+     it and the call site, or the refusal moves into code the caller did not
+     write. *)
+  rejects_check "a predicate is not carried through a generic call"
+    ~needle:"has to be carried by every signature"
+    "(defn outer [s [$t]] () {:where (copyable? $t)} (sort! s))";
+  accepts "and is accepted when it is"
+    "(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))";
+
+  (* 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. *)
+  rejects_check "a map keyed by a type variable that is not hashable?"
+    ~needle:"is not a map key"
+    "(defn f [m {$t i32}] i32 {:where (copyable? $t)} (len m))";
+  accepts "and hashable? is what says it is"
+    "(defn f [m {$t i32}] i32 {:where (hashable? $t)} (len m))";
+
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"
     (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all);
diff --git a/vendor/edn/edn.flan b/vendor/edn/edn.flan
index c12af96..e1efbf4 100644
--- a/vendor/edn/edn.flan
+++ b/vendor/edn/edn.flan
@@ -320,7 +320,7 @@
       ;; A ratio is caught here and not by a "contains a slash" rule over every
       ;; token, because a slash is perfectly ordinary in a symbol: foo/bar is a
       ;; namespaced name and must stay one.
-      (when (match (index-of-byte text \/) (Some _) true None false)
+      (when (match (index-of text \/) (Some _) true None false)
         (fail c err-ratio lo)
         (return (error-token c)))
       (when (match (parse-i64 text) (Some _) true None false)
diff --git a/web/examples/option.flan b/web/examples/option.flan
index ea8ea91..813d419 100644
--- a/web/examples/option.flan
+++ b/web/examples/option.flan
@@ -2,12 +2,12 @@
 
 ;; `some` unwraps Some and early-returns None from *this* function.
 (defn doubled-first [s [i32]] (Option i32)
-  (Some (* 2 (some (index-of-i32 s 15)))))
+  (Some (* 2 (some (index-of s 15)))))
 
 (defn main [] ()
   (match (doubled-first (slice nums 0 4))
     (Some i) (do (print i) (println ""))          ; 4
     None     (println "not found"))
-  (match (index-of-i32 (slice nums 0 4) 99)
+  (match (index-of (slice nums 0 4) 99)
     (Some i) (do (print i) (println ""))
     None     (println "not found")))

From de93ffc89e010f25aaf71b6cc43a790cb30551aa Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 14:52:17 +0700
Subject: [PATCH 09/11] A cast to a type variable, and the container builtins
 over one

(t x) is not a name is_cast knows - t is not a machine type - so it is
its own arm, admitted by numeric? because a cast produces a number.
vec-new, pool-new and map-new all reach the one list of what names a
type, so the spike's line for vec-new had already covered the other two;
zeroed takes its type from the position it is written in. All four are
pinned in programs/generics.flan.
---
 lib/check.ml                | 20 ++++++++++++++++++++
 test/programs/generics.flan | 33 ++++++++++++++++++++++++++++++++-
 test/test_acceptance.ml     |  5 ++++-
 3 files changed, 56 insertions(+), 2 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 99b8955..679d21d 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -4645,6 +4645,26 @@ and named_call ctx ~want loc name args =
                  float goes through (i32 x) first" name
          (Types.to_string other));
     prim (Tast.Cast target) target [ a ]
+  (* A cast to a *type variable*: [(t x)] inside a generic body. The name is
+     not one [is_cast] knows, because [is_cast] asks whether the name is a
+     machine type and [t] is not — so this is its own arm, above the ordinary
+     one and below the enums, and it reaches the same [Cast] prim.
+
+     Inside an instantiation [resolve_name] has already answered with the
+     concrete target, so the copy casts to a real type and the emitter sees
+     nothing unusual. During the abstract pass the target is [Var t] and the
+     [where] clause is what says the cast means anything at all: a cast
+     produces a number, so [numeric?] is what admits it. *)
+  | _ when (List.mem name ctx.env.tyvars || List.mem_assoc name ctx.env.subst)
+           && List.length args = 1 ->
+    let target = resolve_name ctx.env ~seen:[] loc name in
+    unconstrained ctx.env loc ("a cast to " ^ name) ~needs:"numeric?" target;
+    let a = check ctx (List.hd args) in
+    (match a.Tast.ty with
+     | Types.Enum _ -> ()
+     | t when Types.is_numeric t || generic_ty t -> ()
+     | t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
+    prim (Tast.Cast target) target [ a ]
   | _ when is_cast name && List.length args = 1 ->
     let target = resolve_name ctx.env ~seen:[] loc name in
     let a = check ctx (List.hd args) in
diff --git a/test/programs/generics.flan b/test/programs/generics.flan
index 44d4220..1f83cd5 100644
--- a/test/programs/generics.flan
+++ b/test/programs/generics.flan
@@ -62,6 +62,30 @@
   {:where (copyable? $t)}
   (println x))
 
+;; A cast to a type variable. [(t x)] is not a name [is_cast] knows — [t] is
+;; not a machine type — so it is its own arm, and [numeric?] is what admits
+;; it, because a cast produces a number. Inside the copy the target is
+;; concrete and the emitter sees an ordinary cast.
+(defn widen [x i32  d $t] $t
+  {:where (numeric? $t)}
+  (do d (t x)))
+
+;; The builtins that take a *type name* as an argument, over a variable. Each
+;; reaches the one list of what names a type, so all three came at once.
+;; (pool-new t) and (map-new t i32) are the other two; a Pool of a variable
+;; needs it not to be move-only, which [copyable?] is.
+(defn one-of [x $t] (Vec $t)
+  {:where (copyable? $t)}
+  (let [v (vec-new t)]
+    (push v x)
+    v))
+
+;; (zeroed) takes its type from the position it is written in, so a variable
+;; in that position is answered by the instantiation like any other type.
+(defn zero-of [x $t] $t
+  {:where (copyable? $t)}
+  (do x (zeroed)))
+
 (defn main [] ()
   (println (ident 3))
   (println (ident 4.5))
@@ -98,8 +122,15 @@
     (match (min-of (slice ns 0 4)) (Some m) (println m) _ (println -1))
     (match (max-of (slice fs 0 3)) (Some m) (println m) _ (println -1.0))
     (match (index-of (slice ns 0 4) 18) (Some i) (println i) _ (println -1))
+    (println (widen 3 0.0))
+    (println (widen 3 (i64 0)))
+    (println (zero-of 9))
+
     (let [a (arena-new 4096)
-          keep (filter (slice ns 0 4) (fn [x] (> x 5)))]
+          keep (filter (slice ns 0 4) (fn [x] (> x 5)))
+          one (one-of 4.5)]
       (println (len (as-slice keep)))
+      (println (at (as-slice one) 0))
+      (free one)
       (free keep)
       (free-all a))))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 7351bce..30f0507 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1323,7 +1323,10 @@ let () =
     (* Generics end to end: one written body per family, several emitted, and
        the collapsed prelude running underneath it. Every line of the expected
        output is an answer a per-type copy used to give. *)
-    let generics_out = "3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n3\n" in
+    let generics_out =
+      "3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n\
+       3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n3\n3\n0\n3\n4.5\n"
+    in
     outputs "generics" "programs/generics.flan" generics_out;
     outputs ~opt:"-O0" "generics, -O0" "programs/generics.flan" generics_out;
 

From 70af1966a2a5e048a6f99cbe66a325d3a486be40 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 14:58:27 +0700
Subject: [PATCH 10/11] Braces are no longer a type: (Map K V) is the only
 spelling

The author's decision, and it removes the one syntax question generics
had. A return type can no longer be written in braces, so a {...} after
the signature is unambiguously the constraint map and there is no
structural rule to explain.

The reasons for the record: the brace's value meaning and its type
meaning do not correspond the way the bracket's do - [1 2 3] is a value
whose type is [3 i32], but {.x 1} is a value whose type is a name, and a
map value is built by map-new with no braces anywhere - and dropping it
reserves {} in type position for anonymous struct types.

Braces in a type are refused with the surviving spelling named rather
than falling through to "expected a type". Types.to_string and
Cimport's source printer both print (Map K V) now, and Shim refuses the
application spelling where it used to refuse only Ast.Tmap.
---
 lib/cimport.ml          |  3 ++-
 lib/parse.ml            | 47 +++++++++++++++++++++++++++--------------
 lib/shim.ml             |  6 +++++-
 lib/types.ml            |  2 +-
 syntax-sketch.flan      | 16 ++++++++------
 test/test_acceptance.ml |  2 +-
 test/test_flan.ml       | 47 ++++++++++++++++++++++-------------------
 7 files changed, 75 insertions(+), 48 deletions(-)

diff --git a/lib/cimport.ml b/lib/cimport.ml
index a3fede3..f95765a 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -392,7 +392,8 @@ let rec ty_source (t : Ast.texpr) =
   | Ast.Tslice e -> Printf.sprintf "[%s]" (ty_source e)
   | Ast.Tarray (Ast.Lint n, e) -> Printf.sprintf "[%Ld %s]" n (ty_source e)
   | Ast.Tarray (Ast.Lname n, e) -> Printf.sprintf "[%s %s]" n (ty_source e)
-  | Ast.Tmap (k, v) -> Printf.sprintf "{%s %s}" (ty_source k) (ty_source v)
+  | Ast.Tmap (k, v) ->
+    Printf.sprintf "(Map %s %s)" (ty_source k) (ty_source v)
   | Ast.Tfn (ps, r) ->
     Printf.sprintf "(Fn [%s] %s)"
       (String.concat " " (List.map ty_source ps)) (ty_source r)
diff --git a/lib/parse.ml b/lib/parse.ml
index 44020fb..ca23be8 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -65,8 +65,26 @@ let rec texpr (f : Form.t) : Ast.texpr =
   | Vec [ n; elem ] -> mk (Ast.Tarray (len n, texpr elem))
   | Vec _ ->
     fail f "a type in brackets is [T] for a slice or [n T] for a fixed array"
-  | Map [ k; v ] -> mk (Ast.Tmap (texpr k, texpr v))
-  | Map _ -> fail f "a map type is {K V}"
+  (* Braces are not a type. [{K V}] used to spell [(Map K V)] and the two
+     resolved to the same thing; the brace spelling is withdrawn, and the
+     refusal names the surviving one rather than letting the form fall through
+     to "expected a type".
+
+     Two reasons, and the second is the one that decided it. The brace's value
+     meaning and its type meaning do not correspond the way the bracket's do:
+     [[1 2 3]] is a value whose type is [[3 i32]], but [{.x 1 .y 0}] is a
+     value whose type is a *name*, and a map value is built by [map-new] with
+     no braces anywhere. And dropping it reserves [{}] in type position for
+     anonymous struct types, [{.x f32 .y f32}], which is a likelier thing to
+     want than a second spelling of a type that already has one.
+
+     It also settles the one syntax question generics had: a defn's constraint
+     map, [{:where (ordered? $t)}], sits immediately after the return type,
+     and with braces gone from type position there is nothing for it to be
+     confused with. *)
+  | Map _ ->
+    fail f "a map type is written (Map K V), not in braces — braces in type \
+            position are not a type" 
   | List ({ v = Sym "Fn"; _ } :: rest) ->
     (match rest with
      | [ { v = Vec params; _ }; ret ] ->
@@ -99,21 +117,18 @@ let rec fields (f : Form.t) (items : Form.t list) : Ast.field list =
    rather than a bare keyword: it leaves room for further keys without new
    syntax.
 
-   **The disambiguation, since it is the one syntax question the feature had
-   to settle.** [{K V}] is a legal *return type* spelling for [(Map K V)], so
-   [(defn f [xs [$t]] {string i32} {:where ...} body)] puts two braces in a
-   row meaning different things. They are told apart structurally, by the
-   first form inside: a constraint map leads with a *keyword*, and a map type
-   leads with a type — [{string i32}], [{K V}] — and a keyword is not a type
-   anywhere in the language. So [Map ({v = Kw _} :: _)] in the slot after the
-   return type is a constraint map and nothing else can be. The return-type
-   slot itself is never ambiguous: [Parse] takes it unconditionally, before
-   this is consulted. [{K V}] stays exactly as it was — whether it survives is
-   a separate open question, and this feature does not force it.
+   **The one syntax question it had, and how it stopped being one.** [{K V}]
+   used to be a legal *return type* spelling for [(Map K V)], which put two
+   braces in a row meaning different things — [(defn f [xs [$t]] {string i32}
+   {:where ...} body)]. The brace spelling has since been withdrawn from type
+   position entirely ([texpr] above), so the slot after the return type can be
+   nothing but this. A bare [{}] in *expression* position is already refused
+   ([expr] below), so there is nothing for it to be confused with on the other
+   side either.
 
-   A bare [{}] in *expression* position is already refused ([expr] below), so
-   there is also nothing for a constraint map to be confused with once past
-   the return type. *)
+   The leading keyword is still required and still checked, because it is what
+   tells a constraint map from a struct literal's field list, [{.x 1}], which
+   is what braces mean in the position a body starts in. *)
 let constraints (body : Form.t list) : Ast.pred list * Form.t list =
   match body with
   | ({ Form.v = Form.Map (({ Form.v = Form.Kw _; _ } :: _ as kvs)); _ } as m)
diff --git a/lib/shim.ml b/lib/shim.ml
index 6ced73d..00aed2c 100644
--- a/lib/shim.ml
+++ b/lib/shim.ml
@@ -222,7 +222,11 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
       "%s is a fixed array, which C passes as a pointer and Flan as a value — \
        declare (Ptr T) and say which"
       what
-  | Ast.Tmap _ -> fail loc "%s is a map, which has no C representation" what
+  (* Two spellings reach the same type: [Ast.Tmap], which only [Cimport]
+     builds now, and [(Map K V)], which is what source writes since the brace
+     spelling was withdrawn from type position. Both are refused here. *)
+  | Ast.Tmap _ | Ast.Tapp ("Map", _) ->
+    fail loc "%s is a map, which has no C representation" what
   (* A Vec owns its storage, so handing its header to C hands out an owner and
      there is no rule for what C would then be allowed to do with it. The
      elements cross the way any other run of elements does. *)
diff --git a/lib/types.ml b/lib/types.ml
index e080d5e..ee7f714 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -133,7 +133,7 @@ let rec to_string = function
   | Named n | Enum n -> n
   | Slice t -> "[" ^ to_string t ^ "]"
   | Array (n, t) -> Printf.sprintf "[%Ld %s]" n (to_string t)
-  | Map (k, v) -> Printf.sprintf "{%s %s}" (to_string k) (to_string v)
+  | Map (k, v) -> Printf.sprintf "(Map %s %s)" (to_string k) (to_string v)
   | Ptr t -> "(Ptr " ^ to_string t ^ ")"
   | Alloc -> "Allocator"
   | Vec t -> "(Vec " ^ to_string t ^ ")"
diff --git a/syntax-sketch.flan b/syntax-sketch.flan
index de6241e..c533067 100644
--- a/syntax-sketch.flan
+++ b/syntax-sketch.flan
@@ -18,13 +18,17 @@
 ;;   [4 f32]       fixed array — a value, copies on assignment
 ;;   [f32]         slice, ptr+len — a NON-OWNING view, copies the view only
 ;;   (Vec f32)     owning growable, ptr+len+cap — MOVE-ONLY, carries allocator
-;;   {string i32}  owning hashmap — move-only, shorthand for (Map string i32)
+;;   (Map string i32)  owning hashmap — move-only
 ;;
-;; Braces are read by position: in a TYPE position {K V} is a map type; in a
-;; VALUE position {.field v ...} is a struct or condition literal — a field
-;; label is a dot, and the colon is left for keys. There is no map literal yet;
-;; a map is built with make-map and an allocator, and when a literal arrives it
-;; takes {:key value}, which is why the dot is what struct construction uses.
+;; Braces are NOT a type. {K V} used to be a second spelling of (Map K V) and
+;; was withdrawn: the brace's value and type meanings do not correspond the way
+;; the bracket's do, and {} in type position is wanted for anonymous struct
+;; types, {.x f32 .y f32}. In a VALUE position {.field v ...} is a struct or
+;; condition literal — a field label is a dot, and the colon is left for keys.
+;; There is no map literal yet; a map is built with map-new and an allocator,
+;; and when a literal arrives it takes {:key value}, which is why the dot is
+;; what struct construction uses. A defn's constraint map, {:where (ordered?
+;; $t)}, is the other brace form, and it sits after the return type.
 ;;   (Ptr World)   pointer
 ;;   (Fn [f32] bool)  function pointer, no captured environment
 ;;   (Option a)    union from the stdlib
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 30f0507..bffe3cb 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1844,7 +1844,7 @@ ERR@7 unexpected token: not the kind the caller was reading
       "(declare-c takes [xs [4 f32]] \"Takes\")"
       "which C passes as a pointer and Flan as a value";
     shim_refuses "declare-c: a map"
-      "(declare-c takes [m {string i32}] \"Takes\")"
+      "(declare-c takes [m (Map string i32)] \"Takes\")"
       "which has no C representation";
     shim_refuses "declare-c: a returned string"
       "(declare-c name [] string \"Name\")"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 679b673..a2239b7 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -412,8 +412,10 @@ let () =
    | _ -> check "nested array with named lengths" false);
   (match ty "(Ptr Cursor)" with
    | Tapp ("Ptr", [ _ ]) -> () | _ -> check "(Ptr T)" false);
-  (match ty "{string i32}" with
-   | Tmap (_, _) -> () | _ -> check "{K V} is a map type" false);
+  (* A map type is an application like (Ptr T) and (Vec T) now that the brace
+     spelling is gone: [Ast.Tmap] survives only as what [Cimport] builds. *)
+  (match ty "(Map string i32)" with
+   | Tapp ("Map", [ _; _ ]) -> () | _ -> check "(Map K V) is a map type" false);
   (match ty "(Fn [a a] bool)" with
    | Tfn ([ _; _ ], _) -> () | _ -> check "(Fn [T] R)" false);
 
@@ -858,11 +860,11 @@ let () =
      back as generics. *)
   rejects_check "Vec takes one type"    "(defn f [x (Vec i32 i32)] ())"
     ~needle:"exactly one type";
-  (* {K V} resolves now — it is the Map type spelling, and the only one, since
-     a bare map form in expression position is a struct literal's field list.
-     What is still refused is the arity, for the same reason Vec's is: a
-     near-miss would otherwise resolve to a type variable and come back as
-     generics. *)
+  (* (Map K V) is the map type spelling, and now the only one: the brace form
+     is withdrawn from type position, so braces there are refused with the
+     surviving spelling named. What is refused here is the arity, for the same
+     reason Vec's is: a near-miss would otherwise resolve to a type variable
+     and come back as generics. *)
   rejects_check "Map takes two types"   "(defn f [x (Map i32)] ())"
     ~needle:"exactly two types";
   rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)"
@@ -2118,21 +2120,22 @@ let () =
       | [] -> check "a report has a first line" false)
    | None -> check "a report needs a diagnostic" false);
 
-  (* ── Generics: the syntax, the predicates, and the two defaults ──
-     The syntax question the feature had to settle first: [{K V}] is a legal
-     *return type*, so a defn with a map return type and a constraint map puts
-     two braces in a row meaning different things. They are told apart
-     structurally, by the first form inside — a constraint map leads with a
-     keyword and a map type leads with a type — so [{K V}] did not have to go
-     and is still exactly what it was. *)
-  accepts "a map return type is still a map return type"
-    "(defn f [] {string i32} (map-new string i32))";
+  (* ── Generics: the syntax, the predicates, and the two defaults ── *)
+
+  (* The one syntax question the feature had, and how it stopped being one.
+     [{K V}] used to be a legal *return type* spelling for (Map K V), so a
+     defn with a map return type and a constraint map put two braces in a row
+     meaning different things. The brace spelling is now withdrawn from type
+     position entirely, so the slot after the return type can be nothing but
+     the constraint map, and braces in a type say where the spelling went. *)
+  accepts "a map return type, written the one way there is"
+    "(defn f [] (Map string i32) (map-new string i32))";
   accepts "a map return type followed by a constraint map"
-    "(defn f [x $t] {string i32} {:where (copyable? $t)} \
+    "(defn f [x $t] (Map string i32) {:where (copyable? $t)} \
      (do x (map-new string i32)))";
-  rejects_check "a map return type is not read as a constraint map"
-    ~needle:"is not a type variable of f"
-    "(defn f [] {string i32} {:where (ordered? $t)} (map-new string i32))";
+  rejects_check "braces in type position say where the spelling went"
+    ~needle:"written (Map K V)"
+    "(defn f [] {string i32} (map-new string i32))";
 
   (* The predicates, and each one gating the operator it is for. *)
   accepts "ordered? admits <"
@@ -2194,9 +2197,9 @@ let () =
      they are chosen from the concrete type, which does not exist yet. *)
   rejects_check "a map keyed by a type variable that is not hashable?"
     ~needle:"is not a map key"
-    "(defn f [m {$t i32}] i32 {:where (copyable? $t)} (len m))";
+    "(defn f [m (Map $t i32)] i32 {:where (copyable? $t)} (len m))";
   accepts "and hashable? is what says it is"
-    "(defn f [m {$t i32}] i32 {:where (hashable? $t)} (len m))";
+    "(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))";
 
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"

From b3cb657992ba891f03943380e025c1d3e8567bae Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sun, 13 Sep 2026 15:01:49 +0700
Subject: [PATCH 11/11] hashable? gates the type and not the operations, and
 say so where it bites

A map keyed by a type variable cannot be put into inside a generic body:
the hash and the equality are concrete symbols chosen from the concrete
key type, and there is none until the copy exists. The refusal now says
that, and says what hashable? does buy - taking and returning a
(Map $t V) - rather than leaving the reader to infer it.

Closing the hole means adding the map operations to the list of forms
the abstract pass defers to instantiation. That list is print and
println and nothing else, and every member is a place where a refusal
moves from the definition to a call site, which is what the abstract
pass exists to prevent. Two is short enough to hold in your head.

Also written down: four of the prelude's copyable? declarations are
convention rather than checker-enforced. The move analysis tracks
locals, not reads out of a slice, so swap! and friends check without it
- and would still duplicate a header at [(Vec i32)].
---
 lib/check.ml      | 24 +++++++++++++++++++-----
 lib/prelude.ml    | 18 +++++++++++++++---
 test/test_flan.ml | 10 +++++++++-
 3 files changed, 43 insertions(+), 9 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 679d21d..be3594d 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1227,13 +1227,27 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
      than assumed — falling through to [bytewise_key] would hash whatever
      bytes the variable turned out to have, which is the wrong answer for a
      [string] and for any struct with padding. Inside an instantiation this
-     arm is unreachable: [env.subst] has already made [k] concrete. *)
+     arm is unreachable: [env.subst] has already made [k] concrete.
+
+     **This is a known hole and it is deliberate.** It means [hashable?] gates
+     the *type* and not the operations: a generic may take or return a
+     [(Map $t V)] under it, and may not [put], [get] or [has?] into one. The
+     alternative is to add the map operations to the list of forms the
+     abstract pass defers to instantiation — the list [print] and [println]
+     are the only members of — and every member of that list is a place where
+     a refusal moves from the definition to a call site, which is the thing
+     the abstract pass exists to prevent. Two members is a short list worth
+     keeping short; six is a rule nobody can hold in their head. If a generic
+     over maps is ever wanted, this is the decision to revisit, and it is one
+     line here plus one in [key_fns]. *)
   | Types.Var v ->
     Loc.failk "check/generic-map-key" loc
-      "a map keyed by the type variable %s cannot have its hash and equality \
-       emitted here — they are chosen from the concrete type, which does not \
-       exist until this generic is instantiated. The key pair is emitted per \
-       copy, so this operation belongs in a body the checker has substituted" v
+      "a map keyed by the type variable %s cannot be operated on here: the \
+       hash and the equality are emitted as concrete symbols chosen from the \
+       concrete key type, and there is no concrete key type until this \
+       generic is instantiated. {:where (hashable? $%s)} says the map may be \
+       taken and returned, not that its keys can be hashed here — write the \
+       operation in a function over the concrete key type and call that" v v
   | Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str"
   | t when bytewise_key t ->
     Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"
diff --git a/lib/prelude.ml b/lib/prelude.ml
index 553014f..d5f1ee6 100644
--- a/lib/prelude.ml
+++ b/lib/prelude.ml
@@ -166,9 +166,21 @@ let source = {flan|
 ;; stricter rule and assuming it can only refuse a valid program rather than
 ;; admit a broken one: [reduce]'s accumulator is read into [f] and then
 ;; assigned again, which is correct at [i32] and a double move at [(Vec i32)],
-;; and the checker cannot tell which until it substitutes. So the ones that
-;; hold an element in a local say [copyable?] and the ones that only move
-;; elements between slots do not.
+;; and the checker cannot tell which until it substitutes.
+;;
+;; **Two of these ten are forced and the rest are convention, and the
+;; difference is worth knowing.** [filter] and [reduce] do not check without
+;; [copyable?]: the first returns a [(Vec $t)], and a Vec of an owning element
+;; is refused, and the second holds its accumulator in a local and reads it
+;; twice. [swap!], [reverse!], [map!] and [sort-by!] check *without* it,
+;; because the move analysis tracks locals and parameters and does not track a
+;; read out of a slice — so [(let [t (at s i)] ... (set (at s j) t))] is not
+;; seen as a move even when the element owns storage. They declare it anyway,
+;; and should: at [[(Vec i32)]] those bodies would duplicate a header. It is
+;; the one place move-by-default is not conservative, and until element-level
+;; moves are tracked, a [copyable?] on a body that moves elements between
+;; slots is a convention the reader has to keep rather than a fact the checker
+;; enforces.
 ;;
 ;; **What did not collapse, and why it should not.** [sum-i32] and [sum-f32]
 ;; widen their element into [i64] and [f64]; "the wider type $t accumulates
diff --git a/test/test_flan.ml b/test/test_flan.ml
index a2239b7..264355c 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2194,12 +2194,20 @@ let () =
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))";
 
   (* 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. *)
+     they are chosen from the concrete type, which does not exist yet. So
+     hashable? gates the *type* and not the operations — a generic may take
+     and return a (Map $t V) and may not put into one. Pinned because it is a
+     deliberate hole and not an oversight: closing it means adding the map
+     operations to the list of forms the abstract pass defers to
+     instantiation, which is print and println and should stay that short. *)
   rejects_check "a map keyed by a type variable that is not hashable?"
     ~needle:"is not a map key"
     "(defn f [m (Map $t i32)] i32 {:where (copyable? $t)} (len m))";
   accepts "and hashable? is what says it is"
     "(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))";
+  rejects_check "but hashable? does not make the key hashable here"
+    ~needle:"not that its keys can be hashed here"
+    "(defn f [m (Map $t i32)  k $t] () {:where (hashable? $t)} (put m k 1))";
 
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"