An if's arms and a _ function's exits meet at one join in any order, a return inside the last form counts where it is written, and a constant computed by a _ function is refused as with a written type

TODO.org

@@ -43,6 +43,11 @@ The body's own type, never a call site's; parameters are never inferred, and a
 cycle among =_= functions is refused by name unless it gives =()=. Rules out
 use-directed inference.
 
+** DONE An if's arms meet at one join, whichever is written first
+CLOSED: [2026-09-25]
+Lossless widening, const, and dyn beside anything, the same for =_= exits.
+Rules out the then arm deciding the type the else arm is checked at.
+
 ** DONE def, defonce and defconst are the three forms
 CLOSED: [2026-09-20]
 =def= is Common Lisp's =defparameter= and re-initialises on every run; =defonce=

lib/check.ml

@@ -4161,6 +4161,24 @@ let hash_ty = Types.Int Types.U64
    address, so no type written anywhere is ever mistaken for it. What each
    [return] in that body gives is pushed on [infer_seen]. *)
 let infer_ret = Types.Named "_"
+
+(* The type two arms meet at — an [if]'s two, or two exits of a [_] body —
+   the same whichever comes first: the wider where one widens into the other
+   without loss ([Types.join]), the read-only where they differ only in const,
+   and dyn where either is dyn, the other boxed. [None] is a refusal. *)
+let arm_join (a : Types.t) (b : Types.t) =
+  if Types.equal a Types.Never then Some b
+  else if Types.equal b Types.Never then Some a
+  else
+    match Types.join a b with
+    | Some j -> Some j
+    | None ->
+      match Types.const_join a b with
+      | Some j -> Some j
+      | None ->
+        (match a, b with
+         | Types.Dyn, _ | _, Types.Dyn -> Some Types.Dyn
+         | _ -> None)
 let infer_seen : (Types.t * Loc.t * bool) list ref = ref []
 (* What a refused subexpression stands as while recovering. [Zero] of [Never]
    is a value nothing else builds, so it is recognisable; see [check]. *)
@@ -7009,6 +7027,34 @@ and check_if_once ctx ~tail ?want loc c t e =
        bool as before, for that path's messages. A chain whose arms all fit
        is checked once; a refused one re-checks each level below the refusal
        once more, the square of its depth. *)
+    (* The else arm on its own terms, when nothing is wanted: the two arms
+       meet at [arm_join], so the order they are written in decides nothing.
+       Kept when it has the then arm's type, or when the then arm is the one
+       that moves; when the else arm moves it is checked again below at the
+       then arm's type, so its literals are typed there as before. *)
+    let joined =
+      if want <> None || free_join || t.Tast.ty = Types.Never
+         || t.Tast.ty = Types.Bool || and_sentinel e || lone_literal e
+      then None
+      else
+        (* A trial not kept leaves nothing: [trial] puts the context back
+           when it raises, and what it lifted goes here. *)
+        let lifted = ctx.env.lifted in
+        match
+          trial ctx (fun () ->
+              let v = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in
+              match arm_join t.Tast.ty v.Tast.ty with
+              | Some j when Types.equal v.Tast.ty j -> v
+              | _ -> raise (Loc.Error (Loc.diag v.Tast.loc "not kept")))
+        with
+        | Ok v -> Some (v.Tast.ty, v)
+        | Error _ -> ctx.env.lifted <- lifted; None
+    in
+    match joined with
+    | Some (j, v) ->
+      let t = expect ctx t.Tast.loc ~want:(Some j) t in
+      mk loc j (Tast.If (c, t, v))
+    | None ->
     let own_else =
       if want = None && t.Tast.ty = Types.Bool then
         match
@@ -13628,6 +13674,32 @@ let check_parents env =
        | None -> ())
     env.parents
 
