The's refusal of a dyn says what the boundary does at that type, elements that cannot become a dyn are refused against each other, two literal arms meet at the wider type, and the renamed prelude function and a second startup warning stay out of sight

bin/main.ml

@@ -362,6 +362,7 @@ let () =
              p.globals;
            List.iter
              (fun (f : Flan.Tast.fn) ->
+                if not (Flan.Check.internal_name f.name) then
                 Printf.printf "defn %s : (Fn [%s] %s)  %d slots\n" f.name
                   (String.concat " "
                      (List.map Flan.Types.to_string f.params))

lib/check.ml

@@ -5338,6 +5338,17 @@ and check_if ctx ?(tail = false) ?want loc c t e =
        no value on the missing side. `when` desugars to this. *)
     let t = branch ctx (fun () -> in_tail (fun () -> check ctx t)) in
     expect ctx loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
+  (* Two literal arms meet at the wider of their own types, as two literal
+     elements of an array do: [(if c 1 2.5)] is an f64. *)
+  | Some e
+    when want = None && lone_literal t && lone_literal e
+         && (match literal_join ctx t e with
+             | Some j -> not (Types.equal j (Types.Int Types.I32))
+             | None -> false) ->
+    let want = literal_join ctx t e in
+    let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in
+    let e = branch ctx (fun () -> in_tail (fun () -> check ctx ?want e)) in
+    mk loc t.Tast.ty (Tast.If (c, t, e))
   | Some e when want = None && lone_literal t && not (lone_literal e)
                 && not (and_sentinel e) ->
     (* A literal has no type of its own until something asks, so with no
@@ -5392,6 +5403,18 @@ and check_if ctx ?(tail = false) ?want loc c t e =
     in
     mk loc ty (Tast.If (c, t, e))
 
+(* The type two literals meet at, each at its own type — a wide integer at
+   u64, which is the only type that holds one. *)
+and literal_join ctx (a : Ast.expr) (b : Ast.expr) =
+  let own (x : Ast.expr) =
+    match x.Ast.e with
+    | Ast.UInt _ -> Some (Types.Int Types.U64)
+    | _ -> probe ctx x.Ast.loc (fun () -> (check ctx x).Tast.ty)
+  in
+  match own a, own b with
+  | Some x, Some y -> Types.join x y
+  | _ -> None
+
 (* Whether a name would reach a callee if it were called — a global function, a
    generic, or a local holding a function value. The three sources [named_call]
    itself consults, in its own order; builtins are deliberately not among them,
@@ -5725,8 +5748,12 @@ and check_arr ctx ~want loc items =
        expect ctx loc ~want
          (check_arr ctx ~want:(Some (Types.Array (n, t))) loc items)
      | None ->
-       expect ctx loc ~want
+       (match
-         (dyn_vec ctx loc (map_lr (fun i -> check ctx ~want:Types.Dyn i) items)))
+          trial ctx (fun () ->
+            dyn_vec ctx loc (map_lr (fun i -> check ctx ~want:Types.Dyn i) items))
+        with
+        | Ok v -> expect ctx loc ~want v
+        | Error d -> mixed_refusal ctx items d))
   | _ ->
   let items = map_lr (fun i -> check ctx ?want:elem_want i) items in
   let n = Int64.of_int (List.length items) in
@@ -5831,6 +5858,44 @@ and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
       (fun found c -> match found with Some _ -> found | None -> settle c)
       None candidates
 
+(* 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
+   would be about dyn, which the program never mentioned, so the elements are
+   refused against each other instead — the first one's type is what the rest
+   are checked at, and the refusal points back at it. [d] is the answer if
+   that finds nothing. *)
+and mixed_refusal : 'a. ctx -> Ast.expr list -> Loc.diag -> 'a =
+  fun ctx items d ->
+  match items with
+  | [] -> raise (Loc.Error d)
+  | first :: rest ->
+    let first = check ctx first in
+    let want = match first.Tast.ty with Types.Never -> None | t -> Some t in
+    List.iter
+      (fun (i : Ast.expr) ->
+         match check ctx ?want i with
+         | v ->
+           (match want with
+            | Some t when not (Types.fits ~expected:t ~actual:v.Tast.ty) ->
+              fail i.Ast.loc "this array's elements are %s, but this one is %s"
+                (Types.to_string t) (Types.to_string v.Tast.ty)
+            | _ -> ())
+         | exception Loc.Error e when e.Loc.dloc = i.Ast.loc && want <> None ->
+           raise
+             (Loc.Error
+                { e with
+                  Loc.notes =
+                    e.Loc.notes
+                    @ [ Loc.note first.Tast.loc
+                          (Printf.sprintf
+                             "this array's first element is %s, so every \
+                              element is"
+                             (match first.Tast.ty with
+                              | Types.Var v -> "$" ^ v
+                              | t -> Types.to_string t)) ] }))
+      rest;
+    raise (Loc.Error d)
+
 (* 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) =
@@ -5986,10 +6051,29 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
          | "" -> 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
