From 7dcef05df31e6f3ef3a12c9d9466e893aa7cba34 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sat, 26 Sep 2026 16:47:28 +0700
Subject: [PATCH 1/4] A u64 past the largest i64 traps where it crosses into
 dyn, a dyn nil past a fold's first pair traps at run time, and an is-numeric
 $t boxes beside a dyn.

---
 TODO.org                        |  8 ----
 lib/check.ml                    | 81 ++++++++++++++++++++++++++-------
 lib/emit.ml                     |  1 +
 runtime/flan_dyn.c              | 29 ++++++++----
 runtime/flan_dyn.h              |  2 +
 test/programs/dyn-crossing.flan | 59 ++++++++++++++++++++++++
 test/test_acceptance.ml         | 40 ++++++++++++++++
 test/test_flan.ml               | 20 ++++++--
 8 files changed, 204 insertions(+), 36 deletions(-)
 create mode 100644 test/programs/dyn-crossing.flan

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"

From 4d85cefbe2e4cdad326e08de22ebf3b6e03078d0 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sat, 26 Sep 2026 17:18:29 +0700
Subject: [PATCH 2/4] A bare nil in a typed fold is refused in every position
 while a dyn holding nil traps, a fold operand asked on its own terms records
 no literal-local use, and a wide literal at dyn says it has no dyn value.

---
 lib/check.ml                    | 137 ++++++++++++++++++++++++--------
 test/programs/dyn-crossing.flan |  13 ++-
 test/test_acceptance.ml         |   4 +-
 test/test_flan.ml               |  66 ++++++++++++++-
 4 files changed, 183 insertions(+), 37 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index e01bca51..c6acece6 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -4986,6 +4986,56 @@ let const_note ?(fln = false) env ~(want : Types.t) ~(got : Types.t) =
       (Types.spell ~indented:fln want) (Types.spell ~indented:fln got)
   | _ -> ""
 
+let nil_has_no_none loc w =
+  fail loc
+    "nil has no None to become at %s — nil only converts to (Option T) \
+     or to dyn itself; wrap the type in Option, or keep the value dyn"
+    (tyname loc w)
+
+(* A literal boxed where a dyn was wanted, and the literal. It brings no dyn
+   of its own to an operator: (+ nil 1) over a literal 1 checked at dyn is as
+   typed as (+ nil x) over an i32 x. *)
+let boxed_literal (e : Tast.expr) =
+  match e.Tast.e with
+  | Tast.Prim (Tast.Rt ("flan_dyn_from_i64" | "flan_dyn_from_f64"
+                       | "flan_dyn_from_char" | "flan_dyn_from_bool"), [ x ]) ->
+    let x = match x.Tast.e with Tast.Prim (Tast.Cast _, [ y ]) -> y | _ -> x in
+    (match x.Tast.e with
+     | Tast.Int (n, _) when x.Tast.ty <> Types.Char ->
+       (* The type the literal takes where nothing is wanted. *)
+       let k =
+         if Int64.compare n (Int64.of_int32 Int32.max_int) > 0
+         || Int64.compare n (Int64.of_int32 Int32.min_int) < 0
+         then Types.I64 else Types.I32
+       in
+       Some (Types.Int k)
+     | Tast.Int _ | Tast.Float _ | Tast.Bool _ -> Some x.Tast.ty
+     | _ -> None)
+  | _ -> None
+
+(* The operands of an arithmetic, bitwise or ordering operator gone dyn,
+   before they are boxed: a literal [nil] among them with nothing else dyn is
+   refused as [expect] refuses it at a typed want, whichever position it is
+   in and whether or not the form has a want. A dyn that holds nil is the
+   run-time trap's, so (+ 1 2 nil) is refused and (+ 1 2 (the dyn nil))
+   traps. [=] and [!=] ask no such question: nil is unequal to a number. *)
+let no_bare_nil (ops : Tast.expr list) =
+  match List.find_opt is_nil_lit ops with
+  | None -> ()
+  | Some nil ->
+    let makes_dyn (e : Tast.expr) =
+      e.Tast.ty = Types.Dyn && not (is_nil_lit e) && boxed_literal e = None
+    in
+    if not (List.exists makes_dyn ops) then
+      match
+        List.find_map
+          (fun (e : Tast.expr) ->
+             if e.Tast.ty <> Types.Dyn then Some e.Tast.ty else boxed_literal e)
+          ops
+      with
+      | Some t -> nil_has_no_none nil.Tast.loc t
+      | None -> ()
+
 let expect ctx loc ~want (got : Tast.expr) =
   match want with
   | None -> got
