A numeric type's limits are (max-value T) and (min-value T), and an array literal of numbers with no common type is refused with the conversion named

TODO.org

@@ -1079,11 +1079,6 @@ An unknown call whose near miss is a value — =(context-allocator)= against
 =context/allocator=, or a global — says the name is a value written without
 parentheses, and names no call at all when the call had arguments.
 
-** NEXT (max-value T) and (min-value T)
-Decided 2026-09-25: the type-limit constants as a form taking a type, Odin's
-max(T), valid at any numeric type or a numeric?-bounded variable. For a float,
-min-of is the most negative finite value.
-
 ** NEXT (Ptr const T), the pointer beside [const T]
 Decided 2026-09-25: addr through a read-only slice gives a (Ptr const T), which
 nothing writes through; (Ptr T) widens to it and never back; a C parameter
@@ -1565,7 +1560,8 @@ static tracking of destroy, which is move semantics.
 ** DONE A mixed array literal with no want is a dyn vector
 CLOSED: [2026-09-25]
 Elements that agree, numbers meeting at the wider, are typed; elements that mix
-are a dyn vector. Rules out the first element typing the rest.
+are a dyn vector, except numbers with no common type, which are refused. Rules
+out the first element typing the rest.
 
 * Dev loop
 

lib/check.ml

@@ -5792,7 +5792,8 @@ and check_arr ctx ~want loc items =
    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. *)
+   dyn is expected. Numbers that do not agree are refused instead; see
+   [numbers_disagree]. *)
 and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
   let natural (i : Ast.expr) =
     match i.Ast.e with
@@ -5854,9 +5855,52 @@ and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
         the one worth reading. *)
      | _, first :: _ -> ignore (check ctx first); None
      | [], [] -> None)
