(the T e) gives any expression its type, and an array literal nothing names is typed when its elements agree and a dyn vector when they mix

TODO.org

@@ -923,19 +923,13 @@ type an expression cannot hold, such as =(Fn [i32] ())=, is parsed as
 
 ** DONE An array literal cannot say it is [f32]
 CLOSED: [2026-09-25]
-With nothing outside an array literal naming its element type, the first
+=(the [f32] [1 2.5])= names the element type; with nothing naming one, a literal
-element's type is the want for the rest, so =[(f32 1.0) 2.5]= is a =[2 f32]=. A
+element takes the other elements' type. Rules out a =1.0f= suffix for now.
-refusal of a later element carries a note at the first saying it set the type.
-Rules out a =1.0f= suffix for now.
 
-** NEXT A let binding takes no type annotation
+** DONE 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.
+CLOSED: [2026-09-25]
-Everything under the surface is there — the binding carries a type slot and the
+=(the T expr)= gives any expression its want and =let= stays a flat list of
-checker consumes it as the want — and only the way it is written is open, because
+pairs. Rules out a type slot in =let=.
-=let= is a flat list of pairs and cannot disambiguate by count. No longer the
-blocker it was, since =(array 4 T)= answers the case that raised it. plan.org's
-rule is "annotate function signatures, infer locals", so a general annotation is a
-deliberate absence.
 
 ** NEXT A read-only slice type
 Decided 2026-09-25: =[const u8]=, Zig's spelling in Flan's brackets. =bytes-view= answers one and a =set= through it is a compile error; a =[T]= converts to =[const T]= and not back, and the prelude's read-only functions take it. =const= is reserved as a name, since =[n T]= accepts a constant's name for =n=.
@@ -1513,11 +1507,10 @@ incarnation it was made for; every use compares the incarnation, so a destroyed
 arena traps whether or not a later arena-new reused its record. Rules out
 static tracking of destroy, which is move semantics.
 
-** NEXT A mixed array literal with no want is a dyn vector
+** DONE A mixed array literal with no want is a dyn vector
-Decided 2026-09-25: with nothing expected of it, an array literal whose elements
+CLOSED: [2026-09-25]
-agree (numbers widening together) is typed; one whose elements mix — [10 "Hi"],
+Elements that agree, numbers meeting at the wider, are typed; elements that mix
-[nil 1] — is a dyn vector. (the [T] ...) forces a typed one, and a want from
+are a dyn vector. Rules out the first element typing the rest.
-context still wins. Replaces the first-element carry-over.
 
 * Dev loop
 

lib/ast.ml

@@ -126,6 +126,10 @@ and expr_kind =
      dimension; [ArrayFill]'s is the element value itself, evaluated once. *)
   | ArrayFill of len list * expr
   | ArrayGen  of len list * expr
+  (* (the T e) — [e] checked with [T] as its expectation, Common Lisp's
+     special operator. A binding has no type slot, and this is what gives any
+     expression one; it compiles to [e]. *)
+  | The of texpr * expr
   (* These bind names or alter control flow, so none of them can be a call. *)
   | Fn      of string list * expr list        (* (fn [x y] ...) — non-escaping *)
   (* (dotimes :o [i n] ...), (dotimes [i start stop] ...) and
@@ -437,6 +441,7 @@ let map_children f (e : expr) : expr =
        subexpressions. The dimensions are [len]s and hold none. *)
     | ArrayFill (ds, v) -> ArrayFill (ds, ex v)
     | ArrayGen (ds, f) -> ArrayGen (ds, ex f)
+    | The (t, x) -> The (t, ex x)
     | Fn (ps, es) -> Fn (ps, List.map ex es)
     | Dotimes (l, n, b, es) ->
       Dotimes (l, n,

lib/check.ml

@@ -3619,18 +3619,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
      {:xs [1 2]} mean what it reads as. Everywhere else brackets stay the
      fixed-array literal they always were. *)
   | Ast.Arr items when want = Some Types.Dyn ->
