A function's return type can be left to inference, with _ in .flan or no arrow in .fln, and if, match and return paths join their types the same way in either order

TODO.org

@@ -56,6 +56,18 @@ A =defn= writes its return type, and unit is =()=. The parse ambiguity a missing
 slot would open is real, and =()= does not collapse into =dyn=. Rules out the
 optional return slot.
 
+** DONE A return type is read off the body only when the slot says =_=
+CLOSED: [2026-09-25]
+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 or match's arms meet at one join, whichever is written first
+CLOSED: [2026-09-25]
+Each arm is asked the other's type first; only a refusal meets at the join
+(lossless widening, const, dyn beside a dyn value), the same for =_= exits.
+Rules out the first arm's type refusing a wider second arm.
+
 ** 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=

emacs/flan.el

@@ -2501,6 +2501,10 @@ of the tenth name tells you neither how many there were nor which."
     (concat
      (format "this call to %s was compiled for %s, and %s is defined as %s.  "
              callee compiled callee (plist-get site :current))
+     ;; Set when CALLEE's return type is read off its body, which nobody
+     ;; wrote, so the line that changed it is named.
+     (when-let* ((cause (plist-get site :cause)))
+       (concat cause ".  "))
      (if (plist-get site :running)
          ;; `main' is the one caller no evaluation can reach: the program is
          ;; inside the body it started with and never calls it again.

lib/ast.ml

@@ -24,6 +24,11 @@ and texpr_kind =
      them identically — the difference is a fact about the value, and it is
      [Check.resolve] that turns it into one. *)
   | Tfn    of bool * texpr list * texpr
+  (* [_]: the type is read off the body. Only a [defn]'s return slot has a
+     body to read it off, and [Check.resolve] refuses it everywhere else. A
+     constructor rather than [ret = None] because [None] already means ()
+     for [declare] and the shim. *)
+  | Tinfer
   (* An integer written as a generic struct's argument, the 8 in
      (Small 8 i32). Parsed only there; it is not a type anywhere else. *)
   | Tlen   of int64

lib/cimport.ml

@@ -417,6 +417,7 @@ let rec ty_source (t : Ast.texpr) =
   | Ast.Tfn (env, ps, r) ->
     Printf.sprintf "(%s [%s] %s)" (if env then "Fn" else "CFn")
       (String.concat " " (List.map ty_source ps)) (ty_source r)
+  | Ast.Tinfer -> "_"
 
 let tname n = ty (Ast.Tname n)
 

lib/dev.ml

@@ -1022,12 +1022,15 @@ let stale_field (ss : Session.stale list) =
           (List.map
              (fun (x : Session.stale) ->
                 Printf.sprintf
-                  "(:loc %s :caller %s :callee %s :compiled %s :current %s%s)"
+                  "(:loc %s :caller %s :callee %s :compiled %s :current %s%s%s)"
                   (Wire.quote (Loc.to_string x.Session.at))
                   (Wire.quote x.Session.caller) (Wire.quote x.Session.target)
                   (Wire.quote x.Session.compiled)
                   (Wire.quote x.Session.current)
-                  (if x.Session.running then " :running t" else ""))
+                  (if x.Session.running then " :running t" else "")
+                  (match x.Session.cause with
+                   | Some c -> " :cause " ^ Wire.quote c
+                   | None -> ""))
              ss) ]
 
 (* Every refusal a check found, one plist each: beside what a load installed,

lib/indent_printer.ml

@@ -855,8 +855,10 @@ and sugar n (f : Form.t) : string list option =
          | _ -> ("", body)
        in
        let head =
-         i ^ (if d = "defn" then "fn " else "fn- ") ^ name ^ "(" ^ pt ^ ") -> "
+         i ^ (if d = "defn" then "fn " else "fn- ") ^ name ^ "(" ^ pt ^ ")"
-         ^ ty ret ^ where_
+         (* [_] is what the reader makes of no arrow at all. *)
+         ^ (match ret.v with Form.Sym "_" -> "" | _ -> " -> " ^ ty ret)
+         ^ where_
        in
        (match body with
         | [] -> Some [ head ]

lib/indent_reader.ml

@@ -1195,16 +1195,12 @@ and header (s : st) w : Form.t =
     let lp = glued_lp p ~what:"the parameters, in parentheses glued to the name" in
     let ps = params p lp in
     let rp = last p in
-    let ret =
+    (* No arrow reads the return type off the body: the paren syntax's [_]
+       (spec-syntax.md §3.5). *)
+    let ret, ret_text =
       match (peek p).tok with
-      | NAME "->" -> ignore (advance p); ty p
+      | NAME "->" -> ignore (advance p); let r = ty p in (r, text_of r)
-      | _ ->
+      | _ -> (sym rp.loc "_", ")")
-        let n = match name.v with Form.Sym n -> n | _ -> "" in
-        failk "return-type" rp.loc
-          "fn %s has no return type after its parameters, and a .fln \
-           function states one for now. Write it after an arrow: fn %s(...) \
-           -> i32, or -> dyn, or -> () when it returns nothing"
-          n n
     in
     let where_clause =
       match (peek p).tok with
@@ -1253,7 +1249,7 @@ and header (s : st) w : Form.t =
       | NEWLINE ->
         ignore (advance p);
         if (peek p).tok = INDENT then block s ~after:"fn" else []
-      | _ -> stray p ~after:(text_of ret)
+      | _ -> stray p ~after:ret_text
     in
     named (if w = "fn" then "defn" else "defn-")
       (name :: Form.make (Form.Vec ps) lp.loc :: ret :: (where_clause @ body))

lib/load.ml

@@ -221,6 +221,7 @@ let rec rename_texpr owned alias (t : Ast.texpr) : Ast.texpr =
     | Ast.Tfn (env, ps, r) ->
       Ast.Tfn (env, List.map (rename_texpr owned alias) ps,
                rename_texpr owned alias r)
+    | Ast.Tinfer -> Ast.Tinfer
   in
   { t with Ast.t = k }
 
@@ -807,6 +808,7 @@ let rec texpr_uses acc (t : Ast.texpr) =
     acc := (n, t.Ast.tloc) :: !acc;
     List.iter (texpr_uses acc) args
   | Ast.Tfn (_, ps, r) -> List.iter (texpr_uses acc) ps; texpr_uses acc r
+  | Ast.Tinfer -> ()
   | Ast.Tlen _ -> ()
 
 let rec expr_uses acc (e : Ast.expr) =

lib/parse.ml

@@ -124,6 +124,7 @@ let rec texpr (f : Form.t) : Ast.texpr =
      point: it is what [()] parses to, and what the resolver, the shim and the
      emitter go on speaking. *)
   | Sym "Unit" -> fail f "unit is written (), not Unit"
+  | Sym "_" -> mk Ast.Tinfer
   | Sym s -> mk (Ast.Tname s)
   (* [const T] is matched before [n T], which it would otherwise be: [const]
      is a reserved name exactly so that no constant can be called that and
@@ -1645,12 +1646,14 @@ let rec decl (f : Form.t) : Ast.decl =
                 leads, and the slot's own clause follows it. *)
              Loc.failk "parse/return-type-expected" inner
                "%s — this is the return type, which every defn states, and a \
-                function that returns nothing writes ()" msg
+                function that returns nothing writes (), or _ to read it off \
+                the body" msg
            else
              Loc.failk "parse/return-type-expected" ret.Form.loc
                ~notes:[ Loc.note inner msg ]
                "the return type goes here, and this is %s — every defn states \
-                one, and a function that returns nothing writes ()"
+                one, and a function that returns nothing writes (), or _ to \
+                read it off the body"
                (Form.to_string ret)
        in
        let fwhere, body = constraints body in
@@ -1660,7 +1663,8 @@ let rec decl (f : Form.t) : Ast.decl =
      | _ ->
        fail f
          "%s is (%s name [param Type ...] ReturnType body ...). The return \
-          type is not optional; a function that returns nothing writes ()"
+          type is not optional; a function that returns nothing writes (), \
+          and _ reads it off the body"
          head head)
 
   (* ── The dyn side's classes and generic functions ──────────────────
@@ -1719,6 +1723,14 @@ let rec decl (f : Form.t) : Ast.decl =
     (match args with
      | n :: { v = Vec ps; _ } :: ret :: body
        when if generic then body = [] else body <> [] ->
+       (* Every method answers through this one signature, so no single
+          body can say what it returns. *)
+       if ret.v = Sym "_" then
+         Loc.failk "parse/infer-generic" ret.loc
+           "_ asks for the return type to be read off a body, and %s's \
+            methods each have their own. Write the type every method \
+            returns, or dyn"
+           which;
        mk ((if generic then (fun fn -> Ast.Defgeneric fn)
             else fun fn -> Ast.Defmulti fn)
              { Ast.name = dname n; params = dyn_params which ps; praw = None;

lib/session.ml

@@ -37,7 +37,7 @@
    the signature that function had when this body was compiled, and where the
    call is written. A function value taken by name is a site too — the dev
    build checks the signature where the address is taken. *)
-type site = { callee : string; csig : string; sloc : Loc.t }
+type site = { callee : string; csig : string; cret : Types.t; sloc : Loc.t }
 
 (* What the session knows about one compiled body: the declaration it belongs
    to — itself, the function a clause was lifted out of, or the generic a copy
@@ -58,6 +58,9 @@ type stale = {
      again, so compiling [main] again cannot reach it. Changing the callee
      back or re-running the program does. *)
   running  : bool;
+  (* When [target]'s return type is read off its body and that is what
+     changed: which way, and the line that decided it. *)
+  cause    : string option;
 }
 
 type t = {
@@ -119,13 +122,15 @@ let sites_of (p : Tast.program) (fn : Tast.fn) =
   let sigs = Hashtbl.create 64 in
   List.iter
     (fun (f : Tast.fn) ->
-       Hashtbl.replace sigs f.Tast.name (Emit.sig_text f.Tast.params f.Tast.ret))
+       Hashtbl.replace sigs f.Tast.name
+         (Emit.sig_text f.Tast.params f.Tast.ret, f.Tast.ret))
     p.Tast.fns;
   let found = ref [] in
   let see (e : Tast.expr) =
     let at m =
       match Hashtbl.find_opt sigs m with
-      | Some csig -> found := { callee = m; csig; sloc = e.Tast.loc } :: !found
+      | Some (csig, cret) ->
+        found := { callee = m; csig; cret; sloc = e.Tast.loc } :: !found
       | None -> ()
     in
     match e.Tast.e with
@@ -162,13 +167,26 @@ let record_built env (p : Tast.program) (fns : Tast.fn list) m =
    it was compiled for, in source order. A callee [p] does not have is
    skipped rather than reported: nothing could have been installed under it
    since, so the cell still holds what the site was compiled against. *)
-let stale_sites ?(live = SM.empty) ?(running = false) built (p : Tast.program) :
+let stale_sites ?(live = SM.empty) ?(running = false)
-  stale list =
+    ?(inferred = fun _ -> None) built (p : Tast.program) : stale list =
-  let sigs = Hashtbl.create 64 in
+  let sigs = Hashtbl.create 64 and rets = Hashtbl.create 64 in
   List.iter
     (fun (f : Tast.fn) ->
-       Hashtbl.replace sigs f.Tast.name (Emit.sig_text f.Tast.params f.Tast.ret))
+       Hashtbl.replace sigs f.Tast.name (Emit.sig_text f.Tast.params f.Tast.ret);
+       Hashtbl.replace rets f.Tast.name f.Tast.ret)
     p.Tast.fns;
+  (* Nobody wrote an inferred return type, so a change to one is said in
+     terms of the line that made it. *)
+  let cause (st : site) =
+    match inferred st.callee, Hashtbl.find_opt rets st.callee with
+    | Some (l : Loc.t), Some now when not (Types.equal now st.cret) ->
+      Some
+        (Printf.sprintf "%s now returns %s, not %s, because of line %d%s"
+           st.callee (Types.to_string now) (Types.to_string st.cret) l.Loc.line
+           (if String.equal l.Loc.file st.sloc.Loc.file then ""
+            else " of " ^ Filename.basename l.Loc.file))
+    | _ -> None
+  in
   (* Named by the declaration a body belongs to: a clause lifted out of
      [step] is [step]'s call, and a generic's copy is the generic's. *)
   let from ~kept m acc =
@@ -180,7 +198,8 @@ let stale_sites ?(live = SM.empty) ?(running = false) built (p : Tast.program) :
               match Hashtbl.find_opt sigs st.callee with
               | Some now when not (String.equal now st.csig) ->
                 { caller = b.owner; target = st.callee; compiled = st.csig;
-                  current = now; at = st.sloc; running } :: acc
+                  current = now; at = st.sloc; running; cause = cause st }
+                :: acc
               | _ -> acc)
            acc b.sites)
       m acc
@@ -1032,7 +1051,19 @@ let eval ?(origin = "<eval>") ?base ?forms ?pause ?(step = false) ?(running = tr
      refused subexpression (see [Check.check]). One error is still raised as
      [Loc.Error], which is what every caller of one form expects. *)
   let program, env, tolerated =
-    match Check.program_tolerant ~keep_going:true ~tolerate:stale_owner decls with
+    (* A tolerated body whose return type is read off it keeps the
+       signature the process has for it. *)
+    let previous n =
+      List.find_map
+        (fun (f : Tast.fn) ->
+           if String.equal f.Tast.name n then Some (f.Tast.params, f.Tast.ret)
+           else None)
+        t.program.Tast.fns
+    in
+    match
+      Check.program_tolerant ~keep_going:true ~tolerate:stale_owner ~previous
+        decls
+    with
     | r -> r
     | exception Loc.Errors [ d ] -> raise (Loc.Error d)
   in
@@ -1407,7 +1438,9 @@ let eval ?(origin = "<eval>") ?base ?forms ?pause ?(step = false) ?(running = tr
   { ir; x86 = t.x86; names; fns;
     installs =
       fns <> [] || allocates || consts <> [] || run_thunk <> None;
-    stale = stale_sites ~live ~running built program }
+    stale =
+      stale_sites ~live ~running ~inferred:(Check.inferred_cause env) built
+        program }
 
 (* ── Evaluating an expression ──────────────────────────────────────── *)
 

lib/shim.ml

@@ -219,7 +219,7 @@ let rec template_params ?(fuel = 16) env n =
             kinds args
         else List.iter walk args
       | Ast.Tfn (_, ps, r) -> List.iter walk ps; walk r
-      | Ast.Tlen _ -> ()
+      | Ast.Tlen _ | Ast.Tinfer -> ()
     in
     List.iter (fun (f : Ast.field) -> walk f.Ast.fty) fs;
     List.rev !acc
@@ -228,6 +228,7 @@ let rec source (t : Ast.texpr) =
   match t.Ast.t with
   | Ast.Tname n -> n
   | Ast.Tlen n -> Int64.to_string n
+  | Ast.Tinfer -> "_"
   | Ast.Tapp (n, args) ->
     Printf.sprintf "(%s %s)" n (String.concat " " (List.map source args))
   | Ast.Tslice (c, e) -> Printf.sprintf "[%s%s]" (if c then "const " else "") (source e)
@@ -252,7 +253,7 @@ let copy env ~loc n (args : Ast.texpr list) =
         match t.Ast.t with
         | Ast.Tname m when List.mem_assoc (bare m) sub ->
           (List.assoc (bare m) sub).Ast.t
-        | Ast.Tname _ | Ast.Tlen _ -> t.Ast.t
+        | Ast.Tname _ | Ast.Tlen _ | Ast.Tinfer -> t.Ast.t
         | Ast.Tslice (c, e) -> Ast.Tslice (c, go e)
         | Ast.Tarray (Ast.Lname m, e) when List.mem_assoc (bare m) sub ->
           let l =
@@ -362,6 +363,8 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
       what
   | Ast.Tfn _ ->
     fail loc "%s is a function type, and a C callback is not implemented" what
+  | Ast.Tinfer ->
+    fail loc "%s is _, and a C signature writes every type out" what
   | Ast.Tapp (n, _) ->
     fail loc "%s is %s, which is not a type this shim generator knows" what n
   | Ast.Tlen n -> fail loc "%s is %Ld, which is not a type" what n

lib/tast.ml

@@ -471,6 +471,44 @@ let is_watch_guard (c : expr) =
   | Prim (Ne, [ { e = Prim (Rt s, _); _ }; _ ]) -> String.equal s watch_begin
   | _ -> false
 
+(* The value positions of an expression: the forms whose value is the
+   expression's value — a block's last form, both arms of an [if], every
+   arm of a [match] and of a [restart-case]. Everything that asks "what does
+   this expression answer with" walks these, so a form that carries a value
+   through from one of its parts is added here once. [map_tails ~ty] rebuilds
+   the expression with each value position replaced by [f] of it and every
+   form on the way given [ty]; a position that never arrives (its type
+   Never) is left alone unless [all]. A form [stop] answers yes for is taken
+   as a value position whole, not looked into. *)
+let rec map_tails ?(all = false) ?(stop = fun _ -> false) ?ty (f : expr -> expr)
+    (e : expr) : expr =
+  let go = map_tails ~all ~stop ?ty f in
+  let last es =
+    match List.rev es with
+    | x :: rest -> List.rev (go x :: rest)
+    | [] -> es
+  in
+  let retype k =
+    let t = match ty with Some t -> t | None -> e.ty in
+    { e with e = k; ty = (if e.ty = Types.Never then e.ty else t) }
+  in
+  if stop e then f e else
+  match e.e with
+  | Do es -> retype (Do (last es))
+  | Let (bs, es) -> retype (Let (bs, last es))
+  | WithAlloc (a, es) -> retype (WithAlloc (a, last es))
+  | Handled (hs, es) -> retype (Handled (hs, last es))
+  | If (c, a, b) -> retype (If (c, go a, go b))
+  | Match (sc, arms) ->
+    retype (Match (sc, List.map (fun a -> { a with abody = last a.abody }) arms))
+  | RestartCase (cs, body) ->
+    retype
+      (RestartCase (List.map (fun c -> { c with rbody = last c.rbody }) cs, go body))
+  | _ -> if e.ty = Types.Never && not all then e else f e
+
+let iter_tails ?stop (f : expr -> unit) (e : expr) =
+  ignore (map_tails ~all:true ?stop (fun x -> f x; x) e)
+
 let rec walk (f : expr -> unit) (e : expr) =
   f e;
   let go = walk f in

spec-syntax.md

@@ -54,8 +54,12 @@ 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`; `return`s of
+- the return type is the body's type; a `dyn` body gives `dyn`; the exits (the
-  different types give `dyn`; no value gives `()`.
+  last form and each `return`) meet exactly as an `if`'s or `match`'s arms do,
+  in any order: each is asked the others' type first, so a literal, `nil` or
+  arithmetic takes it; only arms that are refused that way meet at the join
+  (lossless widening, the read-only side of a const difference, `dyn` beside
+  a genuinely dyn value); 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
@@ -264,8 +268,9 @@ Each item: the proposal, then the reason in one line.
 
 - `fn name(a: i32, b) -> R` plus a block; `fn name(a) = expr` for one
   expression. Reads `(defn name [a i32 b dyn] R …)`. A `{:where …}` constraint
-  becomes `where ordered?($t)` after the return type. **Built**, with `-> R`
+  becomes `where ordered?($t)` after the return type. **Built**; with no
-  required until step 6; several predicates are `where p, q`.
+  `-> R` the return is `_`, read off the body. Several predicates are
+  `where p, q`.
 - `def x = v`, `def x: T = v`, `once x: T`, `once x = v`, `const n = 3`,
   `def scratch: [4 u8] = uninit`. **Built.** `def x = v` and `once x = v` read
   with `dyn`; `const n = 3` reads `(defconst n 3)`, its type inferred as today.
@@ -347,8 +352,7 @@ Each step lands on its own, with `dune test --root .` green.
    indent stack, then a parser to `Form.t`. Start with what
    `sand.flan` and `algorithms.flan` need, then the fallback, then the sugar
    in section 2 in order of corpus frequency (`set`, `let`, `+`, `at`, `=`,
-   `if`, `dotimes`, …). Until step 6 lands, a `.fln` function must write
+   `if`, `dotimes`, …).
-   `-> T`; omitting it is refused with a message saying inference is coming.
    **Test:** hand-convert `algorithms.flan` and `sand.flan` to `.fln`; the
    forms read from each pair must be equal, ignoring locations.
 2. **Switch readers by extension** at every program-source entry point:
