The literal an array cannot hold is the element blamed, a negative literal in a generic body names a fix for every instantiation, and a doubly negated literal is positive

lib/check.ml

@@ -3583,6 +3583,28 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   let tail = ctx.tail in
   ctx.tail <- false;
   match e.Ast.e with
+  (* A negative literal in a generic body, at an instantiation that made it
+     unsigned. The cast the ordinary refusal names would be wrong at every
+     other type the function is called at, so the fix is one that needs no
+     negative number at all, and the refusal says which call asked. *)
+  | Ast.Int n
+    when Int64.compare n 0L < 0 && ctx.env.chain <> []
+         && (match want with
+             | Some (Types.Int k) -> not (Types.signed k)
+             | _ -> false) ->
+    let t = Option.get want in
+    let gname, _, at = List.nth ctx.env.chain (List.length ctx.env.chain - 1) in
+    let var =
+      match List.find_opt (fun (_, u) -> Types.equal u t) ctx.env.subst with
+      | Some (v, _) -> Printf.sprintf "$%s = %s" v (Types.to_string t)
+      | None -> Types.to_string t
+    in
+    Loc.failk literal_at_want loc
+      ~notes:[ Loc.note at (Printf.sprintf "%s is instantiated at %s here" gname var) ]
+      "%Ld does not fit in %s, which holds no negative number, and %s is called \
+       at %s — the body has to work at every type it is called at, so write \
+       it with no negative literal, as in (- x %Ld) in place of (+ x %Ld)"
+      n (Types.to_string t) gname var (Int64.neg n) n
   | Ast.Int n -> int_literal loc ~want ~preds:ctx.env.tvpreds n
   | Ast.UInt (n, s) -> wide_literal loc ~want n s
   | Ast.Byte b ->
@@ -5874,21 +5896,40 @@ 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 ->
+  | _ :: _ ->
+    (* A literal is not one of the disagreeing types when it fits the others:
+       each is checked at the type the rest meet at — or, with every element a
+       literal, at the u64 a wide one needs — and the first that does not fit
+       is the refusal, its own. *)
+    let lit (e, _) = lone_literal e in
+    let others = List.filter (fun p -> not (lit p)) elems in
+    let meet =
+      match others with
+      | [] ->
+        if List.exists (fun (e, _) -> match e.Ast.e with Ast.UInt _ -> true | _ -> false) elems
+        then Some (Types.Int Types.U64) else None
+      | (_, t) :: ts ->
+        List.fold_left (fun acc (_, u) -> Option.bind acc (fun a -> Types.join a u))
+          (Some t) ts
+    in
+    (match meet with
+     | Some (Types.Int _ as m) ->
+       List.iter
+         (fun (e, t) ->
+            if lone_literal e && (match t with Types.Int _ -> true | _ -> false)
+            then ignore (check ctx ~want:m e))
+         elems
+     | _ -> ());
+    let pool = if others = [] then elems else others in
+    let first, t1 = List.hd pool in
     let second, t2 =
-      match List.find_opt (fun (_, t) -> Types.join t1 t = None) rest with
+      match List.find_opt (fun (_, t) -> Types.join t1 t = None) (List.tl pool) with
       | Some p -> p
-      | None -> List.nth elems (List.length elems - 1)
+      | None ->
+        (match List.find_opt (fun (_, t) -> Types.join t1 t = None) elems with
+         | Some p -> p
+         | None -> List.nth elems (List.length elems - 1))
     in
-    (* An integer literal beside an integer type it does not fit — -1 beside a
-       u64 — is that literal's own refusal, which names the cast. *)
-    let literal_refusal (lit : Ast.expr) t =
-      match lit.Ast.e, t with
-      | Ast.Int _, Types.Int _ -> ignore (check ctx ~want:t lit)
-      | _ -> ()
-    in
-    literal_refusal second t1;
-    literal_refusal first t2;
     let target, moved, moved_ty, other =
       match t1, t2 with
       | Types.Int _, Types.Float _ -> t2, first, t1, second
@@ -7597,10 +7638,12 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      +0.0 — and an integer from 0, which wraps as (- 0 x) does. *)
   | "-" when List.length args = 1 ->
     let x = List.hd args in
-    (match x.Ast.e with
-     | Ast.Int n when n <> Int64.min_int ->
+    (match x.Ast.e, literal_arith x with
+     (* Integer arithmetic over literals alone negates to a literal, so
+        [(- (- 1))] is the literal 1 and fits a u8. *)
+     | _, Some n when n <> Int64.min_int ->
        check ctx ?want { Ast.e = Ast.Int (Int64.neg n); loc }
-     | Ast.Float v -> check ctx ?want { Ast.e = Ast.Float (-.v); loc }
+     | Ast.Float v, _ -> check ctx ?want { Ast.e = Ast.Float (-.v); loc }
      | _ ->
        let v = check ctx ?want:(numeric_want want) x in
        if v.Tast.ty = Types.Dyn then

test/test_flan.ml

@@ -6255,6 +6255,31 @@ let () =
        (let [a [(u64 -1) 18446744073709551615] b [x (u64 -1)] \
              c (the u64 (u64 -1))] \
          (S (u8 -3))))";
+  (* The literal that does not fit is the one blamed, not one that does. *)
+  rejects_check "a negative literal among u64 elements is the one blamed"
+    "(defn f [] () (println [(u64 2) 1 -1]))" ~needle:"-1 does not fit in u64";
+  rejects_check "a negative literal after a u64 element is the one blamed"
+    "(defn f [] () (println [1 (u64 2) -1]))" ~needle:"-1 does not fit in u64";
+  (* In a generic body the cast would break the other instantiations. *)
+  (match
+     checked
+       "(defn add1 [x $t] $t {:where (numeric? $t)} (+ x -1)) \
+        (defn main [] i32 (add1 3) (add1 (u64 5)) 0)"
+   with
+   | _ -> check "a negative literal at a u64 instantiation is refused" false
+   | exception Loc.Error d ->
+     check "the generic's refusal names a fix for every type and the call"
+       (contains d.Loc.dmsg "as in (- x 1) in place of (+ x -1)"
+        && not (contains d.Loc.dmsg "(u64 -1)")
+        && List.exists
+             (fun (n : Loc.note) ->
+                contains n.Loc.nmsg "add1 is instantiated at $t = u64 here")
+             d.Loc.notes));
+  accepts "the generic's fix compiles at both types"
+    "(defn add1 [x $t] $t {:where (numeric? $t)} (- x 1)) \
+     (defn main [] i32 (add1 3) (add1 (u64 5)) 0)";
+  accepts "a doubly negated literal is positive at an unsigned type"
+    "(defn f [] u8 (- (- 1)))";
   rejects_check "a folded constant's conversion is still its type"
     "(defconst a u8 (i32 5))" ~needle:"expected u8, found i32";
   rejects_check "a wide decimal with nothing to say u64"