+      (* What a dyn does at this type is the boundary's own answer, asked of
-        "the checks a value as %s and does not convert one, and this is a dyn \
+         it rather than restated: some types take one where a value is passed,
-         — a dyn becomes a %s where a %s is passed, returned or stored"
+         returned or stored, and the rest do not take one at all. *)
-        tn tn tn
+      let crosses =
+        probe ctx loc (fun () ->
+          ignore (expect ctx v.Ast.loc ~want:(Some ty) (check ctx v)))
+      in
+      match crosses with
+      | Some () ->
+        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
+      | None ->
+        (match check ctx ~want:ty v with
+         | _ ->
+           fail v.Ast.loc
+             "the checks a value as %s and does not convert one, and this is \
+              a dyn" tn
+         | exception Loc.Error d ->
+           fail v.Ast.loc
+             "the checks a value as %s and does not convert one, and this is \
+              a dyn — %s" tn d.Loc.dmsg)
   end;
   let r =
     match ty, v.Ast.e with
@@ -6230,6 +6314,26 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   let literal_arm ((a : Ast.arm), _, _) =
     match List.rev a.Ast.body with last :: _ -> lone_literal last | [] -> false
   in
+  (* Every arm a literal: they meet at the wider of their own types, as an
+     [if]'s two do. *)
+  (if !want = None && resolved <> [] && List.for_all literal_arm resolved then
+     let lasts =
+       List.map (fun ((a : Ast.arm), _, _) -> List.hd (List.rev a.Ast.body))
+         resolved
+     in
+     match lasts with
+     | first :: rest ->
+       let j =
+         List.fold_left
+           (fun acc x ->
+              Option.bind acc (fun a ->
+                Option.bind (literal_join ctx first x) (Types.join a)))
+           (literal_join ctx first first) rest
+       in
+       (match j with
+        | Some t when not (Types.equal t (Types.Int Types.I32)) -> want := Some t
+        | _ -> ())
+     | [] -> ());
   let order =
     let idx = List.mapi (fun i r -> (i, r)) resolved in
     if !want <> None then idx
@@ -7724,8 +7828,12 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           | Types.F64 -> Float.max_float
         in
         mk loc ty (Tast.Float ((if max then m else -.m), k))
-      | Types.Var _ ->
+      | Types.Var v ->
-        unconstrained ctx.env loc name ~needs:"numeric?" ty;
+        if not (declares ctx.env.tvpreds v "numeric?") then
+          Loc.failk "check/unconstrained-type-variable" a.Ast.loc
+            "%s is a limit of a numeric type, and nothing declares $%s \
+             numeric — write {:where (numeric? $%s)} at the head of the body"
+            name v v;
         int_literal loc ~want:(Some ty) ~preds:ctx.env.tvpreds 0L
       | _ ->
         fail a.Ast.loc
@@ -12820,6 +12928,20 @@ let escape_check (fn : Tast.fn) =
    twice. *)
 let prelude_alias = "prelude~"
 
+(* Off for a check whose warnings were already printed for the same source:
+   the dev program re-creating the session its launcher built and warned for. *)
+let print_warnings = ref true
+
+(* A name the renaming above made, which nobody wrote: left out of every
+   listing a person reads, and shown as whose it is where a frame has to be. *)
+let internal_name n = String.starts_with ~prefix:(prelude_alias ^ "/") n
+
+let shown_name n =
+  if internal_name n then
+    let p = String.length prelude_alias + 1 in
+    "the prelude's " ^ String.sub n p (String.length n - p)
+  else n
+
 let shadow_prelude (prelude : Ast.decl list) (decls : Ast.decl list) =
   let fn_name (d : Ast.decl) =
     match d.Ast.d with
@@ -12935,6 +13057,7 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
      reload, which is where a defn is most likely to be written. Printed in
      the shape [Loc] gives an error, so a checker in an editor parses it the
      same way. *)