@@ -400,6 +404,12 @@ Each step lands on its own, with `dune test --root .` green.
    TAB, and a body is its statement's own block, up to its first clause.
 6. **Return-type inference** in `Check`, with the recursion refusal and the
    stale-caller cause. This is independent of steps 1-5 once the marker exists.
+   **Built** (`Check.infer_returns`). `_` is refused outside a `defn`'s return
+   slot, in a generic's, and in `defgeneric`/`defmulti`'s (`defmethod` has no
+   return slot). An exit with no value beside one with a value is refused. A
+   self- or mutually recursive group whose every exit gives `()` is `()`. A
+   stale
+   body with `_` keeps the signature it was compiled with.
 
 Out of scope: dropping macros, built-in replacements for `with-*`/`defedn`,
 printing diagnostics in the new syntax, converting the prelude or vendor

test/programs/arm-want.flan

@@ -0,0 +1,25 @@
+;;;; An arm is checked at the other arm's type first: arithmetic in a
+;;;; narrower arm is done at the wider type, not done narrow and widened, and
+;;;; nil beside an Option is None, whichever arm comes first.
+
+(defn wd [c bool a i64 b i32] i64 (let [v (if c a (+ b 1))] v))
+(defn wd2 [c bool a i64 b i32] i64 (if c a (+ b 1)))
+(defn wd4 [c bool a i64 b i32] i64 (let [v (if c a (* b b))] v))
+(defn wd5 [o (Option i32) a i64 b i32] i64 (let [v (match o (Some q) a None (+ b 1))] v))
+(defn wd6 [c bool a f64 b i32] f64 (let [v (if c a (/ b 2))] v))
+(defn wd7 [c bool a i64 b i32] _ (when c (return a)) (+ b 1))
+
+(defn n1 [c bool p (Option i64)] i64 (let [v (if c nil p)] (match v (Some q) q None -1)))
+(defn n2 [o (Option i32) p (Option i64)] i64
+  (let [v (match o None nil (Some z) p)] (match v (Some q) q None -1)))
+
+(defn main [] i32
+  (println (wd false 0 2147483647))
+  (println (wd2 false 0 2147483647))
+  (println (wd4 false 0 100000))
+  (println (wd5 None 0 2147483647))
+  (println (wd6 false 0.0 3))
+  (println (wd7 false 0 2147483647))
+  (println (n1 false (Some 5)) (n1 true (Some 5)))
+  (println (n2 (Some 1) (Some 5)) (n2 None (Some 5)))
+  0)

