diff --git a/TODO.org b/TODO.org
index 145ceafe..87c5a67c 100644
--- a/TODO.org
+++ b/TODO.org
@@ -40,7 +40,8 @@ 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. Rules out use-directed inference.
+cycle among =_= functions is refused by name unless it gives =()=. Rules out
+use-directed inference.
 
 ** DONE def, defonce and defconst are the three forms
 CLOSED: [2026-09-20]
diff --git a/lib/check.ml b/lib/check.ml
index 9c43282d..d149172d 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -214,6 +214,11 @@ type env = {
   (* 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, unit) 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
@@ -260,6 +265,7 @@ let new_env () = {
   classes = Hashtbl.create 8;
   tracks = Hashtbl.create 16;
   inferred = Hashtbl.create 8;
+  infer_failed = Hashtbl.create 4;
   recovering = false;
   recovered = [];
   poison = 0;
@@ -4479,7 +4485,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
@@ -11334,6 +11340,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. *)
@@ -13475,6 +13488,16 @@ 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 ->
@@ -13667,68 +13690,91 @@ and check_generic env (fn : Ast.fn) =
 
 (* The type one body gives, and the form that decided it: the last form and
    every [return], ignoring what never arrives. All alike give that type;
-   none gives (); any two that differ give dyn, decided by the first one to
-   differ. *)
+   none gives (). When they differ, each one's type is tried as the return
+   type the body is checked against, last form first, so a literal takes the
+   type of the other exits the way an [if]'s arms do; the first that checks
+   is the type. When none does, they meet in dyn. *)
 and read_return env (fn : Ast.fn) params =
-  let lifted = env.lifted and instances = env.instances in
-  let insts = Hashtbl.fold (fun g r acc -> (g, r, !r) :: acc) env.insts [] in
-  let seen = !infer_seen in
-  infer_seen := [];
-  let restore ~copies =
-    env.lifted <- lifted;
-    infer_seen := seen;
-    if copies then begin
-      (* A copy a failed read asked for goes with it, as [tolerant] does. *)
-      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.instances <- instances
-    end
+  (* One check of the body against [ret], thrown away: what it lifted goes,
+     and so do the copies it asked for if it failed, as [tolerant] does. *)
+  let attempt ret =
+    let lifted = env.lifted and instances = env.instances in
+    let insts = Hashtbl.fold (fun g r acc -> (g, r, !r) :: acc) env.insts [] in
+    let seen = !infer_seen in
+    infer_seen := [];
+    let restore ~copies =
+      env.lifted <- lifted;
+      infer_seen := seen;
+      if copies 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.instances <- instances
+      end
+    in
+    match speculate env (fun () -> check_fn ~sign:(params, ret) env fn) with
+    | exception e -> restore ~copies:true; raise e
+    | tf ->
+      let returns = List.rev !infer_seen in
+      restore ~copies:false;
+      (tf, returns)
   in
-  match speculate env (fun () -> check_fn ~sign:(params, infer_ret) env fn) with
-  | exception e -> restore ~copies:true; raise e
-  | tf ->
-    let returns = List.rev !infer_seen in
-    restore ~copies:false;
-    let last =
-      match List.rev tf.Tast.body with
-      | (x : Tast.expr) :: _ -> [ (x.Tast.ty, x.Tast.loc) ]
-      | [] -> []
+  let tf, returns = attempt infer_ret in
+  let last =
+    match List.rev tf.Tast.body with
+    | (x : Tast.expr) :: _ -> [ (x.Tast.ty, x.Tast.loc) ]
+    | [] -> []
+  in
+  let arrive =
+    List.filter (fun (t, _) -> not (Types.equal t Types.Never)) (returns @ last)
+  in
+  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)
+  | _ ->
+    let candidates =
+      List.fold_left
+        (fun acc (t, l) ->
+           if List.exists (fun (u, _) -> Types.equal t u) acc then acc
+           else acc @ [ (t, l) ])
+        [] (List.rev arrive)
     in
-    let arrive =
-      List.filter
-        (fun (t, _) -> not (Types.equal t Types.Never))
-        (returns @ last)
+    let fits (t, _) =
+      match attempt t with _ -> true | exception Loc.Error _ -> false
     in
