diff --git a/lib/ast.ml b/lib/ast.ml
index e80f8ae..76e941b 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -106,6 +106,19 @@ and rclause =
    restart clause's parameters are one, and a clause is part of an expression. *)
 and field = { fname : string; fty : texpr; floc : Loc.t }
 
+(* One slot of a [defn]'s parameter vector, before it is known whether the slot
+   is a name or a type. [(defn f [x y] ...)] is two dyn parameters if [y] is
+   not a type and one parameter [x : y] if it is, and the parser cannot tell:
+   the type names are not all known until macros have run and every file has
+   been loaded. So the vector is carried undecided and paired in [Check], where
+   the set is complete. See the argument in Parse beside the [defn] case. *)
+and pitem =
+  (* A bare symbol: either a parameter's name or a type's. *)
+  | Pname of string * Loc.t
+  (* Anything that cannot be a parameter name — [(Ptr T)], [[T]], [[n T]], [()]
+     — and so is a type whatever the environment says. *)
+  | Ptype of texpr
+
 (* Two unwrap operators, because they are two different things — plan.org. *)
 and unwrap = Usome | Utry
 
@@ -136,6 +149,13 @@ type pred = { pname : string; pvar : string; ploc : Loc.t }
 type fn = {
   name    : string;
   params  : field list;
+  (* [Some items] means the parameter vector has not been paired yet: it was
+     written by a [defn], where a slot with no type means [dyn], and [Check]
+     fills [params] from it before anything reads them. [None] is every other
+     way a signature is built — [declare], the shim, the C importer — where
+     every parameter's type was written out and the pairing was never in
+     doubt. Nothing downstream of [Check.pair_params] sees [Some]. *)
+  praw    : pitem list option;
   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
diff --git a/lib/check.ml b/lib/check.ml
index 9d7b1df..73706d7 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -707,6 +707,14 @@ and resolve_name env ~seen loc n =
       match n with
       | "bool" -> Types.Bool
       | "string" -> Types.String
+      (* Lowercase and concrete, which the rule three screens down says is a
+         type variable. It is spelled this way because it is a primitive and
+         every other primitive is lowercase — [dyn] beside [i64] and [bool]
+         reads as one of them, [Dyn] beside [Vec] and [Option] reads as a
+         container over something. The type-variable rule is reached by a
+         [when] guard below and this arm is before it, so the spelling costs
+         nothing but the note. *)
+      | "dyn" -> Types.Dyn
       | "Unit" -> Types.Unit
       | "Never" -> Types.Never
       (* A builtin opaque type, the way [string] is a builtin ptr+len. There is
@@ -752,6 +760,127 @@ and array_len env loc = function
        fail loc "%s is not a compile-time integer constant, so it cannot be \
                  an array length" n)
 
+(* ── Pairing a defn's parameter vector ──────────────────────────────────
+
+   [(defn f [x y] ...)] is one parameter [x] of type [y] if [y] names a type,
+   and two parameters of type [dyn] if it does not. Parse could not tell — the
+   long argument is beside its [defn] case — so it handed over the slots
+   undecided and this is where they are paired, with every type name in hand:
+   every file loaded, every macro expanded, every C header imported.
+
+   The walk is left to right and takes two slots or one. A name followed by
+   something that is a type takes two and is annotated; a name followed by
+   another name that is not a type, or by nothing, takes one and is [dyn]. That
+   is the whole rule, and it reads the way the vector reads.
+
+   A name that *is* a type name is refused rather than paired. [(defn f [i64 x]
+   ...)] has no good reading: taken as written it is a parameter called [i64],
+   which shadows nothing but confuses everything, and the likelier intent is a
+   pair written backwards. Refusing here costs a rename in the one program that
+   meant it and closes the one place where this rule could still hand somebody
+   a signature they did not write. *)
+let is_type_name env n =
+  Types.ikind_of_name n <> None
+  || Types.fkind_of_name n <> None
+  || List.mem n [ "bool"; "string"; "dyn"; "Unit"; "Never"; "Allocator" ]
+  || Hashtbl.mem env.aliases n
+  || Hashtbl.mem env.structs n
+  || Hashtbl.mem env.datas n
+  || Hashtbl.mem env.unions n
+  || Hashtbl.mem env.enums n
+  (* A type variable: [$t] in a signature is generics' binding site, and a
+     slot holding one is a type however few of them there are. *)
+  || (n <> "" && n.[0] = '$')
+
+(* Before a bare symbol is allowed to become an unannotated parameter, the two
+   ways it is more likely to be a type that went wrong.
+
+   This is the cost dynamic-by-default puts on the parameter vector, and it is
+   worth naming plainly: a slot with no type used to be a syntax error, and now
+   it is a [dyn] parameter. So [(defn f [x f65] ())] — a typo for [f64] — no
+   longer reads as a mistyped type. It reads as two parameters, one of them
+   called [f65], and the function silently takes an argument nobody meant to
+   give it. An arity that changes because of a typo, with no diagnostic, is the
+   failure class Parse's [defn] comment calls the worst available, and the
+   feature reintroduces it in a new place.
+
+   Two rules take most of it back. A name within one edit of a type's name is
+   the typo it looks like, and is refused with the same "did you mean" the
+   resolver gives — the near-miss table is already there and is exactly the
+   right question. And a capitalised name is a type by the convention the whole
+   corpus keeps: not one parameter in the language is capitalised, while [Form],
+   [Cursor], [Vector2] and the rest appear in these vectors constantly. So an
+   unknown capitalised name is an unknown *type*, reported as one, rather than
+   a parameter nobody would have spelled that way.
+
+   What is left uncovered is a lowercase name that resembles no type: [(defn f
+   [x widget] ())] is two dyn parameters and there is no evidence in the text
+   that it was meant to be one. That case is the feature working as specified,
+   and it is the residual the parent owns. *)
+let dyn_param_or_typo env n loc =
+  match near_miss env n with
+  | Some m ->
+    Loc.failk "check/unknown-type" loc
+      "unknown type %s — did you mean %s? A parameter with no type is dyn, so \
+       this would otherwise be read as a second parameter called %s"
+      n m n
+  | None ->
+    if n <> "" && n.[0] = Char.uppercase_ascii n.[0]
+       && n.[0] <> Char.lowercase_ascii n.[0]
+    then
+      Loc.failk "check/unknown-type" loc
+        "unknown type %s. A capitalised name in a parameter vector is a type — \
+         a parameter with no type is dyn, and parameters are lowercase"
+        n
+
+let pair_params env (items : Ast.pitem list) : Ast.field list =
+  let dyn loc = { Ast.t = Ast.Tname "dyn"; tloc = loc } in
+  let rec go = function
+    | [] -> []
+    | Ast.Ptype t :: _ ->
+      Loc.failk "check/parameter-name-expected" t.Ast.tloc
+        "a parameter's name was expected here, and this is a type. \
+         Parameters are [name Type ...], and a name with no type is dyn"
+    | Ast.Pname (n, loc) :: rest when is_type_name env n ->
+      ignore rest;
+      Loc.failk "check/parameter-named-type" loc
+        "%s names a type, so it cannot also be this parameter's name. If the \
+         pair was written backwards it is [name %s]; otherwise rename the \
+         parameter" n n
+    | Ast.Pname (n, loc) :: Ast.Ptype t :: rest ->
+      { Ast.fname = n; fty = t; floc = loc } :: go rest
+    | Ast.Pname (n, loc) :: Ast.Pname (t, tloc) :: rest when is_type_name env t ->
+      { Ast.fname = n; fty = { Ast.t = Ast.Tname t; tloc }; floc = loc } :: go rest
+    (* The slot after this one is not a type, so this one is a parameter with
+       no type written — unless the slot after it only *looks* unlike a type
+       because it was mistyped, which is what the check is for. The next slot
+       is the one interrogated, not this one: this one is a name either way. *)
+    | Ast.Pname (n, loc) :: (Ast.Pname (t, tloc) :: _ as rest) ->
+      dyn_param_or_typo env t tloc;
+      { Ast.fname = n; fty = dyn loc; floc = loc } :: go rest
+    | Ast.Pname (n, loc) :: rest ->
+      { Ast.fname = n; fty = dyn loc; floc = loc } :: go rest
+  in
+  go items
+
+(* Every [defn] in the program, with its parameter vector paired. Run as a pass
+   of its own, after the type names are registered and before any signature is
+   resolved, so that nothing downstream ever sees an unpaired one. *)
+let pair_decls env (decls : Ast.decl list) : Ast.decl list =
+  let fn (f : Ast.fn) =
+    match f.Ast.praw with
+    | None -> f
+    | Some items -> { f with Ast.params = pair_params env items; praw = None }
+  in
+  List.map
+    (fun (d : Ast.decl) ->
+       match d.Ast.d with
+       | Ast.Defn f -> { d with Ast.d = Ast.Defn (fn f) }
+       | Ast.Declare (f, c) -> { d with Ast.d = Ast.Declare (fn f, c) }
+       | Ast.DeclareC (f, c) -> { d with Ast.d = Ast.DeclareC (fn f, c) }
+       | _ -> d)
+    decls
+
 (* ── 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
@@ -5539,6 +5668,13 @@ let collect env (decls : Ast.decl list) =
          Hashtbl.replace env.locs n d.Ast.dloc
        | _ -> ())
     decls;
+  (* Every type name is registered by here — structs, data types and unions by
+     the names-first pass, aliases with them, enums by the pass just above — so
+     this is the first point at which a [defn]'s parameter vector can be paired.
+     It is done before the signature loop below rather than inside it, because a
+     signature may name a type declared further down and pairing must not depend
+     on the order the file was written in. *)
+  let decls = pair_decls env decls in
   List.iter
     (fun (d : Ast.decl) ->
        let loc = d.Ast.dloc in
@@ -5742,7 +5878,13 @@ let collect env (decls : Ast.decl list) =
     if progressed && left <> [] then settle ()
   in
   settle ();
-  List.iter (fun c -> ignore (infer c)) !pending
+  List.iter (fun c -> ignore (infer c)) !pending;
+  (* The paired declarations, handed back so that pass two checks the bodies of
+     the same functions whose signatures this pass registered. Pairing needs the
+     type names, which only this pass has; every pass after it needs the result,
+     and a [defn] still carrying an unpaired vector would check as a function of
+     no parameters at all. *)
+  decls
 
 (* A type that contains itself by value has no finite size. [(Ptr T)] and a
    slice are indirections and break the cycle; a fixed array does not, because
@@ -6460,7 +6602,7 @@ let build_program ~keep_going (decls : Ast.decl list) : Tast.program * env =
      time it runs every signature is sound, so a body that fails to check
      cannot make the next body fail — which is what makes a declaration a
      resync point that needs no resynchronising. *)
-  collect env decls;
+  let decls = collect env decls in
   check_finite env;
   check_union_members env;
   let s = Loc.sink ~on:keep_going in
diff --git a/lib/cimport.ml b/lib/cimport.ml
index bc63572..e4dad44 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -813,7 +813,7 @@ let of_dump ~env ~taken ~bound_syms ~config (d : dump) : imported =
            decls :=
              { Ast.d =
                  Ast.DeclareC
-                   ({ Ast.name = flan; params; ret; fwhere = []; fbody = []; nloc = f.cloc },
+                   ({ Ast.name = flan; params; praw = None; ret; fwhere = []; fbody = []; nloc = f.cloc },
                     f.csym);
                dloc = f.cloc }
              :: !decls)
diff --git a/lib/emit.ml b/lib/emit.ml
index bc82da5..8cbc0f9 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -125,6 +125,13 @@ let rec ll (t : Types.t) =
      and a copy in the IR are the right number of bytes. *)
   | Types.Map _ -> "%map"
   | Types.Option e -> Printf.sprintf "{ i8, %s }" (ll e)
+  (* One word, and [i64] rather than a pointer type: runtime/flan_dyn.h says
+     [typedef uint64_t flan_dyn], and the IR agreeing with that typedef is the
+     whole of what keeps the two sides linkable. Nothing here ever loads
+     through it — a dyn word is only ever passed to a flan_dyn_* call — so the
+     integer spelling costs no casts and keeps the emitter honest about not
+     knowing whether the bits are a pointer. *)
+  | Types.Dyn -> "i64"
   | Types.Var _ ->
     (* The checker rejects it by name — nothing reaches here. *)
     failwith ("no layout for " ^ Types.to_string t)
@@ -318,6 +325,7 @@ let rec lay m (t : Types.t) : int * int =
          match Hashtbl.find_opt m.unions n with
          | Some u -> union_lay m u
          | None -> failwith ("no layout for struct " ^ n))
