diff --git a/TODO.org b/TODO.org
index 1f983138..3aea9494 100644
--- a/TODO.org
+++ b/TODO.org
@@ -31,13 +31,17 @@ crossing, a dyn big int for u64, and any check in a release build.
 ** NEXT Dyn unless annotated
 Decided 2026-09-26, replacing the plain rule: number, bool and char literals are typed,
 their type inferred from their uses inside the function (never across functions); an
-unconstrained integer literal is int (i32) and a float literal float (f32); uses that
+unconstrained integer literal is int (i32) and a float literal f64 (decision 121); uses that
 disagree are refused with a request for an annotation. Vector, map and text literals
 are dyn unless something typed wants them. A typed value is boxed where it goes into
 dyn, and a dyn unboxed (checked) where typed code needs it; typed beside dyn in an
 operator gives dyn. Dyn integers stay i64 and dyn floats f64.
-Done: local inference (check.ml [lit_session]), the f32 float default, an integer and a
-float literal meeting at the float. Waiting: text and vector literals dyn by default, on
+Decision 121: f64 and not f32, because f32 locals lost precision silently — 0.1 summed a
+million times printed 100958. A float literal is f32 only where inference finds typed code
+wanting f32 (a parameter, field, return or operand). A literal local fed only by dyn takes
+the dyn width, i64 or f64.
+Done: local inference (check.ml [lit_session]), an integer and a float literal meeting
+at the float. Waiting: text and vector literals dyn by default, on
 dyn text to str and dyn vec to slice conversion (a lane after views); =FLAN_LIT=dyn=
 measures it, and under it a let-bound one some typed use wants already stays typed.
 ** DONE Dynamic-first, and the dyn half of the language
diff --git a/emacs/test-flan.el b/emacs/test-flan.el
index 39fd3406..7712e455 100644
--- a/emacs/test-flan.el
+++ b/emacs/test-flan.el
@@ -1891,9 +1891,9 @@ already rely on it — so nothing here is a stand-in for the real thing."
           (test-flan--check "a generic's IR is shown copy by copy"
                             (and (string-match-p "\\`; LLVM IR for selection-sort, one copy" text)
                                  (string-match-p "^;; selection-sort at \\$t = i32$" text)
-                                 (string-match-p "^;; selection-sort at \\$t = f32$" text)
+                                 (string-match-p "^;; selection-sort at \\$t = f64$" text)
                                  (string-match-p "^define .*flan\\.selection-sort-i32" text)
-                                 (string-match-p "^define .*flan\\.selection-sort-f32" text)))
+                                 (string-match-p "^define .*flan\\.selection-sort-f64" text)))
           (test-flan--check "each copy names the file the generic was sent from"
                             (string-match-p (regexp-quote file) text)))))
 
diff --git a/lib/check.ml b/lib/check.ml
index 9b5c0747..4f009b3d 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -746,13 +746,14 @@ type lentry =
   | Lbarrier of string
 
 (* Local inference for a number or character literal bound by a [let] or a
-   [loop]: [(let [t 0.0] ... (set t (+ t x)))] makes [t] x's type. The uses
-   are read by checking the form once with the literal locals at their current
-   guess and every hook below recording instead of refusing, then undoing that
-   check; the guesses are solved, and the form is checked for real. A guess
-   that moved is checked again, at most [lit_rounds] times, so a local fed by
-   another settles. One session per function context, opened by its outermost
-   such [let], so a lambda or a generic's copy is inferred on its own and a
+   [loop]: [(let [t 0.0] ... (set t (+ t x)))] makes [t] x's type. The form
+   is checked with every literal local at its current guess while each use
+   records what it says about the local. When the uses agree with the
+   guesses that check is the answer; otherwise it is undone, the guesses are
+   solved and it is checked again. Locals that feed one another are merged
+   into one group (union-find), so a chain of any length settles in one more
+   round. One session per function context, opened by its outermost such
+   [let], so a lambda or a generic's copy is inferred on its own and a
    literal's type never depends on another function.
 
    What a use says about the local:
@@ -760,20 +761,35 @@ type lentry =
      index. The local has to widen into [t].
    - [Down t]: a [t] is [set] into it, or passed to [recur] for it. [t] has to
      widen into the local.
-   - [Hint t]: an operator's other operand, which meets it at either.
-   A [set] of one such local into another links the two, and a group of
-   linked locals takes one type. *)
+   - [Hint t]: an operator's other operand, which meets it at either; or a
+     dyn it meets, as the dyn width ([Types.Dyn] here, i64 or f64 in [solve]).
+   A [set] of arithmetic over such locals and literals into another merges
+   them, as does an operator between two of them. *)
 type lit_con = Up | Down | Hint
 
