diff --git a/lib/check.ml b/lib/check.ml index be99fe93..49013241 100644 --- a/lib/check.ml +++ b/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 diff --git a/test/test_flan.ml b/test/test_flan.ml index 5e673062..33c0209f 100644 --- a/test/test_flan.ml +++ b/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"