@@ -5009,11 +5059,7 @@ let expect ctx loc ~want (got : Tast.expr) =
          actually see — the literal, written right where the mismatch is.
          Refused here, at the offending line, instead of waiting for the
          runtime trap [unbox] would otherwise reach for two arms down. *)
-      | w, Types.Dyn when is_nil_lit got ->
-        fail loc
-          "nil has no None to become at %s — nil only converts to (Option T) \
-           or to dyn itself; wrap the type in Option, or keep the value dyn"
-          (tyname loc w)
+      | w, Types.Dyn when is_nil_lit got -> nil_has_no_none loc w
       | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
       | (Types.String | Types.Slice _ | Types.Array _), Types.Dyn ->
         let opened = into_typed ctx loc w got in
@@ -6817,6 +6863,13 @@ and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n =
       (tyname loc other) n
   | _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default))
 
+(* A wide literal where a dyn is wanted. A global's initialiser adds the fix
+   (its type); anywhere else there is nothing to retype. *)
+and wide_at_dyn s =
+  Printf.sprintf
+    "expected dyn, found the integer literal %s, which is above the largest \
+     dyn int (9223372036854775807), so it has no dyn value" s
+
 (* An integer written at or above 2^63, in decimal or in hex. Only a u64 holds
    one, so it is accepted there and refused everywhere else, in the spelling it
    was written in — its pattern read as an i64 is a different number. *)
@@ -6835,12 +6888,7 @@ and wide_literal loc ~want n s =
       "%s does not fit in i32, the type an integer literal takes when nothing \
        says otherwise — write (u64 %s) for a u64"
       s 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, and no i64 is this large. Give what holds it \
-       the type u64"
-      s
+  | Some Types.Dyn -> Loc.failk literal_at_want loc "%s" (wide_at_dyn s)
   | Some other ->
     Loc.failk literal_at_want loc
       "expected %s, found the integer literal %s, which only a u64 holds"
@@ -9806,6 +9854,10 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
         v.Ast.loc items
     | _ -> expect ctx v.Ast.loc ~want:(Some ty) (check ctx ~want:ty v)
   in
+  (* (the dyn nil) is a dyn value that holds nil, not the literal: at a typed
+     want it traps at run time as any dyn holding nil does, where a bare nil
+     is refused ([is_nil_lit] sees through nothing, so the [Do] hides it). *)
+  let r = if is_nil_lit r && ty = Types.Dyn then mk loc Types.Dyn (Tast.Do [ r ]) else r in
   expect ctx loc ~want r
 
 (* [f] run for its answer alone: whatever it wrote into the context is put
@@ -11903,13 +11955,24 @@ 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"
+    (* Only asked, and asked with the literal locals' uses unrecorded: a
+       [trial] does not take back what the session recorded, and the operand
+       on its own terms is not how the program reads it unless it is a dyn —
+       (+ x y) over an int x and a float y would merge the two and move the
+       refusal onto x. A dyn is then checked again, recorded. *)
+    let unrecorded f =
+      match ctx.lits with
+      | Some s when s.recording ->
+        s.recording <- false;
+        Fun.protect ~finally:(fun () -> s.recording <- true) f
+      | _ -> f ()
     in
-    match trial ctx own with
-    | Ok v -> `Dyn v
-    | Error _ -> fold_operand ctx ty (check ctx ~want:ty arg)
+    let is_dyn =
+      probe ctx arg.Ast.loc (fun () -> unrecorded (fun () -> (check ctx arg).Tast.ty))
+      = Some Types.Dyn
+    in
+    if is_dyn then `Dyn (to_dyn ctx (check ctx arg))
+    else 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
@@ -12023,11 +12086,6 @@ and dyn_fold ctx ~want loc name first rest =
      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 ~ctx loc b; here loc ] in