test/programs/dev-infer.flan

@@ -0,0 +1,20 @@
+;;;; Return types read off the body, for the stale-caller warning's cause.
+;;;; [speed]'s type is inferred and the tests change its body so that it
+;;;; returns something else. [run] is a written caller, [relay] an inferred
+;;;; one that returns what [speed] returns, and [sum] an inferred one whose
+;;;; body stops checking once [speed] returns an f64: [twice] takes an i32.
+
+(defn speed [x i32] _
+  (* x 2))
+
+(defn run [] i32 (speed 3))
+
+(defn relay [x i32] _ (speed x))
+
+(defn twice [x i32] i32 (* x 2))
+
+(defn sum [x i32] _ (twice (speed x)) (speed x))
+
+(defn use-relay [] i32 (+ (relay 1) (sum 1)))
+
+(defn main [] i32 (+ (run) (use-relay)))

test/programs/dyn-opened.flan

@@ -0,0 +1,25 @@
+;;;; A dyn beside a typed value is compared, added and joined as a dyn, in
+;;;; either order, whichever conversion asking for the typed value would have
+;;;; opened it with — a bool compared with a dyn int is false, not a trap.
+
+(defn as-dyn [d dyn] dyn d)
+(defn eqb [b bool d dyn] bool (= b d))
+(defn eqi [b i64 d dyn] bool (= b d))
+(defn addf [b f64 d dyn] dyn (+ b d))
+(defn addi [b i64 d dyn] dyn (+ b d))
+(defn mb [o (Option i32) b bool d dyn] dyn (let [v (match o (Some q) b None d)] v))
+(defn mb2 [o (Option i32) b bool d dyn] dyn (let [v (match o None d (Some q) b)] v))
+(defn ib [c bool b bool d dyn] dyn (let [v (if c b d)] v))
+(defn ib2 [c bool b bool d dyn] dyn (let [v (if c d b)] v))
+
+(defn main [] i32
+  (println (eqb true (as-dyn 1)))
+  (println (eqb true (as-dyn true)))
+  (println (eqi 1 (as-dyn 1.0)))
+  (println (addi 1 (as-dyn 1.5)))
+  (println (addf 1.0 (as-dyn 2)))
+  (println (mb None true (as-dyn 5)))
+  (println (mb2 None true (as-dyn 5)))
+  (println (ib false true (as-dyn 5)))
+  (println (ib2 true true (as-dyn 5)))
+  0)

