From ff88b9dad6075774b9f68f5baf2ab4380ef2d154 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Fri, 25 Sep 2026 17:09:13 +0700
Subject: [PATCH] A defn whose return slot is _ (or a .fln fn with no arrow)
 takes its return type from its own body, recursion through such functions is
 refused by name, and a stale caller of one is told which line changed its
 type

---
 TODO.org                     |   5 +
 emacs/flan.el                |   4 +
 lib/ast.ml                   |   5 +
 lib/check.ml                 | 316 +++++++++++++++++++++++++++++++++--
 lib/cimport.ml               |   1 +
 lib/dev.ml                   |   7 +-
 lib/indent_printer.ml        |   6 +-
 lib/indent_reader.ml         |  16 +-
 lib/load.ml                  |   2 +
 lib/parse.ml                 |  18 +-
 lib/session.ml               |  50 ++++--
 lib/shim.ml                  |   2 +
 spec-syntax.md               |  13 +-
 test/programs/dev-infer.flan |  20 +++
 test/syntax/infer/main.flan  |  27 +++
 test/syntax/infer/main.fln   |  28 ++++
 test/test_flan.ml            |  74 ++++++++
 test/test_session.ml         |  56 +++++++
 test/test_syntax.ml          |  12 +-
 19 files changed, 619 insertions(+), 43 deletions(-)
 create mode 100644 test/programs/dev-infer.flan
 create mode 100644 test/syntax/infer/main.flan
 create mode 100644 test/syntax/infer/main.fln

diff --git a/TODO.org b/TODO.org
index d2c3d726..728dd885 100644
--- a/TODO.org
+++ b/TODO.org
@@ -37,6 +37,11 @@ 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. Rules out use-directed inference.
+
 ** 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 614e91b2..ed118760 100644
--- a/emacs/flan.el
+++ b/emacs/flan.el
@@ -2448,6 +2448,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 bc5f0d67..9ec98ec4 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 array length is an integer or a compile-time constant's name. *)
 and len =
diff --git a/lib/check.ml b/lib/check.ml
index 9ca97cf7..0f1e68c4 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -211,6 +211,9 @@ 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;
 }
 
 let new_env () = {
@@ -243,6 +246,7 @@ let new_env () = {
   in_field = false;
   classes = Hashtbl.create 8;
   tracks = Hashtbl.create 16;
+  inferred = Hashtbl.create 8;
 }
 
 (* Where a named type was declared, and what it has, as a note.
@@ -1217,6 +1221,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, \
@@ -1557,7 +1568,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
   | _ -> ()
 
@@ -1632,6 +1643,13 @@ let pair_params ?(also = fun _ -> false) env (items : Ast.pitem list)
       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 ->
@@ -2023,6 +2041,7 @@ let signature_tyvars (fn : Ast.fn) =
        not over type constructors. A [$t] inside the arguments is ordinary. *)
     | Ast.Tapp (_, args) -> List.iter ty args
     | Ast.Tfn (_, ps, r) -> List.iter ty ps; ty r
+    | Ast.Tinfer -> ()
   in
   List.iter (fun (p : Ast.field) -> ty p.Ast.fty) fn.Ast.params;
   (match fn.Ast.ret with Some r -> ty r | None -> ());
@@ -3527,6 +3546,13 @@ 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 "_"
+let infer_seen : (Types.t * Loc.t) list ref = ref []
+
 let invented_ctx env ret =
   { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
     defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
@@ -4411,6 +4437,17 @@ 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 v = Option.map (check ctx) v in
+    infer_seen :=
+      (match v with
+       | Some (x : Tast.expr) -> (x.Tast.ty, loc)
+       | None -> (Types.Unit, loc))
+      :: !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
@@ -4549,6 +4586,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
@@ -12596,7 +12638,19 @@ let collect env (decls : Ast.decl list) =
            List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
          in
          let ret =
-           match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t
+           match fn.Ast.ret with
+           | 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
          env.tyvars <- [];
          env.tvpreds <- [];
@@ -12604,11 +12658,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)
          end
@@ -12770,8 +12827,10 @@ let check_union_members env =
 
 (* ── Declarations: pass 2, check bodies ────────────────────────────── *)
 
-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
   let ctx = { (invented_ctx env ret) with owner = fn.Ast.name } in
   List.iter2
     (fun (p : Ast.field) ty ->
@@ -12795,13 +12854,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
@@ -12838,6 +12900,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. *)
@@ -12908,6 +12972,233 @@ 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 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. *)
+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
+  in
+  match 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) ]
+      | [] -> []
+    in
+    let arrive =
+      List.filter
+        (fun (t, _) -> not (Types.equal t Types.Never))
+        (returns @ last)
+    in
+    (* Nothing boxes (), so a way out with no value beside one with a value
+       has no type to share — dyn included. *)
+    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 ->
+       (match List.find_opt (fun (u, _) -> not (Types.equal t u)) rest with
+        | None -> (t, l)
+        | Some (_, l') -> (Types.Dyn, l')))
+
+and infer_returns ?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
+    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. *)
+    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)
+         | _ -> raise e)
+    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
+         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
+         (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")))
+    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
@@ -13949,7 +14240,7 @@ 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
   (* ── A declaration left as it was compiled ───────────────────────────
@@ -14045,6 +14336,7 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
   let decls = collect env decls in
   check_finite env;
   check_union_members env;
+  infer_returns ?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
@@ -14144,8 +14436,8 @@ 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 ~tolerate (decls : Ast.decl list) =
-  build_program ~keep_going:false ~tolerate decls
+let program_tolerant ~tolerate ?previous (decls : Ast.decl list) =
+  build_program ~keep_going:false ~tolerate ?previous decls
 
 let program (decls : Ast.decl list) : Tast.program =
   let p, _, _ = build_program ~keep_going:false decls in
@@ -14537,3 +14829,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 9fea9ebe..4b47262e 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -416,6 +416,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 0f4e7e86..00c6700d 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -989,12 +989,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) ]
 
 let eval ?forms ?base ?(extra = []) t ~code ~origin ~pause =