-  let acc =
-    match first with
-    | [ a; b ] -> apply (box ~ctx loc a) b
-    | _ -> assert false
-  in
   let operand arg =
     if bitwise then begin
       let v = check ctx arg in
@@ -12036,7 +12094,14 @@ and dyn_fold ctx ~want loc name first rest =
     end
     else check ctx ~want:Types.Dyn arg
   in
-  let acc = List.fold_left (fun acc arg -> apply acc (operand arg)) acc rest in
+  let rest = map_lr operand rest in
+  no_bare_nil (first @ rest);
+  let acc =
+    match first with
+    | [ a; b ] -> apply (box ~ctx loc a) b
+    | _ -> assert false
+  in
+  let acc = List.fold_left apply acc rest in
   expect ctx loc ~want acc
 
 (* The runtime's entry point for each bit operation on a dyn int. *)
@@ -13483,7 +13548,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        two things being unalike is the answer to "are these equal", not an
        error. The orderings do trap, and rightly — there is no true answer to
        whether a string is less than a vector. *)
-    (* [ops] are every operand, boxed. *)
+    (* [ops] are every operand, not yet boxed. *)
     let dyn_chain ops =
       let sym =
         match name with
@@ -13508,17 +13573,22 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           mk loc Types.Bool (Tast.Prim (Tast.Not, [ cmp ]))
         else cmp
       in
-      let r =
+      let ops =
         match rest with
-        | [] -> link (box ~ctx loc a) (box ~ctx loc b)
-        | _ -> cmp_over ctx loc Types.Dyn ~pairs ~link (ops ())
+        | [] -> [ a; b ]
+        | _ -> ops ()
+      in
+      if not (String.equal sym "flan_dyn_eq") then no_bare_nil ops;
+      let r =
+        match List.map (box ~ctx loc) ops with
+        | [ a; b ] -> link a b
+        | ops -> 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 ~ctx loc a :: box ~ctx loc b
-          :: map_lr (fun e -> box ~ctx loc (check ctx ~want:Types.Dyn e)) rest)
+          a :: b :: map_lr (fun e -> 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
@@ -13560,8 +13630,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          dyn in it is a dyn comparison. *)
       if List.exists (function `Dyn _ -> true | `Typed _ -> false) rest then
         dyn_chain (fun () ->
-            box ~ctx loc a :: box ~ctx loc b
-            :: List.map (function `Dyn d -> d | `Typed v -> box ~ctx loc v) rest)
+            a :: b :: List.map (function `Dyn d -> d | `Typed v -> v) rest)
       else
         let ops =
           a :: b :: List.map (function `Typed v -> v | `Dyn d -> d) rest in
@@ -13643,6 +13712,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
         (fun (v : Tast.expr) ->
            if v.Tast.ty <> Types.Dyn then bits_operand ctx v.Tast.loc name v)
         [ a; b ];
+      no_bare_nil [ a; b ];
       expect ctx loc ~want
         (rt loc Types.Dyn (dyn_bits_sym name) [ box ~ctx loc a; box ~ctx loc b; here loc ])
     end else begin
@@ -19471,6 +19541,11 @@ let check_global env (d : Ast.decl) : Tast.global option =
         { Tast.e = Tast.Uninit ty; ty; loc = d.Ast.dloc }
       | Ast.Init v ->
         let c = ctx () in
+        (match v.Ast.e with
+         | Ast.UInt (_, s) when ty = Types.Dyn ->
+           Loc.failk literal_at_want v.Ast.loc "%s. Give %s the type u64"
+             (wide_at_dyn s) n
+         | _ -> ());
         let v =
           view_global_init := Some (n, kind);
           Fun.protect ~finally:(fun () -> view_global_init := None)
diff --git a/test/programs/dyn-crossing.flan b/test/programs/dyn-crossing.flan
index 41431fa0..4b80b47c 100644
--- a/test/programs/dyn-crossing.flan
+++ b/test/programs/dyn-crossing.flan
@@ -1,6 +1,6 @@
 ;;;; 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.
+;;;; a fold's pair (a bare nil is refused, see test_flan), and an is-numeric $t.
+;;;; With an argument, the program runs the trap that argument names instead.
 
 (defn add-dyn [x $t] dyn
   {:where (is-numeric $t)}
@@ -54,6 +54,11 @@
         (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))))))