+(* Initialiser nodes by identity: two expansions of one macro are two nodes
+   and may print alike. *)
+module Phys = Hashtbl.Make (struct
+  type t = Ast.expr
+  let equal = ( == )
+  let hash = Hashtbl.hash
+end)
+
 type lit_session = {
-  (* The type each literal local is checked at, by its initialiser's node. *)
-  mutable decided : (Ast.expr * Types.t) list;
-  (* On during the recording check and off for the real one. *)
+  (* The type each literal local is checked at. Kept across rounds. *)
+  decided : Types.t Phys.t;
+  (* On while a round checks; off for a final check after one that failed. *)
   mutable recording : bool;
-  mutable cons : (Ast.expr * (lit_con * Types.t * Loc.t)) list;
-  mutable links : (Ast.expr * Ast.expr) list;
-  (* Each literal local the recording check bound, with its name. *)
-  mutable seen : (Ast.expr * string) list;
+  (* This round's locals, numbered as they are bound, and their names. *)
+  ids : int Phys.t;
+  mutable keys : (Ast.expr * string) list;
+  mutable count : int;
+  (* Union-find over the numbers, and each one's uses. *)
+  parent : (int, int) Hashtbl.t;
+  cons : (int, lit_con * Types.t * Loc.t) Hashtbl.t;
+  (* A use its guess could not serve was read at the type it asked for, so
+     this round's check is not a program and is thrown away. *)
+  mutable dirty : bool;
 }
 
 (* Nonzero while any recording check runs: the refusal memos ([arm_failed],
@@ -781,9 +797,15 @@ type lit_session = {
    at a guessed type must not be replayed at the decided one. *)
 let lit_recording = ref 0
 
-(* Set around the one check of an operator's operand that is a literal local,
-   so its use is recorded as a [Hint] and not an [Up]. *)
-let lit_hint = ref false
+(* The operands of the operators being checked that are literal locals, by
+   location: a want reaching one is the other operand's type, a [Hint] and not
+   an [Up], and a refusal there is the operator's to handle. *)
+let lit_operand_locs : Loc.t list ref = ref []
+
+(* Set while arithmetic over literal locals is checked at the type of the
+   local it is stored into ([lit_down]): the locals in it are merged with that
+   one, so the guess it is checked at says nothing about them. *)
+let lit_quiet = ref false
 
 (* Text and bracket literals keep their typed reading while this is set (the
    [dyn] switch only): a [defconst]'s value, and a let-bound one some typed
@@ -3663,8 +3685,9 @@ let dyn_f64 = Types.Float Types.F64
    that half lands. *)
 let lit_mode = try Sys.getenv "FLAN_LIT" with Not_found -> ""
 let lit_has m = List.mem m (String.split_on_char ',' lit_mode)
-(* An unconstrained float literal is an f32, as an integer one is an i32. *)
-let float_default () = Types.F32
+(* An unconstrained float literal is an f64 (decision 121); it is an f32 only
+   where typed code wants one. *)
+let float_default () = Types.F64
 
 (* ── Literal locals ([lit_session]) ────────────────────────────────── *)
 
@@ -3685,7 +3708,7 @@ let lit_kind (e : Ast.expr) =
 (* A text or bracket literal ([`Box]) is dyn, or with a typed use its typed
    reading; [Types.Unit] stands for "typed" in [decided], since the typed
    reading is the literal's own and not one a use names. *)
-let lit_default = function
+let lit_default (_ : Ast.expr) = function
   | `Int -> Types.Int Types.I32
   | `Char -> Types.Int Types.U8
   | `Float -> Types.Float (float_default ())
@@ -3704,78 +3727,121 @@ let lit_admits kind (t : Types.t) =
   | `Box, t -> not (Types.equal t Types.Dyn)
   | _ -> false
 
-let lit_rounds = 3
+(* The rounds a session may take before its last guesses are checked as
+   they stand. Merging makes two the usual count; the bound only stops a
+   pathological program from looping. *)
+let lit_rounds = 8
 
-(* Every literal local the recording check bound, with the type the uses
-   decide for it, and the first pair of uses that no one type satisfies. *)
-let lit_solve (s : lit_session) =
-  let keys =
-    List.fold_left
-      (fun acc (k, n) -> if List.exists (fun (k', _) -> k' == k) acc then acc else (k, n) :: acc)
-      [] s.seen
-  in
-  (* The linked group of [k]: a [set] of one literal local into another. *)
-  let group k =
-    let rec go seen = function
-      | [] -> seen
-      | k :: rest when List.memq k seen -> go seen rest
-      | k :: rest ->
-        let next =
-          List.filter_map
-            (fun (a, b) -> if a == k then Some b else if b == k then Some a else None)
-            s.links
-        in
-        go (k :: seen) (next @ rest)
+let lit_id (s : lit_session) (key : Ast.expr) = Phys.find_opt s.ids key
+
+let rec lit_root (s : lit_session) i =
+  match Hashtbl.find_opt s.parent i with
+  | Some p when p <> i ->
+    let r = lit_root s p in
+    Hashtbl.replace s.parent i r;
+    r
+  | _ -> i
+
+let lit_add (s : lit_session) key c =
+  match lit_id s key with Some i -> Hashtbl.add s.cons i c | None -> ()
+
+let lit_union (s : lit_session) a b =
+  match lit_id s a, lit_id s b with
+  | Some i, Some j ->
+    let ri = lit_root s i and rj = lit_root s j in
+    if ri <> rj then Hashtbl.replace s.parent (max ri rj) (min ri rj)
+  | _ -> ()
+
+(* What earlier sessions decided, while an outermost one is open. An outer
+   session that checks its form again checks every lambda inside it again,
+   and each of those opens a session of its own; starting that one from its
+   last answer makes it settle in one round, where starting from the default
+   made nested lambdas cost a factor per level. Keyed by the node and the
+   type variables' bindings, since a generic's body is one node checked at
+   several types. Only ever a first guess: a wrong one costs a round. *)
+let lit_depth = ref 0
+let lit_memo : ((string * Types.t) list * Types.t) list Phys.t = Phys.create 64
+
+let lit_guess ~subst (s : lit_session) key kind =
+  match Phys.find_opt s.decided key with
+  | Some t -> t
+  | None ->
+    let same (sb, _) =
+      List.equal (fun (a, t) (b, u) -> String.equal a b && Types.equal t u) sb subst
     in
-    go [] [ k ]
-  in
+    match Option.bind (Phys.find_opt lit_memo key) (List.find_opt same) with
+    | Some (_, t) -> t
+    | None -> lit_default key kind
+
+(* Each literal local this round bound, with the type its group's uses decide
+   or the first pair of uses no one type satisfies. Linear in locals and
+   uses. *)
+let lit_solve (s : lit_session) =
+  let keys = Array.of_list (List.rev s.keys) in
+  let n = Array.length keys in
+  let root = Array.init n (lit_root s) in
+  let members = Array.make n [] in
+  for i = n - 1 downto 0 do members.(root.(i)) <- i :: members.(root.(i)) done;
   let widens a b = Types.equal a b || Types.widens_to ~from:a ~into:b in
-  List.map
-    (fun (k, name) ->
-       let members = List.filter (fun m -> List.exists (fun (k', _) -> k' == m) keys) (group k) in
-       let kind =
-         if lit_kind k = Some `Box then `Box
-         else if List.exists (fun m -> lit_kind m = Some `Float) members then `Float
-         else Option.value (lit_kind k) ~default:`Int
-       in
-       let cons =
-         List.filter_map
-           (fun (k', c) -> if List.memq k' members then Some c else None)
-           s.cons
-         |> List.filter (fun (_, t, _) -> lit_admits kind t)
-         |> List.rev
-       in
-       let pick c = List.filter_map (fun (c', t, l) -> if c' = c then Some (t, l) else None) cons in
-       if kind = `Box then (k, name, Ok (if cons = [] then Types.Dyn else Types.Unit)) else
-       let ups = pick Up and downs = pick Down and hints = pick Hint in
-       let res =
-         match ups with
-         | (u0, l0) :: _ ->
-           (match List.find_opt (fun (u, _) -> List.for_all (fun (u', _) -> widens u u') ups) ups with
-            | None ->
-              let (u1, l1) =
-                List.find (fun (u, _) -> not (widens u u0 || widens u0 u)) ups
-              in
-              Error ((u0, l0), (u1, l1))
-            | Some (c, lc) ->
-              (match List.find_opt (fun (d, _) -> not (widens d c)) downs with
-               | None -> Ok c
-               | Some (d, ld) -> Error ((c, lc), (d, ld))))
-         | [] ->
-           (match downs @ hints with
-            | [] -> Ok (lit_default kind)
-            | (t0, l0) :: rest ->
-              let rec fold (t, l) = function
-                | [] -> Ok t
-                | (t', l') :: rest ->
-                  (match Types.join t t' with
-                   | Some j -> fold ((j, if Types.equal j t then l else l')) rest
-                   | None -> Error ((t, l), (t', l')))
-              in
-              fold (t0, l0) rest)
-       in
-       (k, name, res))
-    keys
+  let result = Array.make n (Ok Types.Unit) in
+  Array.iteri
+    (fun r ms ->
+       if ms <> [] then begin
+         let kinds = List.map (fun m -> Option.value (lit_kind (fst keys.(m))) ~default:`Int) ms in
+         let kind =
+           if List.mem `Box kinds then `Box
+           else if List.mem `Float kinds then `Float
+           else if List.mem `Int kinds then `Int
+           else `Char
+         in
+         let dyn_width =
+           match kind with `Float -> Types.Float Types.F64 | _ -> Types.Int Types.I64
+         in
+         let cons =
+           List.concat_map (fun m -> List.rev (Hashtbl.find_all s.cons m)) ms
+           |> List.filter_map (fun (c, t, l) ->
+               if kind <> `Box && Types.equal t Types.Dyn then Some (Hint, dyn_width, l)
+               else if lit_admits kind t then Some (c, t, l)
+               else None)
+         in
+         let pick c = List.filter_map (fun (c', t, l) -> if c' = c then Some (t, l) else None) cons in
+         let res =
+           if kind = `Box then Ok (if cons = [] then Types.Dyn else Types.Unit)
+           else
+             let ups = pick Up and downs = pick Down and hints = pick Hint in
+             match ups with
+             | (u0, l0) :: _ ->
+               (match List.find_opt (fun (u, _) -> List.for_all (fun (u', _) -> widens u u') ups) ups with
+                | None ->
+                  let (u1, l1) = List.find (fun (u, _) -> not (widens u u0 || widens u0 u)) ups in
+                  Error ((u0, l0), (u1, l1))
+                | Some (c, lc) ->
+                  (match List.find_opt (fun (d, _) -> not (widens d c)) downs with
+                   | None -> Ok c
+                   | Some (d, ld) -> Error ((c, lc), (d, ld))))
+             | [] ->
+               (match downs @ hints with
+                | [] ->
+                  (* No use names a type: the widest of the members' own. *)
+                  Ok (List.fold_left
+                        (fun acc m ->
+                           let t = lit_default (fst keys.(m)) kind in
+                           match Types.join acc t with Some j -> j | None -> acc)
+                        (lit_default (fst keys.(r)) kind) ms)
+                | (t0, l0) :: rest ->
+                  let rec fold (t, l) = function
+                    | [] -> Ok t
+                    | (t', l') :: rest ->
+                      (match Types.join t t' with
+                       | Some j -> fold ((j, if Types.equal j t then l else l')) rest
+                       | None -> Error ((t, l), (t', l')))
+                  in
+                  fold (t0, l0) rest)
+         in
+         List.iter (fun m -> result.(m) <- res) ms
+       end)
+    members;
+  Array.to_list (Array.mapi (fun i (k, name) -> (k, name, result.(i))) keys)
 
 (* Converting to whatever width the other side of the boundary wants, with a
    [Cast] and not a silent reinterpretation. The name is for the direction it
@@ -5915,12 +5981,17 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
           (tyname loc other) x
       | _ -> float_default ()
     in
-    (* Past f32's largest value the literal would be infinity, silently. *)
-    if k = Types.F32 && Float.is_finite x && Float.abs x > 3.4028234663852886e38 then
-      Loc.failk literal_at_want loc
-        "%g does not fit in f32, whose largest value is about 3.4e38. Write \
-         %s"
-        x (if fln_source loc then Printf.sprintf "f64(%g)" x else Printf.sprintf "(f64 %g)" x);
+    (* Where f32 is wanted, a literal past its range would be infinity or 0,
+       silently. *)
+    (if k = Types.F32 && Float.is_finite x && x <> 0.0 then
+       let f = Int32.float_of_bits (Int32.bits_of_float x) in
+       if Float.is_integer f && f = 0.0 then
+         Loc.failk literal_at_want loc
+           "%g is too small for f32, which rounds it to 0 — the smallest \
+            f32 above 0 is about 1.4e-45" x
+       else if not (Float.is_finite f) then
+         Loc.failk literal_at_want loc
+           "%g does not fit in f32, whose largest value is about 3.4e38" x);
     mk loc (Types.Float k) (Tast.Float (x, k))
   | Ast.Str s when want = None && lit_has "dyn" && not !typed_literals -> box loc (mk loc Types.String (Tast.Str s))
   | Ast.Str s -> expect ctx loc ~want (mk loc Types.String (Tast.Str s))
@@ -6331,6 +6402,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
     if ctx.in_defer then
       fail loc
         "invoke-restart is not allowed inside a defer";
+    let written = args in
     let args = map_lr (fun a -> check ctx a) args in
     List.iter
       (fun (a : Tast.expr) ->
@@ -6342,6 +6414,22 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
          | _ -> ())
       args;
     let sg = restart_sig (List.map (fun (a : Tast.expr) -> a.Tast.ty) args) in
+    (* What the run-time refusal needs to write its fix, after the signature
+       and a 0x1f: the syntax (i indented, p parenthesised), then each
+       argument as written, or x. Only the message reads past the 0x1f; the
+       comparison is on [type_id sg]. *)
+    let said =
+      let spell (a : Ast.expr) =
+        match a.Ast.e with
+        | Ast.Float x ->
+          let t = Printf.sprintf "%g" x in
+          if String.exists (fun c -> c = '.' || c = 'e' || c = 'n' || c = 'i') t
+          then t else t ^ ".0"
+        | _ -> spell_arg "x" a
+      in
+      String.concat "\x1f"
+        (sg :: (if fln_source loc then "i" else "p") :: List.map spell written)
+    in
     (* Evaluated into slots first, so that an argument which transfers on its
        own is guarded before this form aims the channel, and so that a call
        written in an argument is on the ordinary walk rather than hidden
@@ -6356,7 +6444,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
     in
     let invoke =
       mk loc Types.Never
-        (Tast.InvokeRestart (type_id name, name, locals, sg, type_id sg, loc))
+        (Tast.InvokeRestart (type_id name, name, locals, said, type_id sg, loc))
     in
     expect ctx loc ~want
       (if binds = [] then invoke
@@ -6578,17 +6666,25 @@ and var ctx ?(qualified = false) loc ~want name =
        defn to pass that" builtin_prefix name name builtin_prefix name
   | _ ->
     match lookup ctx name with
-    (* A literal local while its uses are being recorded: the use is noted
-       and read at the type it asks for, so the recording check goes on past
-       a use its guess would have refused. That check is thrown away. *)
+    (* A literal local while its uses are being recorded: the use is noted.
+       One its guess cannot serve is read at the type it asks for, so the
+       check goes on to the uses after it, and the round is marked to be
+       thrown away. A dyn want says the dyn width ([lit_solve]). *)
     | Some ({ blit = Some key; _ } as b)
       when (match ctx.lits, want with
-            | Some s, Some t -> s.recording && lit_admits (Option.value (lit_kind key) ~default:`Int) t
+            | Some s, Some t ->
+              s.recording && not !lit_quiet
+              && (Types.equal t Types.Dyn
+                  || lit_admits (Option.value (lit_kind key) ~default:`Int) t)
             | _ -> false) ->
       let s = Option.get ctx.lits and t = Option.get want in
-      s.cons <- (key, ((if !lit_hint then Hint else Up), t, loc)) :: s.cons;
-      if lit_kind key = Some `Box then expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot))
-      else mk loc t (Tast.Local b.slot)
+      let operand = List.memq loc !lit_operand_locs in
+      let c = if operand || Types.equal t Types.Dyn then Hint else Up in
+      lit_add s key (c, t, loc);
+      (try expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot))
+       with Loc.Error _ when lit_kind key <> Some `Box && not operand ->
+         s.dirty <- true;
+         mk loc t (Tast.Local b.slot))
     | Some b ->
       expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot))
     (* A local of the enclosing function, in a body that was lifted out of it:
@@ -7308,7 +7404,7 @@ and lit_typed_use ctx (e : Ast.expr) =
   | Ast.Var n, Some s when s.recording ->
     (match lookup ctx n with
      | Some { blit = Some key; _ } when lit_kind key = Some `Box ->
-       s.cons <- (key, (Up, Types.Unit, e.Ast.loc)) :: s.cons
+       lit_add s key (Up, Types.Unit, e.Ast.loc)
      | _ -> ())
   | _ -> ()
 
@@ -7318,48 +7414,79 @@ and lit_recorded ctx n =
   | Some s, Some { blit = Some key; _ } when s.recording -> Some key
   | _ -> None
 
+(* [v] read as arithmetic: the literal locals among its operands, and the
+   operands that are something else (a call, an index, a typed name). Number
+   literals are neither. The result's type is the join of all of them, so the
+   locals are merged with whatever [v] is stored into and the others are
+   what it brings. *)
+and lit_parts ctx (v : Ast.expr) =
+  let rec go (v : Ast.expr) (vars, others) =
+    match v.Ast.e with
+    | Ast.Var n ->
+      (match lookup ctx n with
+       | Some { blit = Some k; _ } when lit_kind k <> Some `Box -> (k :: vars, others)
+       | _ -> (vars, v :: others))
+    | Ast.Int _ | Ast.Float _ | Ast.Byte _ -> (vars, others)
+    | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%" | "min" | "max"); _ }, args)
+      when args <> [] ->
+      List.fold_left (fun acc a -> go a acc) (vars, others) args
+    | _ -> (vars, v :: others)
+  in
+  go v ([], [])
+
+(* A float literal, or an integer one past i32, anywhere in [v]'s arithmetic. *)
+and lit_wide_literals (v : Ast.expr) =
+  let rec go (v : Ast.expr) =
+    match v.Ast.e with
+    | Ast.Float _ -> [ (Types.Float (float_default ()), v.Ast.loc) ]
+    | Ast.Int n when Int64.compare n (Int64.of_int32 Int32.max_int) > 0
+                     || Int64.compare n (Int64.of_int32 Int32.min_int) < 0 ->
+      [ (Types.Int Types.I64, v.Ast.loc) ]
+    | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%" | "min" | "max"); _ }, args) ->
+      List.concat_map go args
+    | _ -> []
+  in
+  go v
+
 (* [v] stored into the literal local [key] (a [set] or a [recur]), while
-   recording: checked on its own terms, so its type is what it brings rather
-   than the guess. Another literal local links the two; a float literal says
-   only that it is a float. *)
+   recording: the literal locals it is arithmetic over are merged with [key],
+   and each other operand says, on its own terms, what it brings ([Down]) —
+   never the guess the round happens to have. Then [v] is checked at [key]'s
+   guess, quietly, since a want there is the guess and says nothing. *)
 and lit_down ctx key pty (v : Ast.expr) =
   let s = Option.get ctx.lits in
-  let other =
-    match v.Ast.e with
-    | Ast.Var m -> (match lookup ctx m with Some { blit = Some k; _ } -> Some k | _ -> None)
-    | _ -> None
+  let quietly f =
+    let was = !lit_quiet in
+    lit_quiet := true;
+    Fun.protect ~finally:(fun () -> lit_quiet := was) f
   in
-  match other with
-  | Some k -> s.links <- (key, k) :: s.links; check ctx v
-  | None ->
-    match lit_kind v with
-    | Some `Float ->
-      s.cons <- (key, (Hint, Types.Float (float_default ()), v.Ast.loc)) :: s.cons;
-      check ctx v
-    (* An integer literal fits wherever its value does; one past i32 says
-       the local is at least an i64. *)
-    | Some _ ->
-      (match v.Ast.e with
-       | Ast.Int n when Int64.compare n (Int64.of_int32 Int32.max_int) > 0
-                        || Int64.compare n (Int64.of_int32 Int32.min_int) < 0 ->
-         s.cons <- (key, (Hint, Types.Int Types.I64, v.Ast.loc)) :: s.cons;
-         check ctx ~want:(Types.Int Types.I64) v
-       | _ -> check ctx ~want:pty v)
-    | None ->
-      (match trial ctx (fun () -> check ctx v) with
-       | Ok e ->
-         s.cons <- (key, (Down, e.Tast.ty, v.Ast.loc)) :: s.cons;
-         e
-       | Error _ -> check ctx ~want:pty v)
+  let vars, others = lit_parts ctx v in
+  List.iter (lit_union s key) vars;
+  List.iter (fun (t, l) -> lit_add s key (Hint, t, l)) (lit_wide_literals v);
+  List.iter
+    (fun (o : Ast.expr) ->
+       match trial ctx (fun () -> check ctx o) with
+       | Ok e -> lit_add s key (Down, e.Tast.ty, o.Ast.loc)
+       | Error _ -> ())
+    others;
+  match trial ctx (fun () -> quietly (fun () -> check ctx ~want:pty v)) with
+  | Ok e -> e
+  | Error _ ->
+    s.dirty <- true;
+    quietly (fun () -> check ctx v)
 
 (* The type a literal initialiser is checked at while a session is open —
-   its current guess, or the decision — noting it as seen while recording.
+   its current guess, or the decision — numbering it while recording.
    [None] for anything that is not a literal, or with no session open. *)
 and lit_local ctx name (e : Ast.expr) =
   match ctx.lits, lit_kind e with
   | Some s, Some kind ->
-    if s.recording then s.seen <- (e, name) :: s.seen;
-    Some (match List.assq_opt e s.decided with Some t -> t | None -> lit_default kind)
+    if s.recording && not (Phys.mem s.ids e) then begin
+      Phys.replace s.ids e s.count;
+      s.count <- s.count + 1;
+      s.keys <- (e, name) :: s.keys
+    end;
+    Some (lit_guess ~subst:ctx.env.subst s e kind)
   | _ -> None
 
 (* A literal local's initialiser, at the type [lit_local] gave it: [Unit] is
@@ -7376,44 +7503,100 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
   if ctx.lits <> None || not (List.exists (fun e -> lit_kind e <> None) inits)
   then run ()
   else begin
-    let s = { decided = []; recording = false; cons = []; links = []; seen = [] } in
+    let s = { decided = Phys.create 16; recording = false; ids = Phys.create 16;
+              keys = []; count = 0; parent = Hashtbl.create 16;
+              cons = Hashtbl.create 16; dirty = false } in
     ctx.lits <- Some s;
-    Fun.protect ~finally:(fun () -> ctx.lits <- None) @@ fun () ->
-    let undo = Loc.diag ~kind:"check/lit-undo" loc "undone" in
+    incr lit_depth;
+    let remember () =
+      let subst = ctx.env.subst in
+      List.iter
+        (fun (k, _) ->
+           let kind = Option.value (lit_kind k) ~default:`Int in
+           let t = lit_guess ~subst s k kind in
+           let others =
+             Option.value (Phys.find_opt lit_memo k) ~default:[]
+             |> List.filter (fun (sb, _) -> sb != subst)
+           in
+           Phys.replace lit_memo k ((subst, t) :: others))
+        s.keys
+    in
+    Fun.protect
+      ~finally:(fun () ->
+          ctx.lits <- None;
+          decr lit_depth;
+          if !lit_depth = 0 then Phys.reset lit_memo)
+    @@ fun () ->
+    let unsettled = Loc.diag ~kind:"check/lit-unsettled" loc "unsettled" in
+    (* The decisions the uses recorded so far make, and whether any moved. *)
+    let settle () =
+      let solved = lit_solve s in
+      let moved = ref false in
+      List.iter
+        (fun (k, _, r) ->
+           match r with
+           | Ok t ->
+             let kind = Option.value (lit_kind k) ~default:`Int in
+             if not (Types.equal t (lit_guess ~subst:ctx.env.subst s k kind)) then begin
+               moved := true;
+               Phys.replace s.decided k t
+             end
+           | Error _ -> ())
+        solved;
+      (solved, !moved)
+    in
+    let conflict solved =
+      List.find_map
+        (fun (k, name, r) -> match r with Error e -> Some (k, name, e) | Ok _ -> None)
+        solved
+    in
+    let log () =
+      if lit_has "log" then
+        Phys.iter
+          (fun k t ->
+             let d = lit_default k (Option.value (lit_kind k) ~default:`Int) in
+             if not (Types.equal t d) then
+               Printf.eprintf "LITINF %s:%d:%d %s -> %s\n" k.Ast.loc.Loc.file
+                 k.Ast.loc.Loc.line k.Ast.loc.Loc.col (tyname loc d) (tyname loc t))
+          s.decided
+    in
     let rec round n =
-      s.cons <- []; s.links <- []; s.seen <- [];
+      Phys.reset s.ids; s.keys <- []; s.count <- 0;
+      Hashtbl.reset s.parent; Hashtbl.reset s.cons; s.dirty <- false;
       s.recording <- true;
       incr lit_recording;
-      Fun.protect
-        ~finally:(fun () -> decr lit_recording; s.recording <- false)
-        (fun () -> ignore (trial ctx (fun () -> ignore (run ()); raise (Loc.Error undo))));
-      let solved = lit_solve s in
-      let guess k =
-        match List.assq_opt k s.decided with
-        | Some t -> t
-        | None -> lit_default (Option.value (lit_kind k) ~default:`Int)
+      (* A ref, because [trial] is monomorphic inside this recursive group. *)
+      let answer = ref None in
+      let outcome =
+        Fun.protect
+          ~finally:(fun () -> decr lit_recording; s.recording <- false)
+          (fun () ->
+             trial ctx (fun () ->
+                 let r = run () in
+                 let solved, moved = settle () in
+                 (* The guesses held: this check is the answer. *)
+                 if moved || s.dirty || conflict solved <> None then
+                   raise (Loc.Error unsettled);
+                 answer := Some r;
+                 poison loc))
       in
-      let decided =
-        List.map (fun (k, _, r) -> (k, match r with Ok t -> t | Error _ -> guess k)) solved
-      in
-      let moved = List.exists (fun (k, t) -> not (Types.equal t (guess k))) decided in
-      s.decided <- decided;
-      if moved && n < lit_rounds then round (n + 1)
-      else
-        match List.find_opt (fun (_, _, r) -> Result.is_error r) solved with
-        | Some (k, name, Error ((t1, l1), (t2, l2))) -> lit_conflict k name t1 l1 t2 l2
-        | _ -> ()
+      match outcome, !answer with
+      | Ok _, Some r -> log (); remember (); r
+      | _ ->
+        let solved, moved = settle () in
+        (match conflict solved with
+         | Some (k, name, ((t1, l1), (t2, l2))) -> lit_conflict k name t1 l1 t2 l2
+         | None -> ());
+        if moved && n < lit_rounds then round (n + 1)
+        else begin
+          (* Nothing left to learn: checked for real, so a refusal is the
+             ordinary one and a whole-file check goes on past it. *)
+          log ();
+          remember ();
+          run ()
+        end
     in
-    round 1;
-    if lit_has "log" then
-      List.iter
-        (fun (k, t) ->
-           let d = lit_default (Option.value (lit_kind k) ~default:`Int) in
-           if not (Types.equal t d) then
-             Printf.eprintf "LITINF %s:%d:%d %s -> %s\n" k.Ast.loc.Loc.file
-               k.Ast.loc.Loc.line k.Ast.loc.Loc.col (tyname loc d) (tyname loc t))
-        s.decided;
-    run ()
+    round 1
   end
 
 (* Two uses of a literal local that no one type satisfies. *)
@@ -8804,12 +8987,7 @@ and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
           (fun acc i ->
              if fits t i then acc
              else
-               Option.bind acc (fun a ->
-                 match Option.bind (natural i) (Types.join a), i.Ast.e with
-                 (* A float literal is any float: beside an i32 it takes the
-                    f64 the i32 widens into, not its own f32. *)
-                 | None, Ast.Float _ -> Types.join a (Types.Float Types.F64)
-                 | j, _ -> j))
+               Option.bind acc (fun a -> Option.bind (natural i) (Types.join a)))
           (Some t) lits
       in
       (match t' with
@@ -14678,7 +14856,53 @@ and trial_at ctx (y : Ast.expr) (w : Types.t) =
 
 and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
   match args with
-  | [ x; y ] ->
+  | [ x; y ] -> lit_operands ctx x y (fun () -> binary_pair ctx ~dyn_ok ~join loc ~want x y)
+  | _ -> fail loc "%s takes two arguments" name
+
+(* An operator's two operands, while literal locals' uses are recorded: one
+   beside a literal local says the type it meets it at ([Hint]), and two of
+   them are merged. Checked exactly as ever, so a round whose guesses hold is
+   the program. *)
+and lit_operands ctx (x : Ast.expr) (y : Ast.expr) f =
+  let key (e : Ast.expr) =
+    match e.Ast.e with Ast.Var n -> lit_recorded ctx n | _ -> None
+  in
+  match ctx.lits, key x, key y with
+  | Some s, kx, ky when kx <> None || ky <> None ->
+    let float_lit (e : Ast.expr) = lit_kind e = Some `Float in
+    (* Before the check, which refuses a float literal beside an integer
+       guess. *)
+    (match kx, ky with
+     | Some k, _ when float_lit y -> lit_add s k (Hint, Types.Float (float_default ()), y.Ast.loc)
+     | _, Some k when float_lit x -> lit_add s k (Hint, Types.Float (float_default ()), x.Ast.loc)
+     | _ -> ());
+    let saved = !lit_operand_locs in
+    lit_operand_locs := x.Ast.loc :: y.Ast.loc :: saved;
+    let a, b =
+      try Fun.protect ~finally:(fun () -> lit_operand_locs := saved) f
+      with Loc.Error _ as ex ->
+        (* Refused at the guess, as (+ acc x) is over an i32 guess and an
+           i64 x: what the other operand is on its own terms is the use. *)
+        let own (k, (other : Ast.expr)) =
+          match trial ctx (fun () -> check ctx other) with
+          | Ok e -> lit_add s k (Hint, e.Tast.ty, other.Ast.loc)
+          | Error _ -> ()
+        in
+        (match kx, ky with
+         | Some k, None -> own (k, y)
+         | None, Some k -> own (k, x)
+         | _ -> ());
+        raise ex
+    in
+    (match kx, ky with
+     | Some k1, Some k2 -> lit_union s k1 k2
+     | Some k, None -> lit_add s k (Hint, b.Tast.ty, y.Ast.loc)
+     | None, Some k -> lit_add s k (Hint, a.Tast.ty, x.Ast.loc)
+     | None, None -> ());
+    a, b
+  | _ -> f ()
+
+and binary_pair ctx ~dyn_ok ~join loc ~want (x : Ast.expr) (y : Ast.expr) =
     let y_decides =
       (is_literal x && not (is_literal y))
       || (match x.Ast.e, y.Ast.e with
@@ -14693,35 +14917,7 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
     let needs_want (f : Ast.expr) =
       is_literal f || (match f.Ast.e with Ast.Kw _ -> true | _ -> false)
     in
-    (* While a literal local's uses are recorded, the operand beside it
-       decides and the local is recorded as meeting it ([lit_session]). *)
-    let lv (f : Ast.expr) =
-      match f.Ast.e with Ast.Var n -> lit_recorded ctx n <> None | _ -> false
-    in
-    let hinted f =
-      lit_hint := true;
-      Fun.protect ~finally:(fun () -> lit_hint := false) f
-    in
-    let float_lit (f : Ast.expr) = lit_kind f = Some `Float in
-    if lv x && float_lit y then begin
-      let a = hinted (fun () -> check ctx ~want:(Types.Float (float_default ())) x) in
-      a, check ctx ~want:a.Tast.ty y
-    end
-    else if lv y && float_lit x then begin
-      let b = hinted (fun () -> check ctx ~want:(Types.Float (float_default ())) y) in
-      check ctx ~want:b.Tast.ty x, b
-    end
-    else if lv x && not (lv y) && not (needs_want y) then begin
-      let b = check ctx ?want y in
-      let a = hinted (fun () -> check ctx ~want:b.Tast.ty x) in
-      a, b
-    end
-    else if lv y && not (lv x) && not (needs_want x) then begin
-      let a = check ctx ?want x in
-      let b = hinted (fun () -> check ctx ~want:a.Tast.ty y) in
-      a, b
-    end
-    else if y_decides then begin
+    if y_decides then begin
       let b = check ctx ?want y in
       let a = check ctx ~want:b.Tast.ty x in
       a, b
@@ -14817,7 +15013,6 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
              | _ -> raise (Loc.Error d))
           | _ -> raise (Loc.Error d)
     end
-  | _ -> fail loc "%s takes two arguments" name
 
 (* ── The builtins, said out loud ───────────────────────────────────────
    A name, a signature and one line, for every name [named_call] and [var]
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index b841fec7..c48f6f39 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -1125,13 +1125,82 @@ _Noreturn void flan_restart_fail(const uint8_t *loc, int64_t loclen,
  * dynamic stack, so the invoke site cannot see what it will find, and the
  * frame cannot see who will find it. What each end knows is its own parameter
  * list, so the message is both of them side by side. */
+/* The top-level items of a signature "(a b c)", where an item may itself be
+ * bracketed: "(Ptr i32)", "[3 f64]". Up to [max]; answers how many. */
+static int sig_items(const uint8_t *s, int64_t n, const uint8_t **at,
+                     int64_t *len, int max) {
+  int count = 0, depth = 0;
+  int64_t start = -1;
+  for (int64_t i = 1; i + 1 < n; i++) {
+    uint8_t c = s[i];
+    if (c == ' ' && depth == 0) {
+      if (start >= 0 && count < max) { at[count] = s + start; len[count] = i - start; count++; }
+      start = -1;
+      continue;
+    }
+    if (start < 0) start = i;
+    if (c == '(' || c == '[') depth++;
+    else if (c == ')' || c == ']') depth--;
+  }
+  if (start >= 0 && count < max) { at[count] = s + start; len[count] = n - 1 - start; count++; }
+  return count;
+}
+
+static int is_number_type(const uint8_t *s, int64_t n) {
+  static const char *names[] = { "i8", "i16", "i32", "i64", "u8", "u16",
+                                 "u32", "u64", "f32", "f64" };
+  for (size_t k = 0; k < sizeof names / sizeof names[0]; k++)
+    if ((int64_t)strlen(names[k]) == n && memcmp(names[k], s, (size_t)n) == 0)
+      return 1;
+  return 0;
+}
+
+/* [got] is the invoke site's signature, then after each 0x1f: the syntax
+ * (i or p) and every argument as written. Where the two signatures differ
+ * only in which number type an argument is, the fix is that argument
+ * converted: (f64 2.5), or f64(2.5) in the indented syntax. */
 _Noreturn void flan_restart_args_fail(const uint8_t *loc, int64_t loclen,
                                       const uint8_t *name, int64_t namelen,
                                       const uint8_t *want, int64_t wantlen,
                                       const uint8_t *got, int64_t gotlen) {
-  flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s", (int)namelen,
-           (const char *)name, (int)wantlen, (const char *)want, (int)gotlen,
-           (const char *)got);
+  enum { MAX = 16 };
+  const uint8_t *part[MAX + 2];
+  int64_t plen[MAX + 2];
+  int parts = 0;
+  int64_t start = 0;
+  for (int64_t i = 0; i <= gotlen && parts < MAX + 2; i++)
+    if (i == gotlen || got[i] == 0x1f) {
+      part[parts] = got + start; plen[parts] = i - start; parts++;
+      start = i + 1;
+    }
+  const uint8_t *w[MAX], *g[MAX];
+  int64_t wl[MAX], gl[MAX];
+  int nw = sig_items(want, wantlen, w, wl, MAX);
+  int ng = sig_items(part[0], plen[0], g, gl, MAX);
+  char fix[512];
+  size_t used = 0;
+  fix[0] = 0;
+  int ok = parts >= 2 && nw == ng && ng == parts - 2 && ng > 0;
+  for (int k = 0; ok && k < ng; k++) {
+    if (wl[k] == gl[k] && memcmp(w[k], g[k], (size_t)wl[k]) == 0) continue;
+    if (!is_number_type(w[k], wl[k]) || !is_number_type(g[k], gl[k])) { ok = 0; break; }
+    int indented = plen[1] == 1 && part[1][0] == 'i';
+    int wrote = indented
+      ? snprintf(fix + used, sizeof fix - used, "%s%.*s(%.*s)", used ? ", " : "",
+                 (int)wl[k], (const char *)w[k], (int)plen[k + 2], (const char *)part[k + 2])
+      : snprintf(fix + used, sizeof fix - used, "%s(%.*s %.*s)", used ? ", " : "",
+                 (int)wl[k], (const char *)w[k], (int)plen[k + 2], (const char *)part[k + 2]);
+    if (wrote < 0 || (size_t)wrote >= sizeof fix - used) { ok = 0; break; }
+    used += (size_t)wrote;
+  }
+  if (ok && used > 0)
+    flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s. Write %s",
+             (int)namelen, (const char *)name, (int)wantlen, (const char *)want,
+             (int)plen[0], (const char *)part[0], fix);
+  else
+    flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s", (int)namelen,
+             (const char *)name, (int)wantlen, (const char *)want, (int)plen[0],
+             (const char *)part[0]);
   rt_trap((const uint8_t *)"RestartArity", 12);
 }
 
diff --git a/test/programs/literal-locals.flan b/test/programs/literal-locals.flan
index c9386d34..69bef99a 100644
--- a/test/programs/literal-locals.flan
+++ b/test/programs/literal-locals.flan
@@ -42,6 +42,21 @@
       (set acc (+ acc (at xs i))))
     acc))
 
+;; A chain of sets settles however long it is.
+(defn chained [x i64] i64
+  (let [a0 0 a1 0 a2 0 a3 0 a4 0 a5 0]
+    (set a0 x) (set a1 (+ a0 1)) (set a2 (+ a1 1)) (set a3 (+ a2 1))
+    (set a4 (+ a3 1)) (set a5 (+ a4 1))
+    a5))
+
+;; A dyn number is an i64 or an f64, and so is a literal local it feeds.
+(defn boxed [x] dyn x)
+(defn from-dyn [] ()
+  (let [d (boxed 0.1) s 0.0 n 0]
+    (set s (+ s d))
+    (set n (+ n (boxed 5000000000)))
+    (println s n)))
+
 (defn main [] i32
   (let [xs (the [3 i64] [3000000000 4 5])
         fs (the [2 f64] [0.5 0.25])
@@ -53,6 +68,10 @@
     (println (sum-to 3))                           ; 3000000000
     (println (sum-of (slice xs 0 3)))              ; 3000000009
     (println (sum-of (slice fs 0 2))))             ; 0.75
+  (println (chained 3000000000))                   ; 3000000005
+  (from-dyn)                                       ; 0.1 5000000000
+  (let [x 0.1]
+    (println (= (boxed x) (boxed 0.1))))           ; true
   ;; Nothing says otherwise: an i32 and an f64.
   (let [n 7 f 1.5]
     (println n f))                                 ; 7 1.5
diff --git a/test/programs/restarts.flan b/test/programs/restarts.flan
index 961c079f..b8adc4a5 100644
--- a/test/programs/restarts.flan
+++ b/test/programs/restarts.flan
@@ -101,6 +101,11 @@
   (handler-bind [(AssetMissing [c] (invoke-restart 'use-value 21))]
     (shadowed n)))
 
+;;; A number of another type: the refusal writes the conversion.
+(defn widened [n i32] i32
+  (handler-bind [(AssetMissing [c] (let [big (i64 7)] (invoke-restart 'use-value big)))]
+    (supplied n)))
+
 (defn main [args [str]] i32
   ;; One argument selects a trap; none runs the table's case.
   (if (> (length args) 1)
@@ -110,6 +115,7 @@
         (= k 2) (print (mistyped 91))
         (= k 3) (print (overfull 92))
         (= k 4) (print (mislaid 93))
+        (= k 5) (print (widened 94))
         :else (println "?"))
       (return 0)))
 
diff --git a/test/programs/x86-p12-handler-value.flan b/test/programs/x86-p12-handler-value.flan
index 2bd60423..faa843a2 100644
--- a/test/programs/x86-p12-handler-value.flan
+++ b/test/programs/x86-p12-handler-value.flan
@@ -88,7 +88,7 @@
   (handler-bind [(Oops [c] (invoke-restart 'use-zero))]
     (println (deferred)))                                   ; 9
   (println trace)                                           ; 101 — the defer ran
-  (handler-bind [(Oops [c] (invoke-restart 'use-value (f64 2.5)))]
+  (handler-bind [(Oops [c] (invoke-restart 'use-value 2.5))]
     (println (floating)))                                   ; 5
   (handler-bind [(Oops [c] (invoke-restart 'use-value "supplied"))]
     (println (spelled)))                                    ; supplied
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 79e3d68b..311499d3 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -391,7 +391,7 @@ let () =
     outputs "unit main exits 0" "programs/unit-main.flan" "ok\n";
     let literal_locals_out =
       "3000000009\n0.375\n5000000000\n3000000000\n3000000000\n3000000009\n\
-       0.75\n7 1.5\n"
+       0.75\n3000000005\n0.1 5000000000\ntrue\n7 1.5\n"
     in
     outputs "literal locals take their uses' type" "programs/literal-locals.flan"
       literal_locals_out;
@@ -1400,6 +1400,8 @@ let () =
          have taken them is not consulted. *)
       refuses "a shadowing clause of the same name and a different signature" "4"
         "restart use-value takes (str), given (i32)";
+      refuses "a number of another type is refused with its conversion" "5"
+        "restart use-value takes (i32), given (i64). Write (i32 big)";
       (try Sys.remove exe with Sys_error _ -> ())
     in
     restart_mismatch ();
@@ -3614,7 +3616,7 @@ let () =
        and each read used to make the call again. *)
     let generic_struct_out =
       "60 3 4\nfalse 7.5 3\n(some 3.5) (some 2.5) 1\n2 1 2.5 1.5\n\
-       (Pair i32 {.a 2 .b 1}) (Pair f32 {.a 1 .b 2.5})\n6\n\
+       (Pair i32 {.a 2 .b 1}) (Pair f64 {.a 1 .b 2.5})\n6\n\
        0 1 2\n3 2\n6\n6 3\n(some 34) none 15\n"
     in
     outputs "generic structs" "programs/generic-struct.flan" generic_struct_out;
@@ -3791,9 +3793,9 @@ let () =
        requirement the author wrote down. What is asserted is that it names
        the type passed and the predicate it failed, and not the body. *)
     refuses "a generic over maps, instantiated at a key that cannot be hashed"
-      "programs/generic-map-reject.flan" "f32 is not hashable?";
+      "programs/generic-map-reject.flan" "f64 is not hashable?";
     refuses "and it names the type the call site asked for"
-      "programs/generic-map-reject.flan" "at $t = f32";
+      "programs/generic-map-reject.flan" "at $t = f64";
 
     (* This one is refused either way, so the guard is about *which* refusal:
        with sand.flan out of date the file stops at the import and the needle
diff --git a/test/test_dev.ml b/test/test_dev.ml
index dc32caec..be21fb4e 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -3841,7 +3841,7 @@ let () =
             "(defn use-sort [] ()\n  (let [a [3 1 2]] (selection-sort (slice a 0 3)))\n  \
              (let [b [3.0 1.0]] (selection-sort (slice b 0 2))))"
         in
-        if status r <> "ok" then fail "%s: calling the generic at f32: %s" backend (said r)
+        if status r <> "ok" then fail "%s: calling the generic at f64: %s" backend (said r)
         else begin
           let r = ask () in
           if status r <> "ok" then
@@ -3852,7 +3852,7 @@ let () =
               let types f =
                 Option.value ~default:"" (Wire.string_field f "types")
               in
-              if types a <> "$t = f32" || types b <> "$t = i32" then
+              if types a <> "$t = f64" || types b <> "$t = i32" then
                 fail "%s: the copies are not headed by their types: %s, %s"
                   backend (types a) (types b);
               List.iter
diff --git a/test/test_flan.ml b/test/test_flan.ml
index cdeb8130..4e7e2beb 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1071,7 +1071,7 @@ let def_reading name src gname ~ty =
 let () =
   (* ── Literal defaulting and inference ──────────────────────────── *)
   infers "int defaults to i32"   "42" "i32";
-  infers "float defaults to f32" "0.5" "f32";
+  infers "float defaults to f64" "0.5" "f64";
   infers "byte is u8"            "\\space" "u8";
   infers "string"                "\"hi\"" "str";
   infers "bool"                  "true" "bool";
@@ -1096,13 +1096,15 @@ let () =
     "(defn f [n i64] i64 (loop [i 0 acc 0] (if (< i n) (recur (+ i 1) (+ acc n)) acc)))";
   accepts "a set links two literal locals"
     "(defn f [] i64 (let [a 0 b 0] (set b 3000000000) (set a b) a))";
-  rejects_check "a float literal past f32's range is refused with the f64 spelling"
-    ~needle:"1e+39 does not fit in f32, whose largest value is about 3.4e38. \
-             Write (f64 1e+39)"
+  accepts "a float literal local takes the f32 typed code wants"
+    "(defn f [x f32] f32 (let [s 0.0] (set s (+ s x)) s))";
+  rejects_check "a literal past f32's range where f32 is wanted"
+    ~needle:"1e+39 does not fit in f32, whose largest value is about 3.4e38"
     "(defn f [] f32 1e39)";
-  infers "a float literal converted is built at the target" "(f64 0.1)" "f64";
-  infers "an f32 range literal beside others makes the array f64"
-    "[2.5 1e300]" "[2 f64]";
+  rejects_check "a literal f32 rounds to 0 where f32 is wanted"
+    ~needle:"1e-50 is too small for f32, which rounds it to 0"
+    "(defn f [] f32 1e-50)";
+  infers "a literal past f32's range is an f64 like any other" "(+ 1.0 1e300)" "f64";
   rejects_check "two uses of a literal local disagree"
     ~needle:"x is used as u32 and as i32, and 0 can have only one type. \
              Write the one it should have: (u32 0)"
@@ -1115,7 +1117,7 @@ let () =
      not a zero, which is what lets it be a defonce's initialiser — see
      programs/array-fill.flan for what it puts in the elements. *)
   infers "array-fill, rank 1"    "(array-fill [5] 7)" "[5 i32]";
-  infers "array-fill, rank 2"    "(array-fill [2 3] 0.5)" "[2 [3 f32]]";
+  infers "array-fill, rank 2"    "(array-fill [2 3] 0.5)" "[2 [3 f64]]";
   infers "array-fill, rank 3"    "(array-fill [2 3 4] true)" "[2 [3 [4 bool]]]";
   (* A zero dimension is a legal array with no elements, and the fill loop
      runs no passes over it. *)
@@ -1136,7 +1138,7 @@ let () =
 
   (* An untyped integer constant is usable where a float is wanted, as in
      Odin; the reverse is not. *)
-  infers "int literal into a float" "(+ 1 0.5)" "f32";
+  infers "int literal into a float" "(+ 1 0.5)" "f64";
   rejects_check "float literal into an int"
     "(defn f [] i32 (+ 1 0.5))" ~needle:"expected i32";
 
@@ -3809,7 +3811,7 @@ let () =
   rejects_check "an inline generator's body has to answer the element type"
     "(defonce grid [2 [3 u8]] (array-gen [2 3] (fn [i j] 1.5)))\n\
      (defn f [] i32 0)"
-    ~needle:"expected u8, found f32";
+    ~needle:"expected u8, found f64";
   rejects_check "an inline generator takes one argument per dimension too"
     "(defn f [] i32 (let [a (array-gen [2] (fn [i j] i))] 0))"
     ~needle:"this array-gen has 1 dimension, so its generator is called with \
@@ -6699,7 +6701,7 @@ let () =
     "(defn bump [x $t] $t {:where (integer? $t)} (+ x 300))";
   (* A float at integer?, refused at the call that asked, naming the bound. *)
   rejects_check "a float does not instantiate an integer?-bounded variable"
-    ~needle:"f32 is not integer?"
+    ~needle:"f64 is not integer?"
     "(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))\n\
      (defn main [] () (println (bump 1.5)))";
   (* And dyn is refused by the bound too — the clause's own refusal, the more
@@ -7657,7 +7659,7 @@ let () =
   (* ── An array literal with nothing outside it naming a type ────── *)
   infers "a literal takes the other elements' type" "[(f32 1.0) 2.5]" "[2 f32]";
   infers "numbers meet at the wider" "[(u8 1) 256]" "[2 i32]";
-  infers "an int and a float literal meet at the float" "[1 2.5]" "[2 f32]";
+  infers "an int and a float literal meet at f64" "[1 2.5]" "[2 f64]";
   infers "a wide literal makes the array u64" "[1 18446744073709551615]" "[2 u64]";
   infers "None takes the other element's Option" "[None (Some 1)]" "[2 (Option i32)]";
   infers "a number and a string are a dyn vector" "[10 \"Hi\"]" "dyn";
@@ -7711,10 +7713,10 @@ let () =
      check "max-value at an unbounded type variable names the bound and only it"
        (contains d.Loc.dmsg "write {:where (numeric? $t)}"
         && not (contains d.Loc.dmsg "Fn")));
-  infers "two literal if arms meet at the float" "(if true 1 2.5)" "f32";
+  infers "two literal if arms meet at the wider" "(if true 1 2.5)" "f64";
   infers "two integer if arms stay i32" "(if true 1 2)" "i32";
-  infers "two literal match arms meet at the float"
-    "(match (Some 1) (Some v) 1 None 2.5)" "f32";
+  infers "two literal match arms meet at the wider"
+    "(match (Some 1) (Some v) 1 None 2.5)" "f64";
   accepts "max-value at a type variable the bound admits"
     "(defn f [x $t] $t {:where (integer? $t)} (max-value t))";
   rejects_check "max-value at a type that is not a number names the bound"
@@ -7831,7 +7833,7 @@ let () =
    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] f32";
+     ("(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"
diff --git a/test/test_session.ml b/test/test_session.ml
index 503dd716..328158fd 100644
--- a/test/test_session.ml
+++ b/test/test_session.ml
@@ -212,7 +212,7 @@ let () =
        "(defn scale [x i64] f64 (f64 (* x 2))) (defn other [] f64 (same 2.5))"
    with
    | c ->
-     if not (List.mem "same-f32" c.Session.fns) then
+     if not (List.mem "same-f64" c.Session.fns) then
        fail "a copy a tolerated caller asked for was not generated again: %s"
          (String.concat " " c.Session.fns);
      if List.map (fun (x : Session.stale) -> x.Session.caller) c.Session.stale
@@ -434,7 +434,7 @@ let () =
       not: the recovery half of the same claim. *)
    match Session.eval_expr xt "(println (pick (slice [1.5 0.5] 0 2)))" with
    | e ->
-     if not (has e.Session.ir "pick-f32") then
+     if not (has e.Session.ir "pick-f64") then
        fail "the expression after a refused one carried no copy"
    | exception Loc.Error { Loc.dmsg = m; _ } ->
      fail "the session was poisoned by a bad expression: %s" m);
@@ -1509,7 +1509,7 @@ let () =
           if not (List.mem want c.Session.fns) then
             fail "redefining a generic did not install %s; it installed %s"
               want (String.concat " " c.Session.fns))
-       [ "hold-i32"; "hold-f32" ];
+       [ "hold-i32"; "hold-f64" ];
      (* And only its own copies: [put-at] did not change, and its copies are
         reached through their cells, so reinstalling them would be work with
         no effect. *)
@@ -1530,7 +1530,7 @@ let () =
           if not (List.mem want c.Session.fns) then
             fail "redefining a called generic did not install %s; it \
                   installed %s" want (String.concat " " c.Session.fns))
-       [ "put-at-i32"; "put-at-f32" ]
+       [ "put-at-i32"; "put-at-f64" ]
    | exception Loc.Error { Loc.dmsg = m; _ } ->
      fail "redefining a generic: %s" m);
 
@@ -1561,9 +1561,9 @@ let () =
      fail "a second redefinition of a generic installed nothing");
 
   (* 3. A redefinition that needs a copy the process was never built with. The
-     fixture never calls [pick] at f32, so [pick-f32] exists in no program
+     fixture never calls [pick] at f64, so [pick-f64] exists in no program
      anywhere; redefining the *caller* to ask for it has to build and install
-     it. Nothing in the form names [pick-f32] — it is found by being an
+     it. Nothing in the form names [pick-f64] — it is found by being an
      instantiation the host lacks. *)
   (match
      Session.eval (gen ())
@@ -1572,9 +1572,9 @@ let () =
         (set counter (+ counter (i64 (pick (slice fs 0 3)))))))"
    with
    | c ->
-     if not (List.mem "pick-f32" c.Session.fns) then
+     if not (List.mem "pick-f64" c.Session.fns) then
        fail "a redefinition needing a new instantiation did not install \
-             pick-f32; it installed %s" (String.concat " " c.Session.fns)
+             pick-f64; it installed %s" (String.concat " " c.Session.fns)
    | exception Loc.Error { Loc.dmsg = m; _ } ->
      fail "a redefinition needing a new instantiation: %s" m);
 
@@ -1620,7 +1620,7 @@ let () =
   (let t = gen () in
    match Session.eval_expr t "(println (pick (slice [1.5 0.5] 0 2)))" with
    | e ->
-     if not (has e.Session.ir "pick-f32") then
+     if not (has e.Session.ir "pick-f64") then
        fail "an expression that instantiated a generic did not carry the copy"
    | exception Loc.Error { Loc.dmsg = m; _ } ->
      fail "an expression that instantiates a generic: %s" m);