+  if !print_warnings then
   List.iter
     (fun (d : Loc.diag) ->
        prerr_endline

lib/dev.ml

@@ -1448,7 +1448,10 @@ let describe t =
   ok
     [ ":fns "
       ^ Wire.strings
-          (List.map (fun (f : Tast.fn) -> f.Tast.name)
+          (List.filter_map
+             (fun (f : Tast.fn) ->
+                if Check.internal_name f.Tast.name then None
+                else Some f.Tast.name)
              t.session.Session.program.Tast.fns);
       ":globals "
       ^ Wire.strings
@@ -1560,6 +1563,7 @@ let defs t =
            Hashtbl.replace macro_locs f.Tast.name (Loc.to_string f.Tast.floc);
            None
          | None when List.mem f.Tast.name class_names -> None
+         | None when Check.internal_name f.Tast.name -> None
          | None ->
            Some
              (entry ~name:f.Tast.name ~kind:"fn" ~sign:(signature_of_fn f)
@@ -2007,7 +2011,7 @@ let backtrace_op t =
                  (List.map
                     (fun (name, loc, mine, nslots, _sig, _rsig) ->
                        Wire.list
-                         [ Wire.quote name; Wire.quote loc;
+                         [ Wire.quote (Check.shown_name name); Wire.quote loc;
                            Wire.quote (if mine then "program" else "eval");
                            string_of_int nslots ])
                     frames);
@@ -5811,7 +5815,10 @@ let merged_setup () =
        marshalling a [Session.t] through a file, which buys nothing: the source
        cannot have changed between the two, because the build that produced
        this binary is the one that exec'd it. *)
+    (* Its warnings were printed by the launcher over the same source. *)
+    Check.print_warnings := false;
     let session, _ = Session.create ~debug ~x86 ~file () in
+    Check.print_warnings := true;
     (* The program's output has to reach an editor exactly as it did when the
        daemon held the other end of a pipe. Same pipe, one process: fd 1 is
        replaced before the program starts, and the accept loop drains it —

lib/session.ml

@@ -186,6 +186,10 @@ let stale_sites ?(live = SM.empty) ?(running = false) built (p : Tast.program) :
       m acc
   in
   from ~kept:true live (from ~kept:false built [])
+  (* A caller or callee the prelude-shadowing rename made is not the
+     program's, and there is nothing in the program to recompile for it. *)
+  |> List.filter (fun s ->
+    not (Check.internal_name s.caller || Check.internal_name s.target))
   |> List.sort (fun a b ->
     match String.compare a.at.Loc.file b.at.Loc.file with
     | 0 -> Loc.before a.at b.at

test/test_acceptance.ml

@@ -6637,6 +6637,16 @@ level "1"
     cli_case "--debug and an explicit -O are refused together"
       "build ../calc-me.flan --debug -O2 -o /dev/null" ~code:2
       ~says:[ "--debug"; "-O2"; "Drop one of the two" ];
+    (* The name a shadowed prelude function is moved to is nobody's to read. *)
+    (let code, text = cli "check programs/shadow-prelude.flan" in
+     if code <> 0 || contains text "prelude~"
+        || not (contains text "defn floor-f32")
+     then begin
+       incr failures;
+       Printf.printf
+         "FAIL  check's listing leaves out the renamed prelude function\n\
+         \        got: %S (exit %d)\n" text code
+     end);
     (* A file with no main is refused by name before the link, which would
        otherwise report an undefined reference from crt1.o. *)
     let nomain = Filename.concat scratch "no-main.flan" in

test/test_flan.ml

@@ -6528,6 +6528,24 @@ let () =
   infers "the names the element type of a mixed literal" "(the [dyn] [1 2.5])" "[2 dyn]";
   infers "the with a slice type gives the literal's array type"
     "(the [f32] [1 2.5])" "[2 f32]";
+  (match checked "(defstruct P [x i32]) (defn main [] i32 (let [a [(P 1) 2]] 0))" with
+   | _ -> check "a struct beside a number is refused" false
+   | exception Loc.Error d ->
+     check "elements that cannot become a dyn are refused against the first"
+       (contains d.Loc.dmsg "expected P, found the integer literal 2"
+        && List.exists
+             (fun (n : Loc.note) ->
+                contains n.Loc.nmsg "this array's first element is P")
+             d.Loc.notes));
+  (match checked "(defn g [x $t] i32 (let [a [x 1]] 0))" with
+   | _ -> check "a type variable beside a literal is refused" false
+   | exception Loc.Error d ->
+     check "a type variable beside a literal names the bound and spells $t"
+       (contains d.Loc.dmsg "{:where (numeric? $t)}"
+        && List.exists
+             (fun (n : Loc.note) ->
+                contains n.Loc.nmsg "this array's first element is $t")
+             d.Loc.notes));
   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";
@@ -6535,8 +6553,16 @@ let () =
   (* ── (max-of T) and (min-of T) ──────────────────────────────────── *)
   infers "max-of carries its type" "(max-of u16)" "u16";
   infers "min-of at a float" "(min-of f32)" "f32";
-  rejects_check "max-of at an unbounded type variable names the bound"
+  (match checked "(defn f [x $t] $t (max-of $t))" with
-    "(defn f [x $t] $t (max-of $t))" ~needle:"{:where (numeric? $t)}";
+   | _ -> check "max-of 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"
+       (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"
     "(defn f [x $t] $t {:where (integer? $t)} (max-of t))";
   rejects_check "max-of at a type that is not a number names the bound"
@@ -6553,9 +6579,13 @@ let () =
   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"
+  rejects_check "the refuses a dyn at a type a dyn does not become"
     "(defn f [x dyn] string (the string x))"
-    ~needle:"a dyn becomes a string where a string is passed";
+    ~needle:"dyn — string does not cross into a written type yet";
+  rejects_check "the refuses a dyn at bool, which a dyn becomes where passed"
+    "(defn f [x dyn] bool (the bool x))"
+    ~needle:"a dyn becomes a bool where a bool is passed";
+  accepts "the bool a dyn becomes where it is returned" "(defn f [x dyn] bool x)";
   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)";