+  | Types.Dyn -> 8, 8
   | Types.Var _ -> failwith ("no layout for " ^ Types.to_string t)
 
 (* Size, alignment, and the offset of every member. *)
@@ -543,6 +551,13 @@ let rec dty m d (t : Types.t) : int =
              "!DIDerivedType(tag: DW_TAG_pointer_type, name: \"%s\", \
               baseType: null, size: 64)"
              (Types.to_string t))
+      (* An unsigned word, which is what the typedef says it is. Telling lldb
+         it is a pointer would be a guess about the encoding the compiler has
+         deliberately not made, and telling it nothing would leave [p x] on a
+         dyn local with no answer at all. A raw word is the true and useful
+         reading: it prints, and the person reading it can hand it to the
+         runtime's own printer. *)
+      | Types.Dyn -> basic "dyn" 64 "DW_ATE_unsigned"
       | Types.Var _ ->
         failwith ("no debug type for " ^ Types.to_string t)
     in
diff --git a/lib/js.ml b/lib/js.ml
index c2c8922..018977b 100644
--- a/lib/js.ml
+++ b/lib/js.ml
@@ -235,6 +235,16 @@ let rec refuse_ty loc (t : Types.t) =
       "(Map K V) is not in the JS dialect yet — Odin's open-addressed map is a \
        type-erased runtime over raw bytes and the JS answer is a Map keyed by \
        a structural key, which is its own lane"
+  (* The irony is not lost: JavaScript is the one target where a dyn value
+     needs no boxing at all, because every value there is already one. What is
+     missing is not the representation but the lowering — dyn ops are calls
+     into runtime/flan_dyn.h, and this dialect has no such runtime. It is a
+     lane, not a difficulty. *)
+  | Types.Dyn ->
+    at loc
+      "dyn is not in the JS dialect yet — every JavaScript value is already \
+       dynamic, so this is a matter of lowering the dyn operations onto the \
+       host's own, and that work has not been done"
   | Types.Var n ->
     at loc "a type variable (%s) reached the backend, which cannot happen" n
 
diff --git a/lib/load.ml b/lib/load.ml
index e95b073..aadf66a 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -302,6 +302,20 @@ and rename_place owned alias bound (p : Ast.place) : Ast.place =
 let rename_field owned alias (f : Ast.field) : Ast.field =
   { f with Ast.fty = rename_texpr owned alias f.Ast.fty }
 
+(* An unpaired parameter vector, qualified. The slots are still undecided here
+   — [Check] is what pairs them — so a bare symbol might be a parameter's name
+   or a type's, and this cannot tell. It does not have to: [owned] holds the
+   package's *declared* names, a parameter's name is not one of them, and a
+   parameter named after a type of the same package is refused outright when
+   the vector is paired. So qualifying every owned name and leaving every other
+   alone is right for both readings, and stays right because that refusal is
+   what keeps the two sets apart. *)
+let rename_pitem owned alias (p : Ast.pitem) : Ast.pitem =
+  match p with
+  | Ast.Pname (n, loc) when List.mem n owned -> Ast.Pname (qualify alias n, loc)
+  | Ast.Pname _ -> p
+  | Ast.Ptype t -> Ast.Ptype (rename_texpr owned alias t)
+
 let qualify_decl owned alias (d : Ast.decl) : Ast.decl =
   let loc = d.Ast.dloc in
   let k =
@@ -346,11 +360,26 @@ let qualify_decl owned alias (d : Ast.decl) : Ast.decl =
                    | other -> other))
     | Ast.Defn fn ->
       let params = List.map (rename_field owned alias) fn.Ast.params in
