diff --git a/TODO.org b/TODO.org
index fed58224..30bb5819 100644
--- a/TODO.org
+++ b/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=
diff --git a/emacs/flan.el b/emacs/flan.el
index 1f8ca0db..b96b6eda 100644
--- a/emacs/flan.el
+++ b/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.
diff --git a/lib/ast.ml b/lib/ast.ml
index 210a5738..9658fd36 100644
--- a/lib/ast.ml
+++ b/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
diff --git a/lib/check.ml b/lib/check.ml
index 3bdf5e80..766e7642 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -34,6 +34,12 @@ let fail = Loc.fail
    language from the one the author decided on. *)
 let literal_at_want = "check/literal-at-want"
 
+(* A refusal that is two types failing to meet, a literal's included: what
+   an arm checked at another arm's type says when the two simply differ. *)
+let is_mismatch (d : Loc.diag) =
+  String.equal d.Loc.kind "check/type-mismatch"
+  || String.equal d.Loc.kind literal_at_want
+
 (* [List.map]'s evaluation order is unspecified, and checking allocates frame
    slots as a side effect. Left-to-right is required, not a preference: a later
    let binding sees an earlier one, and slot numbering must be reproducible. *)
@@ -121,6 +127,35 @@ type gstruct = {
    program asks for the copy itself. *)
 let struct_apps : (string, string * Types.t list) Hashtbl.t = Hashtbl.create 16
 
+(* The undo journal a check that may be abandoned writes into: every table
+   write a body's check makes goes through [jreplace]/[jremove]/[jset], which
+   note how to take it back while a [snapshot_env] is open. So abandoning a
+   check costs what it wrote, not the size of the tables it could have. *)
+let journal : (unit -> unit) list ref = ref []
+let journal_open = ref 0
+
+let jot undo = if !journal_open > 0 then journal := undo :: !journal
+
+let jreplace tbl k v =
+  (if !journal_open > 0 then
+     let old = Hashtbl.find_opt tbl k in
+     jot (fun () ->
+         match old with
+         | Some o -> Hashtbl.replace tbl k o
+         | None -> Hashtbl.remove tbl k));
+  Hashtbl.replace tbl k v
+
+let jremove tbl k =
+  (if !journal_open > 0 then
+     match Hashtbl.find_opt tbl k with
+     | Some o -> jot (fun () -> Hashtbl.replace tbl k o)
+     | None -> ());
+  Hashtbl.remove tbl k
+
+let jset r v =
+  (if !journal_open > 0 then let old = !r in jot (fun () -> r := old));
+  r := v
+
 (* The length every length variable has inside a generic body's abstract
    pass. Large so that no constant index into such an array is refused as out
    of bounds there, and within i32 so that [(length a)] is an ordinary index.
@@ -293,6 +328,14 @@ type env = {
      the declare-c forms before [Shim.expand] rewrites them. Keyed by the Flan
      name a program calls. *)
   tracks : (string, Shim.track) Hashtbl.t;
+  (* Every [defn] whose return type was read off its body ([_]), with the
+     form that decided it — what a stale-caller warning points at. *)
+  inferred : (string, Loc.t) Hashtbl.t;
+  (* The [_] bodies whose type could not be read because of an error of
+     their own, while every error is being collected. Each stands in [fns]
+     as Never, a call to one stands as a poison, and pass two reports the
+     body's errors once. *)
+  infer_failed : (string, Loc.diag option) Hashtbl.t;
   (* Recovery: checking goes on past a refused subexpression. See [check].
      [recovering] is on only while a whole-file or session check is collecting
      every error; [recovered] is what it found, newest first; [poison] counts
@@ -347,6 +390,8 @@ let new_env () = {
   in_field = false;
   classes = Hashtbl.create 8;
   tracks = Hashtbl.create 16;
+  inferred = Hashtbl.create 8;
+  infer_failed = Hashtbl.create 4;
   recovering = false;
   recovered = [];
   poison = 0;
@@ -354,6 +399,59 @@ let new_env () = {
   guard_next = false;
 }
 
+(* A check that may be abandoned — a trial, a probe, a return type read and
+   thrown away, a tolerated body — opens one of these: [undo] puts back
+   everything it wrote into [env], [keep] closes it and leaves the writes,
+   which an enclosing one can still undo. Partial undo is the bug this
+   exists for: rewinding [lifted] and not the generic cache left a copy made
+   during a trial with the lambda it lifted gone, which is a link error. So
+   the whole record is named, closed with warning 9: a new field stops this
+   compiling until it is decided here.
+
+   The tables a body's check writes go through the journal ([jreplace]);
+   the lists and flags are held here, which costs nothing; the rest is
+   written by the declaration passes alone, before any body is checked. *)
+let snapshot_env env : (unit -> unit) * (unit -> unit) =
+  let[@warning "+9"] { lifted; instances; tyvars; subst; tvpreds; chain;
+                       deferred; lenvars; len_placeholder; schain; in_field;
+                       recovering; recovered; poison; speculating;
+                       guard_next;
+                       (* Journaled at their writes. *)
+                       structs = _; locs = _; copies = _; insts = _; fns = _;
+                       (* Declaration passes only. *)
+                       datas = _; unions = _; cases = _; aliases = _;
+                       consts = _; enums = _; parents = _; externs = _;
+                       extern_locs = _; fparams = _; fn_locs = _;
+                       privates = _; globals = _; global_locs = _;
+                       generics = _; gsigs = _; refused_generics = _;
+                       gstructs = _; broken = _; glens = _; classes = _;
+                       tracks = _; inferred = _; infer_failed = _ } = env in
+  incr journal_open;
+  let mark = !journal in
+  let close () =
+    decr journal_open;
+    if !journal_open = 0 then journal := []
+  in
+  let undo () =
+    let rec back l =
+      if l != mark then
+        match l with
+        | u :: rest -> u (); back rest
+        | [] -> ()
+    in
+    back !journal;
+    journal := mark;
+    close ();
+    env.lifted <- lifted; env.instances <- instances; env.tyvars <- tyvars;
+    env.subst <- subst; env.tvpreds <- tvpreds; env.chain <- chain;
+    env.deferred <- deferred; env.lenvars <- lenvars;
+    env.len_placeholder <- len_placeholder; env.schain <- schain;
+    env.in_field <- in_field; env.recovering <- recovering;
+    env.recovered <- recovered; env.poison <- poison;
+    env.speculating <- speculating; env.guard_next <- guard_next
+  in
+  (undo, close)
+
 (* A refusal [collect] can go on past: kept while a whole-file check is
    collecting, in the order found, and raised otherwise. *)
 let defer_or_raise env (d : Loc.diag) =
@@ -1401,7 +1499,7 @@ let struct_app g args =
            args)
   in
   if not (Hashtbl.mem struct_apps key) then begin
-    Hashtbl.replace struct_apps key (g, args);
+    jreplace struct_apps key (g, args);
     Hashtbl.replace Types.display key
       (Printf.sprintf "(%s %s)" g
          (String.concat " " (List.map Types.to_string args)))
@@ -1467,6 +1565,13 @@ let tyvar_in_scope env n =
 let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
   let loc = t.Ast.tloc in
   match t.Ast.t with
+  (* The one slot that takes [_] never reaches here: [collect] reads it off
+     the body first. So every [_] that does is in a slot with no body behind
+     it. *)
+  | Ast.Tinfer ->
+    Loc.failk "check/infer-misplaced" loc
+      "_ here asks for a type to be read off a function body, and only a \
+       defn's return slot has a body to read. Write the type out"
   | Ast.Tname "const" ->
     fail loc
       "const is not a type on its own — it marks one that can only be read, \
@@ -1635,8 +1740,8 @@ and struct_copy ?(at_definition = false) env loc name targs =
   let key = struct_app name targs in
   if Hashtbl.mem env.copies key then key
   else if Hashtbl.mem env.broken name then begin
-    Hashtbl.replace env.copies key (List.exists generic_arg targs);
-    Hashtbl.replace env.structs key { Tast.sname = key; fields = [] };
+    jreplace env.copies key (List.exists generic_arg targs);
+    jreplace env.structs key { Tast.sname = key; fields = [] };
     key
   end
   else begin
@@ -1670,9 +1775,9 @@ and struct_copy ?(at_definition = false) env loc name targs =
     let generic = List.exists generic_arg targs in
     (* In before its fields, so a field that names the same copy through a
        pointer — [(defstruct Node [next (Ptr (Node $t))])] — finds it. *)
-    Hashtbl.replace env.copies key generic;
-    Hashtbl.replace env.structs key { Tast.sname = key; fields = [] };
-    Hashtbl.replace env.locs key g.gloc;
+    jreplace env.copies key generic;
+    jreplace env.structs key { Tast.sname = key; fields = [] };
+    jreplace env.locs key g.gloc;
     let saved =
       (env.subst, env.tyvars, env.lenvars, env.tvpreds, env.len_placeholder,
        env.in_field, env.schain)
@@ -1700,13 +1805,13 @@ and struct_copy ?(at_definition = false) env loc name targs =
     with
     | fields ->
       restore ();
-      Hashtbl.replace env.structs key { Tast.sname = key; fields };
+      jreplace env.structs key { Tast.sname = key; fields };
       finite_from env key;
       key
     | exception e ->
       restore ();
-      Hashtbl.remove env.copies key;
-      Hashtbl.remove env.structs key;
+      jremove env.copies key;
+      jremove env.structs key;
       (* A field refused inside the template says nothing about which use
          asked for this copy; the note names it, one per level of copies. *)
       (match e with
@@ -2005,7 +2110,7 @@ let missing_return_type env (fn : Ast.fn) =
         "%s has no return type: (%s ...) stands where the return type goes, \
          and %s is not a type. The return type is written between the \
          parameter vector and the body, and a function that returns nothing \
-         writes () there"
+         writes () there, or _ to read it off the body"
         fn.Ast.name head head
   | _ -> ()
 
@@ -2108,6 +2213,13 @@ let pair_params ?(also = fun _ -> false) ?(declared = fun _ -> None)
       Loc.failk "check/parameter-named-type" loc
         "%s names a type, so it cannot also be this parameter's name. Write \
          [name %s], or rename the parameter" n n
+    (* [_] reads a type off a body, and a parameter has none to read. *)
+    | Ast.Pname (n, _) :: Ast.Pname ("_", tloc) :: _ ->
+      Loc.failk "check/infer-misplaced" tloc
+        "_ here asks for %s's type to be read off a body, and a parameter's \
+         type is never read off anything. Write its type, or leave it out \
+         and %s is dyn"
+        n n
     | Ast.Pname (n, loc) :: Ast.Ptype t :: rest ->
       { Ast.fname = n; fty = t; floc = loc } :: go rest
     | Ast.Pname (n, loc) :: Ast.Pname (t, tloc) :: rest when is_type_name env t ->
@@ -2548,6 +2660,7 @@ let sigil_vars ~kinds_of (ts : Ast.texpr list) =
            ks args
        | _ -> List.iter ty args)
     | Ast.Tfn (_, ps, r) -> List.iter ty ps; ty r
+    | Ast.Tinfer -> ()
     | Ast.Tlen _ -> ()
   in
   List.iter ty ts;
@@ -2887,6 +3000,23 @@ let rec literal_arith (e : Ast.expr) : int64 option =
    over literals alone. *)
 let lone_literal (e : Ast.expr) = is_literal e || literal_arith e <> None
 
+(* A value whose type comes only from defaults — a literal, [nil], [(Some 3)],
+   arithmetic over literals, a [do] ending in one — so it takes the type of whatever
+   meets it. An arm of this kind is checked after the others, at their type,
+   and never decides a join. *)
+let rec adapts (e : Ast.expr) =
+  lone_literal e
+  || (match e.Ast.e with
+      | Ast.Var "nil" -> true
+      | Ast.Call ({ Ast.e = Ast.Var "Some"; _ }, [ x ]) -> adapts x
+      | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%"); _ },
+                  (_ :: _ as xs)) ->
+        List.for_all adapts xs
+      | Ast.Do (_ :: _ as xs) | Ast.Let (_, (_ :: _ as xs)) ->
+        adapts (List.hd (List.rev xs))
+      | Ast.If (_, a, Some b) -> adapts a && adapts b
+      | _ -> false)
+
 
 (* The environment for a lifted body, built once its own body has been checked
    and [caught] is therefore final. spec-memory.md's case 2, and the whole of
@@ -2928,7 +3058,7 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
         (fun (n, ((b : binding), _)) -> { Tast.fname = n; fty = b.bty })
         caught
     in
-    Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields };
+    jreplace fctx.env.structs ename { Tast.sname = ename; fields };
     let ety = Types.Named ename in
     let eslot = fresh_slot fctx (Types.Ptr (Types.Mut, ety)) in
     let binds =
@@ -3814,26 +3944,11 @@ let refuse_frame_escapes (f : Tast.fn) =
        else String.capitalize_ascii who)
       verb (what hit) target whose who fix
   in
-  let rec tails (e : Tast.expr) =
-    match e.Tast.e with
-    | Tast.Do es | Tast.Let (_, es) | Tast.WithAlloc (_, es)
-    | Tast.Handled (_, es) ->
-      (match List.rev es with x :: _ -> tails x | [] -> ())
-    (* A restart clause is a branch of this function whose value is the
-       form's value when that restart is taken. *)
-    | Tast.RestartCase (cs, body) ->
-      List.iter
-        (fun (c : Tast.rclause) ->
-           match List.rev c.Tast.rbody with x :: _ -> tails x | [] -> ())
-        cs;
-      tails body
-    | Tast.If (_, a, b) -> tails a; tails b
-    | Tast.Match (_, arms) ->
-      List.iter
-        (fun (a : Tast.arm) ->
-           match List.rev a.Tast.abody with x :: _ -> tails x | [] -> ())
-        arms
-    | _ ->
+  (* Every value position of the body, walked by [Tast.iter_tails]: a
+     restart clause is a branch of this function whose value is the form's
+     value when that restart is taken, and it is on that list. *)
+  let tails =
+    Tast.iter_tails (fun (e : Tast.expr) ->
       Option.iter
         (fail ~verb:"returns" ~target:""
            ~fix_slice:(fun c ->
@@ -3846,7 +3961,7 @@ let refuse_frame_escapes (f : Tast.fn) =
                else
                  "Return the value, of type " ^ t
                  ^ ", instead of its address: drop the addr"))
-        (escapes 0 e)
+        (escapes 0 e))
   in
   (* Only a store into the global itself can be fixed by changing the
      global's type; for a field, an element or a push, the value's type
@@ -3978,6 +4093,26 @@ let box loc (e : Tast.expr) : Tast.expr =
   | Types.LArray _ ->
     no_dyn_yet loc ~into:true e.Tast.ty ""
 
+(* Every dyn an expectation opened ([expect]'s dyn arm), by the node that
+   opened it, and the box: what lets a caller that asked for a typed value
+   see that the value was a dyn, whichever opening the want picked. Keyed by
+   identity and held weakly, so it is gone with the tree. *)
+module Opened = Ephemeron.K1.Make (struct
+    type t = Tast.expr
+    let equal = ( == )
+    let hash = Hashtbl.hash
+  end)
+let opened_by_want : Tast.expr Opened.t = Opened.create 16
+
+(* What an [expect] mismatch found, by the refusal: the type a caller that
+   skipped a join can still name the way the join would have. *)
+module Found = Ephemeron.K1.Make (struct
+    type t = Loc.diag
+    let equal = ( == )
+    let hash = Hashtbl.hash
+  end)
+let mismatch_found : Types.t Found.t = Found.create 16
+
 let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
   let need sym ty = rt loc ty sym [ e ] in
   match want with
@@ -4355,6 +4490,10 @@ let expect ctx loc ~want (got : Tast.expr) =
       | Types.Dyn, Types.Dyn -> got
       | Types.Dyn, Types.Option t -> box_option ctx loc t got
       | Types.Dyn, _ -> box loc got
+      | Types.Option t, Types.Dyn when not (is_nil_lit got) ->
+        let opened = unbox_option ctx loc t got in
+        Opened.replace opened_by_want opened got;
+        opened
       | Types.Option t, Types.Dyn -> unbox_option ctx loc t got
       (* A bare T has no None to become, and this nil is one the checker can
          actually see — the literal, written right where the mismatch is.
@@ -4366,7 +4505,10 @@ let expect ctx loc ~want (got : Tast.expr) =
            or to dyn itself; wrap the type in Option, or keep the value dyn"
           (Types.to_string w)
       | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
-      | _, Types.Dyn -> unbox loc w got
+      | _, Types.Dyn ->
+        let opened = unbox loc w got in
+        Opened.replace opened_by_want opened got;
+        opened
       (* Implicit widening, and this single arm is the whole of its surface.
          [expect] is called by every site that annotates and by nothing else,
          so an argument, a return, a let or defonce with a type, a struct field
@@ -4412,10 +4554,14 @@ let expect ctx loc ~want (got : Tast.expr) =
          numbers, and it is on this message rather than beside it because a
          reader who has just been told i64 and i32 are different types needs
          to be told, in the same breath, which direction needed nothing. *)
-      Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s"
-        (Types.to_string w) (Types.to_string got.Tast.ty)
-        (numeric_note ~want:w ~got:got.Tast.ty)
-        (const_note ctx.env ~want:w ~got:got.Tast.ty)
+      (try
+         Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s"
+           (Types.to_string w) (Types.to_string got.Tast.ty)
+           (numeric_note ~want:w ~got:got.Tast.ty)
+           (const_note ctx.env ~want:w ~got:got.Tast.ty)
+       with Loc.Error d ->
+         Found.replace mismatch_found d got.Tast.ty;
+         raise (Loc.Error d))
 
 (* Something a [break] may not jump out of, named so the refusal can say which.
    See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@@ -4475,6 +4621,30 @@ let hash_ty = Types.Int Types.U64
    Each caller calls it again rather than sharing one value: [slots] and
    [slot_tys] are counted up per frame, and two frames that shared a context
    would share a slot counter. *)
+(* The return type a body is checked against while it is being read for
+   one ([_] in a defn's return slot; see [infer_returns]). Compared by
+   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]. *)
 let poison loc = { Tast.e = Tast.Zero Types.Never; ty = Types.Never; loc }
@@ -5187,6 +5357,42 @@ let if_failed :
   Hashtbl.create 16
 let if_depth = ref 0
 
+(* An arm refused at the other arm's type, keyed the same way: the arm is
+   then checked on its own terms, and an [if] above it that checks it again
+   — its own trial, then for real — finds the refusal here rather than
+   walking the arm to it once more, which in a chain nested in else arms
+   would be twice per level. Cleared for each program. *)
+let arm_failed :
+  (Loc.t,
+   Ast.expr * ((string * binding) list * Types.t) * Types.t * Loc.diag)
+    Hashtbl.t =
+  Hashtbl.create 16
+
+(* A dyn value opened at a typed want: the box, and the want it was opened
+   at. Two arms that meet this way meet at dyn — the typed one is boxed, not
+   the dyn one opened — whichever is written first. *)
+let not_kept = "check/arm-not-kept"
+
+let to_dyn ctx (x : Tast.expr) = expect ctx x.Tast.loc ~want:(Some Types.Dyn) x
+
+let opened_dyn ~(box : Tast.expr -> Tast.expr) (v : Tast.expr) =
+  (* An opening is a value position of its own, whatever shape the
+     conversion built. *)
+  let stop x = Opened.mem opened_by_want x in
+  let any = ref false in
+  Tast.iter_tails ~stop (fun x -> if stop x then any := true) v;
+  if not !any then None
+  else
+    (* Every value position meets at dyn: an opened one is put back to the
+       box it opened, and any other is boxed. *)
+    Some
+      (Tast.map_tails ~stop ~ty:Types.Dyn
+         (fun x ->
+            match Opened.find_opt opened_by_want x with
+            | Some b -> b
+            | None -> box x)
+         v)
+
 
 (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule —
    so growing it reallocates a block only this function's copy points at, and
@@ -5267,7 +5473,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   else begin
     let seen = env.poison in
     let caused () =
-      env.recovered <> []
+      (env.recovered <> [] || Hashtbl.length env.infer_failed > 0)
       && (env.poison > seen || want = Some Types.Never)
     in
     match check_plain ctx ?want e with
@@ -5586,6 +5792,18 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
       "return is not allowed inside %s yet"
       (match ctx.in_frames with Some n -> n | None -> assert false)
 
+  | Ast.Return v when ctx.ret == infer_ret ->
+    let lit = match v with Some x -> adapts x | None -> false in
+    let v = Option.map (check ctx) v in
+    infer_seen :=
+      (match v with
+       | Some (x : Tast.expr) -> (x.Tast.ty, loc, lit)
+       | None -> (Types.Unit, loc, false))
+      :: !infer_seen;
+    (match ctx.defers, v with
+     | [], _ -> mk loc Types.Never (Tast.Return v)
+     (* Thrown away after, so the order the defers run in is not built. *)
+     | ds, _ -> mk loc Types.Never (Tast.Do (ds @ [ mk loc Types.Never (Tast.Return v) ])))
   | Ast.Return v ->
     let v =
       match v with
@@ -5724,6 +5942,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
     (* Unwrap Some, else early-return None from the enclosing function, so the
        enclosing function must itself return an Option (plan.org). *)
     (match ctx.ret with
+     | _ when ctx.ret == infer_ret ->
+       Loc.failk "check/infer-some" loc
+         "some returns None from the function when there is nothing, and \
+          this function's return type is read off its body, which cannot \
+          say what the Option holds. Write the return type: (Option T)"
      | Types.Option _ ->
        let v = check ctx v in
        (match v.Tast.ty with
@@ -7277,7 +7500,7 @@ and check_if_once ctx ~tail ?want loc c t e =
     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)
+  | Some e when want = None && adapts t && not (adapts e)
                 && not (and_sentinel e) ->
     (* A literal has no type of its own until something asks, so with no
        expectation the other arm decides: [(if c 4000000 n)] over an i64 [n]
@@ -7307,6 +7530,81 @@ 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 at the then arm's type first, as it always was: a value
+       that takes its type from what is asked of it — [(+ b 1)] beside an
+       i64, [nil] beside an Option — is asked the then arm's. Only when that
+       is refused as a mismatch is it checked on its own terms, and the two
+       meet at [arm_join], so [(if c x32 y64)] is the i64 [(if c y64 x32)]
+       is. A dyn opened at the then arm's type is not a meeting: the two
+       meet at dyn, as they do the other way round. The arm is checked once
+       each way at most, and a refusal at the then arm's type is kept
+       ([arm_failed]) for the ifs above that check it again. *)
+    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
+        let alone () = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in
+        let key = (ctx.scope, ctx.ret) in
+        let at_then () =
+          match
+            List.find_opt
+              (fun (n, (sc, r), w, _) ->
+                 n == e && r == ctx.ret && Types.equal w t.Tast.ty
+                 && same_scope sc ctx.scope)
+              (Hashtbl.find_all arm_failed e.Ast.loc)
+          with
+          | Some (_, _, _, d) -> Error d
+          | None ->
+            match
+              trial ctx (fun () ->
+                  branch ctx (fun () ->
+                      in_tail (fun () -> check ctx ~want:t.Tast.ty e)))
+            with
+            | Ok v -> Ok v
+            | Error d ->
+              Hashtbl.add arm_failed e.Ast.loc (e, key, t.Tast.ty, d);
+              Error d
+        in
+        let meet v =
+          match arm_join t.Tast.ty v.Tast.ty with
+          | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v)
+          | None -> None
+        in
+        match at_then () with
+        | Ok v ->
+          (match opened_dyn ~box:(to_dyn ctx) v with
+           | Some box -> Some (Types.Dyn, box)
+           | None -> Some (t.Tast.ty, v))
+        | Error _ when adapts e -> None
+        | Error d ->
+          (* A mismatch, or a dyn the then arm's type could not open: the
+             arm on its own terms meets the then arm. Anything else refused
+             it at the then arm's type, and that refusal is said. *)
+          (match
+             trial ctx (fun () ->
+                 let v = alone () in
+                 if is_mismatch d || Types.equal v.Tast.ty Types.Dyn then v
+                 else raise (Loc.Error (Loc.diag ~kind:not_kept v.Tast.loc "")))
+           with
+           | Ok v -> meet v
+           | Error own when String.equal own.Loc.kind not_kept -> None
+           (* Refused on its own terms too, and not as a mismatch — an
+              unknown name, say: that is the real error, and nothing is said
+              about a type the arm was never going to have. *)
+           | Error own when is_mismatch d && not (is_mismatch own) ->
+             let v = alone () in
+             (match meet v with
+              | Some r -> Some r
+              | None ->
+                Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v))
+           | Error _ -> 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
@@ -8731,7 +9029,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
      the others, as an [if]'s literal arm does. The order is only the order
      they are checked in; they are put back in source order below. *)
   let literal_arm ((a : Ast.arm), _, _) =
-    match List.rev a.Ast.body with last :: _ -> lone_literal last | [] -> false
+    match List.rev a.Ast.body with last :: _ -> adapts last | [] -> false
   in
   (* Every arm a literal: they meet at the wider of their own types, as an
      [if]'s two do. *)
@@ -8753,6 +9051,13 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
         | Some t when not (Types.equal t (Types.Int Types.I32)) -> want := Some t
         | _ -> ())
      | [] -> ());
+  (* With nothing expected, the arms meet at [arm_join], as an [if]'s do, in
+     whatever order they are written: each typed arm is checked on its own
+     terms, the join so far grows with it, and every arm is brought to the
+     final join at the end. An arm that needs an expectation — [nil], a bare
+     struct — is checked at the join so far, as it was at the first arm's
+     type before. *)
+  let free = !want = None in
   let order =
     let idx = List.mapi (fun i r -> (i, r)) resolved in
     if !want <> None then idx
@@ -8795,12 +9100,96 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
            (* Every arm is the tail, exactly as an [if]'s two arms are.
               Restored here because checking the scrutinee withdrew it. *)
            ctx.tail <- tail;
-           let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in
-           if !want = None && body.Tast.ty <> Types.Never then
-             want := Some body.Tast.ty;
+           let arm = (a, ctor, binds) in
+           let body =
+             if free && !want <> None && not (literal_arm arm) then
+               (* As an [if]'s else arm: at the join so far first, on its
+                  own terms only when that is refused as a mismatch. *)
+               let at w () = block ctx ?want:w a.Ast.aloc a.Ast.body in
+               let w = Option.get !want in
+               let head = List.hd a.Ast.body in
+               let at_join () =
+                 match
+                   List.find_opt
+                     (fun (n, (sc, r), w', _) ->
+                        n == head && r == ctx.ret && Types.equal w' w
+                        && same_scope sc ctx.scope)
+                     (Hashtbl.find_all arm_failed head.Ast.loc)
+                 with
+                 | Some (_, _, _, d) -> Error d
+                 | None ->
+                   (match trial ctx (at (Some w)) with
+                    | Ok b -> Ok b
+                    | Error d ->
+                      Hashtbl.add arm_failed head.Ast.loc
+                        (head, (ctx.scope, ctx.ret), w, d);
+                      Error d)
+               in
+               match at_join () with
+               | Ok b ->
+                 (match opened_dyn ~box:(to_dyn ctx) b with
+                  | Some box -> want := Some Types.Dyn; box
+                  | None -> b)
+               | Error d ->
+                 (match
+                    trial ctx (fun () ->
+                        let b = at None () in
+                        if is_mismatch d || Types.equal b.Tast.ty Types.Dyn then b
+                        else
+                          raise (Loc.Error (Loc.diag ~kind:not_kept b.Tast.loc "")))
+                  with
+                  | Ok b -> b
+                  | Error own when String.equal own.Loc.kind not_kept ->
+                    at !want ()
+                  | Error own when is_mismatch d && not (is_mismatch own) ->
+                    at None ()
+                  | Error _ -> at !want ())
+             else block ctx ?want:!want a.Ast.aloc a.Ast.body
+           in
+           (if body.Tast.ty <> Types.Never then
+              match !want with
+              | None -> want := Some body.Tast.ty
+              | Some w when free ->
+                (match arm_join w body.Tast.ty with
+                 | Some j -> want := Some j
+                 | None -> ())
+              | Some _ -> ());
            { Tast.acase = ctor; binds; abody = [ body ] }))
       order
   in
+  let checked =
+    match free, !want with
+    | true, Some j ->
+      (* Said at the arm's value, its last form, as a refusal checked at the
+         join would have been — not at its pattern. *)
+      let rec value (x : Ast.expr) =
+        match x.Ast.e with
+        | Ast.Do (_ :: _ as xs) | Ast.Let (_, (_ :: _ as xs)) ->
+          value (List.hd (List.rev xs))
+        | _ -> x.Ast.loc
+      in
+      let value_loc i =
+        let (a : Ast.arm), _, _ = List.nth resolved i in
+        match List.rev a.Ast.body with
+        | x :: _ -> value x
+        | [] -> a.Ast.aloc
+      in
+      (* Each arm refused on its own, so every arm that cannot meet the join
+         is said, as each would be checked at it. *)
+      List.map
+        (fun (i, (arm : Tast.arm)) ->
+           match arm.Tast.abody with
+           | [ b ] when not (Types.equal b.Tast.ty j || b.Tast.ty = Types.Never) ->
+             let at = value_loc i in
+             let b =
+               try expect ctx at ~want:(Some j) b
+               with Loc.Error d -> refuse_or_poison ctx.env at d
+             in
+             (i, { arm with Tast.abody = [ b ] })
+           | _ -> (i, arm))
+        checked
+    | _ -> checked
+  in
   let arms =
     List.map snd (List.sort (fun (i, _) (j, _) -> compare i j) checked)
   in
@@ -12635,6 +13024,13 @@ and ordinary_call ctx ~want loc name args =
      lifted body captures it by value and then calls the copy. [peek_outer]
      rather than [capture] in the guard, because a guard must not take a copy
      on its way to deciding what a form means. *)
+  (* A [_] function whose body failed has no return type to give; its own
+     errors are reported with its body, so a call to it stands in. *)
+  | _ when ctx.env.recovering && Hashtbl.mem ctx.env.infer_failed name
+           && lookup ctx name = None ->
+    List.iter (fun a -> ignore (check ctx a)) args;
+    ctx.env.poison <- ctx.env.poison + 1;
+    poison loc
   (* A local bound to a refused initialiser's stand-in, called: the refusal
      is already reported, so the call stands in too, its arguments still
      checked. *)
@@ -13343,7 +13739,7 @@ and instantiate env loc gname vars subst cparams cret =
   let cache =
     match Hashtbl.find_opt env.insts gname with
     | Some r -> r
-    | None -> let r = ref [] in Hashtbl.replace env.insts gname r; r
+    | None -> let r = ref [] in jreplace env.insts gname r; r
   in
   let same (ps, r, _) =
     List.length ps = List.length cparams
@@ -13389,8 +13785,8 @@ and instantiate env loc gname vars subst cparams cret =
     (* The entry goes in *before* the body is checked, which is what makes a
        recursive generic function terminate: the call to itself at the same
        types finds this and does not generate a second copy. *)
-    cache := (cparams, cret, sym) :: !cache;
-    Hashtbl.replace env.fns sym (cparams, cret);
+    jset cache ((cparams, cret, sym) :: !cache);
+    jreplace env.fns sym (cparams, cret);
     let saved_subst = env.subst and saved_vars = env.tyvars
     and saved_preds = env.tvpreds and saved_chain = env.chain in
     (* Inside the copy there are no variables left: [resolve_name] answers
@@ -13478,8 +13874,8 @@ and instantiate env loc gname vars subst cparams cret =
         (* A copy whose body did not check is not a copy. Both entries go back
            out, so a second call at the same types is the same refusal again
            rather than a cache hit on a function that does not exist. *)
-        cache := List.filter (fun (_, _, s) -> s <> sym) !cache;
-        Hashtbl.remove env.fns sym;
+        jset cache (List.filter (fun (_, _, s) -> s <> sym) !cache);
+        jremove env.fns sym;
         raise e
     in
     env.instances <- tfn :: env.instances;
@@ -13567,24 +13963,10 @@ and trial ctx f =
      it, so a new field on [ctx] stops this function compiling until somebody
      decides about it, rather than joining the list of things nobody noticed.
 
-     What is *not* restored, once, deliberately: [env.lifted] keeps whatever
-     function an abandoned trial lifted out of an [fn] literal. It is dead —
-     the names are [fn/<owner>/N] handed out by count, so the live pass gets
-     fresh ones and nothing refers to the orphan — and it rides along into the
-     module as a function nobody calls. Left alone because [env] is the
-     program's table and not this form's, and rewinding it would mean deciding
-     what else on [env] a trial may have touched.
-
-     The generic instantiation cache is the other table a trial reaches, and
-     it does not rewind either. [instantiate] rewinds a copy whose *body*
-     refused, which is a different event from a copy the caller abandoned —
-     and the abandoned one does not need rewinding. A generic call's
-     instantiation is read off its arguments and never off the ambient want:
-     an unbound variable is checked with no expectation at all, and a bound
-     one does not widen. So the trial and the live pass ask [instantiate] for
-     the same types, the second ask is a cache hit on the first, and exactly
-     one copy exists either way. Pinned in test_flan, "a generic inside an
-     abandoned trial".
+     [env] is put back the same way, whole, by [snapshot_env]: a function
+     lifted, a generic copy made and cached, a struct registered — all of it
+     goes together, since keeping one of a pair without the other is how a
+     copy ends up calling a lambda that was never emitted.
 
      Only [Loc.Error] is caught. A timeout or a stack overflow is not a
      refusal to reconsider, and silently continuing past one would turn a
@@ -13594,9 +13976,11 @@ and trial ctx f =
                        outer_what; caught; place_ok; envslot; parent = _;
                        in_frames; loops; tail; in_defer;
                        owner = _ } = ctx in
+  let undo, keep = snapshot_env ctx.env in
   match speculate ctx.env f with
-  | r -> Ok r
+  | r -> keep (); Ok r
   | exception Loc.Error d ->
+    undo ();
     ctx.slots <- slots; ctx.slot_tys <- slot_tys;
     ctx.slot_names <- slot_names; ctx.scope <- scope;
     ctx.defers <- defers; ctx.defer_slot <- defer_slot;
@@ -13605,6 +13989,7 @@ and trial ctx f =
     ctx.caught <- caught; ctx.place_ok <- place_ok; ctx.envslot <- envslot;
     ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
     Error d
+  | exception e -> keep (); raise e
 
 (* Whether the trial's refusal is one worth reconsidering. A literal that did
    not fit is not, and neither is a refusal a program cannot make any use of
@@ -13633,6 +14018,25 @@ and join_pair ctx (a : Tast.expr) (y : Ast.expr) (d : Loc.diag) =
      | Some pair -> pair
      | None -> raise (Loc.Error d))
 
+(* [y] checked at [w] in a trial, and a refusal kept ([arm_failed]) so the
+   same operand asked again at the same type, in the same scope, is refused
+   without being walked: a chain of these nested in their second operands is
+   asked once per level above it. *)
+and trial_at ctx (y : Ast.expr) (w : Types.t) =
+  match
+    List.find_opt
+      (fun (n, (sc, r), w', _) ->
+         n == y && r == ctx.ret && Types.equal w' w && same_scope sc ctx.scope)
+      (Hashtbl.find_all arm_failed y.Ast.loc)
+  with
+  | Some (_, _, _, d) -> Error d
+  | None ->
+    (match trial ctx (fun () -> check ctx ~want:w y) with
+     | Ok b -> Ok b
+     | Error d ->
+       Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d);
+       Error d)
+
 and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
   match args with
   | [ x; y ] ->
@@ -13672,6 +14076,19 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
        type, so [(+ x 1)] over a dyn x goes on building an i64 one. *)
     else if dyn_ok && not (needs_want y) then begin
       let a = check ctx ?want x in
+      (* y at [a]'s type first, and on its own terms only if that is
+         refused: checking it both ways every time made a chain of these
+         nested in their second operands twice as slow per level. A dyn
+         opened at [a]'s type is seen for what it was. *)
+      let at_a =
+        if a.Tast.ty = Types.Dyn then None
+        else
+          Some (trial_at ctx y a.Tast.ty)
+      in
+      match at_a with
+      | Some (Ok b') ->
+        (match opened_dyn ~box:(to_dyn ctx) b' with Some box -> a, box | None -> a, b')
+      | _ ->
       let b = check ctx y in
       (* Nothing dyn about this pair after all, so it is put back the way the
          typed path built it. Re-checking only when the types actually differ
@@ -13693,7 +14110,11 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
          that has to move. Nothing is checked a third time — the own-terms [b]
          already in hand is the answer. *)
       else
-        (match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
+        (match
+           match at_a with
+           | Some (Error d) -> Error d
+           | _ -> trial_at ctx y a.Tast.ty
+         with
          | Ok b' -> a, b'
          | Error d ->
            (match
@@ -13704,11 +14125,30 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
     end
     else begin
       let a = check ctx ?want x in
-      match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
+      match trial_at ctx y a.Tast.ty with
       | Ok b -> a, b
       | Error d ->
-        if join && reconsiderable d then join_pair ctx a y d
-        else raise (Loc.Error d)
+        (* The join moves [a] to something wider, and [a] already has the
+           type asked of the whole: that can only be refused, so y is not
+           walked on its own terms to find it out. *)
+        let doomed =
+          match want with Some w -> Types.equal a.Tast.ty w | None -> false
+        in
+        if join && reconsiderable d && not doomed then join_pair ctx a y d
+        else
+          (* Doomed: said the way the join would have been refused — the
+             pair at the wider type, at this form — when y's own refusal
+             names the wider type it found. *)
+          match want, (if doomed then Found.find_opt mismatch_found d else None) with
+          | Some w, Some found
+            when String.equal d.Loc.dloc.Loc.file y.Ast.loc.Loc.file
+                 && d.Loc.dloc = y.Ast.loc ->
+            (match Types.join w found with
+             | Some j when not (Types.equal j w) ->
+               ignore (expect ctx loc ~want:(Some w) (mk loc j Tast.Unit));
+               raise (Loc.Error d)
+             | _ -> raise (Loc.Error d))
+          | _ -> raise (Loc.Error d)
     end
   | _ -> fail loc "%s takes two arguments" name
 
@@ -14248,6 +14688,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
@@ -14707,8 +15173,20 @@ let collect env (decls : Ast.decl list) =
                 in
                 let ret =
                   match fn.Ast.ret with
-                  | None -> Types.Unit
-                  | Some t -> resolve env t
+                  | None -> Some Types.Unit
+                  (* Read off the body by [infer_returns], once every
+                     written signature is in [fns]; until then the name
+                     has none. *)
+                  | Some { Ast.t = Ast.Tinfer; tloc } ->
+                    if vars <> [] then
+                      Loc.failk "check/infer-generic" tloc
+                        "%s is generic, and _ asks for its return type to be \
+                         read off one body — but each call site makes its own \
+                         copy. Write the return type, in terms of the $ \
+                         variables"
+                        fn.Ast.name;
+                    None
+                  | Some t -> Some (resolve env t)
                 in
                 params, ret)
          in
@@ -14716,11 +15194,14 @@ let collect env (decls : Ast.decl list) =
            Hashtbl.replace env.privates fn.Ast.name
              (fn.Ast.nloc, fn.Ast.fprivate);
          if vars = [] then begin
-           Hashtbl.replace env.fns fn.Ast.name (params, ret);
+           Option.iter
+             (fun ret -> Hashtbl.replace env.fns fn.Ast.name (params, ret))
+             ret;
            Hashtbl.replace env.fparams fn.Ast.name fn.Ast.params;
            Hashtbl.replace env.fn_locs fn.Ast.name fn.Ast.nloc
          end
          else begin
+           let ret = Option.get ret in
            Hashtbl.replace env.generics fn.Ast.name fn;
            Hashtbl.replace env.gsigs fn.Ast.name (vars, params, ret);
            Hashtbl.replace env.glens fn.Ast.name lens
@@ -14761,27 +15242,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
-     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 infer (_, v) = (check (invented_ctx env Types.Unit) v).Tast.ty in
-  let pending = ref (List.rev !untyped) 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 ()
+  (* The untyped constants ([settle_consts]). One that calls a [_] function
+     waits for [infer_returns], which needs every signature this pass
+     registers; it is settled after that, and its refusal is the one a
+     written return type would get. *)
+  let inferred_names =
+    List.filter_map
+      (fun (d : Ast.decl) ->
+         match d.Ast.d with
+         | Ast.Defn { Ast.name; ret = Some { Ast.t = Ast.Tinfer; _ }; _ } ->
+           Some name
+         | _ -> None)
+      decls
   in
-  settle ();
-  List.iter (fun c -> ignore (infer c)) !pending;
+  let waits (_, v) =
+    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
@@ -14907,8 +15388,20 @@ let escaping_names ~returns (body : Ast.expr list) : string list =
   if returns then (match List.rev body with x :: _ -> tails x | [] -> ());
   !names
 
-let rec check_fn env (fn : Ast.fn) : Tast.fn =
-  let params, ret = Hashtbl.find env.fns fn.Ast.name in
+let rec check_fn ?sign env (fn : Ast.fn) : Tast.fn =
+  let params, ret =
+    match sign with Some s -> s | None -> Hashtbl.find env.fns fn.Ast.name
+  in
+  (* A [_] body whose type could not be read stands in [fns] as Never (see
+     [infer_returns]); pass two reads it the same way again, so its errors
+     are reported here, once, with every other body's. *)
+  let ret =
+    match sign, fn.Ast.ret with
+    | None, Some { Ast.t = Ast.Tinfer; _ }
+      when Hashtbl.mem env.infer_failed fn.Ast.name ->
+      infer_ret
+    | _ -> ret
+  in
   let ctx = { (invented_ctx env ret) with owner = fn.Ast.name } in
   List.iter2
     (fun (p : Ast.field) ty ->
@@ -14967,13 +15460,16 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
   let body =
     match fn.Ast.fbody with
     | [] ->
-      if Types.equal ret Types.Unit then []
+      if Types.equal ret Types.Unit || ret == infer_ret then []
       else fail fn.Ast.nloc "%s returns %s but has no body" fn.Ast.name
              (Types.to_string ret)
     | body ->
       (* The last form is the return value, unless the function returns Unit,
          in which case whatever it evaluates to is discarded. *)
-      let want = if Types.equal ret Types.Unit then None else Some ret in
+      let want =
+        if Types.equal ret Types.Unit || ret == infer_ret then None
+        else Some ret
+      in
       (* Every form here is at the top level of the function body, so every one
          of them may carry a [defer] — and so may a form inside a [let] written
          here, which is what [ctx.defer_ok] carries down. [check] registers it
@@ -15061,6 +15557,8 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
     in
     match ctx.defers with
     | [] -> body
+    (* A body read only for its type is thrown away after. *)
+    | _ when ret == infer_ret -> body
     (* A body that never falls off the end — its last form a [return], say —
        has no fall-off path to put the defers on, and a copy of them there is
        code after a terminator. *)
@@ -15103,6 +15601,16 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
        | Some s -> guarded_defers s ctx.defers);
     fenv = None; fparent = None; floc = fn.Ast.nloc }
   in
+  let checked =
+    if sign = None && ret == infer_ret then
+      (* Pass two over a [_] body pass one could not read: its errors are
+         raised above; a body that checks has the refusal pass one made
+         about its exits, or waited on one that did, and stands as Never. *)
+      match Hashtbl.find_opt env.infer_failed fn.Ast.name with
+      | Some (Some d) -> raise (Loc.Error d)
+      | _ -> { checked with Tast.ret = Types.Never }
+    else checked
+  in
   refuse_frame_escapes checked;
   checked
 
@@ -15146,9 +15654,9 @@ and check_generic env (fn : Ast.fn) =
      [env.tvpreds] whether the variable was declared to support it, and every
      instantiation asks the concrete type the same question again. *)
   env.tvpreds <- fn.Ast.fwhere;
-  Hashtbl.replace env.fns fn.Ast.name (params, ret);
+  jreplace env.fns fn.Ast.name (params, ret);
   let finish () =
-    Hashtbl.remove env.fns fn.Ast.name;
+    jremove env.fns fn.Ast.name;
     env.lifted <- saved_lifted;
     env.tyvars <- saved_vars;
     env.tvpreds <- saved_preds;
@@ -15159,6 +15667,309 @@ and check_generic env (fn : Ast.fn) =
    | _ -> finish ()
    | exception e -> finish (); raise e)
 
+(* ── Return types read off the body ([_]) ────────────────────────────
+   Between the two passes: every written signature is in [fns], and a [defn]
+   whose return slot is [_] gets its entry here, from its own body and
+   nothing else — never a call site (docs/SPIKE-INFERENCE.md, "The cheap
+   first step"). Its parameters are written, so the body checks exactly as it
+   would with the type written, and the Tast is thrown away: pass two checks
+   the body again against the type found, which is what keeps literals and
+   [return]s coerced the way a written signature would coerce them.
+
+   One such body may call another, so the bodies are read callees first and
+   then to a fixpoint, the untyped-[defconst] loop's shape. A cycle among
+   them never settles and is refused by name; a body that calls its own name
+   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 — meet at
+   [arm_join], the function an [if]'s arms meet at, in any order: the typed
+   ones decide and the lone literals take their type; literals alone meet at
+   the wider of their own types. The body is then checked against that type
+   exactly as a written one would be, so whatever [if] refuses between its
+   arms is refused between exits, in the same words. None gives (); no value
+   beside a value is refused, since () does not take a value's place. *)
+and read_return env (fn : Ast.fn) params =
+  (* One check of the body against [ret], thrown away with everything it
+     wrote into [env] ([snapshot_env]); pass two checks it again for real. *)
+  let attempt ret =
+    let undo, _ = snapshot_env env in
+    let seen = !infer_seen in
+    infer_seen := [];
+    let restore () = undo (); infer_seen := seen in
+    match speculate env (fun () -> check_fn ~sign:(params, ret) env fn) with
+    | exception e -> restore (); raise e
+    | tf ->
+      let returns = List.rev !infer_seen in
+      restore ();
+      (tf, returns)
+  in
+  let tf, returns = attempt infer_ret in
+  let last =
+    match List.rev tf.Tast.body, List.rev fn.Ast.fbody with
+    | (x : Tast.expr) :: _, (a : Ast.expr) :: _ ->
+      [ (x.Tast.ty, x.Tast.loc, adapts a) ]
+    | (x : Tast.expr) :: _, [] -> [ (x.Tast.ty, x.Tast.loc, false) ]
+    | [], _ -> []
+  in
+  let arrive =
+    List.filter (fun (t, _, _) -> not (Types.equal t Types.Never)) (returns @ last)
+  in
+  let unit (t, _, _) = Types.equal t Types.Unit in
+  (match List.find_opt unit arrive, List.find_opt (fun x -> not (unit x)) arrive with
+   | Some (_, bare, _), Some (t, valued, _) ->
+     Loc.failk "check/infer-mixed" bare
+       ~notes:[ Loc.note valued ("this gives " ^ Types.to_string t) ]
+       "%s gives no value here and %s on another path, and its return \
+        type is read off its body. Give this path a value too, or write \
+        the return type"
+       fn.Ast.name (Types.to_string t)
+   | _ -> ());
+  match arrive with
+  | [] -> (Types.Unit, fn.Ast.nloc)
+  | (t, l, _) :: rest
+    when not (List.exists (fun (u, _, _) -> not (Types.equal t u)) rest) ->
+    (t, l)
+  | (t0, l0, _) :: _ ->
+    (* Where no join exists the first typed exit's type is the one checked
+       against, so the refusal is the one [if] gives its else arm. *)
+    let meet = function
+      | [] -> None
+      | ((t, l, _) :: _) as xs ->
+        let j =
+          List.fold_left
+            (fun acc (u, _, _) -> Option.bind acc (fun a -> arm_join a u))
+            (Some t) xs
+        in
+        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
+
+and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
+    (decls : Ast.decl list) =
+  let pending =
+    List.filter_map
+      (fun (d : Ast.decl) ->
+         match d.Ast.d with
+         | Ast.Defn ({ Ast.ret = Some { Ast.t = Ast.Tinfer; _ }; _ } as fn)
+           when not (Hashtbl.mem env.gsigs fn.Ast.name) ->
+           Some fn
+         | _ -> None)
+      decls
+  in
+  if pending <> [] then begin
+    let names = List.map (fun (fn : Ast.fn) -> fn.Ast.name) pending in
+    (* The other pending names each body mentions, with where. A local of
+       the same name is counted too, which only matters once the fixpoint
+       has stalled on a real error, and then only to pick which to show. *)
+    let calls (fn : Ast.fn) =
+      let acc = ref [] in
+      List.iter (Load.expr_uses acc) fn.Ast.fbody;
+      List.filter (fun (n, _) -> List.mem n names) (List.rev !acc)
+    in
+    let deps = List.map (fun (fn : Ast.fn) -> (fn.Ast.name, calls fn)) pending in
+    let byname = List.map (fun (fn : Ast.fn) -> (fn.Ast.name, fn)) pending in
+    (* Callees first, so a program with no cycle settles in one round. *)
+    let order =
+      let visited = Hashtbl.create 16 and out = ref [] in
+      let rec visit n =
+        if not (Hashtbl.mem visited n) then begin
+          Hashtbl.replace visited n ();
+          List.iter (fun (m, _) -> visit m) (List.assoc n deps);
+          out := List.assoc n byname :: !out
+        end
+      in
+      List.iter visit names;
+      List.rev !out
+    in
+    let params_of (fn : Ast.fn) =
+      List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
+    in
+    let settle (fn : Ast.fn) =
+      let params = params_of fn in
+      let ret, cause = read_return env fn params in
+      Hashtbl.replace env.fns fn.Ast.name (params, ret);
+      Hashtbl.replace env.inferred fn.Ast.name cause
+    in
+    (* A body [tolerate] excuses keeps the signature it was compiled with,
+       [previous]'s, the way pass two keeps its compiled body: it is a stale
+       caller, not a change. *)
+    (* A body that fails for its own reasons is left to pass two, which
+       reports its errors with every other body's. Until then it stands as
+       Never, which fits anywhere, so its callers are not refused for its
+       sake; a [_] body that calls it cannot be read either, and waits the
+       same way. *)
+    let failed = env.infer_failed in
+    let fail_quietly ?refusal (fn : Ast.fn) =
+      Hashtbl.replace failed fn.Ast.name refusal;
+      Hashtbl.replace env.fns fn.Ast.name (params_of fn, Types.Never)
+    in
+    (* Only while every error is collected: a check that stops at the first
+       reports this body's own, here. *)
+    let excused (fn : Ast.fn) =
+      match settle fn with
+      | () -> ()
+      | exception (Loc.Error d as e) ->
+        (match tolerate, previous fn.Ast.name with
+         | Some ok, Some (params, ret) when ok env fn.Ast.name d ->
+           Hashtbl.replace env.fns fn.Ast.name (params, ret)
+         | _ -> if keep_going then fail_quietly ~refusal:d fn else raise e)
+    in
+    let rec rounds left =
+      let still =
+        List.filter
+          (fun (fn : Ast.fn) ->
+             if List.exists (fun (m, _) -> Hashtbl.mem failed m)
+                  (List.assoc fn.Ast.name deps)
+             then begin fail_quietly fn; false end
+             else
+               match settle fn with
+               | () -> false
+               | exception Loc.Error _ -> true)
+          left
+      in
+      if still <> [] && List.length still < List.length left then rounds still
+      else still
+    in
+    (* A loop of [_] bodies that give no value on any way out — a
+       countdown that calls itself — is (): each is read with the others
+       taken as (), and kept only when every one of them gives () back. *)
+    let units stuck =
+      List.iter
+        (fun (fn : Ast.fn) ->
+           Hashtbl.replace env.fns fn.Ast.name (params_of fn, Types.Unit))
+        stuck;
+      let all_unit =
+        List.for_all
+          (fun (fn : Ast.fn) ->
+             match read_return env fn (params_of fn) with
+             | t, cause when Types.equal t Types.Unit ->
+               Hashtbl.replace env.inferred fn.Ast.name cause; true
+             | _ -> false
+             | exception Loc.Error _ -> false)
+          stuck
+      in
+      if not all_unit then
+        List.iter
+          (fun (fn : Ast.fn) ->
+             Hashtbl.remove env.fns fn.Ast.name;
+             Hashtbl.remove env.inferred fn.Ast.name)
+          stuck;
+      all_unit
+    in
+    let rec stalled left =
+      let stuck = rounds left in
+      if stuck <> [] then refuse stuck
+    and refuse stuck =
+      let stuck_names = List.map (fun (fn : Ast.fn) -> fn.Ast.name) stuck in
+      let waits n =
+        List.filter (fun (m, _) -> List.mem m stuck_names) (List.assoc n deps)
+      in
+      (* One that waits on nothing else stuck failed on its own body: check
+         it again, unswallowed, and its own error is the report. *)
+      (match List.find_opt (fun n -> waits n = []) stuck_names with
+       | Some n ->
+         excused (List.assoc n byname);
+         stalled (List.filter (fun (fn : Ast.fn) -> fn.Ast.name <> n) stuck)
+       | None ->
+         (* Every one waits on another, so following the first wait from
+            any of them comes back round: that loop is the cycle. *)
+         let rec walk path n =
+           if List.mem n path then
+             let rec from = function
+               | m :: rest when m = n -> m :: rest
+               | _ :: rest -> from rest
+               | [] -> []
+             in
+             from (List.rev path)
+           else walk (n :: path) (fst (List.hd (waits n)))
+         in
+         let cycle = walk [] (List.hd stuck_names) in
+         (* Told from the one written first, which is where a reader of the
+            file meets the loop. *)
+         let cycle =
+           let index n =
+             let rec at i = function
+               | [] -> max_int
+               | m :: rest -> if m = n then i else at (i + 1) rest
+             in
+             at 0 names
+           in
+           let start =
+             List.fold_left (fun a n -> if index n < index a then n else a)
+               (List.hd cycle) cycle
+           in
+           let rec rot = function
+             | m :: rest when m <> start -> rot (rest @ [ m ])
+             | l -> l
+           in
+           rot cycle
+         in
+         if units (List.map (fun n -> List.assoc n byname) cycle) then
+           stalled
+             (List.filter
+                (fun (fn : Ast.fn) -> not (List.mem fn.Ast.name cycle)) stuck)
+         else
+         let first = List.hd cycle in
+         let fn = List.assoc first byname in
+         let next i = List.nth cycle ((i + 1) mod List.length cycle) in
+         let notes =
+           List.mapi
+             (fun i n ->
+                let callee = next i in
+                let at = List.assoc callee (waits n) in
+                Loc.note at
+                  (if n = callee then n ^ " calls itself here"
+                   else Printf.sprintf "%s calls %s here" n callee))
+             cycle
+         in
+         (* Collected like any refusal when every error is: the loop's
+           first member carries it into pass two, the rest stand quietly. *)
+         match
+         (match cycle with
+          | [ n ] ->
+            Loc.failk "check/infer-recursive" fn.Ast.nloc ~notes
+              "%s calls itself, so its return type cannot be read off its \
+               body. Write the return type in its signature" n
+          | _ ->
+            Loc.failk "check/infer-recursive" fn.Ast.nloc ~notes
+              "%s call each other (%s), so %s of their return types can \
+               be read off their bodies. Write the return type of one of \
+               them in its signature"
+              (String.concat " and " cycle)
+              (String.concat " → " (cycle @ [ first ]))
+              (if List.length cycle = 2 then "neither" else "none"))
+         with
+         | () -> ()
+         | exception (Loc.Error d as e) ->
+           if not keep_going then raise e;
+           List.iter
+             (fun n ->
+                fail_quietly
+                  ?refusal:(if n = first then Some d else None)
+                  (List.assoc n byname))
+             cycle;
+           stalled
+             (List.filter
+                (fun (fn : Ast.fn) -> not (List.mem fn.Ast.name cycle)) stuck))
+    in
+    stalled order
+  end
+
 (* The knot from [instantiate]: a call site makes a copy, and making one is
    checking a function. *)
 let () = check_fn_ref := check_fn
@@ -16207,9 +17018,10 @@ let shadow_prelude (prelude : Ast.decl list) (decls : Ast.decl list) =
   in
   (prelude @ decls, warnings)
 
-let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
+let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) :
   Tast.program * env * string list =
   let env = new_env () in
+  Hashtbl.reset arm_failed;
   (* ── A declaration left as it was compiled ───────────────────────────
      A dev session installs a function whose signature changed, and a
      caller compiled against the old one is still in the running program and
@@ -16230,37 +17042,21 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
     match tolerate with
     | None -> f ()
     | Some ok ->
-      let lifted = env.lifted and instances = env.instances in
-      (* The generic-copy cache as well as the copies. A copy the failed body
-         asked for would otherwise stay cached, and the next body asking for
-         it would be handed the name of a copy the program does not have. *)
-      let insts =
-        Hashtbl.fold (fun g r acc -> (g, r, !r) :: acc) env.insts []
-      in
+      (* Everything the failed body wrote into [env] goes with it
+         ([snapshot_env]): a copy it asked for would otherwise stay cached,
+         and the next body asking for it would be handed the name of a copy
+         the program does not have. *)
+      let undo, keep = snapshot_env env in
       (match f () with
-       | x -> x
+       | x -> keep (); x
        | exception ((Loc.Error d | Loc.Errors (d :: _)) as e) ->
          if ok env name d then begin
-           Hashtbl.filter_map_inplace
-             (fun g r ->
-                match List.find_opt (fun (h, _, _) -> String.equal g h) insts with
-                | None ->
-                  List.iter (fun (_, _, sym) -> Hashtbl.remove env.fns sym) !r;
-                  None
-                | Some (_, _, before) ->
-                  List.iter
-                    (fun ((_, _, sym) as e) ->
-                       if not (List.memq e before) then Hashtbl.remove env.fns sym)
-                    !r;
-                  r := before;
-                  Some r)
-             env.insts;
-           env.lifted <- lifted;
-           env.instances <- instances;
+           undo ();
            tolerated := name :: !tolerated;
            None
          end
-         else raise e)
+         else (keep (); raise e)
+       | exception e -> keep (); raise e)
   in
   let decls, prelude_warnings =
     shadow_prelude (Parse.program (Prelude.forms ())) decls
@@ -16311,6 +17107,10 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
       (List.rev !pairing_warnings);
   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
@@ -16375,6 +17175,17 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
            (Loc.entry ~mark:'~' ~label:"warning: " d.Loc.dloc d.Loc.dmsg))
       (List.rev !grow_warnings);
   Loc.finish s;
+  (* The placeholder a [_] body is read against is never a type anything
+     downstream may see; a signature carrying it would be emitted as a
+     struct named _. *)
+  List.iter
+    (fun (f : Tast.fn) ->
+       if f.Tast.ret == infer_ret
+          || List.exists (fun t -> t == infer_ret) f.Tast.params
+       then
+         fail f.Tast.floc "internal: %s left the checker with its return \
+                           type unread" f.Tast.name)
+    fns;
   (* The handler clauses lifted out along the way. They are ordinary functions
      from here down; nothing in the backend knows they were written inside
      something else. *)
@@ -16434,8 +17245,9 @@ let program_with_env (decls : Ast.decl list) : Tast.program * env =
 (** The same, with [tolerate] deciding which body failures leave a
     declaration out rather than refuse it — see [build_program]. The names
     left out come back beside the program; nothing else about it changes. *)
-let program_tolerant ?(keep_going = false) ~tolerate (decls : Ast.decl list) =
-  build_program ~keep_going ~tolerate decls
+let program_tolerant ?(keep_going = false) ~tolerate ?previous
+    (decls : Ast.decl list) =
+  build_program ~keep_going ~tolerate ?previous decls
 
 let program (decls : Ast.decl list) : Tast.program =
   let p, _, _ = build_program ~keep_going:false decls in
@@ -16864,3 +17676,7 @@ let memory_sites ?file (p : Tast.program) : Loc.diag list =
        | false, true -> 1
        | _ -> Loc.before a.Loc.dloc b.Loc.dloc)
     (List.rev !found)
+
+(* The form that decided an inferred return type, for a name whose return
+   slot was [_]; [None] for one whose type was written. *)
+let inferred_cause env name = Hashtbl.find_opt env.inferred name
diff --git a/lib/cimport.ml b/lib/cimport.ml
index 266879f5..e1df2a27 100644
--- a/lib/cimport.ml
+++ b/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)
 
diff --git a/lib/dev.ml b/lib/dev.ml
index 028e350a..7bf0d8d6 100644
--- a/lib/dev.ml
+++ b/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,
diff --git a/lib/indent_printer.ml b/lib/indent_printer.ml
index 844f2dda..3e89aecd 100644
--- a/lib/indent_printer.ml
+++ b/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 ^ ") -> "
-         ^ ty ret ^ where_
+         i ^ (if d = "defn" then "fn " else "fn- ") ^ name ^ "(" ^ pt ^ ")"
+         (* [_] 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 ]
diff --git a/lib/indent_reader.ml b/lib/indent_reader.ml
index 13d6b434..9f29aebc 100644
--- a/lib/indent_reader.ml
+++ b/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
-      | _ ->
-        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
+      | NAME "->" -> ignore (advance p); let r = ty p in (r, text_of r)
+      | _ -> (sym rp.loc "_", ")")
     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))
diff --git a/lib/load.ml b/lib/load.ml
index 930fdda8..3c8be027 100644
--- a/lib/load.ml
+++ b/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) =
diff --git a/lib/parse.ml b/lib/parse.ml
index 4651dd4c..1d4ab27b 100644
--- a/lib/parse.ml
+++ b/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;
diff --git a/lib/session.ml b/lib/session.ml
index dc4683b5..fb8f54df 100644
--- a/lib/session.ml
+++ b/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) :
-  stale list =
-  let sigs = Hashtbl.create 64 in
+let stale_sites ?(live = SM.empty) ?(running = false)
+    ?(inferred = fun _ -> None) built (p : Tast.program) : stale list =
+  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 ──────────────────────────────────────── *)
 