test/programs/dyn-tails.flan

@@ -0,0 +1,88 @@
+;;;; A dyn in any value position of an operand or an arm — the last form
+;;;; of a let, either arm of an if, an arm of a match, the operand an and
+;;;; or an or answers with — meets its typed partner as a dyn, so what the
+;;;; runtime compares or adds is the dyn value and nothing traps.
+
+(defn as-dyn [d dyn] dyn d)
+
+(defn a1-t [c bool i i64 d dyn] dyn (+ i (let [z 1] d)))
+(defn a2-t [c bool i i64 d dyn] dyn (+ i (if c d d)))
+(defn a3-t [c bool i i64 d dyn] dyn (+ i (if c d 2)))
+(defn a4-t [c bool i i64 d dyn] dyn (= i (if c d 2)))
+(defn a5-t [c bool i i64 d dyn] dyn (* i (match (Some 1) (Some q) d None d)))
+(defn a6-t [c bool i i64 d dyn] dyn (let [v (if c i (let [z 1] d))] v))
+(defn a7-t [c bool i i64 d dyn] dyn (let [v (match (Some 1) (Some q) i None (let [z 1] d))] v))
+(defn a8-t [c bool i i64 d dyn] dyn (let [v (match (Some 1) None i (Some q) (if c d d))] v))
+(defn a9-t [c bool i i64 d dyn] dyn (- i (do (println 0) d)))
+(defn o1-t [c bool b bool i i64 d dyn] dyn (= b (and d)))
+(defn o2-t [c bool b bool i i64 d dyn] dyn (= b (or d)))
+(defn o3-t [c bool b bool i i64 d dyn] dyn (= b (and c d)))
+(defn o4-t [c bool b bool i i64 d dyn] dyn (= b (not d)))
+(defn o6-t [c bool b bool i i64 d dyn] dyn (let [v (if c b (and d))] v))
+(defn w1-t [c bool b bool d dyn] bool (= b (do (println 0) d)))
+(defn w2-t [c bool b bool d dyn] bool (= b (let [z 1] d)))
+(defn w3-t [c bool b bool d dyn] bool (= b (if c d d)))
+(defn w4-t [c bool b bool d dyn] bool (= b (if c d false)))
+(defn w5-t [c bool b bool d dyn] bool (= b (if c false d)))
+(defn w6-t [c bool b bool d dyn] bool (= b (match (Some 1) (Some q) d None d)))
+(defn w7-t [c bool b bool d dyn] bool (= (do d) b))
+(defn w9-t [c bool b bool d dyn] bool (= b (cond c d :else d)))
+(defn w10-t [c bool b bool d dyn] bool (= b (as-dyn d)))
+(defn w11-t [c bool b bool d dyn] bool (let [v (if c b (let [z 1] d))] (= v v)))
+(defn w12-t [c bool b bool d dyn] bool (= b (if c (do d) (do d))))
+(defn w13-t [c bool b bool d dyn] bool (!= b (let [z 1] (println z) d)))
+
+(defn main [] i32
+  (println (a1-t true 1 (as-dyn 1.5)))
+  (println (a1-t false 1 (as-dyn 1.5)))
+  (println (a2-t true 1 (as-dyn 1.5)))
+  (println (a2-t false 1 (as-dyn 1.5)))
+  (println (a3-t true 1 (as-dyn 1.5)))
+  (println (a3-t false 1 (as-dyn 1.5)))
+  (println (a4-t true 1 (as-dyn 1.5)))
+  (println (a4-t false 1 (as-dyn 1.5)))
+  (println (a5-t true 1 (as-dyn 1.5)))
+  (println (a5-t false 1 (as-dyn 1.5)))
+  (println (a6-t true 1 (as-dyn 1.5)))
+  (println (a6-t false 1 (as-dyn 1.5)))
+  (println (a7-t true 1 (as-dyn 1.5)))
+  (println (a7-t false 1 (as-dyn 1.5)))
+  (println (a8-t true 1 (as-dyn 1.5)))
+  (println (a8-t false 1 (as-dyn 1.5)))
+  (println (a9-t true 1 (as-dyn 1.5)))
+  (println (a9-t false 1 (as-dyn 1.5)))
+  (println (o1-t true true 1 (as-dyn 1)))
+  (println (o1-t true true 1 (as-dyn true)))
+  (println (o2-t true true 1 (as-dyn 1)))
+  (println (o2-t true true 1 (as-dyn true)))
+  (println (o3-t true true 1 (as-dyn 1)))
+  (println (o3-t true true 1 (as-dyn true)))
+  (println (o4-t true true 1 (as-dyn 1)))
+  (println (o4-t true true 1 (as-dyn true)))
+  (println (o6-t true true 1 (as-dyn 1)))
+  (println (o6-t true true 1 (as-dyn true)))
+  (println (w1-t true true (as-dyn 5)))
+  (println (w1-t false true (as-dyn 5)))
+  (println (w2-t true true (as-dyn 5)))
+  (println (w2-t false true (as-dyn 5)))
+  (println (w3-t true true (as-dyn 5)))
+  (println (w3-t false true (as-dyn 5)))
+  (println (w4-t true true (as-dyn 5)))
+  (println (w4-t false true (as-dyn 5)))
+  (println (w5-t true true (as-dyn 5)))
+  (println (w5-t false true (as-dyn 5)))
+  (println (w6-t true true (as-dyn 5)))
+  (println (w6-t false true (as-dyn 5)))
+  (println (w7-t true true (as-dyn 5)))
+  (println (w7-t false true (as-dyn 5)))
+  (println (w9-t true true (as-dyn 5)))
+  (println (w9-t false true (as-dyn 5)))
+  (println (w10-t true true (as-dyn 5)))
+  (println (w10-t false true (as-dyn 5)))
+  (println (w11-t true true (as-dyn 5)))
+  (println (w11-t false true (as-dyn 5)))
+  (println (w12-t true true (as-dyn 5)))
+  (println (w12-t false true (as-dyn 5)))
+  (println (w13-t true true (as-dyn 5)))
+  (println (w13-t false true (as-dyn 5)))
+  0)

