diff --git a/lib/check.ml b/lib/check.ml
index d149172d..94812188 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -218,7 +218,7 @@ type env = {
      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;
+  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
@@ -3690,7 +3690,7 @@ let hash_ty = Types.Int Types.U64
    address, so no type written anywhere is ever mistaken for it. What each
    [return] in that body gives is pushed on [infer_seen]. *)
 let infer_ret = Types.Named "_"
-let infer_seen : (Types.t * Loc.t) list ref = ref []
+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 }
@@ -4788,11 +4788,12 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
       (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 -> lone_literal 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)
-       | None -> (Types.Unit, loc))
+       | 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)
@@ -13644,6 +13645,15 @@ let rec check_fn ?sign env (fn : Ast.fn) : Tast.fn =
        | None -> ctx.defers
        | Some s -> guarded_defers s ctx.defers);
     fenv = None; fparent = None; floc = fn.Ast.nloc }
+  |> fun (tf : Tast.fn) ->
+  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)
+    | _ -> { tf with Tast.ret = Types.Never }
+  else tf
 
 (* The generic body, checked once with its variables abstract. Nothing is kept
    — the [Tast.fn] it produces is thrown away, and so is anything it lifted —
@@ -13688,12 +13698,15 @@ and check_generic env (fn : Ast.fn) =
    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 last form and
-   every [return], ignoring what never arrives. All alike give that type;
-   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. *)
+(* The type one body gives, and the form that decided it. The exits — the
+   last form and every [return], less what never arrives — combine the way
+   an [if]'s arms do ([check_if_once]): the first one that is not a lone
+   literal decides and the literals take its type, a bool meets a dyn at
+   dyn, and 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: what it lifted goes,
      and so do the copies it asked for if it failed, as [tolerant] does. *)
@@ -13732,67 +13745,48 @@ and read_return env (fn : Ast.fn) params =
   in
   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) ]
-    | [] -> []
+    match List.rev tf.Tast.body, List.rev fn.Ast.fbody with
+    | (x : Tast.expr) :: _, (a : Ast.expr) :: _ ->
+      [ (x.Tast.ty, x.Tast.loc, lone_literal 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)
+    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, _) :: 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)
+  | (t0, l0, _) :: _ ->
+    let decided =
+      match List.filter (fun (_, _, lit) -> not lit) arrive with
+      | (Types.Bool, l, _) :: others
+        when List.exists (fun (u, _, _) -> Types.equal u Types.Dyn) others ->
+        (Types.Dyn, l)
+      | (t, l, _) :: _ -> (t, l)
+      | [] ->
+        let joined =
+          List.fold_left
+            (fun acc (u, _, _) ->
+               match acc with Some a -> Types.join a u | None -> None)
+            (Some t0) arrive
+        in
+        (Option.value joined ~default:t0, l0)
     in
-    let fits (t, _) =
-      match attempt t with _ -> true | exception Loc.Error _ -> false
-    in
-    (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
-          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 \
-               return type is read off its body. Give this path a value \
-               too, or write the return type"
-              fn.Ast.name (Types.to_string other)
-          else
-            Loc.failk "check/infer-mixed" at ~notes
-              "%s gives %s here and %s on another path, and its return type \
-               is read off its body. Two types meet only in dyn, and %s does \
-               not box into it. Give every path one type, or write the \
-               return type"
-              fn.Ast.name (Types.to_string bad) (Types.to_string other)
-              (Types.to_string bad)
-        | None ->
-          let t, _ = List.hd arrive in
-          let _, l' = List.find (fun (u, _) -> not (Types.equal t u)) arrive in
-          (Types.Dyn, l')))
+    ignore (attempt (fst decided));
+    decided
 
 and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
     (decls : Ast.decl list) =
@@ -13849,8 +13843,8 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
        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 ();
+    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
@@ -13862,7 +13856,7 @@ and infer_returns ~keep_going ?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)
-         | _ -> if keep_going then fail_quietly fn else raise e)
+         | _ -> if keep_going then fail_quietly ~refusal:d fn else raise e)
     in
     let rec rounds left =
       let still =