+        (when (= a "nil-min") (println (min 1 2 nothing)))
+        (when (= a "nil-bits") (println (bit-or 1 2 nothing)))
+        ;; At a typed want too: the dyn nil traps in any position.
+        (let [r (the i32 0)]
+          (when (= a "nil-want-first") (set r (+ (the dyn nil) 1 2)))
+          (when (= a "nil-want-last") (set r (+ 1 2 (the dyn nil))))
+          (println r)))))
   0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 4c35b408..c75a53ff 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -5688,7 +5688,9 @@ level "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" ]
+        "nil-bits", "58:41", "dyn bit-or: int and nil";
+        "nil-want-first", "61:50", "dyn: an i32 is wanted here, and this is nil";
+        "nil-want-last", "62:46", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)" ]
     in
     List.iter
       (fun x86 ->
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 0c7fa3e0..836e7433 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2066,6 +2066,70 @@ 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 bare nil in an arithmetic, bitwise or ordering operator with nothing
+     else dyn is refused in every position, with or without a want; a dyn that
+     holds nil is left to trap at run time (dyn-crossing.flan). *)
+  (* The 1-based column of [sub] in [form], placed at column [base]. *)
+  let col_of base form sub =
+    let n = String.length sub in
+    let rec at i = if String.sub form i n = sub then i else at (i + 1) in
+    base + at 0
+  in
+  List.iter
+    (fun form ->
+       List.iter
+         (fun (what, base, src) ->
+            let col = col_of base form "nil" in
+            match
+              (try ignore (checked src); None with Loc.Error d -> Some d)
+            with
+            | Some d when contains d.Loc.dmsg "nil has no None to become at i32"
+                          && d.Loc.dloc.Loc.col = col -> ()
+            | Some d ->
+              incr failures;
+              Printf.printf "FAIL  a bare nil in %s, %s: got %d: %s\n" form what
+                d.Loc.dloc.Loc.col d.Loc.dmsg
+            | None ->
+              incr failures;
+              Printf.printf "FAIL  a bare nil in %s, %s: accepted\n" form what)
+         [ "at a want", 16,
+           Printf.sprintf "(defn f [] i32 %s)\n(defn main [] i32 (f))" form;
+           "with none", 25,
+           Printf.sprintf "(defn f [] i32 (println %s) 0)\n(defn main [] i32 (f))" form ])
+    [ "(+ nil 1 2)"; "(+ 1 nil 2)"; "(+ 1 2 nil)"; "(+ 1 nil)";
+      "(< nil 1 2)"; "(< 1 2 nil)"; "(min 1 2 nil)"; "(bit-or nil 1 2)";
+      "(bit-or 1 2 nil)" ];
+  accepts "a dyn holding nil in a fold is left to the run time"
+    "(defn f [p dyn] i32 (+ 1 2 p (the dyn nil)))\n\
+     (defn g [] i32 (let [r (the i32 0)] (set r (+ (the dyn nil) 1 2)) r))\n\
+     (defn main [] i32 (println (< 1 2 (the dyn nil))) 0)";
+  accepts "nil beside a real dyn in a fold is left to the run time"
+    "(defn f [p dyn] dyn (+ 1 2 p nil))\n(defn main [] i32 0)";
+  (* An operand past the pair asked on its own terms records nothing: the
+     float y is blamed, not the int x it would have merged with. *)
+  List.iter
+    (fun form ->
+       let col = col_of 45 form "y)" in
+       match
+         (try ignore (checked ("(defn main [] i32 (let [x 5 y 2.5] (println "
+                               ^ form ^ ")) 0)")); None
+          with Loc.Error d -> Some d)
+       with
+       | Some d when d.Loc.dloc.Loc.col = col -> ()
+       | Some d ->
+         incr failures;
+         Printf.printf "FAIL  %s blames col %d, not y at %d: %s\n" form
+           d.Loc.dloc.Loc.col col d.Loc.dmsg
+       | None -> incr failures; Printf.printf "FAIL  %s: accepted\n" form)
+    [ "(+ (the i64 1) 2 (+ x y))"; "(* (the i64 1) 2 (* x y))";
+      "(max (the i64 1) 2 (max x y))"; "(< (the i64 1) 2 (+ x y))" ];
+  rejects_check "a wide literal at dyn with nothing to retype"
+    "(defn main [] i32 (println (the dyn 0xFFFFFFFFFFFFFFFF)) 0)"
+    ~needle:"0xFFFFFFFFFFFFFFFF, which is above the largest dyn int \
+             (9223372036854775807), so it has no dyn value";
+  rejects_check "a wide literal beside a dyn"
+    "(defn main [] i32 (println (+ (the dyn 0) 0xFFFFFFFFFFFFFFFF)) 0)"
+    ~needle:"so it has no dyn value";
   (* 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"
@@ -8032,7 +8096,7 @@ let () =
     ~needle:"the member A of E is 0xFFFFFFFFFFFFFFFF, which does not fit i32";
   rejects_check "a wide literal in a dyn global names the type u64"
     "(defonce big 0xFFFFFFFFFFFFFFFF)"
-    ~needle:"no i64 is this large. Give what holds it the type u64";
+    ~needle:"so it has no dyn value. Give big 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

From c60cc33b9516f8f2c1a9c4dece82cc2c6d7aefcd Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sat, 26 Sep 2026 17:30:44 +0700
Subject: [PATCH 3/4] A dyn operand in a fold's first pair keeps the form dyn
 at a typed want, so only the answer is opened and every position gives the
 same result.

---
 lib/check.ml                    | 15 ++++++++++++---
 test/programs/dyn-crossing.flan | 17 +++++++++++++++++
 test/test_acceptance.ml         | 16 ++++++++++++++--
 3 files changed, 43 insertions(+), 5 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index c6acece6..84dd80ba 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -17212,8 +17212,17 @@ and binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want (x : Ast.expr) (y : Ast.exp
     let needs_want (f : Ast.expr) =
       is_literal f || (match f.Ast.e with Ast.Kw _ -> true | _ -> false)
     in
+    (* A dyn the want opened is put back: beside a dyn a typed operand gives
+       dyn (rule 117), so the pair is the dyn runtime's and only its answer
+       is opened at the want. Opening the operand first made (+ p 1 1) at an
+       i32 want an i32 add that wraps, where (+ 1 1 p) was a dyn add whose
+       answer traps at the i32. *)
+    let reopen (v : Tast.expr) =
+      if not dyn_ok then v
+      else match opened_dyn ~box:(to_dyn ctx) v with Some d -> d | None -> v
+    in
     if y_decides then begin
-      let b = check ctx ?want y in
+      let b = reopen (check ctx ?want y) in
       (* An integer literal before a char, under [+] or [-], is an integer:
          the pair is char arithmetic ([char_step]). *)
       let a =
@@ -17240,7 +17249,7 @@ and binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want (x : Ast.expr) (y : Ast.exp
        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 a = reopen (check ctx ?want x) in
       (* y at [a]'s type first, and on its own terms only if that is
          refused: checking it both ways every time made a chain of these
          nested in their second operands twice as slow per level. A dyn
@@ -17289,7 +17298,7 @@ and binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want (x : Ast.expr) (y : Ast.exp
             | None -> raise (Loc.Error d)))
     end
     else begin
-      let a = check ctx ?want x in
+      let a = reopen (check ctx ?want x) in
       match trial_at ctx y a.Tast.ty with
       | Ok b -> a, b
       | Error d ->
diff --git a/test/programs/dyn-crossing.flan b/test/programs/dyn-crossing.flan
index 4b80b47c..def9fecb 100644
--- a/test/programs/dyn-crossing.flan
+++ b/test/programs/dyn-crossing.flan
@@ -60,5 +60,22 @@
         (let [r (the i32 0)]
           (when (= a "nil-want-first") (set r (+ (the dyn nil) 1 2)))
           (when (= a "nil-want-last") (set r (+ 1 2 (the dyn nil))))
+          (set r (+ r (at-i32 a)))
           (println r)))))
   0)
