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

@@ -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 ->
+      | w, Types.Dyn when is_nil_lit got -> 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)
       | _, 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 ->
+  | Some Types.Dyn -> Loc.failk literal_at_want loc "%s" (wide_at_dyn s)
-    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 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 () =
+    (* Only asked, and asked with the literal locals' uses unrecorded: a
-      let v = check ctx arg in
+       [trial] does not take back what the session recorded, and the operand
-      if v.Tast.ty = Types.Dyn then v else fail arg.Ast.loc "not a dyn"
+       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
+    let is_dyn =
-    | Ok v -> `Dyn v
+      probe ctx arg.Ast.loc (fun () -> unrecorded (fun () -> (check ctx arg).Tast.ty))
-    | Error _ -> fold_operand ctx ty (check ctx ~want:ty arg)
+      = 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)
+        | [] -> [ a; b ]
-        | _ -> cmp_over ctx loc Types.Dyn ~pairs ~link (ops ())
+        | _ -> 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
+          a :: b :: map_lr (fun e -> check ctx ~want:Types.Dyn e) rest)
-          :: 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
@@ -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
+            a :: b :: List.map (function `Dyn d -> d | `Typed v -> v) rest)
-            :: 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
@@ -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)

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
+;;;; a fold's pair (a bare nil is refused, see test_flan), and an is-numeric $t.
-;;;; program runs the trap that argument names instead.
+;;;; 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-min") (println (min 1 2 nothing)))
-        (when (= a "nil-bits") (println (bit-or 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)

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

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