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)))