diff --git a/TODO.org b/TODO.org
index e23add54..c1ee43de 100644
--- a/TODO.org
+++ b/TODO.org
@@ -800,14 +800,6 @@ One spelling for one operation; != stays, and not= is refused with a suggestion
 of !=.
 
 * Checker
-** TODO A u64 above the i64 maximum becomes -1 when it crosses into dyn
-=(+ z u)= and =(max u 0 z)= with u = u64 max read u as -1, silently. It should trap at
-the crossing, as a u64 field read through a view already does.
-** TODO A dyn nil past the first pair of a fold is refused at compile time
-=(+ 1 2 (the dyn nil))= says nil has no None at i32, while =(+ (the dyn nil) 1 2)= traps
-at run time. Both should trap at run time.
-** TODO A generic $t beside a dyn operand is refused
-"does not cross into a written type yet"; rule 117 says typed beside dyn gives dyn.
 ** WAIT Checking a wide fold of let operands is slow
 Parked 2026-09-26: design first; remeasure on a quiet machine, it was timed under load 20.
 A 2000-operand (bit-and (let …) …) takes 32 s to check (37 s before the bit operators);
diff --git a/lib/check.ml b/lib/check.ml
index 48360e96..e01bca51 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -4415,6 +4415,10 @@ let box ?ctx loc (e : Tast.expr) : Tast.expr =
   (* Dyn text is immutable and a String is not, so a String crosses as a copy
      of its bytes rather than as the view any other struct would be. *)
   | t when is_string_ty t -> dyn "flan_dyn_from_string" [ string_vec loc e ]