test/programs/trial-generic.flan

@@ -0,0 +1,23 @@
+;;;; A generic copy first made while an if's else arm is tried on its own,
+;;;; then kept when the arm is checked again: whatever the copy lifted — a
+;;;; lambda, a condition's message printer — has to be kept with it, or the
+;;;; program links against a function nobody emitted.
+
+(defstruct MyErr :parent Error [code i32  why string])
+
+(defn ap [x i32 f (Fn [i32] i32)] i32 (f x))
+
+(defn g [x $t] i32 (ap 21 (fn [y] (+ y y))))
+
+(defn h [x $t] i32
+  (when (< 21 0) (error (MyErr {.code 3 .why "negative"})))
+  21)
+
+(defn pick [c bool a i64 b i32] i64 (let [v (if c a (g b))] v))
+
+(defn pick2 [c bool a i64 b i32] i64 (let [v (if c a (h b))] v))
+
+(defn main [] i32
+  (println (pick false 1 21))
+  (println (pick2 false 1 21))
+  0)

test/syntax/infer/main.flan

@@ -0,0 +1,40 @@
+;; Return types read off the body: _ in the return slot here, no arrow in
+;; main.fln. Each shape the rule has: one type, a call's type, a literal
+;; that takes the other exit's type, a dyn beside a literal, nothing (()), a return
+;; that never falls off the end, and a function that calls itself and gives
+;; nothing.
+
+(defn add [x i32 y i32] _ (+ x y))
+
+(defn half [x f64] _ (/ x 2.0))
+
+(defn quarter [x f64] _ (half (half x)))
+
+(defn pick [c bool] _
+  (when c (return 1))
+  2.5)
+
+(defn label [c bool d dyn] _
+  (when c (return d))
+  0)
+
+(defn say [x i32] _ (println x))
+
+(defn- floor0 [x i32] _
+  (if (< x 0) (return 0) x))
+
+(defn countdown [n i32] _
+  (when (> n 0)
+    (println n)
+    (countdown (- n 1))))
+
+(defn main [] i32
+  (println (add 1 2))
+  (println (quarter 10.0))
+  (println (+ (pick true) 0.5))
+  (println (pick false))
+  (println (label true "yes") (label false "yes"))
+  (say 4)
+  (println (floor0 -3) (floor0 5))
+  (countdown 2)
+  0)

test/syntax/infer/main.fln

@@ -0,0 +1,42 @@
+;; Return types read off the body: no arrow here, _ in the return slot in
+;; main.flan. Each shape the rule has: one type, a call's type, a literal
+;; that takes the other exit's type, a dyn beside a literal, nothing (()), a return
+;; that never falls off the end, and a function that calls itself and gives
+;; nothing.
+
+fn add(x: i32, y: i32) = x + y
+
+fn half(x: f64) = x / 2.0
+
+fn quarter(x: f64) = half(half(x))
+
+fn pick(c: bool)
+  if c
+    return 1
+  2.5
+
+fn label(c: bool, d)
+  if c
+    return d
+  0
+
+fn say(x: i32) = println(x)
+
+fn- floor0(x: i32)
+  if x < 0 then return 0 else x
+
+fn countdown(n: i32)
+  if n > 0
+    println(n)
+    countdown(n - 1)
+
+fn main() -> i32
+  println(add(1, 2))
+  println(quarter(10.0))
+  println(pick(true) + 0.5)
+  println(pick(false))
+  println(label(true, "yes"), label(false, "yes"))
+  say(4)
+  println(floor0(-3), floor0(5))
+  countdown(2)
+  0

test/test_acceptance.ml

@@ -590,6 +590,30 @@ let () =
       "programs/return-defer.flan" rd_out;
     outputs ~x86:true "a return computes its value before its defers, x86"
       "programs/return-defer.flan" rd_out;