diff --git a/lib/shim.ml b/lib/shim.ml
index e142a53a..395dedf7 100644
--- a/lib/shim.ml
+++ b/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
diff --git a/lib/tast.ml b/lib/tast.ml
index c6eda366..cba851e2 100644
--- a/lib/tast.ml
+++ b/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
diff --git a/spec-syntax.md b/spec-syntax.md
index 5f05b1ef..d4e741db 100644
--- a/spec-syntax.md
+++ b/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
-  different types give `dyn`; no value gives `()`.
+- the return type is the body's type; a `dyn` body gives `dyn`; the exits (the
+  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`
-  required until step 6; several predicates are `where p, q`.
+  becomes `where ordered?($t)` after the return type. **Built**; with no
+  `-> 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
-   `-> T`; omitting it is refused with a message saying inference is coming.
+   `if`, `dotimes`, …).
    **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
diff --git a/test/programs/arm-want.flan b/test/programs/arm-want.flan
new file mode 100644
index 00000000..58cf9dce
--- /dev/null
+++ b/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)
diff --git a/test/programs/dev-infer.flan b/test/programs/dev-infer.flan
new file mode 100644
index 00000000..25d39c7b
--- /dev/null
+++ b/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)))
diff --git a/test/programs/dyn-opened.flan b/test/programs/dyn-opened.flan
new file mode 100644
index 00000000..529b3db5
--- /dev/null
+++ b/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)
diff --git a/test/programs/dyn-tails.flan b/test/programs/dyn-tails.flan
new file mode 100644
index 00000000..dc73e56a
--- /dev/null
+++ b/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)
diff --git a/test/programs/trial-generic.flan b/test/programs/trial-generic.flan
new file mode 100644
index 00000000..9ae05f20
--- /dev/null
+++ b/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)
diff --git a/test/syntax/infer/main.flan b/test/syntax/infer/main.flan
new file mode 100644
index 00000000..02e896d7
--- /dev/null
+++ b/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)
diff --git a/test/syntax/infer/main.fln b/test/syntax/infer/main.fln
new file mode 100644
index 00000000..bdcfe51c
--- /dev/null
+++ b/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
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 7f36ed7b..f12aca6d 100644
--- a/test/test_acceptance.ml
+++ b/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"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 773d2303..c186c9dd 100644
--- a/test/test_flan.ml
+++ b/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 ()
diff --git a/test/test_session.ml b/test/test_session.ml
index 3fdda3f9..d0f5b417 100644
--- a/test/test_session.ml
+++ b/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
diff --git a/test/test_syntax.ml b/test/test_syntax.ml
index 611a2161..d56ff658 100644
--- a/test/test_syntax.ml
+++ b/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"