@@ -13972,6 +13966,9 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
                    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
@@ -13984,7 +13981,20 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
                them in its signature"
               (String.concat " and " cycle)
               (String.concat " → " (cycle @ [ first ]))
-              (if List.length cycle = 2 then "neither" else "none")))
+              (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
@@ -15199,6 +15209,17 @@ let build_program ~keep_going ?tolerate ?previous (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. *)
diff --git a/spec-syntax.md b/spec-syntax.md
index 0f2de937..050bdfd8 100644
--- a/spec-syntax.md
+++ b/spec-syntax.md
@@ -54,8 +54,10 @@ warns about; the new syntax must not inherit it.
 
 **The return type is inferred when omitted.** Body-local only, as
 `docs/SPIKE-INFERENCE.md` ("The cheap first step" and "Verdict") scopes it:
-- the return type is the body's type; a `dyn` body gives `dyn`; `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`) combine exactly as an `if`'s arms do, so a
+  literal takes the other exits' type and what `if` refuses is refused; no
+  value gives `()`.
 - it reads only the function's own body, never a call site.
 - a self-recursive or mutually recursive function must write its return type.
   Refuse by name, naming the whole cycle. The corpus has 17 self-recursive
@@ -361,11 +363,9 @@ Each step lands on its own, with `dune test --root .` green.
    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). 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`. 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
+   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`,
diff --git a/test/syntax/infer/main.flan b/test/syntax/infer/main.flan
index b197b9ad..02e896d7 100644
--- a/test/syntax/infer/main.flan
+++ b/test/syntax/infer/main.flan
@@ -1,6 +1,6 @@
 ;; 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, two types (dyn), nothing (()), a return
+;; 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.
 
@@ -14,8 +14,8 @@
   (when c (return 1))
   2.5)
 
-(defn label [c bool] _
-  (when c (return "yes"))
+(defn label [c bool d dyn] _
+  (when c (return d))
   0)
 
 (defn say [x i32] _ (println x))
@@ -33,7 +33,7 @@
   (println (quarter 10.0))
   (println (+ (pick true) 0.5))
   (println (pick false))
-  (println (label true) (label false))
+  (println (label true "yes") (label false "yes"))
   (say 4)
   (println (floor0 -3) (floor0 5))
   (countdown 2)
diff --git a/test/syntax/infer/main.fln b/test/syntax/infer/main.fln
index 8ade8d50..bdcfe51c 100644
--- a/test/syntax/infer/main.fln
+++ b/test/syntax/infer/main.fln
@@ -1,6 +1,6 @@
 ;; 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, two types (dyn), nothing (()), a return
+;; 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.
 
@@ -15,9 +15,9 @@ fn pick(c: bool)
     return 1
   2.5
 
-fn label(c: bool)
+fn label(c: bool, d)
   if c
-    return "yes"
+    return d
   0
 
 fn say(x: i32) = println(x)
@@ -35,7 +35,7 @@ fn main() -> i32
   println(quarter(10.0))
   println(pick(true) + 0.5)
   println(pick(false))
-  println(label(true), label(false))
+  println(label(true, "yes"), label(false, "yes"))
   say(4)
   println(floor0(-3), floor0(5))
   countdown(2)
diff --git a/test/test_flan.ml b/test/test_flan.ml
index b3c2a9e3..ea94d0d5 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -7326,8 +7326,12 @@ let () =
      ("(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 \"s\")) 2)" ^ main) "f" "f [bool] dyn";
+   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";
+   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 ()"
@@ -7364,10 +7368,6 @@ let () =
   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 [] ())";
-  rejects_check "a struct on one path and a number on another"
-    ~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 =
@@ -7392,7 +7392,30 @@ let () =
    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);
+      (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 an i64 exit, as if refuses them"
+    ~needle:"expected i32, found i64"
+    "(defn f [x i32 y i64 c bool] _ (when c (return x)) y)\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 "some under an inferred return"
     ~needle:"Write the return type: (Option T)"
     "(defn f [o (Option i32)] _ (+ 1 (some o)))\n(defn main [] ())";