-      let bound = List.map (fun (p : Ast.field) -> p.Ast.fname) fn.Ast.params in
+      let praw = Option.map (List.map (rename_pitem owned alias)) fn.Ast.praw in
+      (* The names a body may shadow. With the vector still unpaired, every
+         bare symbol in it is a candidate — an owned one is a type and is
+         dropped, because it is a name the body should go on qualifying, and
+         what is left is the parameter names and at worst a type of some other
+         package, which no body of this one refers to as a value. *)
+      let bound =
+        match praw with
+        | Some items ->
+          List.filter_map
+            (function
+              | Ast.Pname (n, _) when not (List.mem n owned) -> Some n
+              | _ -> None)
+            items
+        | None -> List.map (fun (p : Ast.field) -> p.Ast.fname) fn.Ast.params
+      in
       Ast.Defn
         { fn with
           Ast.name = qualify alias fn.Ast.name;
-          params;
+          params; praw;
           ret = Option.map (rename_texpr owned alias) fn.Ast.ret;
           fbody = List.map (rename_expr owned alias bound) fn.Ast.fbody }
     | Ast.Package _ -> Ast.Package alias
@@ -634,6 +663,16 @@ let decl_uses acc (d : Ast.decl) =
   let field (f : Ast.field) = texpr_uses acc f.Ast.fty in
   let fn (f : Ast.fn) =
     List.iter field f.Ast.params;
+    (* An unpaired vector names types too, and a bare symbol in it may be one.
+       Every such symbol is recorded as a use: a parameter's name recorded here
+       resolves to nothing and costs nothing, where a type's name left out
+       would drop a real dependency and the import would not be loaded. Over-
+       recording is the safe direction for a dependency set. *)
+    Option.iter
+      (List.iter (function
+         | Ast.Pname (n, loc) -> acc := (n, loc) :: !acc
+         | Ast.Ptype t -> texpr_uses acc t))
+      f.Ast.praw;
     Option.iter (texpr_uses acc) f.Ast.ret;
     List.iter (expr_uses acc) f.Ast.fbody
   in
diff --git a/lib/parse.ml b/lib/parse.ml
index b1007c8..ab9d9d1 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -111,6 +111,29 @@ 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)
 