-    let v = fresh_slot ctx Types.Dyn in
+    dyn_vec ctx loc (map_lr (fun x -> check ctx ~want:Types.Dyn x) items)
-    let vval = mk loc Types.Dyn (Tast.Local v) in
-    let pushes =
-      List.map
-        (fun x ->
-           rt loc Types.Unit "flan_dyn_push"
-             [ vval; check ctx ~want:Types.Dyn x; here loc ])
-        items
-    in
-    mk loc Types.Dyn
-      (Tast.Let ([ (v, rt loc Types.Dyn "flan_dyn_vec_new" []) ],
-                 pushes @ [ vval ]))
   | Ast.Arr items -> check_arr ctx ~want loc items
   (* (array 4 rl/Vector2). Parse already assembled the whole array type, so
      there is nothing to infer: resolve it and hand back its all-bytes-zero
@@ -3645,6 +3634,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     fail loc "this is a type, and a value is wanted here"
   | 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.The (t, v) -> check_the ctx ~want loc t v
   | 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
@@ -3922,8 +3912,8 @@ and var ctx ?(qualified = false) loc ~want name =
        fail loc "expected %s, found None" (Types.to_string other)
      | _ ->
        fail loc
-         "nothing here says what None is an Option of — annotate the \
+         "nothing here says what None is an Option of — use it where an \
-          function's return type or the binding")
+          Option is expected, or name one, as in (the (Option i32) None)")
   (* spec-memory.md puts the allocator in the calling convention as
      [context/allocator] and [context/temp]. They read as names rather than
      calls because that is how the spec writes them, and they are dynamic
@@ -5493,63 +5483,27 @@ and check_arr ctx ~want loc items =
     | Some (Types.Slice t) -> Some t
     | _ -> None
   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, _ :: _ ->
-    | None, first :: rest ->
+    (match arr_elem_type ctx items with
-      let first_ast = first in
+     | Some t ->
-      let first = check ctx first in
+       let n = Int64.of_int (List.length items) in
-      let want =
+       expect ctx loc ~want
-        match first.Tast.ty with Types.Never -> None | t -> Some t
+         (check_arr ctx ~want:(Some (Types.Array (n, t))) loc items)
-      in
+     | None ->
-      (* A refusal of the element itself says where its type came from. *)
+       expect ctx loc ~want
-      let one (i : Ast.expr) =
+         (dyn_vec ctx loc (map_lr (fun i -> check ctx ~want:Types.Dyn i) items)))
-        (match i.Ast.e, want with
+  | _ ->
-         | Ast.UInt (_, text), Some (Types.Int k) when k <> Types.U64 ->
+  let items = map_lr (fun i -> check ctx ?want:elem_want i) items in
-           let first_src =
-             match first_ast.Ast.e with
-             | Ast.Int _ | Ast.Byte _ -> Some (spell_arg "" first_ast)
-             | _ -> None
-           in
-           Loc.failk literal_at_want i.Ast.loc
-             ~notes:
-               [ Loc.note first.Tast.loc
-                   (Printf.sprintf
-                      "this array's first element is %s, so every element is"
-                      (Types.ikind_name k)) ]
-             "%s does not fit in %s, and only a u64 holds it%s" text
-             (Types.ikind_name k)
-             (match first_src with
-              | Some f ->
-                Printf.sprintf " — write the first element as (u64 %s) for an \
-                                array of u64" f
-              | None -> " — make the first element a u64 for an array of u64")
-         | _ -> ());
-        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
     | Some t, _ -> t
     | None, first :: _ -> first.Tast.ty
     | None, [] ->
-      fail loc "an empty array literal needs a type — annotate the binding"
+      fail loc
+        "an empty array literal needs a type — use it where one is expected, \
+         or name it, as in (the [0 i32] [])"
   in
   List.iter
     (fun (i : Tast.expr) ->
@@ -5565,6 +5519,96 @@ and check_arr ctx ~want loc items =
      an array literal does not satisfy a slice expectation. *)
   expect ctx loc ~want (mk loc (Types.Array (n, elem)) (Tast.Arr items))
 
+(* The element type of an array literal nothing outside it names, or [None]
+   for a dyn vector. Every element is looked at on its own terms first, by
+   [probe], so nothing here is checked for real — [check_arr] does that once,
+   at the answer.
+
+   Elements that agree are a typed array: one type, or numbers that meet at
+   the wider of them the way two operands of [+] do. A literal takes the
+   others' type if it fits it, so [[(f32 1.0) 2.5]] is an [[2 f32]] and
+   [[(u8 1) 300]] an [[2 i32]]. An element that cannot be checked without
+   being told what it is — [None], a bare struct — takes the same type.
+   Elements that do not agree — [[10 "Hi"]], a dyn beside anything that is
+   not one — are a dyn vector, which is what the same brackets are where a
+   dyn is expected. *)
+and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
+  let natural (i : Ast.expr) =
+    match i.Ast.e with
+    (* Refused with no want, and only a u64 holds one. *)
+    | Ast.UInt _ -> Some (Types.Int Types.U64)
+    | _ -> probe ctx i.Ast.loc (fun () -> (check ctx i).Tast.ty)
+  in
+  let fits t (i : Ast.expr) =
+    probe ctx i.Ast.loc (fun () -> ignore (check ctx ~want:t i)) <> None
+  in
+  let lits, rest = List.partition lone_literal items in
+  let typed, needs =
+    List.partition_map
+      (fun i ->
+         match natural i with Some t -> Left (i, t) | None -> Right i)
+      rest
+  in
+  let tys =
+    List.filter (fun t -> t <> Types.Never) (List.map snd typed)
+  in
+  let lit_tys = List.filter_map natural lits in
+  let join_all = function
+    | [] -> None
+    | t :: ts ->
+      List.fold_left
+        (fun acc t -> Option.bind acc (fun a -> Types.join a t)) (Some t) ts
+  in
+  let mixed_dyn =
+    List.mem Types.Dyn tys
+    && (List.exists (fun t -> t <> Types.Dyn) tys || lits <> [])
+  in
+  let all_fit t = List.for_all (fits t) lits && List.for_all (fits t) needs in
+  (* A candidate the literals do not all fit is widened by the ones that do
+     not, once: [[x 2.5]] over an i32 [x] meets at f64. *)
+  let settle = function
+    | None -> None
+    | Some t when all_fit t -> Some t
+    | Some t ->
+      let t' =
+        List.fold_left
+          (fun acc i ->
+             if fits t i then acc
+             else Option.bind acc (fun a -> Option.bind (natural i) (Types.join a)))
+          (Some t) lits
+      in
+      (match t' with
+       | Some t' when not (Types.equal t' t) && all_fit t' -> Some t'
+       | _ -> None)
+  in
+  let candidates =
+    if tys <> [] then [ join_all tys ]
+    else join_all lit_tys :: List.map Option.some lit_tys
+  in
+  if mixed_dyn then None
+  else if tys = [] && lits = [] then
+    (match typed, needs with
+     | _ :: _, [] -> Some Types.Never
+     (* Nothing here says what any of them is. The first one's own refusal is
+        the one worth reading. *)
+     | _, first :: _ -> ignore (check ctx first); None
+     | [], [] -> None)
+  else List.fold_left
+      (fun found c -> match found with Some _ -> found | None -> settle c)
+      None candidates
+
+(* A dyn vector built where it stands from elements already checked at dyn:
+   the runtime's own vec, pushed to in order. *)
+and dyn_vec ctx loc (items : Tast.expr list) =
+  let v = fresh_slot ctx Types.Dyn in
+  let vval = mk loc Types.Dyn (Tast.Local v) in
+  let pushes =
+    List.map (fun x -> rt loc Types.Unit "flan_dyn_push" [ vval; x; here loc ])
+      items
+  in
+  mk loc Types.Dyn
+    (Tast.Let ([ (v, rt loc Types.Dyn "flan_dyn_vec_new" []) ], pushes @ [ vval ]))
+
 (* ── (array-fill [r c] v) and (array-gen [r c] f) ──────────────────────
 
    TODO.org, "A value-producing array constructor". [(array 4 T)] is
@@ -5683,6 +5727,59 @@ and array_build ctx loc ns elem ~pre ~element =
     (Tast.Let (pre @ [ (arr, mk loc aty (Tast.Zero aty)) ],
                [ nest ns islots; arrv ]))
 
+(* (the T e): [e] with [T] as its expectation, which is every conversion an
+   annotation would make — a literal built at T, a narrower number widened —
+   and nothing more. A dyn operand is the exception: an expectation would
+   unbox it and trap at run time on a mismatch, and [the] is a statement about
+   the type rather than a conversion, so it is refused and the cast named.
+
+   [(the [T] [...])] asks for the literal's element type and answers the
+   [n T] the literal is, since an array literal is never a slice. *)
+and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
+  let ty = resolve ctx.env t in
+  let is_nil = match v.Ast.e with Ast.Var "nil" -> true | _ -> false in
+  if ty <> Types.Dyn && not is_nil
+     && probe ctx loc (fun () -> (check ctx v).Tast.ty) = Some Types.Dyn
+  then begin
+    let tn = Types.to_string ty in
+    let numeric = match ty with Types.Int _ | Types.Float _ -> true | _ -> false in
+    if numeric then
+      fail v.Ast.loc
+        "the checks a value as %s and does not convert one, and this is a dyn \
+         — %s"
+        tn
+        (match spell_arg "" v with
+         | "" -> Printf.sprintf "convert it with the %s cast instead" tn
+         | s -> Printf.sprintf "write (%s %s) to convert it" tn s)
+    else
+      fail v.Ast.loc
+        "the checks a value as %s and does not convert one, and this is a dyn \
+         — a dyn becomes a %s where a %s is passed, returned or stored"
+        tn tn tn
+  end;
+  let r =
+    match ty, v.Ast.e with
+    | Types.Slice elem, Ast.Arr items ->
+      check_arr ctx
+        ~want:(Some (Types.Array (Int64.of_int (List.length items), elem)))
+        v.Ast.loc items
+    | _ -> expect ctx v.Ast.loc ~want:(Some ty) (check ctx ~want:ty v)
+  in
+  expect ctx loc ~want r
+
+(* [f] run for its answer alone: whatever it wrote into the context is put
+   back whether it succeeded or not, so a form can be checked once to see what
+   it is and then checked again for real. [None] if it was refused. *)
+and probe : 'a. ctx -> Loc.t -> (unit -> 'a) -> 'a option = fun ctx loc f ->
+  let answer = ref None in
+  (match
+     trial ctx (fun () ->
+       answer := Some (f ());
+       raise (Loc.Error (Loc.diag loc "probe")))
+   with
+   | _ -> ());
+  !answer
+
 and check_array_fill ctx ~want loc dims v =
   let ns = array_dims ctx loc dims in
   let elem_want = array_elem_want (List.length ns) want in
@@ -7285,7 +7382,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | _ ->
        fail loc
          "zeroed needs to know the type it is zeroing — use it where one is \
-          expected, as in (set grid (zeroed))")
+          expected, or name it, as in (the [4 i32] (zeroed))")
 
   (* [zeroed]'s two siblings, and the same shape exactly: a value of whatever
      type is expected of it, so [(set grid (filled 0xFF))] is how a place is
@@ -7382,7 +7479,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | _ ->
        fail loc
          "%s needs to know the type it is filling — use it where one is \
-          expected, as in (set grid (%s))"
+          expected, or name it, as in (the [4 u32] (%s))"
          name (if is_byte then "filled 0xFF" else name))
 
   (* The one half of a destructuring [let] that [Parse] cannot do on its own.
@@ -10400,9 +10497,9 @@ let builtins : (string * string * string) list =
       not hold. It becomes None where an (Option T) is wanted, and stays dyn \
       everywhere else.");
     ("None", "None (Option T)",
-     "The absent Option. It takes its type from its context — a return type \
+     "The absent Option. It takes its type from its context — a return type, \
-      or an annotated binding — because nothing about the word says what it \
+      a parameter, or (the (Option i32) None) — because nothing about the \
-      is an Option of.");
+      word says what it is an Option of.");
     ("context/allocator", "context/allocator Allocator",
      "The allocator in effect here: what with-allocator rebinds, and what an \
       allocating operation uses when none is named at the site.");

lib/load.ml

@@ -315,6 +315,7 @@ let rec rename_expr owned alias bound (e : Ast.expr) : Ast.expr =
        other reference to it. *)
     | Ast.ArrayFill (ds, v) -> Ast.ArrayFill (List.map (rename_len owned alias) ds, go v)
     | Ast.ArrayGen (ds, v) -> Ast.ArrayGen (List.map (rename_len owned alias) ds, go v)
+    | Ast.The (t, v) -> Ast.The (rename_texpr owned alias t, go v)
     | Ast.Fn (ps, body) ->
       Ast.Fn (ps, List.map (rename_expr owned alias (ps @ bound)) body)
     | Ast.Dotimes (l, i, b, body) ->
@@ -790,6 +791,7 @@ let rec expr_uses acc (e : Ast.expr) =
   | Ast.MapLit (_, kvs) -> List.iter (fun (k, v) -> go k; go v) kvs
   | Ast.Arr items -> gos items
   | Ast.ArrayOf t | Ast.TypeArg t -> texpr_uses acc t
+  | Ast.The (t, v) -> texpr_uses acc t; go v
   (* A dimension written as a name is a use of that constant, exactly as it is
      inside [Tarray]. *)
   | Ast.ArrayFill (ds, v) | Ast.ArrayGen (ds, v) ->

lib/parse.ml

@@ -496,6 +496,15 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
      array of integers — the wrong reading, and a silent one. Read here, the
      brackets are [len]s: the same integer-or-constant's-name the [n T] type
      spelling takes, refused by [len] when they are anything else. *)
+  (* ── (the T e) ──────────────────────────────────────────────────── *)
+  | Sym "the" ->
+    (match args with
+     | [ t; v ] -> mk (Ast.The (texpr t, expr v))
+     | _ ->
+       fail f
+         "the is (the TYPE value), as in (the u8 0) — the value, checked as \
+          a TYPE")
+
   | Sym (("array-fill" | "array-gen") as which) ->
     let usage () =
       fail f

test/programs/array-first-element.flan

@@ -1,6 +1,6 @@
 ;;;; 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
+;;;; takes that from the elements that are not literals: [(f32 1.0) 2.5] is a
-;;;; 2.5 is an f32 literal rather than an f64 refused for not being one.
+;;;; [2 f32], and the 2.5 is an f32 literal rather than an f64.
 (defn sum3 [a [3 f32]] f32 (+ (at a 0) (at a 1) (at a 2)))
 
 (defn main [] i32

test/programs/array-mixed.flan

@@ -0,0 +1,59 @@
+;;;; An array literal with nothing outside it naming a type: elements that agree
+;;;; are a typed array, numbers meeting at the wider and a literal taking the
+;;;; others' type, and elements that do not are a dyn vector.
+(defstruct P [x i32 y i32])
+(defn mixed [] i32
+  (let [x (i32 4)
+        a [(f32 1.0) 2.5 3.25]
+        b [(i64 1) 2 3]
+        c [(u8 1) 300]
+        d [x 2.5]
+        e [1 18446744073709551615]
+        f [10 "Hi"]
+        g [nil 1]
+        h [None (Some 3)]
+        i [(P 1 2) {.x 3 .y 4}]
+        j [[1 2] [3 4]]
+        k [1 2.5]
+        m [x (i64 5)]
+        dd [:a "b" 3]]
+    (println (length a))
+    (println (+ (at c 1) (i32 (at c 0))))
+    (println (at d 1))
+    (println (at e 1))
+    (println f)
+    (println g)
+    (println (length f))
+    (println (match (at h 1) None 0 (Some v) v))
+    (println (.y (at i 1)))
+    (println (at (at j 1) 0))
+    (println (at k 0))
+    (println (+ (at m 0) (i64 9000000000)))
+    (println dd))
+  0)
+
+;; (the T e) gives any expression its type.
+(defn the-forms [] i32
+  (let [a (the u8 200)
+        b (the i64 5000000000)
+        c (the f32 2.5)
+        d (the [3 f32] [1 2 3.5])
+        e (the [f32] [1 2.5])
+        f (the (Option i32) None)
+        g (the (Option i32) nil)
+        h (the dyn 3)
+        n (the i64 (+ (the i32 1) 2))
+        v (the (Vec i32) (vec-new))]
+    (println (+ a (u8 55)))
+    (println b)
+    (println (* c (f32 2.0)))
+    (println (+ (at d 0) (at d 2)))
+    (println (length e))
+    (println (match f None 0 (Some x) x))
+    (println (match g None 7 (Some x) x))
+    (println h)
+    (println n)
+    (println (length v)))
+  0)
+
+(defn main [] i32 (mixed) (the-forms))

test/test_acceptance.ml

@@ -551,13 +551,22 @@ let () =
       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
+    (* A literal element takes its type from the other elements when nothing
-       nothing outside it names one. *)
+       outside the array 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;
+    (* An array literal whose elements agree is typed and one whose elements
+       mix is a dyn vector; (the T e) gives any expression its type. *)
+    let mixed_out =
+      "3\n301\n2.5\n18446744073709551615\n[ 10 \"Hi\"]\n[ nil 1]\n2\n3\n4\n\
+       3\n1\n9000000004\n[ :a \"b\" 3]\n\
+       255\n5000000000\n5\n4.5\n2\n0\n7\n3\n3\n0\n" in
+    outputs "mixed array literals and the" "programs/array-mixed.flan" mixed_out;
+    outputs ~x86:true "mixed array literals and the, x86"
+      "programs/array-mixed.flan" mixed_out;
     (* (- x) negates, on every numeric type, a type variable and a dyn. *)
     let neg_out =
       "-3\n7\n-2.5\n-inf\n-1.5\n255\n-4\n-2.5\n-inf\n-9000000000\n\

test/test_flan.ml

@@ -1214,7 +1214,7 @@ let () =
   accepts "return type types the literal" "(defn f [] u8 0)";
   accepts "return type types None"        "(defn f [] (Option f64) None)";
   rejects_check "bare None has no type"   "(defconst x None)"
-    ~needle:"what None is an Option of";
+    ~needle:"(the (Option i32) None)";
   accepts "param types the literal"
     "(defn g [x u8] ()) (defn f [] () (g 3))";
   rejects_check "wrong argument type"
@@ -2905,7 +2905,7 @@ let () =
     ~needle:"needs to know the type it is filling";
   rejects_check "a dead-beef in a position with no expected type"
     "(defn f [] () (print (dead-beef)))"
-    ~needle:"needs to know the type it is filling";
+    ~needle:"(the [4 u32] (dead-beef))";
   (* The byte is a u8 and the ordinary literal rule applies to it — there is
      no range check of this builtin's own, and there does not need to be. *)
   rejects_check "a fill byte out of range"
@@ -6365,17 +6365,49 @@ 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 ───────────── *)
+  (* ── An array literal with nothing outside it naming a type ────── *)
-  accepts "an f32 array literal from its first element"
+  infers "a literal takes the other elements' type" "[(f32 1.0) 2.5]" "[2 f32]";
-    "(defn main [] i32 (let [a [(f32 1.0) 2.5]] (i32 (length a))))";
+  infers "numbers meet at the wider" "[(u8 1) 256]" "[2 i32]";
-  (match checked "(defn main [] i32 (let [a [(u8 1) 256]] 0))" with
+  infers "an int and a float literal meet at f64" "[1 2.5]" "[2 f64]";
-   | _ -> check "an element that does not fit the first element's type" false
+  infers "a wide literal makes the array u64" "[1 18446744073709551615]" "[2 u64]";
-   | exception Loc.Error d ->
+  infers "None takes the other element's Option" "[None (Some 1)]" "[2 (Option i32)]";
-     check "the refusal says the first element set the type"
+  infers "a number and a string are a dyn vector" "[10 \"Hi\"]" "dyn";
-       (List.exists
+  infers "nil beside a number is a dyn vector" "[nil 1]" "dyn";
-          (fun (n : Loc.note) ->
+  infers "two dyns are a typed array of dyn" "[nil nil]" "[2 dyn]";
-             contains n.Loc.nmsg "this array's first element is u8")
+  infers "the names the element type of a mixed literal" "(the [dyn] [1 2.5])" "[2 dyn]";
-          d.Loc.notes));
+  infers "the with a slice type gives the literal's array type"
+    "(the [f32] [1 2.5])" "[2 f32]";
+  rejects_check "every element needing a type names the first's refusal"
+    "(defn main [] i32 (let [a [None None]] 0))"
+    ~needle:"what None is an Option of";
+
+  (* ── (the T e) ─────────────────────────────────────────────────── *)
+  infers "the gives a literal its type" "(the u8 200)" "u8";
+  infers "the widens as an annotation does" "(the i64 (the i32 1))" "i64";
+  rejects_check "the does not narrow"
+    "(defn f [x i64] i32 (the i32 x))" ~needle:"expected i32, found i64";
+  rejects_check "the refuses a dyn and names the cast"
+    "(defn f [x dyn] i32 (the i32 x))" ~needle:"write (i32 x) to convert it";
+  accepts "the cast that refusal names compiles" "(defn f [x dyn] i32 (i32 x))";
+  rejects_check "the refuses a dyn at a type that has no cast"
+    "(defn f [x dyn] string (the string x))"
+    ~needle:"a dyn becomes a string where a string is passed";
+  accepts "the at an Option takes nil" "(defn f [] (Option i32) (the (Option i32) nil))";
+  parse_rejects "the takes a type and a value" "(defn f [] i32 (the i32))"
+    ~needle:"the is (the TYPE value)";
+  (* The refusals of a form with no type of its own name the as a way out, and
+     the spellings they name compile. *)
+  rejects_check "an empty array literal names the"
+    "(defn main [] i32 (let [a []] 0))" ~needle:"(the [0 i32] [])";
+  accepts "the empty array that refusal names compiles"
+    "(defn main [] i32 (let [a (the [0 i32] [])] (length a)))";
+  accepts "the None that refusal names compiles"
+    "(defn main [] i32 (let [a (the (Option i32) None)] 0))";
+  accepts "the zeroed that refusal names compiles"
+    "(defn main [] i32 (let [a (the [4 i32] (zeroed))] (at a 0)))";
+  accepts "the fills that refusal names compile"
+    "(defn main [] i32 (let [a (the [4 u32] (filled 0xFF)) \
+                             b (the [4 u32] (dead-beef))] 0))";
 
   (* ── A wide literal's follow-ups ──────────────────────────────── *)
   parse_rejects "a wide enum member is refused for its range"
@@ -6396,10 +6428,7 @@ let () =
     "(defmacro idm [x] x) \
      (defn f [] u64 (idm 18446744073709551615))";
 
-  rejects_check "a wide element after a narrow first names the u64 array"
+  accepts "a u64 array with a cast first element"
-    "(defn main [] i32 (let [a [1 18446744073709551615]] 0))"
-    ~needle:"write the first element as (u64 1) for an array of u64";
-  accepts "the u64 array that refusal names compiles"
     "(defn main [] i32 (let [a [(u64 1) 18446744073709551615]] 0))";
 
   (* ── Suggestions that compile ─────────────────────────────────── *)