+
+;; A dyn beside typed operands at an i32 want: the whole form is dyn, and only
+;; its answer is opened at i32, so every position wraps nowhere and traps alike.
+(defn at-i32 [a str] i32
+  (let [big (the dyn 2147483647)
+        none (the dyn nil)]
+    (cond
+      (= a "big-first") (+ big 1 1)
+      (= a "big-mid") (+ 1 big 1)
+      (= a "big-last") (+ 1 1 big)
+      (= a "big-pair") (+ 1 big)
+      (= a "big-shift") (<< big 1)
+      (= a "i32-nil-first") (+ none 1 1)
+      (= a "i32-nil-mid") (+ 1 none 1)
+      (= a "i32-nil-last") (+ 1 1 none)
+      :else 0)))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 045f1acd..c10ec35e 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -5686,6 +5686,8 @@ level "1"
       "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 too_wide n =
+      "dyn: an i32 is wanted here, and the int " ^ n ^ " is outside an i32's range" in
     let crossing_traps =
       [ "u64", "51:36", too_big;
         "u64-max", "52:40", too_big;
@@ -5695,8 +5697,18 @@ level "1"
         "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";
-        "nil-want-first", "61:50", "dyn: an i32 is wanted here, and this is nil";
-        "nil-want-last", "62:46", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)" ]
+        "nil-want-first", "61:47", "dyn +: nil and int, and it takes two numbers — (+ nil 1)";
+        "nil-want-last", "62:46", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)";
+        (* At an i32 want the form is dyn in every position and only its
+           answer is opened: no position wraps. *)
+        "big-first", "73:25", too_wide "2147483649";
+        "big-mid", "74:23", too_wide "2147483649";
+        "big-last", "75:24", too_wide "2147483649";
+        "big-pair", "76:24", too_wide "2147483648";
+        "big-shift", "77:25", too_wide "4294967294";
+        "i32-nil-first", "78:29", "dyn +: nil and int, and it takes two numbers — (+ nil 1)";
+        "i32-nil-mid", "79:27", "dyn +: int and nil, and it takes two numbers — (+ 1 nil)";
+        "i32-nil-last", "80:28", "dyn +: int and nil, and it takes two numbers — (+ 2 nil)" ]
     in
     List.iter
       (fun x86 ->

From d14cffa23af9a5522dd098b78c0e3d8c1ae93214 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Sat, 26 Sep 2026 17:44:27 +0700
Subject: [PATCH 4/4] (the dyn <literal>) beside nil traps at run time, and a
 dyn opened at f64 or bool traps at its site.

---
 lib/check.ml                    | 16 +++++++++++-----
 lib/emit.ml                     |  2 ++
 runtime/flan_dyn.c              | 12 ++++++++----
 runtime/flan_dyn.h              |  3 +++
 test/programs/dyn-crossing.flan | 15 ++++++++++++++-
 test/test_acceptance.ml         | 10 +++++++++-
 test/test_flan.ml               |  4 ++++
 7 files changed, 51 insertions(+), 11 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 84dd80ba..fc987993 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -4573,14 +4573,14 @@ module Found = Ephemeron.K1.Make (struct
 let mismatch_found : Types.t Found.t = Found.create 16
 
 let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
-  let need sym ty = rt loc ty sym [ e ] in
+  let need sym ty = rt loc ty sym [ e; here loc ] in
   match want with
-  | Types.Float Types.F64 -> need "flan_dyn_need_f64" dyn_f64
+  | Types.Float Types.F64 -> need "flan_dyn_need_f64_at" dyn_f64
   | Types.Bool ->
     (* The ABI answers an [int32_t]; [bool] is an [i1]. The narrowing is the
        language's own cast and cannot fail — the runtime already decided the
        value was a bool, so what comes back is 0 or 1. *)
-    widen loc Types.Bool (need "flan_dyn_need_bool" (Types.Int Types.I32))
+    widen loc Types.Bool (need "flan_dyn_need_bool_at" (Types.Int Types.I32))
   (* Only a dyn char: an int is a number until (char n) converts it. *)
   | Types.Char -> rt loc Types.Char "flan_dyn_need_char" [ e; here loc ]
   (* Any integer width, checked at run time at this site (TODO.org, "Dyn
@@ -9856,8 +9856,14 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
   in
   (* (the dyn nil) is a dyn value that holds nil, not the literal: at a typed
      want it traps at run time as any dyn holding nil does, where a bare nil
-     is refused ([is_nil_lit] sees through nothing, so the [Do] hides it). *)
-  let r = if is_nil_lit r && ty = Types.Dyn then mk loc Types.Dyn (Tast.Do [ r ]) else r in
+     is refused. (the dyn 1) is likewise a dyn, not a literal that brings
+     nothing dyn to an operator ([no_bare_nil]). [is_nil_lit] and
+     [boxed_literal] see through nothing, so the [Do] hides both. *)
+  let r =
+    if ty = Types.Dyn && (is_nil_lit r || boxed_literal r <> None) then
+      mk loc Types.Dyn (Tast.Do [ r ])
+    else r
+  in
   expect ctx loc ~want r
 
 (* [f] run for its answer alone: whatever it wrote into the context is put
diff --git a/lib/emit.ml b/lib/emit.ml
index d18cb4c3..c519af35 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -5149,6 +5149,8 @@ declare ptr @flan_dev_literal(ptr, i64)
 declare i64 @flan_dyn_need_i64(i64)
 declare double @flan_dyn_need_f64(i64)
 declare i32 @flan_dyn_need_bool(i64)
+declare double @flan_dyn_need_f64_at(i64, ptr, i64)
+declare i32 @flan_dyn_need_bool_at(i64, ptr, i64)
 declare i32 @flan_dyn_need_i32(i64, ptr, i64)
 declare i64 @flan_dyn_need_int(i64, i32, ptr, i64)
 declare i64 @flan_dyn_int_of(i64)
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index 455bff6e..78a91b30 100644
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@@ -2817,11 +2817,14 @@ int64_t flan_dyn_need_i64(flan_dyn v) {
  * makes rather than a surprise somebody meets. Softening the check here is the
  * option not to take: this function sees a tag and nothing else, so it could
  * not tell (g 1) from (g (length xs)). */
-double flan_dyn_need_f64(flan_dyn v) {
+/* The _at forms trap at the site the checker hands over; the plain ones are
+ * for C callers that have none. */
+double flan_dyn_need_f64_at(flan_dyn v, const uint8_t *loc, int64_t loclen) {
   if (flan_dyn_tag(v) != FLAN_DYN_TAG_FLOAT)
-    trap1(NULL, 0, TYPE_TRAP, "f64", "a float was wanted", v);
+    trap1(loc, loclen, TYPE_TRAP, "f64", "a float was wanted", v);
   return dyn_num_value(v);
 }
+double flan_dyn_need_f64(flan_dyn v) { return flan_dyn_need_f64_at(v, NULL, 0); }
 
 static const char *an(const char *w);   /* forward: "a" or "an" */
 
@@ -2914,11 +2917,12 @@ uint32_t flan_dyn_need_char(flan_dyn v, const uint8_t *loc, int64_t loclen) {
   flan_trap((const uint8_t *)"DynType", 7);
 }
 
-uint8_t flan_dyn_need_bool(flan_dyn v) {
+uint8_t flan_dyn_need_bool_at(flan_dyn v, const uint8_t *loc, int64_t loclen) {
   if (flan_dyn_tag(v) != FLAN_DYN_TAG_BOOL)
-    trap1(NULL, 0, TYPE_TRAP, "bool", "a bool was wanted", v);
+    trap1(loc, loclen, TYPE_TRAP, "bool", "a bool was wanted", v);
   return (uint8_t)(dyn_payload(v) ? 1 : 0);
 }
+uint8_t flan_dyn_need_bool(flan_dyn v) { return flan_dyn_need_bool_at(v, NULL, 0); }
 
 /* ── A numeric cast opening a box ───────────────────────────────────────
  *
diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h
index bfb8c85d..d938545c 100644
--- a/runtime/flan_dyn.h
+++ b/runtime/flan_dyn.h
@@ -306,6 +306,9 @@ void flan_dyn_emit_watch(flan_dyn v);
 int64_t flan_dyn_need_i64(flan_dyn v);
 double  flan_dyn_need_f64(flan_dyn v);
 uint8_t flan_dyn_need_bool(flan_dyn v);
+/* The same, trapping at the site [loc] names. */
+double  flan_dyn_need_f64_at(flan_dyn v, const uint8_t *loc, int64_t loclen);
+uint8_t flan_dyn_need_bool_at(flan_dyn v, const uint8_t *loc, int64_t loclen);
 /* For a typed integer of width [kind], 0..7 for i8 u8 i16 u16 i32 u32 i64
  * u64: an int in range, or a char's code point where it fits (ASCII only
  * into a byte), as an i64 the caller narrows. Anything else traps at [loc].
diff --git a/test/programs/dyn-crossing.flan b/test/programs/dyn-crossing.flan
index def9fecb..f4f61684 100644
--- a/test/programs/dyn-crossing.flan
+++ b/test/programs/dyn-crossing.flan
@@ -60,7 +60,7 @@
         (let [r (the i32 0)]
           (when (= a "nil-want-first") (set r (+ (the dyn nil) 1 2)))
           (when (= a "nil-want-last") (set r (+ 1 2 (the dyn nil))))
-          (set r (+ r (at-i32 a)))
+          (set r (+ r (at-i32 a))) (the-literal a)
           (println r)))))
   0)
 
@@ -79,3 +79,16 @@
       (= a "i32-nil-mid") (+ 1 none 1)
       (= a "i32-nil-last") (+ 1 1 none)
       :else 0)))
+
+;; (the dyn <literal>) is a dyn like any other: beside nil it traps at run
+;; time, as a dyn bound to a name does. And opening one at f64 or bool names
+;; its site.
+(defn the-literal [a str] ()
+  (let [x (the f64 0.0)
+        b false]
+    (when (= a "lit-int") (println (+ (the dyn 1) nil)))
+    (when (= a "lit-float") (println (+ (the dyn 1.5) nil)))
+    (when (= a "lit-bool") (println (+ (the dyn true) nil)))
+    (when (= a "lit-let") (let [d (the dyn 1)] (println (+ d nil))))
+    (when (= a "want-f64") (set x (the dyn 3)) (println x))
+    (when (= a "want-bool") (set b (the dyn 3)) (println b))))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index c10ec35e..6cb47fec 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -5708,7 +5708,15 @@ level "1"
         "big-shift", "77:25", too_wide "4294967294";
         "i32-nil-first", "78:29", "dyn +: nil and int, and it takes two numbers — (+ nil 1)";
         "i32-nil-mid", "79:27", "dyn +: int and nil, and it takes two numbers — (+ 1 nil)";
-        "i32-nil-last", "80:28", "dyn +: int and nil, and it takes two numbers — (+ 2 nil)" ]
+        "i32-nil-last", "80:28", "dyn +: int and nil, and it takes two numbers — (+ 2 nil)";
+        (* (the dyn <literal>) beside nil traps as a named dyn does, and an
+           f64 or bool opening names its site. *)
+        "lit-int", "89:36", "dyn +: int and nil, and it takes two numbers — (+ 1 nil)";
+        "lit-float", "90:38", "dyn +: float and nil, and it takes two numbers — (+ 1.5 nil)";
+        "lit-bool", "91:37", "dyn +: bool and nil, and it takes two numbers — (+ true nil)";
+        "lit-let", "92:57", "dyn +: int and nil, and it takes two numbers — (+ 1 nil)";
+        "want-f64", "93:35", "dyn f64: int, and a float was wanted — (f64 3)";
+        "want-bool", "94:36", "dyn bool: int, and a bool was wanted — (bool 3)" ]
     in
     List.iter
       (fun x86 ->
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 836e7433..9154491e 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2103,6 +2103,10 @@ let () =
     "(defn f [p dyn] i32 (+ 1 2 p (the dyn nil)))\n\
      (defn g [] i32 (let [r (the i32 0)] (set r (+ (the dyn nil) 1 2)) r))\n\
      (defn main [] i32 (println (< 1 2 (the dyn nil))) 0)";
+  accepts "nil beside (the dyn <literal>) is left to the run time"
+    "(defn main [] i32\n\
+     (println (+ (the dyn 1) nil) (+ (the dyn 1.5) nil) (+ (the dyn true) nil)\n\
+     (< (the dyn 1) nil) (min 2 (the dyn 1.5) nil)) 0)";
   accepts "nil beside a real dyn in a fold is left to the run time"
     "(defn f [p dyn] dyn (+ 1 2 p nil))\n(defn main [] i32 0)";
   (* An operand past the pair asked on its own terms records nothing: the