diff --git a/lib/check.ml b/lib/check.ml
index 9a8deda..50be294 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1972,12 +1972,38 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     let name =
       match c.Tast.ty with
       | Types.Named n -> n
+      (* Its own arm ahead of the general one, because "a condition is a
+         struct, not dyn" would read as a rule about shape when the answer is a
+         milestone. A condition crosses a handler boundary as a pointer to a
+         frame that is still alive, and a dyn payload has to stay rooted across
+         that transfer — which is the collector's question, not this one's, and
+         it is milestone 2's. *)
+      | Types.Dyn ->
+        no_dyn_yet c.Tast.loc ~into:false Types.Dyn
+          " — a condition crosses a handler boundary and a dyn payload has to \
+           stay rooted across the transfer, which is milestone 2"
       | t ->
         fail c.Tast.loc
           "a condition is a struct, not %s — matching is by type and there is \
            no condition hierarchy"
           (Types.to_string t)
     in
+    (* And the same refusal for a condition that merely *holds* one. The
+       payload is what crosses, so a dyn field is the dyn payload the note
+       above is about, whatever the struct around it is called. *)
+    (match Hashtbl.find_opt ctx.env.structs name with
+     | Some (s : Tast.structure) ->
+       List.iter
+         (fun (f : Tast.field) ->
+            if f.Tast.fty = Types.Dyn then
+              no_dyn_yet c.Tast.loc ~into:false Types.Dyn
+                (Printf.sprintf
+                   " — the field %s of the condition %s is one, and a payload \
+                    has to stay rooted across a handler transfer, which is \
+                    milestone 2"
+                   f.Tast.fname name))
+         s.Tast.fields
+     | None -> ());
     (* §1 and §2. [signal] is Unit whatever it finds; [error] is Never,
        because the only way past it is a handler that transfers — one that
        returns normally has not answered it, and the program stops. *)
@@ -3357,12 +3383,10 @@ and fold_left_prim ctx ~want loc name p ok what args =
   let x, y, rest =
     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
-  (* One dyn operand makes the whole fold dyn. [binary] has already checked the
-     second against the first, so a mixed pair arrives with the typed side
-     boxed — [(+ x 1)] over a dyn [x] checked the literal at dyn and got an i64
-     five in a box. What is left is to fold with the runtime's operator instead
-     of the machine's. *)
+  let a, b = binary ctx ~dyn_ok:true name loc ~want:(numeric_want want) [ x; y ] in
+  (* One dyn operand makes the whole fold dyn, whichever side it is on. The
+     typed side is boxed by [dyn_fold]; a literal was already built at dyn by
+     [binary], so [(+ x 1)] over a dyn x folds an i64 one. *)
   if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
     dyn_fold ctx ~want loc name [ a; b ] rest
   else begin
@@ -3695,7 +3719,7 @@ and named_call ctx ~want loc name args =
      nobody writes on purpose. *)
   | "%" ->
     arity loc name 2 args;
-    let a, b = binary ctx name loc ~want:(numeric_want want) args in
+    let a, b = binary ctx ~dyn_ok:true name loc ~want:(numeric_want want) args in
     if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
       dyn_fold ctx ~want loc name [ a; b ] []
     else begin
@@ -3710,7 +3734,7 @@ and named_call ctx ~want loc name args =
       | "<=" -> Tast.Le | ">" -> Tast.Gt | _ -> Tast.Ge
     in
     arity loc name 2 args;
-    let a, b = binary ctx name loc ~want:None args in
+    let a, b = binary ctx ~dyn_ok:true name loc ~want:None args in
     (* A comparison with a dyn operand answers a *bool*, not a dyn, even though
        the runtime's own entry point answers a dyn holding one. The reason is
        where the result goes: a comparison is overwhelmingly the test of an
@@ -4056,6 +4080,25 @@ and named_call ctx ~want loc name args =
      out. *)
   | "vec-new" ->
     let elem, args = vec_new_elem ctx ~want loc args in
+    (* [(vec-new dyn)] is not a [(Vec dyn)]. At milestone 1 the heterogeneous
+       container is the dyn runtime's own object, and its type is [dyn] like
+       everything else the runtime hands back — which is what lets [push], [at]
+       and [len] on it go through the dyn operations rather than through a
+       type-erased Vec over eight-byte elements.
+
+       The two could be made to coincide later, and the reason not to now is
+       the collector: a Flan Vec's storage comes from an allocator the program
+       named, and the words in it would be roots the collector has to find
+       inside a block it does not own. The runtime's own vector is storage the
+       collector already knows about. *)
+    if elem = Types.Dyn then begin
+      if args <> [] then
+        fail loc
+          "(vec-new dyn) takes no allocator — the dyn container's storage is \
+           the dyn runtime's, which is what lets the collector find the values \
+           inside it";
+      expect loc ~want (rt loc Types.Dyn "flan_dyn_vec_new" [])
+    end else begin
     let a = allocator_arg ctx loc args in
     let v = fresh_slot ctx (Types.Vec elem) in
     let attempt =
@@ -4073,12 +4116,23 @@ and named_call ctx ~want loc name args =
                       region_check ctx.env loc
                         (mk loc (Types.Vec elem) (Tast.Local v))
                         (mk loc (Types.Vec elem) (Tast.Local v)) ])))