+  (* A dyn int is an i64, so a u64 past the largest i64 has none to become:
+     read as its bits it would be a different, negative number. It traps
+     here, at the crossing, as one read through a view does. *)
+  | Types.Int Types.U64 -> dyn "flan_dyn_from_u64" [ e; here loc ]
   | Types.Int _ -> dyn "flan_dyn_from_i64" [ widen loc dyn_i64 e ]
   | Types.Float _ -> dyn "flan_dyn_from_f64" [ widen loc dyn_f64 e ]
   (* The ABI takes an [int32_t], because a C signature that says [_Bool] is a
@@ -4435,6 +4439,28 @@ let box ?ctx loc (e : Tast.expr) : Tast.expr =
     Loc.failk "check/dyn-unit" loc
       "() does not box into dyn. The absent dyn value is nil — write nil"
   | Types.Never -> e
+  (* A [$t] is seen only in a generic's abstract pass; each copy is checked
+     again at its concrete type, where the value boxes as that type does, and
+     this node is thrown away with the rest of the pass. Admitting it is sound
+     only when every type the variable can be at crosses, or a refusal would
+     move from the definition to whichever call instantiates it at a pointer,
+     an enum or a function, with no written requirement to blame — the rule
+     beside [println]'s deferral. Every [is-numeric] type crosses (a u64 past
+     the largest i64 traps at run time, not at a copy's check), so that bound
+     admits it. [is-ordered] and [is-equal] do not: both admit an enum, which
+     has no dyn value. The node is a cast rather than [flan_dyn_nil] because
+     [is_nil_lit] would read that as a nil literal. *)
+  | Types.Var v
+    when (match ctx with
+          | Some c -> declares c.env.tvpreds v "is-numeric"
+          | None -> false) ->
+    mk loc Types.Dyn (Tast.Prim (Tast.Cast Types.Dyn, [ e ]))
+  | Types.Var _ ->
+    let t = tyname loc e.Tast.ty in
+    Loc.failk "check/dyn-type-variable" loc
+      "%s may be a type with no dyn value, such as a pointer or an enum, so \
+       it crosses into dyn only as a number. Write %s at the head of the body"
+      t (where_text loc "is-numeric" t)
   (* A view, not a copy: the box holds a small record naming where the
      storage is and what one element is (its descriptor, [view_desc]), and
      every read or write goes straight through to the container's own
@@ -4522,7 +4548,7 @@ let box ?ctx loc (e : Tast.expr) : Tast.expr =
      caller that starts doing that gets a sentence instead of a silent
      mis-lowering. *)
   | Types.Named _ | Types.Enum _ | Types.Option _ | Types.Ptr _
-  | Types.Alloc | Types.Fn _ | Types.CFn _ | Types.Var _ | Types.Len _
+  | Types.Alloc | Types.Fn _ | Types.CFn _ | Types.Len _
   | Types.LArray _ | Types.Vec _ | Types.Array _ | Types.Slice _ ->
     no_dyn_yet loc ~into:true e.Tast.ty ""
 
@@ -6812,9 +6838,9 @@ and wide_literal loc ~want n s =
   | Some Types.Dyn ->
     Loc.failk literal_at_want loc
       "expected dyn, found the integer literal %s, which only a u64 holds — a \
-       dyn integer is an i64. Write (u64 %s) for the u64, which a dyn holds as \
-       the i64 with the same bits, %Ld"
-      s s n
+       dyn integer is an i64, and no i64 is this large. Give what holds it \
+       the type u64"
+      s
   | Some other ->
     Loc.failk literal_at_want loc
       "expected %s, found the integer literal %s, which only a u64 holds"
@@ -11820,7 +11846,7 @@ and fold_left_prim ctx ~want loc name p ~needs ok what args =
             | `Typed v -> steps (mk loc acc.Tast.ty (Tast.Prim (p, [ acc; v ]))) tl
             | `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
         else
-          match fold_operand ctx acc.Tast.ty (check ctx ~want:acc.Tast.ty arg) with
+          match fold_arg ctx acc.Tast.ty arg with
           | `Typed v -> steps (mk loc acc.Tast.ty (Tast.Prim (p, [ acc; v ]))) tl
           | `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
     in
@@ -11847,7 +11873,7 @@ and fold_left_prim ctx ~want loc name p ~needs ok what args =
   let rec steps acc = function
     | [] -> expect ctx loc ~want acc
     | arg :: tl ->
-      match fold_operand ctx ty (check ctx ~want:ty arg) with
+      match fold_arg ctx ty arg with
       | `Typed v -> steps (mk loc ty (Tast.Prim (p, [ acc; v ]))) tl
       | `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
   in
@@ -11865,6 +11891,26 @@ and fold_operand ctx ty (v : Tast.expr) =
     | Some d -> `Dyn d
     | None -> `Typed v
 
+(* An operand past a fold's first pair, from the source: at the type so far,
+   and on its own terms only when that is refused, as [binary_pair] checks
+   the second of the pair. A dyn it turns out to be joins the fold as a dyn,
+   so (+ 1 2 (the dyn nil)) traps at run time as (+ (the dyn nil) 1 2) does
+   instead of being refused for a nil with no value at i32, and a dyn beside
+   a [$t] is not opened at the variable. Anything else is checked at the type
+   again, for real, so its refusal is the one it always gave and recovery
+   records it. *)
+and fold_arg ctx ty (arg : Ast.expr) =
+  match trial_at ctx arg ty with
+  | Ok v -> fold_operand ctx ty v
+  | Error _ ->
+    let own () =
+      let v = check ctx arg in
+      if v.Tast.ty = Types.Dyn then v else fail arg.Ast.loc "not a dyn"
+    in
+    match trial ctx own with
+    | Ok v -> `Dyn v
+    | Error _ -> fold_operand ctx ty (check ctx ~want:ty arg)
+
 (* A pair an arithmetic operator refused, when one operand is a char: that
    is the refusal to give, rather than the mismatch between the two. Asked
    only after the refusal, so a pair that checks costs nothing more. *)
@@ -11976,10 +12022,10 @@ and dyn_fold ctx ~want loc name first rest =
      language's type error, and until now it printed with no file, no line and
      no column — [here loc] is the same string literal [cast_dyn] hands the
      runtime, and the runtime prints it as a GNU prefix. *)
-  let apply acc b = rt loc Types.Dyn sym [ acc; box loc b; here loc ] in
+  let apply acc b = rt loc Types.Dyn sym [ acc; box ~ctx loc b; here loc ] in
   let acc =
     match first with
-    | [ a; b ] -> apply (box loc a) b
+    | [ a; b ] -> apply (box ~ctx loc a) b
     | _ -> assert false
   in
   let operand arg =
@@ -13464,15 +13510,15 @@ and named_call ?(qualified = false) ctx ~want loc name args =
       in
       let r =
         match rest with
-        | [] -> link (box loc a) (box loc b)
+        | [] -> link (box ~ctx loc a) (box ~ctx loc b)
         | _ -> cmp_over ctx loc Types.Dyn ~pairs ~link (ops ())
       in
       expect ctx loc ~want r
     in
     if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
       dyn_chain (fun () ->
-          box loc a :: box loc b
-          :: map_lr (fun e -> box loc (check ctx ~want:Types.Dyn e)) rest)
+          box ~ctx loc a :: box ~ctx loc b
+          :: map_lr (fun e -> box ~ctx loc (check ctx ~want:Types.Dyn e)) rest)
     else begin
     (* [=] and [!=] admit types [<] does not. A handle is one: a pair of
        numbers in one word and where being the same entity is the question the
@@ -13508,14 +13554,14 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     | _ ->
       let ty = a.Tast.ty in
       let link u v = mk loc Types.Bool (Tast.Prim (p, [ u; v ])) in
-      let rest = map_lr (fun e -> fold_operand ctx ty (check ctx ~want:ty e)) rest in
+      let rest = map_lr (fold_arg ctx ty) rest in
       (* A dyn past the first pair makes the whole chain the dyn runtime's,
          for [fold_operand]'s reason: a chain is its pairs, and a pair with a
          dyn in it is a dyn comparison. *)
       if List.exists (function `Dyn _ -> true | `Typed _ -> false) rest then
         dyn_chain (fun () ->
-            box loc a :: box loc b
-            :: List.map (function `Dyn d -> d | `Typed v -> box loc v) rest)
+            box ~ctx loc a :: box ~ctx loc b
+            :: List.map (function `Dyn d -> d | `Typed v -> box ~ctx loc v) rest)
       else
         let ops =
           a :: b :: List.map (function `Typed v -> v | `Dyn d -> d) rest in
@@ -13598,7 +13644,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
            if v.Tast.ty <> Types.Dyn then bits_operand ctx v.Tast.loc name v)
         [ a; b ];
       expect ctx loc ~want
-        (rt loc Types.Dyn (dyn_bits_sym name) [ box loc a; box loc b; here loc ])
+        (rt loc Types.Dyn (dyn_bits_sym name) [ box ~ctx loc a; box ~ctx loc b; here loc ])
     end else begin
     bits_operand ctx loc name a;
     (* A shift by the operand's own width or more is poison in LLVM, which at
@@ -13663,7 +13709,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     let rec steps acc = function
       | [] -> expect ctx loc ~want acc
       | arg :: tl ->
-        match fold_operand ctx ty (check ctx ~want:ty arg) with
+        match fold_arg ctx ty arg with
         | `Typed v -> steps (pick acc v) tl
         | `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
     in
@@ -20745,6 +20791,9 @@ let memory_class (sym : string) (args : Tast.expr list) =
   | "flan_dyn_from_i64" when (match args with [ x ] -> int_may_spill x | _ -> true) ->
     gc "may allocate: an i64 outside ±2^47 does not fit a dyn's payload and \
         spills onto the collector's heap"
+  | "flan_dyn_from_u64" when (match args with x :: _ -> int_may_spill x | [] -> true) ->
+    gc "may allocate: a u64 above 2^47 does not fit a dyn's payload and \
+        spills onto the collector's heap"
   (* ── An allocator the program named ── *)
   | "flan_arena_new" ->
     native "allocates: an arena takes its whole region from the host here"
diff --git a/lib/emit.ml b/lib/emit.ml
index 12bf55ca..d18cb4c3 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -5067,6 +5067,7 @@ declare void @flan_alloc_set_budget(ptr, i64)
 ; ever looks inside one, so every operation on a dyn value is one of these.
 declare i64 @flan_dyn_nil()
 declare i64 @flan_dyn_from_i64(i64)
+declare i64 @flan_dyn_from_u64(i64, ptr, i64)
 declare i64 @flan_dyn_from_f64(double)
 declare i64 @flan_dyn_from_bool(i32)
 declare i64 @flan_dyn_from_bytes(ptr, i64)
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index d3c8fcbf..455bff6e 100644
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@@ -1909,6 +1909,26 @@ flan_dyn flan_dyn_from_i64(int64_t x) {
   return dyn_make(BOX_OBJ, (uint64_t)(uintptr_t)o);
 }
 
+/* A u64 has a dyn int to become only up to the largest i64; past it the trap
+ * names the number, which read as an i64 would be a different one. [what] is
+ * "u64" for a scalar crossing and "u64 element" for one read through a view,
+ * so both say the same sentence. */
+static flan_dyn u64_to_dyn(const uint8_t *loc, int64_t loclen, const char *op,
+                           const char *what, uint64_t x) {
+  if (x > (uint64_t)INT64_MAX) {
+    flan_say(loc, loclen,
+             "dyn%s%s: this %s is %llu, above the largest dyn int "
+             "(9223372036854775807), so it has no dyn value",
+             op[0] ? " " : "", op, what, (unsigned long long)x);
+    dyn_trap((const uint8_t *)"DynRange", 8);
+  }
+  return flan_dyn_from_i64((int64_t)x);
+}
+
+flan_dyn flan_dyn_from_u64(uint64_t x, const uint8_t *loc, int64_t loclen) {
+  return u64_to_dyn(loc, loclen, "", "u64", x);
+}
+
 flan_dyn flan_dyn_from_f64(double x) {
   flan_dyn v;
   /* Every NaN becomes the one positive quiet NaN, which is what keeps a
@@ -4046,14 +4066,7 @@ static flan_dyn view_read(const uint8_t *loc, int64_t loclen, const char *op,
   case 'L': {
     uint64_t x;
     memcpy(&x, p, 8);
-    if (x > (uint64_t)INT64_MAX) {
-      flan_say(loc, loclen,
-               "dyn %s: this u64 element is %llu, above the largest dyn int "
-               "(9223372036854775807), so it has no dyn value",
-               op, (unsigned long long)x);
-      dyn_trap((const uint8_t *)"DynRange", 8);
-    }
-    return flan_dyn_from_i64((int64_t)x);
+    return u64_to_dyn(loc, loclen, op, "u64 element", x);
   }
   case 'f': { float x;  memcpy(&x, p, 4); return flan_dyn_from_f64((double)x); }
   case 'd': { double x; memcpy(&x, p, 8); return flan_dyn_from_f64(x); }
diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h
index e7399cca..bfb8c85d 100644
--- a/runtime/flan_dyn.h
+++ b/runtime/flan_dyn.h
@@ -86,6 +86,8 @@ typedef struct flan_desc {
 
 flan_dyn flan_dyn_nil(void);
 flan_dyn flan_dyn_from_i64(int64_t x);
+/* Traps at [loc] on a u64 above the largest i64, which no dyn int holds. */
+flan_dyn flan_dyn_from_u64(uint64_t x, const uint8_t *loc, int64_t loclen);
 flan_dyn flan_dyn_from_f64(double x);
 flan_dyn flan_dyn_from_bool(uint8_t b);
 
diff --git a/test/programs/dyn-crossing.flan b/test/programs/dyn-crossing.flan
new file mode 100644
index 00000000..41431fa0
--- /dev/null
+++ b/test/programs/dyn-crossing.flan
@@ -0,0 +1,59 @@
+;;;; Typed values crossing into dyn beside a dyn operand: a u64, a dyn nil past
+;;;; a fold's first pair, and a $t bounded by is-numeric. With an argument, the
+;;;; program runs the trap that argument names instead.
+
+(defn add-dyn [x $t] dyn
+  {:where (is-numeric $t)}
+  (+ x (the dyn 1)))
+
+(defn add-late [x $t d dyn] dyn
+  {:where (is-numeric $t)}
+  (+ x 1 d))
+
+(defn dyn-first [x $t d dyn] dyn
+  {:where (is-numeric $t)}
+  (* d x 2))
+
+(defn less-late [x $t d dyn] bool
+  {:where (is-numeric $t)}
+  (< x 10 d))
+
+(defn biggest [x $t d dyn] dyn
+  {:where (is-numeric $t)}
+  (max x d 0))
+
+(defn low-bits [x $t d dyn] dyn
+  {:where (is-integer $t)}
+  (bit-and x 7 d))
+
+(defn boxed [x $t] dyn
+  {:where (is-numeric $t)}
+  (the dyn x))
+
+(defn main [args [str]] i32
+  (let [z (the dyn 0)
+        n (the dyn 4)
+        small (the u64 9223372036854775807)
+        big (the u64 18446744073709551615)
+        nothing (the dyn nil)]
+    ;; A u64 up to the largest i64 crosses as its value.
+    (println (+ z small) (max small 0 z) (the dyn small) (= small (+ z small)))
+    ;; A $t at i32, f64 and u64, beside a dyn in any position.
+    (println (add-dyn 2) (add-dyn 2.5) (add-dyn (the u64 7)))
+    (println (add-late 2 n) (add-late 2.5 n) (dyn-first 3 n) (dyn-first 1.5 n))
+    (println (less-late 1 n) (less-late 1 (the dyn 20)) (less-late 0.5 (the dyn 10.5)))
+    (println (biggest 3 n) (biggest -2.5 (the dyn -1)) (low-bits 13 n) (low-bits (the u8 255) n))
+    (println (boxed 7) (boxed 0.25) (boxed small))
+    ;; A nil past the pair is compared, not refused.
+    (println (= 1 1 nothing) (!= 1 2 nothing) (= 1 1 (the dyn nil)))
+    (when (> (length args) 1)
+      (let [a (at args 1)]
+        (when (= a "u64") (println (+ z big)))
+        (when (= a "u64-max") (println (max big 0 z)))
+        (when (= a "u64-generic") (println (boxed big)))
+        (when (= a "nil-first") (println (+ (the dyn nil) 1 2)))
+        (when (= a "nil-last") (println (+ 1 2 (the dyn nil))))
+        (when (= a "nil-less") (println (< 1 2 (the dyn nil))))
+        (when (= a "nil-min") (println (min 1 2 nil)))
+        (when (= a "nil-bits") (println (bit-or 1 2 nothing))))))
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 1233fb1c..4c35b408 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -5665,6 +5665,46 @@ level "1"
              (if x86 then ", --x86" else "") text code
          end)
       [ false; true ];
+    (* A u64, a dyn nil past the pair and an is-numeric $t, each beside a
+       dyn: the typed value crosses, and what cannot cross traps at its site. *)
+    let crossing_out =
+      "9223372036854775807 9223372036854775807 9223372036854775807 true\n\
+       3 3.5 8\n7 7.5 24 12\nfalse true true\n4 0 4 4\n\
+       7 0.25 9223372036854775807\nfalse true false\n"
+    in
+    outputs "dyn: typed values crossing beside a dyn" "programs/dyn-crossing.flan"
+      crossing_out;
+    outputs ~opt:"-O0" "dyn: typed values crossing beside a dyn, -O0"
+      "programs/dyn-crossing.flan" crossing_out;
+    outputs ~x86:true "dyn: typed values crossing beside a dyn, --x86"
+      "programs/dyn-crossing.flan" crossing_out;
+    let too_big = "dyn: this u64 is 18446744073709551615, above the largest \
+                   dyn int (9223372036854775807), so it has no dyn value" in
+    let crossing_traps =
+      [ "u64", "51:36", too_big;
+        "u64-max", "52:40", too_big;
+        "u64-generic", "31:12", too_big;
+        "nil-first", "54:42", "dyn +: nil and int, and it takes two numbers — (+ nil 1)";
+        "nil-last", "55:41", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)";
+        "nil-less", "56:41", "dyn <: int and nil";
+        "nil-min", "57:40", "dyn min: int and nil";
+        "nil-bits", "58:41", "dyn bit-or: int and nil" ]
+    in
+    List.iter
+      (fun x86 ->
+         let exe = compile ~x86 "programs/dyn-crossing.flan" in
+         List.iter
+           (fun (arg, at, msg) ->
+              let code, text = run exe (Some arg) in
+              let want = "programs/dyn-crossing.flan:" ^ at ^ ": " ^ msg in
+              if code <> 134 || not (contains text want) then begin
+                incr failures;
+                Printf.printf "FAIL  dyn: crossing trap %s%s\n        \
+                               got: %S (exit %d)\n"
+                  arg (if x86 then ", --x86" else "") text code
+              end)
+           crossing_traps)
+      [ false; true ];
     List.iter
       (fun x86 ->
          let exe = compile ~x86 "programs/char-arith.flan" in
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 59b8221e..0c7fa3e0 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2066,6 +2066,18 @@ let () =
   rejects_check "nil at a bare T is refused at compile time"
     "(defn take [n i32] i32 n)\n(defn main [] i32 (take nil))"
     ~needle:"nil has no None to become";
+  (* A $t crosses into dyn only under a bound every type of which has a dyn
+     value; an unbounded one could be a pointer, refused at no call site. *)
+  rejects_check "an unbounded $t does not cross into dyn"
+    "(defn f [x $t] dyn (+ x (the dyn 1)))\n\
+     (defn main [] i32 (println (f 2)) 0)"
+    ~needle:"$t may be a type with no dyn value, such as a pointer or an \
+             enum, so it crosses into dyn only as a number. Write \
+             {:where (is-numeric $t)}";
+  rejects_check "an is-ordered $t does not cross into dyn"
+    "(defn f [x $t] dyn {:where (is-ordered $t)} (the dyn x))\n\
+     (defn main [] i32 (println (f 2)) 0)"
+    ~needle:"crosses into dyn only as a number";
   rejects_check "nil at a bare T is refused at compile time, return position"
     "(defn f [] i64 nil)\n(defn main [] i32 0)"
     ~needle:"nil has no None to become";
@@ -8018,11 +8030,11 @@ let () =
   parse_rejects "a wide enum member is refused for its range"
     "(defenum E [A 0xFFFFFFFFFFFFFFFF B])"
     ~needle:"the member A of E is 0xFFFFFFFFFFFFFFFF, which does not fit i32";
-  rejects_check "a wide literal in a dyn global names the u64 cast"
+  rejects_check "a wide literal in a dyn global names the type u64"
     "(defonce big 0xFFFFFFFFFFFFFFFF)"
-    ~needle:"Write (u64 0xFFFFFFFFFFFFFFFF) for the u64";
-  accepts "the cast the dyn refusal names compiles"
-    "(defonce big (u64 0xFFFFFFFFFFFFFFFF))";
+    ~needle:"no i64 is this large. Give what holds it the type u64";
+  accepts "the type the dyn refusal names compiles"
+    "(defonce big u64 0xFFFFFFFFFFFFFFFF)";
   (* A macro's Form has one integer case; the literal comes back wide all the
      same, and is refused where it would have been refused unexpanded. *)
   rejects_check "a wide literal through a macro is still wide"