diff --git a/lib/indent_printer.ml b/lib/indent_printer.ml
index eb3bfd38..84fbc811 100644
--- a/lib/indent_printer.ml
+++ b/lib/indent_printer.ml
@@ -577,8 +577,10 @@ and sugar n ~last (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 a5ea3a81..af77e655 100644
--- a/lib/indent_reader.ml
+++ b/lib/indent_reader.ml
@@ -1159,16 +1159,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
@@ -1201,7 +1197,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 70bb75cb..17c323c2 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -218,6 +218,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 }
 
@@ -802,6 +803,7 @@ let rec texpr_uses acc (t : Ast.texpr) =
   | Ast.Tmap (k, v) -> texpr_uses acc k; texpr_uses acc v
   | Ast.Tapp (_, args) -> List.iter (texpr_uses acc) args
   | Ast.Tfn (_, ps, r) -> List.iter (texpr_uses acc) ps; texpr_uses acc r
+  | Ast.Tinfer -> ()
 
 let rec expr_uses acc (e : Ast.expr) =
   let go = expr_uses acc in
diff --git a/lib/parse.ml b/lib/parse.ml
index e5190994..ba533003 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -88,6 +88,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
@@ -1498,12 +1499,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
@@ -1513,7 +1516,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 ──────────────────
@@ -1556,6 +1560,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 d79508bc..36642efd 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
@@ -969,7 +988,16 @@ let eval ?(origin = "<eval>") ?base ?forms ?pause ?(running = true) t src : chan
          t.built
   in
   let program, env, tolerated =
-    Check.program_tolerant ~tolerate:stale_owner decls
+    (* A tolerated body whose return type is read off it keeps the
+       signature the process has for it. *)
+    Check.program_tolerant ~tolerate:stale_owner
+      ~previous:(fun 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)
+      decls
   in
   let program =
     if tolerated = [] then program
@@ -1296,7 +1324,9 @@ let eval ?(origin = "<eval>") ?base ?forms ?pause ?(running = true) t src : chan
   { 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 c3070b04..26be806b 100644
--- a/lib/shim.ml
+++ b/lib/shim.ml
@@ -254,6 +254,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
 
diff --git a/spec-syntax.md b/spec-syntax.md
index c62dcd24..c3838ddf 100644
--- a/spec-syntax.md
+++ b/spec-syntax.md
@@ -232,8 +232,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.
@@ -315,8 +316,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:
@@ -358,6 +358,11 @@ Each step lands on its own, with `dune test --root .` green.
      (`ast.ml:491-492`).
 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). Two ways out of one body with a value on one and none on the
+   other are refused rather than made `dyn`, since `()` does not box. 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/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/syntax/infer/main.flan b/test/syntax/infer/main.flan
new file mode 100644
index 00000000..69dccae0
--- /dev/null
+++ b/test/syntax/infer/main.flan
@@ -0,0 +1,27 @@
+;; 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.
+
+(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 say [x i32] _ (println x))
+
+(defn- floor0 [x i32] _
+  (if (< x 0) (return 0) x))
+
+(defn main [] i32
+  (println (add 1 2))
+  (println (quarter 10.0))
+  (println (pick true))
+  (println (pick false))
+  (say 4)
+  (println (floor0 -3) (floor0 5))
+  0)
diff --git a/test/syntax/infer/main.fln b/test/syntax/infer/main.fln
new file mode 100644
index 00000000..6ce6975a
--- /dev/null
+++ b/test/syntax/infer/main.fln
@@ -0,0 +1,28 @@
+;; 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.
+
+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 say(x: i32) = println(x)
+
+fn- floor0(x: i32)
+  if x < 0 then return 0 else x
+
+fn main() -> i32
+  println(add(1, 2))
+  println(quarter(10.0))
+  println(pick(true))
+  println(pick(false))
+  say(4)
+  println(floor0(-3), floor0(5))
+  0
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 4d0f57f7..65da5f42 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -7078,4 +7078,78 @@ 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 "two types give dyn"
+     ("(defn f [c bool] _ (when c (return 1)) 2.5)" ^ main) "f" "f [bool] dyn";
+   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] _ (b n))\n(defn b [n i32] _ (c n))\n\
+     (defn c [n i32] _ (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 [] ())";
+  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 5af415c9..ffe2a9f9 100644
--- a/test/test_session.ml
+++ b/test/test_session.ml
@@ -1764,4 +1764,60 @@ 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");
+
   Test_support.report ~label:"session" ()
diff --git a/test/test_syntax.ml b/test/test_syntax.ml
index d8dc6426..70422f0f 100644
--- a/test/test_syntax.ml
+++ b/test/test_syntax.ml
@@ -83,6 +83,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 ->
@@ -286,7 +287,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)";
   (* Characters, lexed before brackets and separators. *)
   reads "character literals" "x = [\\( \\, \\space \\)]" "(set x [\\( \\, \\space \\)])";
   reads "character arguments" "f(\\,, \\))" "(f \\, \\))";
@@ -552,7 +556,11 @@ let run_both path want =
 let () =
   if Test_support.have "clang" then begin
     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\n2.5\n4\n0 5\n")
+      [ "syntax/infer/main.flan"; "syntax/infer/main.fln" ]
   end
   else print_endline "syntax: no clang, the import programs are not built"