+    end
   (* Unit, not a Result and not an ignorable error code: see [alloc_guard]. *)
   | "push" ->
     arity loc name 2 args;
     (match args with
      | [ target; x ] ->
        let target = check ctx target in
+       (* A push into a dyn container is a call and nothing else: no allocation
+          guard, no restart, no region check. The dyn runtime owns the storage
+          and answers a failure to grow it on its own terms — the guard and the
+          retry restart exist for an allocator the *program* named, and here
+          there is none to name. *)
+       if target.Tast.ty = Types.Dyn then
+         expect loc ~want
+           (rt loc Types.Unit "flan_dyn_push"
+              [ target; check ctx ~want:Types.Dyn x ])
+       else begin
        let elem = vec_elem loc "push" target.Tast.ty in
        let x = check ctx ~want:elem x in
        (* The element is bound before the loop so that a [retry] re-attempts
@@ -4101,6 +4155,7 @@ and named_call ctx ~want loc name args =
                            (with_note loc (alloc_guard ctx loc attempt)
                               (reg_note loc "flan_dev_reg_note_vec" target
                                  [ size_of loc elem ] elem)) ])))
+       end
      | _ -> assert false)
   | "reserve" ->
     arity loc name 2 args;
@@ -4824,6 +4879,14 @@ and named_call ctx ~want loc name args =
      | Types.Map _ ->
        let n = rt loc (Types.Int Types.I64) "flan_map_len" [ a; here loc ] in
        expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
+     (* A dyn length is an i32 like every other length here, not a dyn holding
+        one. [len] is what an index loop compares against, and handing back a
+        boxed number would make [(< i (len xs))] a dyn comparison and a pair of
+        allocations per iteration. The runtime answers a dyn; it is unboxed at
+        once and narrowed the way the Vec's i64 above is. *)
+     | Types.Dyn ->
+       let n = unbox loc (Types.Int Types.I64) (rt loc Types.Dyn "flan_dyn_len" [ a ]) in
+       expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
      | other ->
        fail loc
          "len takes an array, a slice, a string, a Vec or a Map, found %s"
@@ -4836,6 +4899,19 @@ and named_call ctx ~want loc name args =
         | Types.Vec _ ->
           let p, elem = vec_at ctx loc target idx in
           expect loc ~want (mk loc elem (Tast.Deref p))
+        (* One index, because a dyn container is one dimension: the nested
+           [(at grid r c)] spelling walks a type the compiler can see through,
+           and here it cannot. [(at (at g r) c)] is the spelling that works and
+           is what the refusal names. *)
+        | Types.Dyn ->
+          (match idx with
+           | [ i ] ->
+             expect loc ~want
+               (rt loc Types.Dyn "flan_dyn_at" [ target; check ctx ~want:Types.Dyn i ])
+           | _ ->
+             fail loc
+               "(at ...) over a dyn takes one index — the compiler cannot see \
+                the shape of a dyn container, so write (at (at x i) j)")
         | _ ->
           let idx, ty = indexed ctx target idx in
           prim Tast.At ty (target :: idx))
@@ -5466,7 +5542,7 @@ and numeric_want want =
    widening, so one side has to decide it. Check the side that carries the most
    information first: a non-literal over a literal, and a float literal over an
    integer one, since an integer constant converts to a float and not back. *)
-and binary ctx name loc ~want args =
+and binary ctx ?(dyn_ok = false) name loc ~want args =
   match args with
   | [ x; y ] ->
     let y_decides =
@@ -5475,11 +5551,46 @@ and binary ctx name loc ~want args =
           | (Ast.Int _ | Ast.Byte _), Ast.Float _ -> true
           | _ -> false)
     in
+    (* A form that cannot be checked without being told what is wanted. A
+       literal takes its width from the expectation, and a keyword has no
+       meaning at all without one — [:lo] resolves against the enum the site
+       expects and there is no keyword type to fall back on. Everything else
+       checks on its own terms. *)
+    let needs_want (f : Ast.expr) =
+      is_literal f || (match f.Ast.e with Ast.Kw _ -> true | _ -> false)
+    in
     if y_decides then begin
       let b = check ctx ?want y in
       let a = check ctx ~want:b.Tast.ty x in
       a, b