+(* Untyped constants to a fixpoint, and for the same reason: one untyped
+   constant may be defined in terms of another declared after it. A constant
+   that still does not check once no progress is left has a real error, so
+   the last round is run without swallowing it. *)
+let settle_consts env consts =
+  let infer (_, v) = (check (invented_ctx env Types.Unit) v).Tast.ty in
+  let pending = ref consts in
+  let rec settle () =
+    let left =
+      List.filter
+        (fun ((n, _) as c) ->
+           match speculate env (fun () -> infer c) with
+           | ty -> Hashtbl.replace env.globals n (ty, true); false
+           | exception Loc.Error _ -> true)
+        !pending
+    in
+    let progressed = List.length left < List.length !pending in
+    pending := left;
+    if progressed && left <> [] then settle ()
+  in
+  settle ();
+  List.iter (fun c -> ignore (infer c)) !pending
+
+(* Set by [collect], read by [build_program] once [infer_returns] ran. *)
+let consts_after_infer : (string * Ast.expr) list ref = ref []
+
 let collect env (decls : Ast.decl list) =
   (* One pass over every declaration kind before any of the others, because
      the tables below are per-kind — structs, data types, aliases, enums, functions
@@ -14155,27 +14227,27 @@ let collect env (decls : Ast.decl list) =
            "internal: a method of %s reached the checker unexpanded — \
             Classes.expand did not run over this declaration list" m.Ast.mgen)
     decls;
-  (* Also to a fixpoint, and for the same reason: one untyped constant may be
+  (* The untyped constants ([settle_consts]). One that calls a [_] function
-     defined in terms of another declared after it. A constant that still does
+     waits for [infer_returns], which needs every signature this pass
-     not check once no progress is left has a real error, so the last round is
+     registers; it is settled after that, and its refusal is the one a
-     run without swallowing it. *)
+     written return type would get. *)
-  let infer (_, v) = (check (invented_ctx env Types.Unit) v).Tast.ty in
+  let inferred_names =
-  let pending = ref (List.rev !untyped) in
+    List.filter_map
-  let rec settle () =
+      (fun (d : Ast.decl) ->
-    let left =
+         match d.Ast.d with
-      List.filter
+         | Ast.Defn { Ast.name; ret = Some { Ast.t = Ast.Tinfer; _ }; _ } ->
-        (fun ((n, _) as c) ->
+           Some name
-           match speculate env (fun () -> infer c) with
+         | _ -> None)
-           | ty -> Hashtbl.replace env.globals n (ty, true); false
+      decls
-           | exception Loc.Error _ -> true)
-        !pending
-    in
-    let progressed = List.length left < List.length !pending in
-    pending := left;
-    if progressed && left <> [] then settle ()
   in