-    (* Two types meet in dyn only if both box into it, and () and a struct
-       do not: said here, with both ways out, rather than as a boxing
-       refusal at one of them in pass two. *)
-    let boxes (t, _) =
-      match t with
-      | Types.Int _ | Types.Float _ | Types.Bool | Types.String | Types.Dyn ->
-        true
-      | _ -> false
-    in
-    (match arrive with
-     | (t0, _) :: _
-       when List.exists (fun (u, _) -> not (Types.equal t0 u)) arrive ->
+    (match List.find_opt fits candidates with
+     | Some found -> found
+     | None ->
+       (* Two types meet in dyn only if both box into it, and () and a
+          struct do not: said here, with both ways out, rather than as a
+          boxing refusal at one of them in pass two. *)
+       let boxes (t, _) =
+         match t with
+         | Types.Int _ | Types.Float _ | Types.Bool | Types.String
+         | Types.Dyn -> true
+         | _ -> false
+       in
        (match List.find_opt (fun x -> not (boxes x)) arrive with
         | Some (bad, at) ->
           let other, oloc =
             List.find (fun (u, _) -> not (Types.equal u bad)) arrive
           in
-          let notes = [ Loc.note oloc ("this gives " ^ Types.to_string other) ] in
+          let notes =
+            [ Loc.note oloc ("this gives " ^ Types.to_string other) ]
+          in
           if Types.equal bad Types.Unit then
             Loc.failk "check/infer-mixed" at ~notes
               "%s gives no value here and %s on another path, and its \
@@ -13743,16 +13789,12 @@ and read_return env (fn : Ast.fn) params =
                return type"
               fn.Ast.name (Types.to_string bad) (Types.to_string other)
               (Types.to_string bad)
-        | None -> ())
-     | _ -> ());
-    (match arrive with
-     | [] -> (Types.Unit, fn.Ast.nloc)
-     | (t, l) :: rest ->
-       (match List.find_opt (fun (u, _) -> not (Types.equal t u)) rest with
-        | None -> (t, l)
-        | Some (_, l') -> (Types.Dyn, l')))
+        | None ->
+          let t, _ = List.hd arrive in
+          let _, l' = List.find (fun (u, _) -> not (Types.equal t u)) arrive in
+          (Types.Dyn, l')))
 
-and infer_returns ?tolerate ?(previous = fun _ -> None) env
+and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
     (decls : Ast.decl list) =
   let pending =
     List.filter_map
@@ -13798,21 +13840,21 @@ and infer_returns ?tolerate ?(previous = fun _ -> None) env
       Hashtbl.replace env.fns fn.Ast.name (params, ret);
       Hashtbl.replace env.inferred fn.Ast.name cause
     in
-    let rec rounds left =
-      let still =
-        List.filter
-          (fun fn ->
-             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 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 (fn : Ast.fn) =
+      Hashtbl.replace failed fn.Ast.name ();
+      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
       | () -> ()
@@ -13820,7 +13862,49 @@ and infer_returns ?tolerate ?(previous = fun _ -> None) env
         (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)
-         | _ -> raise e)
+         | _ -> if keep_going then fail_quietly 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
@@ -13870,6 +13954,11 @@ and infer_returns ?tolerate ?(previous = fun _ -> None) env
            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
@@ -15051,7 +15140,7 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) :
       (List.rev !pairing_warnings);
   check_finite env;
   check_union_members env;
-  infer_returns ?tolerate ?previous env decls;
+  infer_returns ~keep_going ?tolerate ?previous env decls;
   let s = Loc.sink ~on:keep_going in
   ignore (Loc.caught s (fun () -> check_main env decls));
   (* Every generic body, checked once with its variables left abstract, and
diff --git a/spec-syntax.md b/spec-syntax.md
index 9b327b3e..0f2de937 100644
--- a/spec-syntax.md
+++ b/spec-syntax.md
@@ -363,7 +363,9 @@ Each step lands on its own, with `dune test --root .` green.
    slot, in a generic's, and in `defgeneric`/`defmulti`'s (`defmethod` has no
    return slot). Two ways out of one body whose types differ and cannot both
    box (a value and `()`, a number and a struct) are refused rather than made
-   `dyn`. A stale
+   `dyn`. Exits of different types are first tried at each other's type, so a
+   literal `return 0` beside an `i64` gives `i64`. 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`,
diff --git a/test/syntax/infer/main.flan b/test/syntax/infer/main.flan
index 69dccae0..b197b9ad 100644
--- a/test/syntax/infer/main.flan
+++ b/test/syntax/infer/main.flan
@@ -1,6 +1,8 @@
 ;; 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, two types
-;; (dyn), nothing (()), and a return that never falls off the end.
+;; main.fln. Each shape the rule has: one type, a call's type, a literal
+;; that takes the other exit's type, two types (dyn), 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))
 
@@ -12,16 +14,27 @@
   (when c (return 1))
   2.5)
 
+(defn label [c bool] _
+  (when c (return "yes"))
+  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))
+  (println (+ (pick true) 0.5))
   (println (pick false))
+  (println (label true) (label false))
   (say 4)
   (println (floor0 -3) (floor0 5))
+  (countdown 2)
   0)
diff --git a/test/syntax/infer/main.fln b/test/syntax/infer/main.fln
index 6ce6975a..8ade8d50 100644
--- a/test/syntax/infer/main.fln
+++ b/test/syntax/infer/main.fln
@@ -1,6 +1,8 @@
 ;; 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, two types
-;; (dyn), nothing (()), and a return that never falls off the end.
+;; main.flan. Each shape the rule has: one type, a call's type, a literal
+;; that takes the other exit's type, two types (dyn), 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
 
@@ -13,16 +15,28 @@ fn pick(c: bool)
     return 1
   2.5
 
+fn label(c: bool)
+  if c
+    return "yes"
+  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))
+  println(pick(true) + 0.5)
   println(pick(false))
+  println(label(true), label(false))
   say(4)
   println(floor0(-3), floor0(5))
+  countdown(2)
   0
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 5d255063..b3c2a9e3 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -7320,8 +7320,19 @@ let () =
      ("(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 "two types give dyn"
-     ("(defn f [c bool] _ (when c (return 1)) 2.5)" ^ main) "f" "f [bool] dyn";
+     ("(defn f [c bool] _ (when c (return \"s\")) 2)" ^ main) "f" "f [bool] dyn";
+   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 [] ()";
@@ -7341,8 +7352,8 @@ let () =
      (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] _ (b n))\n(defn b [n i32] _ (c n))\n\
-     (defn c [n i32] _ (a n))\n(defn main [] ())";
+    "(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\
@@ -7357,6 +7368,31 @@ let () =
     ~needle:"f gives P here and i32 on another path"
     "(defstruct P [x i32])\n\
      (defn f [c bool] _ (when c (return (P {.x 1}))) 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);
   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 [] ())";
diff --git a/test/test_syntax.ml b/test/test_syntax.ml
index 429a0afb..4f6414f6 100644
--- a/test/test_syntax.ml
+++ b/test/test_syntax.ml
@@ -564,7 +564,7 @@ let () =
     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\n2.5\n4\n0 5\n")
+      (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"