+    (* A dyn in any value position of an operand or an arm is a dyn. *)
+    let dt_out = "2.5\n2.5\n2.5\n2.5\n2.5\n3\nfalse\nfalse\n1.5\n1.5\n1\n1.5\n1\n1\n1.5\n1.5\n0\n-0.5\n0\n-0.5\nfalse\ntrue\nfalse\ntrue\nfalse\ntrue\nfalse\nfalse\ntrue\ntrue\n0\nfalse\n0\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\ntrue\ntrue\nfalse\nfalse\n1\ntrue\n1\ntrue\n" in
+    outputs "a dyn in a value position stays a dyn" "programs/dyn-tails.flan" dt_out;
+    outputs ~x86:true "a dyn in a value position stays a dyn, x86"
+      "programs/dyn-tails.flan" dt_out;
+    (* A dyn opened by the other operand's or arm's type is seen as a dyn. *)
+    let do_out = "false\ntrue\ntrue\n2.5\n3\n5\n5\n5\n5\n" in
+    outputs "a dyn beside a typed value stays a dyn" "programs/dyn-opened.flan" do_out;
+    outputs ~x86:true "a dyn beside a typed value stays a dyn, x86"
+      "programs/dyn-opened.flan" do_out;
+    (* An arm is checked at the other arm's type first. *)
+    let aw_out =
+      "2147483648\n2147483648\n10000000000\n2147483648\n1.5\n2147483648\n\
+       5 -1\n5 -1\n"
+    in
+    outputs "an arm takes the other arm's type" "programs/arm-want.flan" aw_out;
+    outputs ~x86:true "an arm takes the other arm's type, x86"
+      "programs/arm-want.flan" aw_out;
+    (* A generic copy made during an abandoned trial keeps what it lifted. *)
+    outputs "a trial's generic copy keeps its lambda and its message printer"
+      "programs/trial-generic.flan" "42\n21\n";
+    outputs ~x86:true
+      "a trial's generic copy keeps its lambda and its message printer, x86"
+      "programs/trial-generic.flan" "42\n21\n";
     (* Constant arithmetic folds before a bounded variable checks it. *)
     let fold_out = "10\n0\n7.5\n7\n" in
     outputs "constant arithmetic at a bounded variable"

test/test_flan.ml

@@ -7773,4 +7773,345 @@ let () =
   accepts "calc-me.flan type checks"
     (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all);
 
+
+  (* ── Return types read off the body ([_]) ──────────────────────── *)
+  (* What each shape reads as, by the signature the editor is shown. *)
+  (let sign src name =
+     match checked src with
+     | p ->
+       (match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = name) p.Tast.fns with
+        | Some f -> Dev.signature_of_fn f
+        | None -> "missing")
+     | exception Loc.Error { Loc.dmsg = m; _ } -> "refused: " ^ m
+   in
+   let reads_as what src name want =
+     let got = sign src name in
+     if got <> want then begin
+       incr failures;
+       Printf.printf "FAIL  %s\n        got: %s\n     wanted: %s\n" what got want
+     end
+   in
+   let main = "\n(defn main [] ())" in
+   reads_as "an inferred return is the body's type"
+     ("(defn f [x i32] _ (+ x 1))" ^ main) "f" "f [i32] i32";
+   reads_as "an inferred return follows a call to another"
+     ("(defn g [x f64] _ (f x))\n(defn f [x f64] _ (* x 2.0))" ^ main) "g" "g [f64] f64";
+   reads_as "a literal return takes the other exit's type"
+     ("(defn f [c bool] _ (when c (return 1)) 2.5)" ^ main) "f" "f [bool] f64";
+   reads_as "a literal return takes a parameter's type"
+     ("(defn f [x i64] _ (when (< x 0) (return 0)) x)" ^ main) "f" "f [i64] i64";
+   reads_as "a literal return takes an f32"
+     ("(defn f [c bool x f32] _ (when c (return 1)) x)" ^ main) "f" "f [bool f32] f32";
+   reads_as "a dyn exit beside a literal gives dyn"
+     ("(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") ];
+   (* A match's arms meet at the same join, in either order. *)
+   List.iter
+     (fun (what, sg, body, want) ->
+        reads_as what ("(defn f " ^ sg ^ " _ " ^ body ^ ")" ^ main) "f" want)
+     [ ("match i32 then i64", "[o (Option i32) x i32 y i64]",
+        "(match o (Some q) x None y)", "f [(Option i32) i32 i64] i64");
+       ("match i64 then i32", "[o (Option i32) x i32 y i64]",
+        "(match o (Some q) y None x)", "f [(Option i32) i32 i64] i64");
+       ("match i8 then dyn", "[o (Option i32) x i8 y dyn]",
+        "(match o (Some q) x None y)", "f [(Option i32) i8 dyn] dyn");
+       ("match writable then read-only", "[o (Option i32) x [u8] y [const u8]]",
+        "(match o (Some q) x None y)", "f [(Option i32) [u8] [const u8]] [const u8]");
+       ("match literal arms, i32 then i64", "[n i32 x i32 y i64]",
+        "(match n 1 x _ y)", "f [i32 i32 i64] i64");
+       ("match a typed arm and a literal arm", "[o (Option i32) x i8]",
+        "(match o (Some q) x None 1)", "f [(Option i32) i8] i8");
+       ("match an arm that needs the join", "[o (Option i32) d dyn]",
+        "(match o (Some q) d None nil)", "f [(Option i32) dyn] 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 ()"
+     ("(defn f [n i32] _ (when (> n 0) (println n) (f (- n 1))))" ^ main) "f" "f [i32] ()";
+   reads_as "two that call each other and give nothing are ()"
+     ("(defn ev [n i32] _ (when (> n 0) (od (- n 1))))\n\
+       (defn od [n i32] _ (when (> n 0) (ev (- n 1))))" ^ main) "od" "od [i32] ()";
+   reads_as "a dyn body gives dyn" ("(defn f [x] _ x)" ^ main) "f" "f [dyn] dyn";
+   reads_as "no value gives ()" ("(defn f [x i32] _ (println x))" ^ main) "f" "f [i32] ()";
+   reads_as "an empty body gives ()" ("(defn f [] _)" ^ main) "f" "f [] ()";
+   reads_as "a return that never falls off the end"
+     ("(defn f [x i32] _ (if (< x 0) (return 0) x))" ^ main) "f" "f [i32] i32";
+   reads_as "a local that shares a name is not a call"
+     ("(defn f [x i32] _ (let [f 2] (+ x f)))" ^ main) "f" "f [i32] i32";
+   reads_as "defn- reads it too" ("(defn- f [x i32] _ x)" ^ main) "f" "f [i32] i32");
+  rejects_check "an inferred function that calls itself"
+    ~needle:"fact calls itself, so its return type cannot be read off its body"
+    "(defn fact [n i32] _ (if (< n 2) 1 (* n (fact (- n 1)))))\n(defn main [] ())";
+  rejects_check "inferred functions that call each other, named in order"
+    ~needle:"ev and od call each other (ev → od → ev), so neither"
+    "(defn top [n i32] _ (ev n))\n\
+     (defn ev [n i32] _ (if (= n 0) true (od (- n 1))))\n\
+     (defn od [n i32] _ (if (= n 0) false (ev (- n 1))))\n\
+     (defn main [] ())";
+  rejects_check "a cycle of three is named whole"
+    ~needle:"a and b and c call each other (a → b → c → a), so none"
+    "(defn a [n i32] _ (+ 1 (b n)))\n(defn b [n i32] _ (+ 1 (c n)))\n\
+     (defn c [n i32] _ (+ 1 (a n)))\n(defn main [] ())";
+  accepts "a written return type breaks the cycle"
+    "(defn ev [n i32] bool (if (= n 0) true (od (- n 1))))\n\
+     (defn od [n i32] _ (if (= n 0) false (ev (- n 1))))\n\
+     (defn main [] ())";
+  rejects_check "a body error behind an inferred return is its own"
+    ~needle:"expected i32, found string"
+    "(defn f [x i32] _ (+ x \"a\"))\n(defn g [x i32] _ (f x))\n(defn main [] ())";
+  rejects_check "no value on one path and a value on another"
+    ~needle:"f gives no value here and i32 on another path"
+    "(defn f [x i32] _ (when (> x 0) (return 1)) (println 2))\n(defn main [] ())";
+  (* Every error in the file is still reported, a [_] body's included, and
+     a call to a [_] function whose body failed adds none of its own. *)
+  (let count src =
+     match program src |> Check.program_all with
+     | _ -> 0
+     | exception Loc.Error _ -> 1
+     | exception Loc.Errors ds -> List.length ds
+   in
+   let errors what src n =
+     let got = count src in
+     if got <> n then begin
+       incr failures;
+       Printf.printf "FAIL  %s: %d errors, wanted %d\n" what got n
+     end
+   in
+   errors "a _ body's error does not hide the others"
+     "(defn bad1 [x i32] _ (+ x \"s\"))\n\
+      (defn bad2 [x i32] i32 (+ x \"t\"))\n\
+      (defn bad3 [x i32] i32 (undefined-thing x))\n(defn main [] i32 0)" 3;
+   errors "every error in one _ body"
+     "(defn bad1 [x i32] _ (+ x \"s\") (foo) (bar))\n(defn main [] i32 0)" 3;
+   errors "a call to a failed _ body adds nothing"
+     "(defn bad1 [x i32] _ (+ x \"s\"))\n(defn g [x i32] _ (bad1 x))\n\
+      (defn h [x i32] i32 (+ 1 (g x)))\n\
+      (defn main [] i32 (println (bad1 1)) 0)" 1;
+   errors "a refused loop does not hide the others"
+     "(defn a [n i32] _ (if (> n 0) (b (- n 1)) 5))\n(defn b [n i32] _ (a n))\n\
+      (defn z [n i32] i32 (+ n \"q\"))\n(defn main [] i32 (a 3) 0)" 2;
+   errors "a refused exit does not hide the others"
+     "(defn u [c bool] _ (when c (return)) 1)\n\
+      (defn z [n i32] i32 (+ n \"q\"))\n(defn main [] i32 (u true) 0)" 2);
+  (* Exits meet as an if's arms do, and are refused where those are. *)
+  rejects_check "a struct exit and a literal exit"
+    ~needle:"expected Pt, found the integer literal 1"
+    "(defstruct Pt [x i32 y i32])\n\
+     (defn m [c bool] _ (when c (return (Pt {.x 1 .y 2}))) 1)\n(defn main [] ())";
+  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 a u32 exit, which neither widens into"
+    ~needle:"expected i32, found u32"
+    "(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)";
+  (* An else arm refused on its own terms is not also blamed for a type it
+     was never going to have. *)
+  (let n =
+     match
+       program "(defn g [c bool a i32 b i64] i64 (let [v (if c a (+ b (nope2 1)))] v))\n\
+                (defn main [] i32 0)"
+       |> Check.program_all
+     with
+     | _ -> 0
+     | exception Loc.Error _ -> 1
+     | exception Loc.Errors ds -> List.length ds
+   in
+   if n <> 1 then begin
+     incr failures;
+     Printf.printf "FAIL  an else arm's own error alone: %d errors\n" n
+   end);
+  (* An arm that needs the other's type, and is refused at it too, says why
+     at that type — not that it has no type on its own. *)
+  rejects_check "a bare struct else arm with an unknown name in it"
+    ~needle:"unknown name q2"
+    "(defstruct P [x i32 y i32])\n\
+     (defn b3 [c bool p P] i32 (let [v (if c p {.x q2 .y 2})] (.y v)))\n\
+     (defn main [] i32 0)";
+  rejects_check "a bare struct match arm with an unknown name in it"
+    ~needle:"unknown name q2"
+    "(defstruct P [x i32 y i32])\n\
+     (defn a3 [o (Option i32) p P] i32 \
+        (let [v (match o (Some q) p None {.x q2 .y 2})] (.y v)))\n\
+     (defn main [] i32 0)";
+  (* A match arm that does not meet the others is refused at its value. *)
+  (match
+     checked
+       "(defn m4 [o (Option i32) x i8] i32 \
+          (let [v (match o (Some q) x None (do (println \"a\") \"lit\"))] 0))\n\
+        (defn main [] i32 0)"
+   with
+   | _ -> check "a match arm of another type is refused" false
+   | exception Loc.Error { Loc.dloc; dmsg; _ } ->
+     check "a match arm of another type is refused at its value"
+       (dloc.Loc.col = 87 && contains dmsg "expected i8, found string"));
+  (* Nested arms that meet at a wider type are checked once each, not once
+     per level above them — when the else arm fits the then arm's type, and
+     when it is wider, so that every level's first attempt is refused. *)
+  (let nest kind depth =
+     let rec go k e =
+       if k = 0 then e
+       else
+         go (k - 1)
+           (match kind with
+            | `If -> Printf.sprintf "(if c a (+ (idg b) (i32 %s)))" e
+            | `Match ->
+              Printf.sprintf "(match o (Some q) a None (+ (idg b) (i32 %s)))" e
+            | `If_wider -> Printf.sprintf "(if c b (+ a (i64 %s)))" e
+            | `Match_wider ->
+              Printf.sprintf "(match o (Some q) b None (+ a (i64 %s)))" e)
+     in
+     go depth "(i32 b)"
+   in
+   let structs =
+     String.concat ""
+       (List.init 300 (Printf.sprintf "(defstruct S%d [a i32 b i64])\n"))
+   in
+   List.iter
+     (fun (kind, sg, what) ->
+        let src =
+          "(defn idg [x $t] $t x)\n" ^ structs
+          ^ "(defn f " ^ sg ^ " i64 (let [v " ^ nest kind 20 ^ "] v))\n\
+             (defn g " ^ sg ^ " _ " ^ nest kind 20 ^ ")"
+        in
+        let t0 = Unix.gettimeofday () in
+        match checked src with
+        | p ->
+          check (what ^ " twenty deep checks fast")
+            (Unix.gettimeofday () -. t0 < 3.0);
+          check (what ^ " twenty deep meets at i64")
+            (List.exists
+               (fun (f : Tast.fn) ->
+                  f.Tast.name = "g" && Types.equal f.Tast.ret (Types.Int Types.I64))
+               p.Tast.fns)
+        | exception Loc.Error { Loc.dmsg; _ } ->
+          check (what ^ " twenty deep checks: " ^ dmsg) false)
+     [ (`If, "[c bool a i64 b i32]", "an if");
+       (`Match, "[o (Option i32) a i64 b i32]", "a match");
+       (`If_wider, "[c bool a i64 b i32]", "an if whose else arm is wider");
+       (`Match_wider, "[o (Option i32) a i64 b i32]",
+        "a match whose last arm is wider") ]);
+  (* An arm is asked the other arm's type first, so a value that takes its
+     type from what is asked — nil, (Some 3), arithmetic — gets it, and the
+     two meet the same way whichever is written first. *)
+  (let reads_as_top what src name want =
+     let got =
+       match checked src with
+       | p ->
+         (match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = name) p.Tast.fns with
+          | Some f -> Dev.signature_of_fn f
+          | None -> "missing")
+       | exception Loc.Error { Loc.dmsg = m; _ } -> "refused: " ^ m
+     in
+     if got <> want then begin
+       incr failures;
+       Printf.printf "FAIL  %s\n        got: %s\n     wanted: %s\n" what got want
+     end
+   in
+  List.iter
+    (fun (what, sg, body, want) ->
+       reads_as_top what ("(defn f " ^ sg ^ " _ " ^ body ^ ")\n(defn main [] ())") "f" want)
+    [ ("nil beside an Option", "[c bool p (Option i64)]", "(if c p nil)",
+       "f [bool (Option i64)] (Option i64)");
+      ("nil first beside an Option", "[c bool p (Option i64)]", "(if c nil p)",
+       "f [bool (Option i64)] (Option i64)");
+      ("(Some 3) beside an Option", "[c bool p (Option i64)]", "(if c p (Some 3))",
+       "f [bool (Option i64)] (Option i64)");
+      ("float arithmetic beside an f32", "[c bool p f32]", "(if c p (* 2.0 3.0))",
+       "f [bool f32] f32");
+      ("a do ending in a literal beside a u8", "[c bool p u8]",
+       "(if c p (do (println 1) 7))", "f [bool u8] u8");
+      ("a match's nil arm first", "[o (Option i32) p (Option i64)]",
+       "(match o None nil (Some z) p)", "f [(Option i32) (Option i64)] (Option i64)") ]);
+  (* Thirty deep, each level's first try refused: a chain of matches whose
+     last arm is wider, and sums nested in their second operands. *)
+  List.iter
+    (fun (what, src) ->
+       let t0 = Unix.gettimeofday () in
+       (match checked src with
+        | _ -> ()
+        | exception Loc.Error { Loc.dmsg; _ } -> check (what ^ ": " ^ dmsg) false);
+       check (what ^ " checks fast") (Unix.gettimeofday () -. t0 < 3.0))
+    (let nest f = let rec go k e = if k = 0 then e else go (k - 1) (f e) in go 30 in
+     [ ("thirty matches whose last arm is wider",
+        "(defn f [o (Option i32) a i64 b i32] i64 (let [v "
+        ^ nest (Printf.sprintf "(match o (Some q) (+ q 1) None (+ b %s))") "a"
+        ^ "] v))");
+       ("thirty matches with the narrow arm last",
+        "(defn f [o (Option i32) a i64 b i32] i64 (let [v "
+        ^ nest (Printf.sprintf "(match o None b (Some q) (+ b %s))") "a"
+        ^ "] v))");
+       ("thirty matches over a dyn at the bottom",
+        "(defn f [o (Option i32) d dyn b i32] dyn (let [v "
+        ^ nest (Printf.sprintf "(match o (Some q) q None (+ b %s))") "d"
+        ^ "] v))");
+       ("thirty sums nested in their second operands",
+        "(defn f [a i64 b i32] i64 (let [v "
+        ^ nest (Printf.sprintf "(+ b %s)") "a" ^ "] v))") ]);
+  rejects_check "an Option compared with a dyn, as before"
+    ~needle:"(Option i64) does not cross into dyn yet"
+    "(defn eqo [b (Option i64) d dyn] bool (= b d))\n(defn main [] ())";
+  rejects_check "nil beside a string, as before"
+    ~needle:"string"
+    "(defn f [c bool s string] string (let [v (if c s nil)] v))\n(defn main [] ())";
+  rejects_check "an else arm's own error is the one reported"
+    ~needle:"unknown function nope2"
+    "(defn g [c bool a i32 b i64] i64 (let [v (if c a (+ b (nope2 1)))] v))\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 [] ())";
+  rejects_check "_ in a generic's return slot" ~needle:"f is generic, and _"
+    "(defn f [x $t] _ x)\n(defn main [] ())";
+  rejects_check "_ as a parameter type"
+    ~needle:"_ here asks for x's type to be read off a body"
+    "(defn f [x _] i32 3)\n(defn main [] ())";
+  rejects_check "_ as a field type" ~needle:"only a defn's return slot"
+    "(defstruct P [x _])\n(defn main [] ())";
+  rejects_check "_ in a function type" ~needle:"only a defn's return slot"
+    "(defn main [] () (let [f (the (Fn [i32] _) (fn [x] x))] (f 1)))";
+  rejects_check "_ in a declare" ~needle:"only a defn's return slot"
+    "(declare cabs [x i32] _ \"abs\")\n(defn main [] ())";
+  parse_rejects "_ in a defgeneric's return slot"
+    ~needle:"defgeneric's methods each have their own"
+    "(defgeneric area [s] _)";
+
   Test_support.report ()

test/test_session.ml

@@ -1927,6 +1927,61 @@ let () =
    | _ -> fail "a package's bare name resolved from the program's own file"
    | exception Loc.Error _ -> ());
 
+  (* ── A return type read off the body changes ───────────────────────
+     [speed]'s return slot is [_], and a new body makes it an f64. It
+     installs like a written change, and each stale caller says why the
+     signature moved and which line moved it: nobody wrote the old or the
+     new type. [relay] returns what [speed] returns, so its own signature
+     moves too and its caller is named for that, at [relay]'s line. [sum]
+     no longer checks, and is a stale caller like [run]: it keeps the
+     signature it was compiled with. *)
+  (let t, _ = Session.create ~file:"programs/dev-infer.flan" () in
+   match
+     Session.eval ~origin:"programs/dev-infer.flan" t
+       "(defn speed [x i32] _\n  (* (f64 x) 2.5))"
+   with
+   | exception Loc.Error { Loc.dmsg = m; _ } ->
+     fail "an inferred return type that changed was refused: %s" m
+   | c ->
+     if not (List.mem "speed" c.Session.fns) then
+       fail "the inferred change was not installed";
+     let got =
+       List.map
+         (fun (x : Session.stale) ->
+            (x.Session.caller, x.Session.target,
+             Option.value x.Session.cause ~default:"-"))
+         c.Session.stale
+     in
+     let want =
+       [ ("run", "speed", "speed now returns f64, not i32, because of line 2");
+         ("relay", "speed", "speed now returns f64, not i32, because of line 2");
+         ("sum", "speed", "speed now returns f64, not i32, because of line 2");
+         ("sum", "speed", "speed now returns f64, not i32, because of line 2");
+         ("use-relay", "relay",
+          "relay now returns f64, not i32, because of line 12") ]
+     in
+     if got <> want then
+       fail "the stale callers of an inferred change were %s"
+         (String.concat "; "
+            (List.map (fun (a, b, c) -> Printf.sprintf "%s->%s (%s)" a b c) got));
+     (match
+        List.find_opt
+          (fun (f : Tast.fn) -> f.Tast.name = "sum")
+          t.Session.program.Tast.fns
+      with
+      | Some f when Types.equal f.Tast.ret (Types.Int Types.I32) -> ()
+      | Some f ->
+        fail "the stale inferred caller sum now returns %s"
+          (Types.to_string f.Tast.ret)
+      | None -> fail "the stale inferred caller sum left the program"));
+  (* A written return type that changes names no cause. *)
+  (let t, _ = Session.create ~file:"programs/dev-stale.flan" () in
+   match Session.eval t "(defn scale [x i64] i32 (i32 x))" with
+   | exception Loc.Error { Loc.dmsg = m; _ } -> fail "a written change: %s" m
+   | c ->
+     if List.exists (fun (x : Session.stale) -> x.Session.cause <> None)
+          c.Session.stale
+     then fail "a written return type's change named a cause");
   (* ── Every error in the form sent ───────────────────────────────────
      A refused subexpression stands as a value that fits anywhere, so the
      check goes on past it: three bad expressions are three errors, one three

test/test_syntax.ml

@@ -242,6 +242,7 @@ let pair flan fln =
 let () =
   pair "syntax/algorithms.flan" "syntax/algorithms.fln";
   pair "../sand.flan" "syntax/sand.fln";
+  pair "syntax/infer/main.flan" "syntax/infer/main.fln";
   (* Checked, never run: sand opens a window. *)
   List.iter
     (fun f ->
@@ -448,7 +449,10 @@ let () =
     "fn g(h: Fn(i32, i32) -> bool) -> () = h(1, 2)"
     "(defn g [h (Fn [i32 i32] bool)] () (h 1 2))";
   reads "untyped parameter is dyn" "fn id(x) -> dyn = x" "(defn id [x dyn] dyn x)";
-  refuses "no return type" "fn f(x)\n  x" "indent/return-type" "-> i32";
+  reads "no arrow infers the return" "fn f(x)\n  x" "(defn f [x dyn] _ x)";
+  reads "no arrow, one expression" "fn f(x: i32) = x + 1" "(defn f [x i32] _ (+ x 1))";
+  reads "no arrow, with where" "fn f(x: $t) where ordered?($t) = x"
+    "(defn f [x $t] _ {:where (ordered? $t)} x)";
   (* The fix is .fln's commas whatever the file is called: [read] names it
      <syntax>. *)
   refuses "where predicates joined with and"
@@ -977,7 +981,11 @@ let () =
     List.iter run_converted
       [ "syntax/flat/shadows.flan"; "syntax/flat/macros.flan"; "syntax/flat/capture.flan" ];
     run_both "syntax/mixed/main.flan" "12\n12\n0\n55\n";
-    run_both "syntax/mixed/main.fln" "25\n7\nfar\n3\n"
+    run_both "syntax/mixed/main.fln" "25\n7\nfar\n3\n";
+    (* Return types read off the body, in both spellings of [_]. *)
+    List.iter
+      (fun p -> run_both p "3\n2.5\n1.5\n2.5\nyes 0\n4\n0 5\n2\n1\n")
+      [ "syntax/infer/main.flan"; "syntax/infer/main.fln" ]
   end
   else print_endline "syntax: no clang, the import programs are not built"