An array literal's first element types the rest, constant arithmetic folds at a bounded type variable, and a pointer or a plain union takes a byte fill

TODO.org

@@ -659,19 +659,20 @@ it would entail =ordered?= and =equal?= and not =numeric?=, so the cast rule
 becomes a disjunction and the refusal has to name whichever the reader meant. Each
 part of that is a decision and the author has not been asked.
 
-** NEXT The Ptr and union arms of the fill boundary are relaxable
+** DONE The Ptr and union arms of the fill boundary are relaxable
-Decided 2026-09-25: relax both. A =Ptr= may be byte-filled, a poisoned pointer being the useful case, and an untagged union is filled over its whole size.
+CLOSED: [2026-09-25]
-What may be byte-filled is numbers, and structs and fixed arrays of numbers.
+A =Ptr= may be byte-filled, and an untagged union is filled over its whole
-A =Ptr= is refused so the rule stays one sentence, and an untagged union
+size when every member may be, its members walked as a struct's fields are; a
-because the walk goes over a struct's fields rather than a union's members.
+union with a =dyn= member is refused naming the =dyn=. Everything else the rule
-Both are named in the decision as the arms to relax first if it is reopened,
+refused it still refuses.
-and a poisoned pointer is arguably the useful case.
 
-** NEXT A compound constant expression at a bounded type variable
+** DONE A compound constant expression at a bounded type variable
-Decided 2026-09-25: fold constant integer arithmetic before the bounded-variable literal check, so =(+ x (+ 1 2))= is accepted where =(+ x 3)= is.
+CLOSED: [2026-09-25]
-=(+ x (+ 1 2))= at a bounded variable is refused where =(+ x 3)= works — the
+Integer arithmetic over literals alone (=Check.literal_arith=) is folded to the
-literal arm admits a bare constant and nothing folds the compound first.
+literal it computes wherever a type variable is wanted, so =(+ x (+ 1 2))= is
-Walk-backable, so it waits until a body actually wants it.
+admitted exactly where =(+ x 3)= is. A defconst's name does not fold, since it
+has a type of its own. The instantiation checks the form unfolded, at its
+concrete type.
 
 ** DONE Generics by monomorphisation, checked abstractly, with where predicates
 CLOSED: [2026-09-13]
@@ -896,13 +897,12 @@ ordinary expressions and the builtin reads the type back out of one
 type an expression cannot hold, such as =(Fn [i32] ())=, is parsed as
 =Ast.TypeArg=. Rules out a type expression anywhere else in expression position.
 
-** NEXT An array literal cannot say it is [f32]
+** DONE An array literal cannot say it is [f32]
-Decided 2026-09-25: the first element's type carries to the rest, so =[(f32 1.0) 2.5]= is an =[f32]=; that is refused today and is a bug. No =1.0f= suffix for now.
+CLOSED: [2026-09-25]
-A float literal defaults to =f64=, an array literal has no context, and a =let=
+With nothing outside an array literal naming its element type, the first
-has no annotation. Same shape as =(vec-new [u8])= and probably the same fix.
+element's type is the want for the rest, so =[(f32 1.0) 2.5]= is a =[2 f32]=. A
-Not the same fix: a bracket literal has no argument to put a type in. Decision:
+refusal of a later element carries a note at the first saying it set the type.
-how a literal names its element type — a spelling of its own, or a =let=
+Rules out a =1.0f= suffix for now.
-annotation.
 
 ** NEXT A let binding takes no type annotation
 Decided 2026-09-25: =(the T expr)=, Common Lisp's special operator, gives any expression its want; checked at compile time like any other want, and it compiles to nothing. =let= is unchanged. On a =dyn= operand it is refused, naming the cast. The refusals that say "annotate the binding" — =None=, an empty =[]=, and =(zeroed)=/=(filled)=/=(dead-beef)= with no want — suggest it instead, because today their suggestion cannot compile.

lib/check.ml

@@ -1082,29 +1082,30 @@ let rec no_zeroed_fn loc what (t : Types.t) =
    - [string] and a slice. Two words, the second of which is a length every
      bounds check believes. A filled length is a bounds check that passes and
      an access that does not.
-   - [Ptr]. Not walked by the collector, and a poisoned pointer is arguably
-     the useful case — but it is still a value every [deref] in the language
-     trusts, and admitting it would make the rule "plain data, except one
-     kind of address". Kept out so the rule is one sentence. This is the arm
-     to relax first if the question is reopened.
    - [bool]. The one refusal that is about the backends rather than the
      runtime: a bool is a byte here and an [i1] to LLVM, which reads the low
      bit, where x86 compares the whole byte against zero. 0xDE is false on
      one and true on the other, and byte-identical behaviour across the two
      backends is the property this feature is pinned on.