-  else List.fold_left
+  else
-      (fun found c -> match found with Some _ -> found | None -> settle c)
+    match
-      None candidates
+      List.fold_left
+        (fun found c -> match found with Some _ -> found | None -> settle c)
+        None candidates
+    with
+    | Some t -> Some t
+    | None ->
+      let numeric t = match t with Types.Int _ | Types.Float _ -> true | _ -> false in
+      if needs = [] && List.for_all numeric (tys @ lit_tys) then
+        numbers_disagree ctx
+          (List.filter_map
+             (fun i -> Option.map (fun t -> (i, t)) (natural i)) items)
+      else None
+
+(* Numbers with no type they all meet at — an i32 beside an f32, an i64 beside
+   a u64 — are refused rather than boxed into a dyn vector: the elements are
+   all numbers, and which one should move is the program's to say. The fix
+   named converts the second of the first disagreeing pair, into the float
+   when one of the two is a float and into the first's type otherwise. *)
+and numbers_disagree : 'a. ctx -> (Ast.expr * Types.t) list -> 'a =
+  fun ctx elems ->
+  match elems with
+  | [] -> fail Loc.unknown "internal: an array of numbers with no elements"
+  | (first, t1) :: rest ->
+    let second, t2 =
+      match List.find_opt (fun (_, t) -> Types.join t1 t = None) rest with
+      | Some p -> p
+      | None -> List.nth elems (List.length elems - 1)
+    in
+    let target, moved, moved_ty, other =
+      match t1, t2 with
+      | Types.Int _, Types.Float _ -> t2, first, t1, second
+      | _ -> t1, second, t2, first
+    in
+    ignore ctx;
+    let tn = Types.to_string target in
+    Loc.failk "check/array-numbers-disagree" moved.Ast.loc
+      ~notes:[ Loc.note other.Ast.loc (Printf.sprintf "this element is %s" tn) ]
+      "this array's elements are %s and %s, and neither holds every value of \
+       the other — %s"
+      (Types.to_string moved_ty) tn
+      (match spell_arg "" moved with
+       | "" ->
+         Printf.sprintf "convert the %s element with the %s cast" (Types.to_string moved_ty) tn
+       | x -> Printf.sprintf "convert one, as in (%s %s)" tn x)
 
 (* Elements that do not agree and cannot all become a dyn either: a struct
    beside a number, a type variable beside a literal. The dyn vector's refusal
@@ -7263,6 +7307,16 @@ and file_guard ctx loc ~path_slot ~op mk_steps =
    missing annotation for a program that had written one. One list, read by
    both callers, so the next kind of type added cannot be added to one of
    them. *)
+(* An argument written as a type: a type expression, or a bare name that is a
+   type and not a local or a global of the same spelling. *)
+and type_arg ctx (a : Ast.expr) =
+  type_of_expr a <> None
+  || (match a.Ast.e with
+      | Ast.Var n ->
+        lookup ctx n = None && (not (Hashtbl.mem ctx.env.globals n))
+        && type_named ctx n
+      | _ -> false)
+
 and type_named ctx n =
   (* A type variable names a type here too, which is what lets [(vec-new t)]
      and [(vec-new $t)] be written in a generic body: inside an instantiation
@@ -7783,31 +7837,34 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     expect ctx loc ~want
       (List.fold_left (fun acc arg -> pick acc (check ctx ~want:ty arg))
          (pick a b) rest)
-  (* (max-of T) and (min-of T): the type-limit constants, by type, so a
+  (* A type handed to the prelude's slice reductions: the reach for the
+     type-limit constants under the name of the reduction beside them. *)
+  | ("max-of" | "min-of")
+    when (not (shadows_builtin ctx loc name))
+         && (match args with [ a ] -> type_arg ctx a | _ -> false) ->
+    let which = if String.equal name "max-of" then "max-value" else "min-value" in
+    fail loc
+      "%s reduces a slice to its %s element, and this is a type — the %s value \
+       of a type is (%s %s)"
+      name (if which = "max-value" then "largest" else "least")
+      (if which = "max-value" then "largest" else "least") which
+      (spell_arg "i32" (List.hd args))
+  (* (max-value T) and (min-value T): the type-limit constants, by type, so a
      generic body can name its own type's. Odin's max(T) and min(T), and the
      same answer for a float: the largest finite value and its negation, not
-     the smallest positive one. Given a value rather than a type, the name is
+     the smallest positive one. *)
-     the prelude's reduction of a slice, and the call is an ordinary one —
+  | "max-value" | "min-value" ->
-     the same split [vec-new] makes between a type and an allocator. *)
+    arity ctx loc name 1 args;
-  | ("max-of" | "min-of")
+    if not (type_arg ctx (List.hd args)) then
-    when (match args with
+      fail (List.hd args).Ast.loc "%s takes a type, as in (%s i32)" name name;
-          | [ a ] ->
-            type_of_expr a <> None
-            || (match a.Ast.e with
-                | Ast.Var n ->
-                  lookup ctx n = None
-                  && (not (Hashtbl.mem ctx.env.globals n))
-                  && type_named ctx n
-                | _ -> false)
-          | _ -> false) ->
     let a = List.hd args in
     let ty =
       match type_of_expr a, a.Ast.e with
       | Some t, _ -> resolve ctx.env t
       | _, Ast.Var n -> resolve_name ctx.env ~seen:[] a.Ast.loc n
-      | _ -> fail a.Ast.loc "internal: max-of's type argument is not a type"
+      | _ -> fail a.Ast.loc "internal: %s's type argument is not a type" name
     in
-    let max = String.equal name "max-of" in
+    let max = String.equal name "max-value" in
     let v =
       match ty with
       | Types.Int k ->
@@ -10734,6 +10791,13 @@ let builtins : (string * string * string) list =
       i16-y) is an i16.");
     ("max", "max [ordered? ...] ordered?",
      "The largest of two or more operands, each evaluated exactly once.");
+    ("max-value", "max-value [type] T",
+     "The largest value of a numeric type: (max-value u8) is 255, and at a \
+      float the largest finite value. Takes a type variable under \
+      {:where (numeric? $t)}.");
+    ("min-value", "min-value [type] T",
+     "The least value of a numeric type: (min-value i8) is -128, 0 at an \
+      unsigned type, and at a float the negation of the largest finite value.");
     ("zeroed", "zeroed [] T",
      "The all-bytes-zero value of whatever it is being stored into, so it \
       only means anything where a type is expected of it.");

lib/prelude.ml

@@ -427,8 +427,7 @@ let source = {flan|
 ;; or more numbers, and a defn cannot shadow a builtin: nothing shadows [+]
 ;; either. These reduce a slice, which is a different operation with a
 ;; different arity, so the different name is honest rather than a workaround.
-;; Given a type instead of a slice, (min-of i8) and (max-of $t) are the type's
+;; A type's own limits are (min-value T) and (max-value T).
-;; limits, and the checker answers those itself.
 (defn min-of [s [$t]] (Option $t)
   {:where (ordered? $t)}
   (if (= (length s) 0)

test/programs/max-value.flan

@@ -1,4 +1,4 @@
-;;;; (max-of T) and (min-of T): a numeric type's limits, named by the type, at
+;;;; (max-value T) and (min-value T): a numeric type's limits, named by the type, at
 ;;;; a concrete type and inside a generic whose bound admits numbers.
 
 ;; A selection sort, descending, whose running best starts at the least value
@@ -6,7 +6,7 @@
 (defn sort-desc [s [$t]] ()
   {:where (numeric? $t)}
   (dotimes [i (length s)]
-    (let [best (min-of $t)
+    (let [best (min-value $t)
           at-best i]
       (dotimes [j (- (length s) i)]
         (let [k (+ i j)]
@@ -17,7 +17,7 @@
 
 (defn largest [s [$t]] $t
   {:where (numeric? $t)}
-  (let [best (min-of t)]
+  (let [best (min-value t)]
     (dotimes [i (length s)]
       (when (> (at s i) best) (set best (at s i))))
     best))
@@ -31,16 +31,16 @@
   (println ""))
 
 (defn main [] i32
-  (println (max-of u8))
+  (println (max-value u8))
-  (println (min-of u8))
+  (println (min-value u8))
-  (println (max-of i8))
+  (println (max-value i8))
-  (println (min-of i8))
+  (println (min-value i8))
-  (println (max-of i32))
+  (println (max-value i32))
-  (println (min-of i64))
+  (println (min-value i64))
-  (println (max-of u64))
+  (println (max-value u64))
-  (println (= (max-of f32) f32-max))
+  (println (= (max-value f32) f32-max))
-  (println (= (min-of f64) (- f64-max)))
+  (println (= (min-value f64) (- f64-max)))
-  (println (= (max-of i16) i16-max))
+  (println (= (max-value i16) i16-max))
   (let [a [(i32 3) -7 12 0 -2147483648 5]
         b [2.5 -1.0 1e300 -1e308]
         c [(u8 4) 0 200 9]]

test/test_acceptance.ml

@@ -585,14 +585,14 @@ let () =
     outputs "a prelude function shadowed" "programs/shadow-prelude.flan" sp_out;
     outputs ~x86:true "a prelude function shadowed, x86"
       "programs/shadow-prelude.flan" sp_out;
-    (* (max-of T) and (min-of T), concrete and inside a generic. *)
+    (* (max-value T) and (min-value T), concrete and inside a generic. *)
     let maxof_out =
       "255\n0\n127\n-128\n2147483647\n-9223372036854775808\n\
        18446744073709551615\ntrue\ntrue\ntrue\n\
        12 5 3 0 -7 -2147483648 \n1e+300 2.5 -1 -1e+308 \n200\n-5\ntrue\n" in
-    outputs "max-of and min-of" "programs/max-of.flan" maxof_out;
+    outputs "max-value and min-value" "programs/max-value.flan" maxof_out;
-    outputs ~opt:"-O0" "max-of and min-of, -O0" "programs/max-of.flan" maxof_out;
+    outputs ~opt:"-O0" "max-value and min-value, -O0" "programs/max-value.flan" maxof_out;
-    outputs ~x86:true "max-of and min-of, x86" "programs/max-of.flan" maxof_out;
+    outputs ~x86:true "max-value and min-value, x86" "programs/max-value.flan" maxof_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

@@ -6546,30 +6546,44 @@ let () =
              (fun (n : Loc.note) ->
                 contains n.Loc.nmsg "this array's first element is $t")
              d.Loc.notes));
+  rejects_check "numbers with no common type are refused and the fix named"
+    "(defn f [x i32 y f32] i32 (let [a [x y]] 0))"
+    ~needle:"elements are i32 and f32, and neither holds every value of the \
+             other — convert one, as in (f32 x)";
+  accepts "the conversion that refusal names compiles"
+    "(defn f [x i32 y f32] i32 (let [a [(f32 x) y]] 0))";
+  rejects_check "two integer types with no common type are refused"
+    "(defn f [x i64 y u64] i32 (let [a [x y]] 0))" ~needle:"as in (i64 y)";
+  accepts "the integer conversion that refusal names compiles"
+    "(defn f [x i64 y u64] i32 (let [a [x (i64 y)]] 0))";
   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";
 
-  (* ── (max-of T) and (min-of T) ──────────────────────────────────── *)
+  (* ── (max-value T) and (min-value T) ──────────────────────────────── *)
-  infers "max-of carries its type" "(max-of u16)" "u16";
+  infers "max-value carries its type" "(max-value u16)" "u16";
-  infers "min-of at a float" "(min-of f32)" "f32";
+  infers "min-value at a float" "(min-value f32)" "f32";
-  (match checked "(defn f [x $t] $t (max-of $t))" with
+  (match checked "(defn f [x $t] $t (max-value $t))" with
-   | _ -> check "max-of at an unbounded type variable is refused" false
+   | _ -> check "max-value at an unbounded type variable is refused" false
    | exception Loc.Error d ->
-     check "max-of at an unbounded type variable names the bound and only it"
+     check "max-value at an unbounded type variable names the bound and only it"
        (contains d.Loc.dmsg "write {:where (numeric? $t)}"
         && not (contains d.Loc.dmsg "Fn")));
   infers "two literal if arms meet at the wider" "(if true 1 2.5)" "f64";
   infers "two integer if arms stay i32" "(if true 1 2)" "i32";
   infers "two literal match arms meet at the wider"
     "(match (Some 1) (Some v) 1 None 2.5)" "f64";
-  accepts "max-of at a type variable the bound admits"
+  accepts "max-value at a type variable the bound admits"
-    "(defn f [x $t] $t {:where (integer? $t)} (max-of t))";
+    "(defn f [x $t] $t {:where (integer? $t)} (max-value t))";
-  rejects_check "max-of at a type that is not a number names the bound"
+  rejects_check "max-value at a type that is not a number names the bound"
-    "(defn f [] string (max-of string))"
+    "(defn f [] string (max-value string))"
-    ~needle:"max-of takes a numeric? type, and string is not one";
+    ~needle:"max-value takes a numeric? type, and string is not one";
-  accepts "max-of of a slice is still the prelude's reduction"
+  rejects_check "max-value of a value says it takes a type"
+    "(defn f [x i32] i32 (max-value x))" ~needle:"max-value takes a type";
+  accepts "max-of of a slice is the prelude's reduction"
     "(defn f [xs [i32]] (Option i32) (max-of xs))";
+  rejects_check "max-of of a type names max-value"
+    "(defn f [] u8 (max-of u8))" ~needle:"the largest value of a type is (max-value u8)";
 
   (* ── (the T e) ─────────────────────────────────────────────────── *)
   infers "the gives a literal its type" "(the u8 200)" "u8";