+(* A [defn]'s parameter vector, left undecided — the long argument is beside
+   the [defn] case. A bare symbol could be either half of a pair and is carried
+   as one; everything else is a type by its shape alone, and is resolved now so
+   that a malformed type is still reported at the character that is wrong.
+
+   [fields] applies [no_pattern] to the name half of each pair, and this cannot:
+   which half a slot is has not been decided. A map is the one shape that can be
+   settled here anyway — braces are not a type in any position ([texpr] refuses
+   them), so a map in this vector is a destructuring pattern and nothing else,
+   and it gets the sentence that says so rather than a complaint about map type
+   syntax. A bracket cannot be settled the same way, because [[a b]] is a
+   pattern in a name slot and a slice type in a type slot; one written in a name
+   slot comes back from [Check] as "a parameter's name was expected here", which
+   is true and is as close as this can get. *)
+and pitems (items : Form.t list) : Ast.pitem list =
+  List.map
+    (fun (it : Form.t) ->
+       match it.v with
+       | Sym s -> Ast.Pname (s, it.loc)
+       | Map _ -> no_pattern it; assert false
+       | _ -> Ast.Ptype (texpr it))
+    items
+
 (* ── 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
@@ -914,7 +937,47 @@ let rec decl (f : Form.t) : Ast.decl =
      Mandatory removes the guess: nothing is consulted, [()] is what a function
      that returns nothing writes, and a mistyped type is a mistyped type --
      [(defn f [] f65 0.0)] reaches the resolver's near-miss check and comes back
-     as *did you mean f64*, where it used to come back as an unknown name. *)
+     as *did you mean f64*, where it used to come back as an unknown name.
+
+     The return slot stays mandatory now that parameters may be left
+     unannotated, and it is worth saying why the two do not move together.
+     Dynamic-by-default means a *parameter* with no type is [dyn]; the return
+     type could have been given the same rule, and was not, because the
+     ambiguity there has no syntactic resolution at all. [(defn f [] (Rune
+     {.code 65}) (bar))] is the case above: a capitalised head in a list is a
+     type application and also a struct literal -- see [Struct] in [expr] --
+     and no rule separates them, so an optional return slot is a coin toss
+     between a type and the first form of a body. A parameter vector has no
+     such case: every slot in it is a name or a type and never an expression.
+     So [dyn] is written out in the return position, which costs one token and
+     keeps a decision this file paid for twice in one day.
+
+     ── The parameter vector ──────────────────────────────────────────────
+
+     [(defn f [x y])] is one parameter [x] of type [y], or two parameters [x]
+     and [y] of type [dyn], and which one it is depends on whether [y] names a
+     type. That is the lookup this comment's first half says was removed for
+     being brittle, and it is being asked for again -- so it is not done here.
+     The vector is carried undecided, as [Ast.pitem]s, and paired in [Check],
+     where the set of type names is complete.
+
+     The move is not cosmetic. What the old rule got wrong was consulting a set
+     that was not finished being built: it ran per-file, at parse time, before
+     macros had generated their definitions, and macros generating definitions
+     is exactly what widened the failure. By the time [Check] pairs the vector,
+     every file is loaded, every macro has expanded and every C header has been
+     imported, so the set is not a guess about what might be a type -- it is
+     the types. That is strictly more than the parser could ever know, and it
+     is the whole of the argument for the placement.
+
+     What deferring does not buy is immunity. The set is complete at a point in
+     time and not across time: [(defn f [x y] ...)] is two dyn parameters until
+     somebody writes [(defstruct y ...)] or imports a header that declares one,
+     and then it is one parameter of type [y], with no edit to [f]. The
+     signature changes under it. That residual is real, it is the dictated
+     rule's and not this file's, and [Session.compatible] is where it is felt --
+     a redefinition that changes a signature is refused there, and this is a
+     way for a signature to change with nothing redefined. *)
   | List ({ v = Sym "defn"; _ } :: args) ->
     (match args with
      | n :: { v = Vec ps; _ } :: ret :: body ->
@@ -930,7 +993,7 @@ let rec decl (f : Form.t) : Ast.decl =
               function that returns nothing writes ()" msg
        in
        let fwhere, body = constraints body in
-       mk (Ast.Defn { Ast.name = sym n; params = fields f ps;
+       mk (Ast.Defn { Ast.name = sym n; params = []; praw = Some (pitems ps);
                       ret = Some rty; fwhere; fbody = body_of body;
                       nloc = n.loc })
      | _ ->
@@ -961,10 +1024,10 @@ let rec decl (f : Form.t) : Ast.decl =
      | { v = Str csym; _ } :: rest ->
        (match List.rev rest with
         | [ n; { v = Form.Vec ps; _ } ] ->
-          mk (mkd { Ast.name = sym n; params = fields f ps;
+          mk (mkd { Ast.name = sym n; params = fields f ps; praw = None;
                     ret = None; fwhere = []; fbody = []; nloc = n.loc } csym)
         | [ n; { v = Form.Vec ps; _ }; r ] ->
-          mk (mkd { Ast.name = sym n; params = fields f ps;
+          mk (mkd { Ast.name = sym n; params = fields f ps; praw = None;
                     ret = Some (texpr r); fwhere = []; fbody = [];
                     nloc = n.loc } csym)
         | _ -> fail f "%s" usage)
@@ -1140,6 +1203,10 @@ 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 } ];
+               (* Written out, not deferred: a macro takes [[Form]] and
+                  returns a [Form], and neither half of that is the user's to
+                  leave off. *)
+               praw = None;
                ret = Some form_t; fwhere = []; fbody = body_of body;
                nloc = n.loc })
      | _ :: { v = Form.Vec ps; _ } :: body when body <> [] ->
diff --git a/lib/types.ml b/lib/types.ml
index 6c93489..f8f218a 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -47,6 +47,17 @@ type t =
   | Option of t                       (* (Option T) *)
   | Fn     of t list * t              (* (Fn [T ...] R) *)
   | Var    of string                  (* a type variable — milestone 5 *)
+  (* [dyn]: one machine word whose contents the runtime knows and this module
+     does not. It is a written type — [(defvar x dyn 5)] boxes the 5 — and it
+     is also what an unannotated [defn] parameter means, which is why it is a
+     case here and not a Named type the prelude declares: the checker has to
+     recognise it to choose the boxing and the dyn op lowering, and a name in a
+     table cannot be matched on.
+
+     Nothing about the representation is stated here on purpose. The word is
+     opaque to the compiler — runtime/flan_dyn.h owns which bits are a tag —
+     so that milestone 2 can change the encoding without touching Emit. *)
+  | Dyn
 
 let signed = function
   | I8 | I16 | I32 | I64 -> true
@@ -121,6 +132,7 @@ let rec to_string = function
     Printf.sprintf "(Fn [%s] %s)"
       (String.concat " " (List.map to_string ps)) (to_string r)
   | Var n -> n
+  | Dyn -> "dyn"
 
 let is_numeric = function Int _ | Float _ -> true | _ -> false
 
diff --git a/lib/x86.ml b/lib/x86.ml
index 008ed21..9053482 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -475,6 +475,23 @@ let is_agg (t : Types.t) =
   | Types.Unit | Types.Never -> false
   | Types.String | Types.Slice _ | Types.Array _ | Types.Map _ | Types.Vec _
   | Types.Option _ | Types.Named _ -> true
+  (* Refused by name rather than classified. A dyn word is one machine word and
+     would classify trivially — it is not the representation that is missing,
+     it is every operation on it, which is a call into runtime/flan_dyn.h that
+     this backend does not emit. Saying "a dyn value" here rather than letting
+     it through to fail at the first [+] means the reader is told the one true
+     thing about their program instead of something about an opcode.
+
+     The sentence naming [--llvm] is not written here on purpose: both callers
+     add it, and each says it differently for a good reason — Session because
+     the daemon takes this backend by default and the reader chose a program
+     rather than a code generator, and main.ml only when [--x86] was not typed
+     out. Repeating it here would say it twice to the one reader and to the
+     wrong one. *)
+  | Types.Dyn ->
+    unsupported
+      "a dyn value. Every operation on one is a call into the dynamic runtime, \
+       and this backend emits none of them"
   | Types.Var v -> unsupported "type variable %s" v
 
 let is_void (t : Types.t) = match t with Types.Unit | Types.Never -> true | _ -> false
diff --git a/raylib-imported b/raylib-imported
new file mode 100755
index 0000000..ab898b2
Binary files /dev/null and b/raylib-imported differ
diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h
new file mode 100644
index 0000000..4dd5c38
--- /dev/null
+++ b/runtime/flan_dyn.h
@@ -0,0 +1,110 @@
+/* flan_dyn — the dynamic-value ABI.
+ *
+ * Milestone 1 of dynamic-by-default. A [flan_dyn] is one machine word, and
+ * every operation the compiler cannot type statically becomes a call to one of
+ * the functions below. The compiler emits these declarations from Emit; this
+ * header is the same contract written for C, and the two are diffed rather
+ * than trusted to agree.
+ *
+ * The word is opaque. Nothing outside the runtime may read a tag out of it,
+ * because which bits carry the tag is the runtime's business and milestone 2
+ * moves them: the compiler only ever passes words it was given back to the
+ * functions here. That is what lets boxing change representation without a
+ * recompile of the emitter.
+ *
+ * Every function takes and returns scalars, for the reason flan_rt.c gives:
+ * nothing returns a struct by value, so the emitted .ll never has to agree
+ * with a platform's struct-return ABI.
+ */
+
+#ifndef FLAN_DYN_H
+#define FLAN_DYN_H
+
+#include <stdint.h>
+
+typedef uint64_t flan_dyn;
+
+/* ── Construction ──────────────────────────────────────────────────────
+ *
+ * The typed-to-dyn direction. Integer literals in dyn context box as i64:
+ * there is one integer width behind a dyn value, so the defaulting question
+ * that a wider set of boxes would raise does not arise.
+ *
+ * [flan_dyn_nil] is the absent value, and is what an [if] with no else branch
+ * answers in dyn context. It is not Unit — Unit does not box, because a value
+ * of the zero-sized type carries nothing a dyn word could hold. */
+flan_dyn flan_dyn_nil(void);
+flan_dyn flan_dyn_from_i64(int64_t v);
+flan_dyn flan_dyn_from_f64(double v);
+flan_dyn flan_dyn_from_bool(int32_t v);
+
+/* A string, as ptr+len — the shape [T] and string already have in Emit.ll.
+ * The runtime copies: the bytes behind a Flan string may be a literal in
+ * rodata or a slice of a buffer the program goes on to write. */
+flan_dyn flan_dyn_from_bytes(const uint8_t *ptr, int64_t len);
+
+/* The heterogeneous vector. In milestone 1 this is the runtime's own object
+ * rather than a Flan (Vec T) that happens to hold dyn words, which is why
+ * push/at/len on it go through the dyn ops below: the compiler knows only
+ * that it holds a dyn. */
+flan_dyn flan_dyn_vec_new(void);
+
+/* ── Operations ────────────────────────────────────────────────────────
+ *
+ * Arithmetic dispatches on what the two words actually hold and traps through
+ * flan_trap_hook when they do not agree. The message is the runtime's: it is
+ * the side that knows which pair of types arrived, and a message assembled by
+ * the compiler could only name the static types, which are dyn and dyn. */
+flan_dyn flan_dyn_add(flan_dyn a, flan_dyn b);
+flan_dyn flan_dyn_sub(flan_dyn a, flan_dyn b);
+flan_dyn flan_dyn_mul(flan_dyn a, flan_dyn b);
+flan_dyn flan_dyn_div(flan_dyn a, flan_dyn b);
+flan_dyn flan_dyn_rem(flan_dyn a, flan_dyn b);
+
+/* The orderings answer a dyn holding a bool, not a C int: the result of an
+ * operation on dyn operands is a dyn, so that a comparison can be pushed into
+ * a heterogeneous vector like anything else. Where the compiler needs an i1 to
+ * branch on it follows with flan_dyn_need_bool. */
+flan_dyn flan_dyn_lt(flan_dyn a, flan_dyn b);
+flan_dyn flan_dyn_le(flan_dyn a, flan_dyn b);
+flan_dyn flan_dyn_gt(flan_dyn a, flan_dyn b);
+flan_dyn flan_dyn_ge(flan_dyn a, flan_dyn b);
+
+/* Structural, and never traps. Two values of unrelated types are not an error
+ * to compare — they are unequal. This is the one op where a type mismatch has
+ * an answer instead of a trap, and = is the operator most likely to meet a
+ * heterogeneous container. */
+flan_dyn flan_dyn_eq(flan_dyn a, flan_dyn b);
+
+flan_dyn flan_dyn_len(flan_dyn v);
+flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i);
+void     flan_dyn_set_at(flan_dyn v, flan_dyn i, flan_dyn x);
+void     flan_dyn_push(flan_dyn v, flan_dyn x);
+void     flan_dyn_print(flan_dyn v);
+
+/* ── Extraction ────────────────────────────────────────────────────────
+ *
+ * The dyn-to-typed direction, and the only one: a dyn reaches a typed slot
+ * through an annotation the programmer wrote — a typed parameter, a typed
+ * binding — and never by inference. A mismatch traps; the runtime owns the
+ * message for the reason given above. */
+int64_t flan_dyn_need_i64(flan_dyn v);
+double  flan_dyn_need_f64(flan_dyn v);
+int32_t flan_dyn_need_bool(flan_dyn v);
+
+/* ── Roots ─────────────────────────────────────────────────────────────
+ *
+ * The collector is precise, so it has to be told where the live dyn words on
+ * the machine stack are. A dyn local or temporary that lives across a call or
+ * an allocation is pushed as a root at its binding and popped at scope exit,
+ * one [flan_dyn_root_pop] per scope carrying the count the scope pushed.
+ *
+ * The address is registered, not the word: the slot is written again while it
+ * is rooted, and a collection in between has to see the current value. */
+void flan_dyn_root_push(flan_dyn *slot);
+void flan_dyn_root_pop(int64_t n);
+
+/* Called once from main before any other function here. */
+void flan_gc_init(void);
+
+#endif /* FLAN_DYN_H */
diff --git a/runtime/flan_dyn_stub.c b/runtime/flan_dyn_stub.c
new file mode 100644
index 0000000..ae0d469
--- /dev/null
+++ b/runtime/flan_dyn_stub.c
@@ -0,0 +1,317 @@
+/* flan_dyn_stub — a standing-in implementation of the flan_dyn.h ABI.
+ *
+ * THE MERGE REPLACES THIS FILE WITH runtime/flan_dyn.c. It exists so that the
+ * compiler side of dynamic-by-default can be built and run against the fixed
+ * ABI before the real runtime lands; the real one is being written in parallel
+ * against the same header, and flan_dyn.h is the contract the two are diffed
+ * against.
+ *
+ * What it is not: it mallocs and never frees, it collects nothing, and
+ * flan_dyn_root_push / flan_dyn_root_pop record their arguments and do nothing
+ * with them. That last point matters for anyone reading a passing test here —
+ * root emission is *not* exercised by this file. A program with entirely wrong
+ * root discipline passes every test that runs against this stub. The check
+ * that does bite is the one over the emitted IR, counting pushes against pops
+ * per function; see the acceptance tests.
+ *
+ * The representation is the simplest thing that satisfies the header's rule
+ * that the word is opaque: every value is a pointer to a heap cell, including
+ * the small ones. The real runtime will not do this.
+ */
+
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+
+#include "flan_dyn.h"
+
+/* flan_rt.c's own [rt_trap] is static, so this mirrors it rather than calling
+ * it: print the sentence, offer the name to the dev daemon's hook, and leave
+ * with flan_rt's exit code so that a dyn trap is indistinguishable from any
+ * other trap to whoever is watching. The hook is flan_rt.c's global, and a
+ * program links both files. */
+extern void (*flan_trap_hook)(const uint8_t *name, int64_t namelen);
+
+static _Noreturn void dyn_trap(const char *name, const char *sentence) {
+  fflush(stdout);
+  fprintf(stderr, "%s\n", sentence);
+  fflush(stderr);
+  if (flan_trap_hook != NULL)
+    flan_trap_hook((const uint8_t *)name, (int64_t)strlen(name));
+  _exit(134);
+}
+
+enum tag { T_NIL, T_I64, T_F64, T_BOOL, T_STR, T_VEC };
+
+typedef struct cell {
+  enum tag tag;
+  union {
+    int64_t i;
+    double  f;
+    int32_t b;
+    struct { uint8_t *ptr; int64_t len; } s;
+    struct { struct cell **items; int64_t len, cap; } v;
+  } u;
+} cell;
+
+static cell *alloc(enum tag t) {
+  cell *c = calloc(1, sizeof *c);
+  if (c == NULL) dyn_trap("OutOfMemory", "the dyn runtime could not allocate");
+  c->tag = t;
+  return c;
+}
+
+static cell *as(flan_dyn d) { return (cell *)(uintptr_t)d; }
+static flan_dyn word(cell *c) { return (flan_dyn)(uintptr_t)c; }
+
+/* ── Construction ──────────────────────────────────────────────────── */
+
+flan_dyn flan_dyn_nil(void) { return word(alloc(T_NIL)); }
+
+flan_dyn flan_dyn_from_i64(int64_t v) {
+  cell *c = alloc(T_I64); c->u.i = v; return word(c);
+}
+
+flan_dyn flan_dyn_from_f64(double v) {
+  cell *c = alloc(T_F64); c->u.f = v; return word(c);
+}
+
+flan_dyn flan_dyn_from_bool(int32_t v) {
+  cell *c = alloc(T_BOOL); c->u.b = (v != 0); return word(c);
+}
+
+flan_dyn flan_dyn_from_bytes(const uint8_t *ptr, int64_t len) {
+  cell *c = alloc(T_STR);
+  c->u.s.ptr = malloc((size_t)len + 1);
+  if (c->u.s.ptr == NULL) dyn_trap("OutOfMemory", "the dyn runtime could not allocate");
+  if (len > 0) memcpy(c->u.s.ptr, ptr, (size_t)len);
+  c->u.s.ptr[len] = 0;
+  c->u.s.len = len;
+  return word(c);
+}
+
+flan_dyn flan_dyn_vec_new(void) {
+  cell *c = alloc(T_VEC);
+  c->u.v.cap = 8;
+  c->u.v.items = calloc((size_t)c->u.v.cap, sizeof(cell *));
+  if (c->u.v.items == NULL) dyn_trap("OutOfMemory", "the dyn runtime could not allocate");
+  return word(c);
+}
+
+/* ── Arithmetic ────────────────────────────────────────────────────── */
+
+/* Two numbers promote to f64 when either is one, which is the rule a reader
+ * expects of a dynamic language and is not the rule the typed language uses.
+ * The typed language has no implicit widening at all; here there is no
+ * annotation to have been written, so refusing would leave (+ 1 2.5) with no
+ * spelling that works. */
+static int numeric(cell *c) { return c->tag == T_I64 || c->tag == T_F64; }
+static double as_f(cell *c) { return c->tag == T_I64 ? (double)c->u.i : c->u.f; }
+
+static flan_dyn arith(flan_dyn a, flan_dyn b, char op) {
+  cell *x = as(a), *y = as(b);
+  if (!numeric(x) || !numeric(y)) dyn_trap("DynArithType", "this arithmetic needs two numbers, and one of the two values is not one");
+  if (x->tag == T_I64 && y->tag == T_I64) {
+    int64_t p = x->u.i, q = y->u.i, r = 0;
+    switch (op) {
+      case '+': r = p + q; break;
+      case '-': r = p - q; break;
+      case '*': r = p * q; break;
+      case '/': if (q == 0) dyn_trap("DivideByZero", "division by zero"); r = p / q; break;
+      case '%': if (q == 0) dyn_trap("DivideByZero", "division by zero"); r = p % q; break;
+    }
+    return flan_dyn_from_i64(r);
+  }
+  {
+    double p = as_f(x), q = as_f(y), r = 0;
+    switch (op) {
+      case '+': r = p + q; break;
+      case '-': r = p - q; break;
+      case '*': r = p * q; break;
+      case '/': r = p / q; break;
+      /* fmod without math.h, to keep the stub's link line as short as the
+       * real runtime's is meant to be. */
+      case '%': r = p - q * (double)(int64_t)(p / q); break;
+    }
+    return flan_dyn_from_f64(r);
+  }
+}
+
+flan_dyn flan_dyn_add(flan_dyn a, flan_dyn b) { return arith(a, b, '+'); }
+flan_dyn flan_dyn_sub(flan_dyn a, flan_dyn b) { return arith(a, b, '-'); }
+flan_dyn flan_dyn_mul(flan_dyn a, flan_dyn b) { return arith(a, b, '*'); }
+flan_dyn flan_dyn_div(flan_dyn a, flan_dyn b) { return arith(a, b, '/'); }
+flan_dyn flan_dyn_rem(flan_dyn a, flan_dyn b) { return arith(a, b, '%'); }
+
+/* ── Ordering and equality ─────────────────────────────────────────── */
+
+static int cmp(flan_dyn a, flan_dyn b) {
+  cell *x = as(a), *y = as(b);
+  if (x->tag == T_STR && y->tag == T_STR) {
+    int64_t n = x->u.s.len < y->u.s.len ? x->u.s.len : y->u.s.len;
+    int r = memcmp(x->u.s.ptr, y->u.s.ptr, (size_t)n);
+    if (r != 0) return r < 0 ? -1 : 1;
+    return x->u.s.len == y->u.s.len ? 0 : (x->u.s.len < y->u.s.len ? -1 : 1);
+  }
+  if (!numeric(x) || !numeric(y)) dyn_trap("DynCompareType", "these two values have no ordering between them");
+  if (x->tag == T_I64 && y->tag == T_I64)
+    return x->u.i == y->u.i ? 0 : (x->u.i < y->u.i ? -1 : 1);
+  {
+    double p = as_f(x), q = as_f(y);
+    return p == q ? 0 : (p < q ? -1 : 1);
+  }
+}
+
+flan_dyn flan_dyn_lt(flan_dyn a, flan_dyn b) { return flan_dyn_from_bool(cmp(a, b) <  0); }
+flan_dyn flan_dyn_le(flan_dyn a, flan_dyn b) { return flan_dyn_from_bool(cmp(a, b) <= 0); }
+flan_dyn flan_dyn_gt(flan_dyn a, flan_dyn b) { return flan_dyn_from_bool(cmp(a, b) >  0); }
+flan_dyn flan_dyn_ge(flan_dyn a, flan_dyn b) { return flan_dyn_from_bool(cmp(a, b) >= 0); }
+
+/* Structural, and never traps — the header's one exception. */
+static int eq(cell *x, cell *y) {
+  if (numeric(x) && numeric(y)) {
+    if (x->tag == T_I64 && y->tag == T_I64) return x->u.i == y->u.i;
+    return as_f(x) == as_f(y);
+  }
+  if (x->tag != y->tag) return 0;
+  switch (x->tag) {
+    case T_NIL:  return 1;
+    case T_BOOL: return x->u.b == y->u.b;
+    case T_STR:  return x->u.s.len == y->u.s.len
+                     && memcmp(x->u.s.ptr, y->u.s.ptr, (size_t)x->u.s.len) == 0;
+    case T_VEC: {
+      if (x->u.v.len != y->u.v.len) return 0;
+      for (int64_t i = 0; i < x->u.v.len; i++)
+        if (!eq(x->u.v.items[i], y->u.v.items[i])) return 0;
+      return 1;
+    }
+    default: return 0;
+  }
+}
+
+flan_dyn flan_dyn_eq(flan_dyn a, flan_dyn b) {
+  return flan_dyn_from_bool(eq(as(a), as(b)));
+}
+
+/* ── Containers ────────────────────────────────────────────────────── */
+
+static cell *need_vec(flan_dyn v) {
+  cell *c = as(v);
+  if (c->tag != T_VEC) dyn_trap("DynNotAVec", "this value is not a vector, so it has no elements");
+  return c;
+}
+
+static int64_t need_index(flan_dyn i) {
+  cell *c = as(i);
+  if (c->tag != T_I64) dyn_trap("DynIndexType", "an index must be an integer");
+  return c->u.i;
+}
+
+flan_dyn flan_dyn_len(flan_dyn v) {
+  cell *c = as(v);
+  if (c->tag == T_STR) return flan_dyn_from_i64(c->u.s.len);
+  return flan_dyn_from_i64(need_vec(v)->u.v.len);
+}
+
+flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i) {
+  cell *c = need_vec(v);
+  int64_t k = need_index(i);
+  if (k < 0 || k >= c->u.v.len) dyn_trap("Bounds", "index out of bounds");
+  return word(c->u.v.items[k]);
+}
+
+void flan_dyn_set_at(flan_dyn v, flan_dyn i, flan_dyn x) {
+  cell *c = need_vec(v);
+  int64_t k = need_index(i);
+  if (k < 0 || k >= c->u.v.len) dyn_trap("Bounds", "index out of bounds");
+  c->u.v.items[k] = as(x);
+}
+
+void flan_dyn_push(flan_dyn v, flan_dyn x) {
+  cell *c = need_vec(v);
+  if (c->u.v.len == c->u.v.cap) {
+    int64_t cap = c->u.v.cap * 2;
+    cell **items = realloc(c->u.v.items, (size_t)cap * sizeof(cell *));
+    if (items == NULL) dyn_trap("OutOfMemory", "the dyn runtime could not allocate");
+    c->u.v.items = items;
+    c->u.v.cap = cap;
+  }
+  c->u.v.items[c->u.v.len++] = as(x);
+}
+
+static void print_cell(cell *c) {
+  switch (c->tag) {
+    case T_NIL:  fputs("nil", stdout); break;
+    case T_I64:  printf("%lld", (long long)c->u.i); break;
+    /* %g, so that a whole-numbered f64 does not print as an i64 would and
+     * the two remain distinguishable in a test's expected output. */
+    case T_F64:  printf("%g", c->u.f); break;
+    case T_BOOL: fputs(c->u.b ? "true" : "false", stdout); break;
+    case T_STR:  printf("%.*s", (int)c->u.s.len, (const char *)c->u.s.ptr); break;
+    case T_VEC:
+      fputc('[', stdout);
+      for (int64_t i = 0; i < c->u.v.len; i++) {
+        if (i > 0) fputc(' ', stdout);
+        print_cell(c->u.v.items[i]);
+      }
+      fputc(']', stdout);
+      break;
+  }
+}
+
+void flan_dyn_print(flan_dyn v) { print_cell(as(v)); }
+
+/* ── Extraction ────────────────────────────────────────────────────── */
+
+int64_t flan_dyn_need_i64(flan_dyn v) {
+  cell *c = as(v);
+  if (c->tag != T_I64) dyn_trap("DynExpectedI64", "this value was required to be an i64 and is not");
+  return c->u.i;
+}
+
+double flan_dyn_need_f64(flan_dyn v) {
+  cell *c = as(v);
+  /* An i64 satisfies an f64 slot, because a dyn integer literal is an i64 by
+   * the header's rule and (defvar x f64 (f 1)) would otherwise be unwritable
+   * for any f returning dyn. The reverse is not true: f64 to i64 loses. */
+  if (c->tag == T_I64) return (double)c->u.i;
+  if (c->tag != T_F64) dyn_trap("DynExpectedF64", "this value was required to be an f64 and is not");
+  return c->u.f;
+}
+
+int32_t flan_dyn_need_bool(flan_dyn v) {
+  cell *c = as(v);
+  if (c->tag != T_BOOL) dyn_trap("DynExpectedBool", "this value was required to be a bool and is not");
+  return c->u.b;
+}
+
+/* ── Roots ─────────────────────────────────────────────────────────────
+ *
+ * Recorded and otherwise ignored. The shadow stack is kept, and its depth
+ * checked against the pops, only so that a badly unbalanced emission fails
+ * loudly here rather than silently: an over-pop is a compiler bug worth
+ * dying on even in a stub that collects nothing. Under-pushing is invisible,
+ * and stays invisible until the real collector lands. */
+
+static flan_dyn **roots = NULL;
+static int64_t    roots_len = 0, roots_cap = 0;
+
+void flan_dyn_root_push(flan_dyn *slot) {
+  if (roots_len == roots_cap) {
+    int64_t cap = roots_cap == 0 ? 64 : roots_cap * 2;
+    flan_dyn **r = realloc(roots, (size_t)cap * sizeof(flan_dyn *));
+    if (r == NULL) dyn_trap("OutOfMemory", "the dyn runtime could not allocate");
+    roots = r;
+    roots_cap = cap;
+  }
+  roots[roots_len++] = slot;
+}
+
+void flan_dyn_root_pop(int64_t n) {
+  if (n < 0 || n > roots_len) dyn_trap("DynRootUnderflow", "the dyn root stack was popped further than it was pushed - a compiler bug");
+  roots_len -= n;
+}
+
+void flan_gc_init(void) { /* nothing to initialise: this stub never collects */ }
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 5d46e1e..817e0bd 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -399,9 +399,15 @@ let () =
    | Arr [ _; _; _ ] -> () | _ -> check "array literal" false);
 
   (* ── Types: brackets mean different things by position ─────────── *)