-   - an enum, a data type, a union, an [(Option T)], a function value. Each
+   - an enum, a data type, an [(Option T)], a function value. Each
      carries a tag or a case index that something later reads as a small
      number with a meaning, and a filled one names a case that does not
      exist.
 
    Floats are in: every bit pattern is a float, NaNs included, and both
-   backends move one as bytes. *)
+   backends move one as bytes. So is a [Ptr], which the collector does not
+   walk and whose poisoned value is the useful case, and an untagged union
+   whose members are all admitted, filled over its whole size. *)
 let rec unfillable env seen (t : Types.t) : Types.t option =
   match t with
-  | Types.Int _ | Types.Float _ -> None
+  | Types.Int _ | Types.Float _ | Types.Ptr _ -> None
   | Types.Array (_, e) -> unfillable env seen e
   | Types.Named n when not (List.mem n seen) ->
-    (match Hashtbl.find_opt env.structs n with
+    (match
+       match Hashtbl.find_opt env.structs n with
+       | Some s -> Some s
+       | None -> Hashtbl.find_opt env.unions n
+     with
      | Some s ->
        List.fold_left
          (fun acc (fl : Tast.field) ->
@@ -1112,9 +1113,8 @@ let rec unfillable env seen (t : Types.t) : Types.t option =
             | Some _ -> acc
             | None -> unfillable env (n :: seen) fl.Tast.fty)
          None s.Tast.fields
-     (* A data type or a union, which are the two [Named] things that are not
+     (* A data type, the one [Named] thing in neither table: its tag names a
-        in [structs]. Both overlay their members, so the type itself is what
+        case, so the type itself is what the refusal names. *)
-        the refusal names. *)
      | None -> Some t)
   | _ -> Some t
 
@@ -1995,6 +1995,30 @@ let mk loc ty e : Tast.expr = { Tast.e; ty; loc }
 
 let unit_at loc = mk loc Types.Unit Tast.Unit
 
+(* Integer arithmetic over literals alone, folded. Unlike [const_int] no name
+   is read: a defconst has a type of its own, and only an untyped constant may
+   stand at a type variable. *)
+let rec literal_arith (e : Ast.expr) : int64 option =
+  match e.Ast.e with
+  | Ast.Int n -> Some n
+  | Ast.Call ({ Ast.e = Ast.Var op; _ }, x :: y :: rest) ->
+    let step a b =
+      match op with
+      | "+" -> Some (Int64.add a b)
+      | "-" -> Some (Int64.sub a b)
+      | "*" -> Some (Int64.mul a b)
+      | "/" when b <> 0L -> Some (Int64.div a b)
+      | "%" when b <> 0L && rest = [] -> Some (Int64.rem a b)
+      | _ -> None
+    in
+    List.fold_left
+      (fun acc e ->
+         match acc, literal_arith e with
+         | Some a, Some b -> step a b
+         | _ -> None)
+      (literal_arith x) (y :: rest)
+  | _ -> None
+
 
 (* The environment for a lifted body, built once its own body has been checked
    and [caught] is therefore final. spec-memory.md's case 2, and the whole of
@@ -3597,6 +3621,14 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   | Ast.ArrayFill (dims, v) -> check_array_fill ctx ~want loc dims v
   | Ast.ArrayGen (dims, f) -> check_array_gen ctx ~want loc dims f
   | Ast.Match (scrutinee, arms) -> check_match ctx ~tail ?want loc scrutinee arms
+  (* Constant integer arithmetic where a type variable is wanted is folded to
+     the literal it computes first, so [(+ x (+ 1 2))] is admitted wherever
+     [(+ x 3)] is. The instantiation re-checks the form unfolded, at a concrete
+     type, where the ordinary arithmetic is fine. *)
+  | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%"); _ }, _)
+    when (match want with Some (Types.Var _) -> true | _ -> false)
+         && literal_arith e <> None ->
+    int_literal loc ~want ~preds:ctx.env.tvpreds (Option.get (literal_arith e))
   | Ast.Call (head, args) -> check_call ctx ~want loc head args
   | Ast.Unwrap (Ast.Usome, v) ->
     (* Unwrap Some, else early-return None from the enclosing function, so the
@@ -5426,7 +5458,34 @@ and check_arr ctx ~want loc items =
     | Some (Types.Slice t) -> Some t
     | _ -> None
   in
-  let items = map_lr (fun i -> check ctx ?want:elem_want i) items in
+  (* With nothing outside saying what the elements are, the first one says:
+     [[(f32 1.0) 2.5]] is an [[2 f32]], its [2.5] checked at [f32] the way it
+     would be at an [f32] parameter. *)
+  let items =
+    match elem_want, items with
+    | Some _, _ | None, [] -> map_lr (fun i -> check ctx ?want:elem_want i) items
+    | None, first :: rest ->
+      let first = check ctx first in
+      let want =
+        match first.Tast.ty with Types.Never -> None | t -> Some t
+      in
+      (* A refusal of the element itself says where its type came from. *)
+      let one (i : Ast.expr) =
+        try check ctx ?want i with
+        | Loc.Error d when d.Loc.dloc = i.Ast.loc && want <> None ->
+          raise
+            (Loc.Error
+               { d with
+                 Loc.notes =
+                   d.Loc.notes
+                   @ [ Loc.note first.Tast.loc
+                         (Printf.sprintf
+                            "this array's first element is %s, so every \
+                             element is"
+                            (Types.to_string first.Tast.ty)) ] })
+      in
+      first :: map_lr one rest
+  in
   let n = Int64.of_int (List.length items) in
   let elem =
     match elem_want, items with
@@ -7160,8 +7219,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
         | Some bad ->
           Loc.failk "check/fill-not-plain-data" loc
             "%s writes raw bytes over %s, and %s is not plain data — %s. \
-             Fill only numbers, and structs and fixed arrays built out of \
+             Fill only numbers and pointers, and structs, unions and fixed \
-             them"
+             arrays built out of them"
             name (Types.to_string ty)
             (if Types.equal bad ty then "it" else Types.to_string bad)
             (match bad with
@@ -7173,8 +7232,6 @@ and named_call ?(qualified = false) ctx ~want loc name args =
                 a filled header frees a wild address"
              | Types.String | Types.Slice _ ->
                "it is a pointer and a length every bounds check believes"
-             | Types.Ptr _ ->
-               "it is an address every deref trusts"
              | Types.Bool ->
                "a bool is an i1 to LLVM and a whole byte to the x86 backend, \
                 so a filled one would not even agree with itself across the \
@@ -7188,15 +7245,6 @@ and named_call ?(qualified = false) ctx ~want loc name args =
              | Types.Named n when Hashtbl.mem ctx.env.datas n ->
                "it carries a tag that names a case, and no byte pattern \
                 names a real one"
-             | Types.Named n when Hashtbl.mem ctx.env.unions n ->
-               (* Untagged, per [env.unions]'s own note — so the reason is
-                  not a tag. It is that a union's members overlay, and this
-                  rule walks a struct's fields rather than a union's members:
-                  nothing here has shown they are all plain data, and a
-                  member that is not would be filled through the one that
-                  is. *)
-               "a union's members overlay, and this rule does not walk them \
-                — so nothing here has shown that every member is plain data"
              | Types.Enum _ ->
                "an enum's values are the members it declared, and no byte \
                 pattern is one of them"

test/programs/array-first-element.flan

@@ -0,0 +1,14 @@
+;;;; An array literal with nothing outside it saying what its elements are
+;;;; takes that from its first element: [(f32 1.0) 2.5] is a [2 f32], and the
+;;;; 2.5 is an f32 literal rather than an f64 refused for not being one.
+(defn sum3 [a [3 f32]] f32 (+ (at a 0) (at a 1) (at a 2)))
+
+(defn main [] i32
+  (let [a [(f32 1.0) 2.5 3.25]
+        b [(i64 1) 2 3]
+        c [(u8 1) 255]]
+    (println (length a))
+    (println (sum3 a))
+    (println (+ (at b 1) (i64 9000000000)))
+    (println (at c 1)))
+  0)

test/programs/fill-ptr-union.flan

@@ -0,0 +1,18 @@
+;;;; A pointer and an untagged union take a byte fill. The union is filled
+;;;; over its whole size, so its widest member reads back every byte; the
+;;;; pointer is read back through a union that overlays it with a u64, since
+;;;; there is no other way to see an address as a number.
+(defunion U [a u32  b [8 u8]])
+(defunion W [p (Ptr i32)  n u64])
+
+(defn main [] i32
+  (let [u (array 1 U)]
+    (set u (filled 0xAB))
+    (println (.a (at u 0)))                   ; 2880154539
+    (println (at (.b (at u 0)) 7)))           ; 171
+  (let [w (array 1 W)]
+    (set (.p (at w 0)) (dead-beef))
+    (println (.n (at w 0)))                   ; 17275436393656397278
+    (set (at w 0) (filled 0x01))
+    (println (.n (at w 0))))                  ; 72340172838076673
+  0)

test/programs/generic-fold.flan

@@ -0,0 +1,11 @@
+;;;; Constant integer arithmetic stands where a bounded type variable is
+;;;; wanted, as the single literal it folds to would.
+(defn f [x $t] t {:where (numeric? $t)} (+ x (* 2 (+ 1 2))))
+(defn g [x $t] t {:where (integer? $t)} (- x (% 7 4)))
+
+(defn main [] i32
+  (println (f 4))              ; 10
+  (println (f (u8 250)))       ; 0, u8 arithmetic wrapping
+  (println (f 1.5))            ; 7.5
+  (println (g (i64 10)))       ; 7
+  0)

test/test_acceptance.ml

@@ -529,6 +529,26 @@ let () =
     outputs "a u64 constant in decimal" "programs/u64-decimal.flan" u64_out;
     outputs ~x86:true "a u64 constant in decimal, x86"
       "programs/u64-decimal.flan" u64_out;
+    (* Constant arithmetic folds before a bounded variable checks it. *)
+    let fold_out = "10\n0\n7.5\n7\n" in
+    outputs "constant arithmetic at a bounded variable"
+      "programs/generic-fold.flan" fold_out;
+    outputs ~x86:true "constant arithmetic at a bounded variable, x86"
+      "programs/generic-fold.flan" fold_out;
+    (* A pointer and an untagged union take a byte fill. *)
+    let fpu_out =
+      "2880154539\n171\n17275436393656397278\n72340172838076673\n" in
+    outputs "a pointer and a union filled" "programs/fill-ptr-union.flan"
+      fpu_out;
+    outputs ~x86:true "a pointer and a union filled, x86"
+      "programs/fill-ptr-union.flan" fpu_out;
+    (* An array literal takes its element type from its first element when
+       nothing outside it names one. *)
+    let first_out = "3\n6.75\n9000000002\n255\n" in
+    outputs "an array literal's first element types the rest"
+      "programs/array-first-element.flan" first_out;
+    outputs ~x86:true "an array literal's first element types the rest, x86"
+      "programs/array-first-element.flan" first_out;
     (* into. The count of pulls is the assertion a unit test cannot make: one
        pass, one call per element per stage it reaches, and no intermediate
        collection anywhere. The two show lines either side of it are the same

test/test_flan.ml

@@ -2852,10 +2852,9 @@ let () =
   rejects_check "a string cannot be filled"
     "(defn f [] () (let [s \"hi\"] (set s (filled 0xFF))))"
     ~needle:"a length every bounds check believes";
-  rejects_check "a pointer field cannot be filled"
+  accepts "a pointer field may be filled"
     "(defstruct S [p (Ptr i32)]) \
-     (defn f [] () (let [s (S {})] (set s (filled 0xFF))))"
+     (defn f [] () (let [s (S {})] (set s (filled 0xFF))))";
-    ~needle:"an address every deref trusts";
   (* The one refusal that is about the two backends rather than the runtime:
      LLVM reads a bool's low bit and x86 compares the whole byte, so 0xDE is
      false on one and true on the other. Byte-identical behaviour across the
@@ -2864,15 +2863,17 @@ let () =
   rejects_check "a bool cannot be filled"
     "(defn f [] () (let [b false] (set b (filled 0xFF))))"
     ~needle:"would not even agree with itself";
-  (* Each of the tagged and address-carrying types names its own reason. They
+  (* An untagged union is filled over its whole size when every member may be
-     shared one "it carries a tag that names a case" line until review caught
+     filled, and refused for the member that may not. *)
-     that it was false for two of them — a union is untagged (env.unions is
+  accepts "a union of numbers may be filled"
-     "the untagged unions") and a function value is a code pointer, not a
-     tag. Pinned per type so the reasons cannot quietly re-merge. *)
-  rejects_check "a union cannot be filled, and not because of a tag"
     "(defunion U [a i32 b f64]) \
+     (defn f [] () (let [u (U {})] (set u (dead-beef))))";
+  rejects_check "a union with a dyn member cannot be filled"
+    "(defunion U [a i32 d dyn]) \
      (defn f [] () (let [u (U {})] (set u (dead-beef))))"
-    ~needle:"a union's members overlay";
+    ~needle:"a root pointing at nothing";
+  (* Each of the tagged and address-carrying types names its own reason, so
+     the reasons cannot quietly merge into one that is false for some. *)
   rejects_check "a function value cannot be filled"
     "(defn g [] ()) (defn f [] () (let [h g] (set h (dead-beef))))"
     ~needle:"it is a code address";
@@ -6343,6 +6344,18 @@ let () =
   parse_rejects "the $ refusal names the bare spelling"
     "(defn $foo [x i32] i32 x)" ~needle:"Name it foo";
 
+  (* ── An array literal's first element types the rest ───────────── *)
+  accepts "an f32 array literal from its first element"
+    "(defn main [] i32 (let [a [(f32 1.0) 2.5]] (i32 (length a))))";
+  (match checked "(defn main [] i32 (let [a [(u8 1) 256]] 0))" with
+   | _ -> check "an element that does not fit the first element's type" false
+   | exception Loc.Error d ->
+     check "the refusal says the first element set the type"
+       (List.exists
+          (fun (n : Loc.note) ->
+             contains n.Loc.nmsg "this array's first element is u8")
+          d.Loc.notes));
+
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"
     (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all);