-    end else begin
+    end
+    (* [dyn_ok] is set by the operators that have a dyn lowering, and it exists
+       to stop the second operand being coerced to the first's type before
+       anybody has asked whether the pair is a dyn one.
+
+       Without it [(+ n x)] over an [i64] n and a dyn x threads [i64] into the
+       second check, [expect] does what an annotation site asked for and
+       unboxes, and the result is a *machine* add of a value the runtime was
+       never asked about: the program traps on a float instead of promoting,
+       and nothing in the source says why. The mirror image [(+ x n)] boxed
+       correctly, so the bug was visible only in one operand order.
+
+       Both sides are checked on their own terms here and the caller decides.
+       That is safe exactly when neither operand needs an expectation, which is
+       what [needs_want] settles — a literal still gets the first operand's
+       type, so [(+ x 1)] over a dyn x goes on building an i64 one. *)
+    else if dyn_ok && not (needs_want y) then begin
+      let a = check ctx ?want x in
+      let b = check ctx y in
+      (* Nothing dyn about this pair after all, so it is put back the way the
+         typed path built it. Re-checking only when the types actually differ
+         keeps the common case to one check of each operand. *)
+      if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn
+         || Types.equal a.Tast.ty b.Tast.ty
+      then a, b
+      else a, check ctx ~want:a.Tast.ty y
+    end
+    else begin
       let a = check ctx ?want x in
       let b = check ctx ~want:a.Tast.ty y in
       a, b
@@ -5921,6 +6032,19 @@ let collect env (decls : Ast.decl list) =
            | Types.Int _ | Types.Float _ | Types.Bool | Types.Ptr _
            | Types.Enum _ | Types.Unit -> ()
            | Types.String | Types.Slice _ when what = "a parameter" -> ()
+           (* Its own arm, because the general advice below is wrong for it and
+              dangerously so. A dyn is one machine word and would cross without
+              complaint — [(Ptr dyn)] is not the fix and there is nothing for a
+              shim to read: what the C side would receive is a word whose
+              meaning only the dyn runtime knows, and C has no way to ask.
+              Refused by name rather than let through as an integer. *)
+           | Types.Dyn ->
+             fail loc
+               "%s of %s is dyn, which does not cross to C. A dyn is one word \
+                and would pass as an integer, but what the word means is the \
+                dyn runtime's and there is nothing on the C side that can ask \
+                — take the value at a written type and pass that"
+               what fn.Ast.name
            | _ ->
              fail loc
                "%s of %s is %s, which cannot cross to C directly — pass \
diff --git a/lib/emit.ml b/lib/emit.ml
index fcd3cdf..6d4264f 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -2343,6 +2343,17 @@ and cast f ~guard (x : Tast.expr) target =
          runtime answers a pointer or NULL and the Option is built in the
          checker, so the null test is one integer compare on the address. *)
       | Types.Ptr _, Types.Int Types.I64 -> "ptrtoint"
+      (* Not written in the surface language either — this language has no
+         conversion between bool and a number, and deliberately. The dyn
+         boundary needs both halves: runtime/flan_dyn.h takes and answers a
+         bool as an [int32_t], because a C signature saying [_Bool] is a width
+         question nobody wants, and [bool] is an [i1] here.
+
+         The truncation is safe in the one direction it runs: what comes back
+         from [flan_dyn_need_bool] is 0 or 1, because the runtime has already
+         decided the value was a bool, so the discarded bits are zero. *)
+      | Types.Bool, Types.Int _ -> "zext"
+      | Types.Int _, Types.Bool -> "trunc"
       | _ -> failwith "unsupported cast"
     in
     if op = "bitcast" then v
diff --git a/lib/types.ml b/lib/types.ml
index 18c2ba2..a780fa2 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -83,7 +83,7 @@ let fkind_of_name = function
    is spelled [()] in source, and [Parse.texpr] refuses the word. *)
 let primitive_names =
   [ "i8"; "i16"; "i32"; "i64"; "u8"; "u16"; "u32"; "u64";
-    "f32"; "f64"; "bool"; "string"; "Unit"; "Never"; "Allocator" ]
+    "f32"; "f64"; "bool"; "string"; "dyn"; "Unit"; "Never"; "Allocator" ]
 
 let ikind_name k =
   (if signed k then "i" else "u") ^ string_of_int (bits k)
diff --git a/mix b/mix
new file mode 100755
index 0000000..362c28d
Binary files /dev/null and b/mix differ
diff --git a/test/programs/dyn-vec.flan b/test/programs/dyn-vec.flan
new file mode 100644
index 0000000..6d74b5a
--- /dev/null
+++ b/test/programs/dyn-vec.flan
@@ -0,0 +1,24 @@
+;;;; A container holding four different types at once.
+;;;;
+;;;; (vec-new dyn) is not a (Vec dyn) — it is the dyn runtime's own vector, and
+;;;; its type is dyn like everything else the runtime hands back. That is what
+;;;; lets push, at and len on it be the dyn operations rather than a
+;;;; type-erased Vec over eight-byte elements, and it is why no allocator is
+;;;; named: the storage is the collector's to walk.
+
+(defn main [] ()
+  (let [xs (vec-new dyn)]
+    (push xs 1)
+    (push xs 2.5)
+    (push xs "three")
+    (push xs true)
+    (print (len xs))
+    (print "\n")
+    (print xs)
+    (print "\n")
+    ;; Read back out one at a time, to show that at answers a dyn and that the
+    ;; four of them are still four different things.
+    (dotimes [i (len xs)]
+      (print (at xs i))
+      (print " "))
+    (print "\n")))