-  settle ();
+  let waits (_, v) =
-  List.iter (fun c -> ignore (infer c)) !pending;
+    let acc = ref [] in
+    Load.expr_uses acc v;
+    List.exists (fun (n, _) -> List.mem n inferred_names) !acc
+  in
+  let late, now = List.partition waits (List.rev !untyped) in
+  consts_after_infer := late;
+  settle_consts env now;
   check_parents env;
   (* The paired declarations, handed back so that pass two checks the bodies of
      the same functions whose signatures this pass registered. Pairing needs the
@@ -14539,14 +14611,13 @@ and check_generic env (fn : Ast.fn) =
    is the cycle of one. *)
 
 (* The type one body gives, and the form that decided it. The exits — the
-   last form and every [return], less what never arrives — combine the way
+   last form and every [return], less what never arrives — meet at
-   an [if]'s arms do ([check_if_once]): the first one that is not a lone
+   [arm_join], the function an [if]'s arms meet at, in any order: the typed
-   literal decides and the literals take its type, a bool meets a dyn at
+   ones decide and the lone literals take their type; literals alone meet at
-   dyn, and literals alone meet at the wider of their own types. The body is
+   the wider of their own types. The body is then checked against that type
-   then checked against that type exactly as a written one would be, so
+   exactly as a written one would be, so whatever [if] refuses between its
-   whatever [if] refuses between its arms is refused between exits, in the
+   arms is refused between exits, in the same words. None gives (); no value
-   same words. None gives (); no value beside a value is refused, since ()
+   beside a value is refused, since () does not take a value's place. *)
-   does not take a value's place. *)
 and read_return env (fn : Ast.fn) params =
   (* One check of the body against [ret], thrown away: what it lifted goes,
      and so do the copies it asked for if it failed, as [tolerant] does. *)
@@ -14610,20 +14681,30 @@ and read_return env (fn : Ast.fn) params =
     when not (List.exists (fun (u, _, _) -> not (Types.equal t u)) rest) ->
     (t, l)
   | (t0, l0, _) :: _ ->
-    let decided =
+    (* Where no join exists the first typed exit's type is the one checked
-      match List.filter (fun (_, _, lit) -> not lit) arrive with
+       against, so the refusal is the one [if] gives its else arm. *)
-      | (Types.Bool, l, _) :: others
+    let meet = function
-        when List.exists (fun (u, _, _) -> Types.equal u Types.Dyn) others ->
+      | [] -> None
-        (Types.Dyn, l)
+      | ((t, l, _) :: _) as xs ->
-      | (t, l, _) :: _ -> (t, l)
+        let j =
-      | [] ->
-        let joined =
           List.fold_left
-            (fun acc (u, _, _) ->
+            (fun acc (u, _, _) -> Option.bind acc (fun a -> arm_join a u))
-               match acc with Some a -> Types.join a u | None -> None)
+            (Some t) xs
-            (Some t0) arrive
         in
-        (Option.value joined ~default:t0, l0)
+        let at =
+          match j with
+          | Some j ->
+            (match List.find_opt (fun (u, _, _) -> Types.equal u j) xs with
+             | Some (_, l', _) -> l'
+             | None -> l)
+          | None -> l
+        in
+        Some (Option.value j ~default:t, at)
+    in
+    let decided =
+      match meet (List.filter (fun (_, _, lit) -> not lit) arrive) with
+      | Some d -> d
+      | None -> Option.value (meet arrive) ~default:(t0, l0)
     in
     ignore (attempt (fst decided));
     decided
@@ -15992,6 +16073,9 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) :
   check_finite env;
   check_union_members env;
   infer_returns ~keep_going ?tolerate ?previous env decls;
+  (let late = !consts_after_infer in
+   consts_after_infer := [];
+   settle_consts env late);
   let s = Loc.sink ~on:keep_going in
   (match env.deferred with
    | Some ds -> s.Loc.found <- ds; env.deferred <- None

spec-syntax.md

@@ -55,9 +55,10 @@ warns about; the new syntax must not inherit it.
 **The return type is inferred when omitted.** Body-local only, as
 `docs/SPIKE-INFERENCE.md` ("The cheap first step" and "Verdict") scopes it:
 - the return type is the body's type; a `dyn` body gives `dyn`; the exits (the
-  last form and each `return`) combine exactly as an `if`'s arms do, so a
+  last form and each `return`) meet exactly as an `if`'s arms do, through one
-  literal takes the other exits' type and what `if` refuses is refused; no
+  join and in any order: lossless widening, the read-only side of a const
-  value gives `()`.
+  difference, `dyn` beside anything; a literal takes the other exits' type
+  and what `if` refuses is refused; no value gives `()`.
 - it reads only the function's own body, never a call site.
 - a self-recursive or mutually recursive function must write its return type.
   Refuse by name, naming the whole cycle. The corpus has 17 self-recursive

test/test_flan.ml

@@ -7531,6 +7531,30 @@ let () =
      ("(defn f [d dyn c bool] _ (when c (return d)) 1)" ^ main) "f" "f [dyn bool] dyn";
    reads_as "a literal before the typed exit still takes its type"
      ("(defn f [x i16] _ (when (< x 0) (return x)) 0)" ^ main) "f" "f [i16] i16";