+  (* Read out of [praw], not [params]: a defn's parameter vector is carried
+     undecided until Check pairs it, so the parser no longer fills [params] at
+     all. Every type spelled here is one the parser still resolves on sight —
+     brackets and lists are types by their shape whatever the environment says
+     — so [Ptype] is the shape under test and a [Pname] here would mean the
+     spelling stopped being recognised as a type. *)
   let ty src =
     match parse_decl (Printf.sprintf "(defn f [x %s] ())" src) with
-    | { d = Defn { params = [ { fty; _ } ]; _ }; _ } -> fty.t
+    | { d = Defn { praw = Some [ Pname ("x", _); Ptype t ]; _ }; _ } -> t.t
     | _ -> failwith "bad type test"
   in
   (match ty "[u8]" with Tslice _ -> () | _ -> check "[T] is a slice" false);
@@ -421,7 +427,7 @@ let () =
 
   (* ── Declarations ──────────────────────────────────────────────── *)
   (match (parse_decl "(defn f [x i32] bool x)").d with
-   | Defn { ret = Some _; params = [ _ ]; fbody = [ _ ]; _ } -> ()
+   | Defn { ret = Some _; praw = Some [ _; _ ]; fbody = [ _ ]; _ } -> ()
    | _ -> check "defn with return type" false);
   (* () is the unit return type, and the body is what follows it. *)
   (match (parse_decl "(defn f [x i32] () (g x))").d with
@@ -840,9 +846,22 @@ let () =
   rejects_check "a mistyped struct"
     "(defstruct Cursor [x i32]) (defn f [c Curser] ())"
     ~needle:"did you mean Cursor?";
-  (* Nothing close: the type-variable rule still applies, and still names the
-     milestone. *)
-  rejects_check "a real type variable" "(defn f [x t] ())"
+  (* [(defn f [x t] ())] used to be one parameter of an unimplemented generic
+     type and is now two parameters of type dyn — a lowercase name resembling
+     no type is a parameter, which is the whole of dynamic-by-default. The
+     milestone-5 reading is still reachable, by writing the type variable with
+     the sigil the signature binds it with. *)
+  (match checked "(defn f [x t] ())" with
+   | p ->
+     (match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = "f") p.Tast.fns with
+      | Some { Tast.params = [ Types.Dyn; Types.Dyn ]; _ } -> ()
+      | _ -> check "an unannotated pair is two dyn parameters" false)
+   | exception _ -> check "an unannotated pair is two dyn parameters" false);
+  (* A bare lowercase name is still an unimplemented type variable everywhere a
+     type is the only thing a slot can hold. A defn's parameter vector stopped
+     being such a place — a slot there may be a parameter instead — so the rule
+     is exercised where it still decides, at a field. *)
+  rejects_check "a real type variable" "(defstruct Holder [x elem])"
     ~needle:"milestone 5";
   rejects_check "an unknown concrete type" "(defn f [x Widget] ())"
     ~needle:"unknown type Widget";
@@ -1327,7 +1346,7 @@ let () =
      defn's body that just answers one says nothing about them. *)
   rejects_check "an fn with nothing to say what it takes"
     "(defn f [] () (fn [x] x))" ~needle:"nothing here says what this fn";
-  rejects_check "type variables are milestone 5" "(defn f [x a] ())"
+  rejects_check "type variables are milestone 5" "(defn f [] a 0)"
     ~needle:"milestone 5";
   (* The other half: a name in value position now *works*, and the arity is
      checked against the function it names. *)