+   (* Arms and exits meet at one join, whichever comes first. *)
+   List.iter
+     (fun (what, sg, body, want) ->
+        reads_as what ("(defn f " ^ sg ^ " _ " ^ body ^ ")" ^ main) "f" want)
+     [ ("if i32 then i64", "[c bool x i32 y i64]", "(if c x y)", "f [bool i32 i64] i64");
+       ("if i64 then i32", "[c bool x i32 y i64]", "(if c y x)", "f [bool i32 i64] i64");
+       ("if f32 then f64", "[c bool x f32 y f64]", "(if c x y)", "f [bool f32 f64] f64");
+       ("if u8 then i32", "[c bool x u8 y i32]", "(if c x y)", "f [bool u8 i32] i32");
+       ("if dyn then i8", "[c bool x i8 d dyn]", "(if c d x)", "f [bool i8 dyn] dyn");
+       ("if i8 then dyn", "[c bool x i8 d dyn]", "(if c x d)", "f [bool i8 dyn] dyn");
+       ("if i64 then dyn", "[c bool x i64 d dyn]", "(if c x d)", "f [bool i64 dyn] dyn");
+       ("if i8 then a literal", "[c bool x i8]", "(if c x 1)", "f [bool i8] i8");
+       ("exits i32 then i64", "[c bool x i32 y i64]", "(when c (return x)) y", "f [bool i32 i64] i64");
+       ("exits i64 then i32", "[c bool x i32 y i64]", "(when c (return y)) x", "f [bool i32 i64] i64");
+       ("a return inside the last form, in source order", "[c bool x i64 y i32]",
+        "(if c x (return y))", "f [bool i64 i32] i64");
+       ("exits writable then read-only slice", "[c bool a [u8] b [const u8]]",
+        "(when c (return a)) b", "f [bool [u8] [const u8]] [const u8]");
+       ("exits read-only then writable slice", "[c bool a [u8] b [const u8]]",
+        "(when c (return b)) a", "f [bool [u8] [const u8]] [const u8]");
+       ("exits writable then read-only pointer", "[c bool a (Ptr i32) b (Ptr const i32)]",
+        "(when c (return a)) b", "f [bool (Ptr i32) (Ptr const i32)] (Ptr const i32)");
+       ("exits dyn then a literal", "[c bool d dyn]", "(when c (return d)) 1", "f [bool dyn] dyn");
+       ("exits nil then a literal", "[c bool]", "(when c (return nil)) 1", "f [bool] dyn") ];
    reads_as "an f32 exit and a float literal"
      ("(defn f [x f32] _ (when (< x 0.0) (return x)) 0.0)" ^ main) "f" "f [f32] f32";
    reads_as "a function that calls itself and gives nothing is ()"
@@ -7608,15 +7632,24 @@ let () =
   rejects_check "no value on one exit and a value on the other"
     ~needle:"u gives no value here and i32 on another path"
     "(defn u [c bool] _ (when c (return)) 1)\n(defn main [] ())";
-  rejects_check "an i32 exit and an i64 exit, as if refuses them"
+  rejects_check "an i32 exit and a u32 exit, which neither widens into"
-    ~needle:"expected i32, found i64"
+    ~needle:"expected i32, found u32"
-    "(defn f [x i32 y i64 c bool] _ (when c (return x)) y)\n(defn main [] ())";
+    "(defn f [x i32 y u32 c bool] _ (when c (return x)) y)\n(defn main [] ())";
+  rejects_check "a u32 exit and an i32 exit, the other order"
+    ~needle:"expected u32, found i32"
+    "(defn f [x i32 y u32 c bool] _ (when c (return y)) x)\n(defn main [] ())";
+  rejects_check "an if over i32 and u32, either order"
+    ~needle:"expected i32, found u32"
+    "(defn f [x i32 y u32 c bool] i32 (let [v (if c x y)] 0))\n(defn main [] ())";
   rejects_check "a literal that does not fit the typed exit"
     ~needle:"300 does not fit in u8"
     "(defn f [c bool] _ (when c (return 300)) (u8 2))\n(defn main [] ())";
   rejects_check "a string exit and a number exit"
     ~needle:"expected string, found the integer literal 1"
     "(defn f [c bool] _ (when c (return \"s\")) 1)\n(defn main [] ())";
+  rejects_check "a constant computed by a _ function, as by a written one"
+    ~needle:"a constant's value must be a compile-time constant — the constant K is computed"
+    "(defn five [] _ 5)\n(defconst K (five))\n(defn main [] i32 0)";
   rejects_check "some under an inferred return"
     ~needle:"Write the return type: (Option T)"
     "(defn f [o (Option i32)] _ (+ 1 (some o)))\n(defn main [] ())";