diff --git a/TODO.org b/TODO.org
index 080e6e45..ac9e5c99 100644
--- a/TODO.org
+++ b/TODO.org
@@ -52,11 +52,19 @@ next free-temp. Rules out copy-in/copy-out at a call, and rooting the text in th
 ** 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.
+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
 CLOSED: [2026-09-20]
 An unannotated parameter or return is =dyn=: a NaN-boxed value over a mark-sweep
diff --git a/lib/check.ml b/lib/check.ml
index 406137b1..fb6c733a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -70,6 +70,10 @@ type binding = {
      that the field is already in hand. [None] everywhere else, and a refusal
      with [None] says exactly what it said before. *)
   bwhat : string option;
+  (* The literal a [let] or [loop] bound this name to, when its type is read
+     off the uses ([lit_session]). The initialiser's node, by identity, is the
+     key: two expansions of one macro are two nodes. *)
+  blit : Ast.expr option;
 }
 
 (* A class slot's type: what a value stored into it is checked against. A
@@ -745,11 +749,84 @@ type lentry =
   | Lrecur   of (int * Types.t) list
   | 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 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:
+   - [Up t]: the local flows into a [t] — a parameter, a return, a field, an
+     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; 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. 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;
+  (* 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],
+   [if_failed], [truthy_failed]) are not written then, since a refusal made
+   at a guessed type must not be replayed at the decided one. *)
+let lit_recording = ref 0
+
+(* 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
+   use wants. *)
+let typed_literals = ref false
+let with_typed_literals f =
+  let was = !typed_literals in
+  typed_literals := true;
+  Fun.protect ~finally:(fun () -> typed_literals := was) f
+
 (* Per-function state. Slots are never reused, so [slots] is also the frame
    size — the interpreter allocates one array of this length per call. *)
 type ctx = {
   env           : env;
   ret           : Types.t;
+  (* The literal-inference session of this function, while one is open. *)
+  mutable lits  : lit_session option;
   mutable slots : int;
   (* The type of each slot, newest first. A backend needs it to size the
      frame — nothing else records it, since the IR refers to slots by index. *)
@@ -930,7 +1007,7 @@ let render_ctx ctx (emit : Render.emitter) : Render.ctx =
    variables properly means emitting a [!DILexicalBlock] per [Let] and moving
    the [llvm.dbg.declare]s out of the entry block to the binding sites, which
    needs block structure this IR does not carry. *)
-let bind ctx ?what name bty ~assignable =
+let bind ctx ?what ?lit name bty ~assignable =
   let taken n = List.exists (fun s -> s = Some n) ctx.slot_names in
   let name' =
     if not (taken name) then name
@@ -944,10 +1021,24 @@ let bind ctx ?what name bty ~assignable =
   let slot = fresh_slot ~name:name' ctx bty in
   (* [ctx.scope] keeps the *source* name: the suffix is a debug-info artifact
      and resolving [v] must still find the innermost binding. *)
-  ctx.scope <- (name, { slot; bty; assignable; bwhat = what }) :: ctx.scope;
+  ctx.scope <- (name, { slot; bty; assignable; bwhat = what; blit = lit }) :: ctx.scope;
   slot
 
-let lookup ctx name = List.assoc_opt name ctx.scope
+(* The last answer for each name, with the scope it was read from. A body is
+   checked under one scope for long stretches and names the same local
+   several times per form, so compared by identity this answers most
+   lookups without walking a scope that, in a long [let], holds thousands of
+   names. *)
+let lookup_cache : (string, (string * binding) list * binding option) Hashtbl.t =
+  Hashtbl.create 64
+
+let lookup ctx name =
+  match Hashtbl.find_opt lookup_cache name with
+  | Some (sc, r) when sc == ctx.scope -> r
+  | _ ->
+    let r = List.assoc_opt name ctx.scope in
+    Hashtbl.replace lookup_cache name (ctx.scope, r);
+    r
 
 (* Capture, spec-memory.md's case 2: a body lifted into a function of its own —
    an [fn] literal or a handler clause — naming a local of the function it was
@@ -976,7 +1067,7 @@ let rec capture ctx loc name =
      a [let] inside the body restores what it displaced, and the copy's
      binding goes with it. One field, not two: the environment is keyed by the
      source name. *)
-  | Some (outer, slot) -> Some { slot; bty = outer.bty; assignable = false; bwhat = None }
+  | Some (outer, slot) -> Some { slot; bty = outer.bty; assignable = false; bwhat = None; blit = None }
   | None ->
     let from_parent () =
       (* Not a local of the body directly around this one, so ask whether that
@@ -997,7 +1088,7 @@ let rec capture ctx loc name =
     | Some _, Some (outer : binding) ->
       let slot = bind ctx name outer.bty ~assignable:false in
       ctx.caught <- ctx.caught @ [ (name, (outer, slot)) ];
-      Some { slot; bty = outer.bty; assignable = false; bwhat = None }
+      Some { slot; bty = outer.bty; assignable = false; bwhat = None; blit = None }
     | _ -> None
 
 (* The one thing [capture] does not answer for. A captured name is a copy, so
@@ -1017,7 +1108,7 @@ and peek_outer ctx name =
   if ctx.outer_what = None then None
   else
     match List.assoc_opt name ctx.caught with
-    | Some ((b : binding), slot) -> Some { slot; bty = b.bty; assignable = false; bwhat = None }
+    | Some ((b : binding), slot) -> Some { slot; bty = b.bty; assignable = false; bwhat = None; blit = None }
     | None ->
       match List.assoc_opt name ctx.outer with
       | Some b -> Some b
@@ -3605,6 +3696,171 @@ let restart_sig tys =
 let dyn_i64 = Types.Int Types.I64
 let dyn_f64 = Types.Float Types.F64
 
+(* The switch the unfinished half of TODO.org's "Dyn unless annotated" is
+   measured with: [dyn] makes an unwanted text or bracket literal dyn (a
+   let-bound one stays typed when a use wants it, [lit_session]), and [log]
+   prints each literal local inference moved off its default. Deleted when
+   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 f64 (decision 121); it is an f32 only
+   where typed code wants one. *)
+let float_default () = Types.F64
+
+(* ── Literal locals ([lit_session]) ────────────────────────────────── *)
+
+(* The literal a [let] or [loop] initialiser is, when its type is to be read
+   off the uses: a number or a character, negated or not. A bool has one type
+   and a wide literal one (u64), so neither has anything to infer. *)
+let lit_kind (e : Ast.expr) =
+  match e.Ast.e with
+  | Ast.Int _ -> Some `Int
+  | Ast.Byte _ -> Some `Char
+  | Ast.Float _ -> Some `Float
+  | Ast.Call ({ Ast.e = Ast.Var "-"; _ }, [ { Ast.e = Ast.Int _; _ } ]) -> Some `Int
+  | Ast.Call ({ Ast.e = Ast.Var "-"; _ }, [ { Ast.e = Ast.Float _; _ } ]) -> Some `Float
+  | Ast.Str _ | Ast.Arr (_ :: _) when lit_has "dyn" -> Some `Box
+  | _ -> None
+
+(* What the literal is with no use to say otherwise. *)
+(* 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 (_ : Ast.expr) = function
+  | `Int -> Types.Int Types.I32
+  | `Char -> Types.Int Types.U8
+  | `Float -> Types.Float (float_default ())
+  | `Box -> Types.Dyn
+
+(* The types a use can give it: any number for an integer or a character,
+   since an untyped integer constant is usable where a float is wanted, and
+   only a float for a float. A type variable is admitted and left to
+   [int_literal] to judge against its bound. Anything else — dyn, a struct —
+   says nothing about the literal's type; the local keeps its guess and the
+   use is checked as it always was. *)
+let lit_admits kind (t : Types.t) =
+  match kind, t with
+  | (`Int | `Char), (Types.Int _ | Types.Float _ | Types.Var _) -> true
+  | `Float, (Types.Float _ | Types.Var _) -> true
+  | `Box, t -> not (Types.equal t Types.Dyn)
+  | _ -> false
+
+(* 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
+
+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
+    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
+  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
    was written for: runtime/flan_dyn.h boxes integers as [i64] and floats as
@@ -4779,6 +5035,16 @@ let arm_join (a : Types.t) (b : Types.t) =
         (match a, b with
          | Types.Dyn, _ | _, Types.Dyn -> Some Types.Dyn
          | _ -> None)
+(* The type two untyped literals meet at: the wider of their own types, and
+   an integer beside a float at the float — [(if c 1 2.5)] is an f32, though
+   i32 does not widen into f32, because the 1 was never an i32 to lose. Only
+   for literals: a typed i32 beside a float literal still has to be converted. *)
+let literal_meet (a : Types.t) (b : Types.t) =
+  match Types.join a b, a, b with
+  | Some j, _, _ -> Some j
+  | None, Types.Int _, Types.Float _ -> Some b
+  | None, Types.Float _, Types.Int _ -> Some a
+  | None, _, _ -> None
 let infer_seen : (Types.t * Loc.t * bool) list ref = ref []
 (* What a refused subexpression stands as while recovering. [Zero] of [Never]
    is a value nothing else builds, so it is recognisable; see [check]. *)
@@ -4838,7 +5104,7 @@ let with_recovery env ~on f =
   end
 
 let invented_ctx env ret =
-  { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
+  { env; ret; lits = None; 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;
     in_defer = false; defer_ok = false; defer_block = "a nested form";
     owner = "<none>" }
@@ -5786,9 +6052,21 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
       | Some other when other <> Types.Never ->
         Loc.failk literal_at_want loc "expected %s, found the float literal %g"
           (tyname loc other) x
-      | _ -> Types.F64
+      | _ -> float_default ()
     in
+    (* 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))
   | Ast.Kw k ->
     (* Two keywords in one spelling, told apart by the expectation. Where an
@@ -5884,11 +6162,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
      integer type, since the real one is answered again per copy. A local of
      the same name shadows it. *)
   | Ast.Var name
-    when (not (List.mem_assoc name ctx.scope))
-         && (List.mem name ctx.env.lenvars
-             || (match List.assoc_opt name ctx.env.subst with
-                 | Some (Types.Len _) -> true
-                 | _ -> false)) ->
+    when (List.mem name ctx.env.lenvars
+          || (match List.assoc_opt name ctx.env.subst with
+              | Some (Types.Len _) -> true
+              | _ -> false))
+         && lookup ctx name = None ->
     let n =
       match List.assoc_opt name ctx.env.subst with
       | Some (Types.Len n) -> n
@@ -6037,6 +6315,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
     let v = check ctx ~want:Types.Dyn v in
     expect ctx loc ~want
       (rt loc Types.Unit "flan_dyn_slot_set" [ target; k; v; here loc ])
+  | Ast.Set ((Ast.Pvar n as p), v) when lit_recorded ctx n <> None ->
+    let key = Option.get (lit_recorded ctx n) in
+    let p, pty = check_place ctx loc p in
+    let v = lit_down ctx key pty v in
+    expect ctx loc ~want (mk loc Types.Unit (Tast.Set (p, v)))
   (* (set (.name x) v) on a dyn is (put x :name v): a class slot's declared
      type is checked by put, and a map takes a key it did not hold. Not
      [flan_dyn_slot_set], which refuses a plain map — .name reads either, so
@@ -6083,6 +6366,8 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
      fixed-array literal they always were. *)
   | Ast.Arr items when want = Some Types.Dyn ->
     dyn_vec ctx loc (map_lr (fun x -> check ctx ~want:Types.Dyn x) items)
+  | Ast.Arr items when want = None && lit_has "dyn" && not !typed_literals ->
+    dyn_vec ctx loc (map_lr (fun x -> check ctx ~want:Types.Dyn x) items)
   | Ast.Arr items -> check_arr ctx ~want loc items
   (* (array 4 rl/Vector2). Parse already assembled the whole array type, so
      there is nothing to infer: resolve it and hand back its all-bytes-zero
@@ -6190,6 +6475,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) ->
@@ -6201,6 +6487,31 @@ 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"
+        | _ ->
+          (* The argument as written, when it is on one line of a file the
+             checker can read; otherwise an ellipsis. *)
+          let l = a.Ast.loc in
+          match Loc.source_line l with
+          | Some line
+            when l.Loc.macro = None && l.Loc.eline = l.Loc.line && l.Loc.col >= 1
+                 && l.Loc.ecol > l.Loc.col && l.Loc.ecol - 1 <= String.length line ->
+            String.sub line (l.Loc.col - 1) (l.Loc.ecol - l.Loc.col)
+          | _ -> spell_arg "\u{2026}" 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
@@ -6215,7 +6526,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
@@ -6437,6 +6748,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.
+       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 && 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
+      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:
@@ -7149,13 +7479,307 @@ and defer_counter_zero slot loc =
 (* [defer_ok] says whether *this* let has the function's extent. If it does, so
    does every form in its body, including a nested let — which is why the flag
    is handed to the body rather than consumed here. *)
+(* A text or bracket literal local used where only its typed reading works —
+   sliced, its address taken, cloned, destructured: a typed use, recorded. *)
+and lit_typed_use ctx (e : Ast.expr) =
+  match e.Ast.e, ctx.lits with
+  | Ast.Var n, Some s when s.recording ->
+    (match lookup ctx n with
+     | Some { blit = Some key; _ } when lit_kind key = Some `Box ->
+       lit_add s key (Up, Types.Unit, e.Ast.loc)
+     | _ -> ())
+  | _ -> ()
+
+(* The literal local [n] names, while its uses are being recorded. *)
+and lit_recorded ctx n =
+  match ctx.lits, lookup ctx n with
+  | 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) =
+  (* [env]: names a [let] inside [v] binds, with what they were bound to, so
+     (let [t a0] t) passes a0 through as (do a0) and an if's arms do. *)
+  let rec go env (v : Ast.expr) (vars, others) =
+    match v.Ast.e with
+    | Ast.Var n ->
+      (match List.assoc_opt n env with
+       | Some (Some (vs, os)) -> (vs @ vars, os @ others)
+       | Some None -> (vars, v :: others)
+       | None ->
+         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 env a acc) (vars, others) args
+    | Ast.Do (_ :: _ as xs) -> go env (List.nth xs (List.length xs - 1)) (vars, others)
+    | Ast.Let (bs, (_ :: _ as xs)) ->
+      let env =
+        List.fold_left
+          (fun env (b : Ast.binding) ->
+             (b.Ast.bname,
+              if b.Ast.bty = None then Some (go env b.Ast.bval ([], [])) else None)
+             :: env)
+          env bs
+      in
+      go env (List.nth xs (List.length xs - 1)) (vars, others)
+    | Ast.If (_, t, Some e) -> go env e (go env t (vars, others))
+    | _ -> (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: 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 quietly f =
+    let was = !lit_quiet in
+    lit_quiet := true;
+    Fun.protect ~finally:(fun () -> lit_quiet := was) f
+  in
+  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 — 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 && 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
+   a text or bracket literal's typed reading ([lit_default]). *)
+and lit_init ctx t (e : Ast.expr) =
+  if Types.equal t Types.Unit then with_typed_literals (fun () -> check ctx e)
+  else check ctx ~want:t e
+
+(* [run] is a [let] or a [loop] with some of [inits] literals, and the
+   outermost such form of this function: the session opens here. See
+   [lit_session]. *)
+and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
+  fun ctx loc inits run ->
+  if ctx.lits <> None || not (List.exists (fun e -> lit_kind e <> None) inits)
+  then run ()
+  else begin
+    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;
+    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, written into
+       [s.decided], and the locals whose decision moved. *)
+    let settle () =
+      let solved = lit_solve s in
+      let moved = ref [] in
+      List.iter
+        (fun (k, name, 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 := (k, name, t) :: !moved;
+               Phys.replace s.decided k t
+             end
+           | Error _ -> ())
+        solved;
+      (solved, List.rev !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 =
+      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;
+      (* A ref, because [trial] is monomorphic inside this recursive group. *)
+      let answer = ref None in
+      (* What the settle inside the trial found, which has already written
+         its decisions: settling again outside would see nothing move. *)
+      let settled = 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
+                 settled := Some (solved, moved);
+                 (* 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
+      match outcome, !answer with
+      | Ok _, Some r -> log (); remember (); r
+      | _ ->
+        let solved, moved =
+          match !settled with Some sm -> sm | None -> 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 if moved <> [] then begin
+          (* Still moving: a local fed through more calls than the rounds
+             follow. It is the local that needs its type written. *)
+          let k, name, t = List.hd moved in
+          lit_unsettled k name t
+        end
+        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
+  end
+
+(* A literal local whose uses kept changing its type past [lit_rounds]. *)
+and lit_unsettled (k : Ast.expr) name t =
+  let lit = lit_spelling k in
+  let fix =
+    if fln_source k.Ast.loc then Printf.sprintf "let %s: %s = %s" name (tyname k.Ast.loc t) lit
+    else Printf.sprintf "(%s %s)" (tyname k.Ast.loc t) lit
+  in
+  Loc.failk "check/literal-unsettled" k.Ast.loc
+    "the type of %s depends on too long a chain of the values stored into it \
+     to be read off them. Write the type it should have: %s"
+    name fix
+
+and lit_spelling (k : Ast.expr) =
+  let lit =
+    match k.Ast.e with
+    | Ast.Int n -> Int64.to_string n
+    | Ast.Float x -> Printf.sprintf "%g" x
+    | Ast.Byte b -> Printf.sprintf "\\%c" (Char.chr b)
+    | Ast.Call (_, [ { Ast.e = Ast.Int n; _ } ]) -> Int64.to_string (Int64.neg n)
+    | Ast.Call (_, [ { Ast.e = Ast.Float x; _ } ]) -> Printf.sprintf "%g" (-.x)
+    | _ -> "..."
+  in
+  let whole = lit <> "" && String.for_all (fun c -> (c >= '0' && c <= '9') || c = '-') lit in
+  if whole && lit_kind k = Some `Float then lit ^ ".0" else lit
+
+(* Two uses of a literal local that no one type satisfies. *)
+and lit_conflict (k : Ast.expr) name t1 l1 t2 l2 =
+  let lit =
+    match k.Ast.e with
+    | Ast.Int n -> Int64.to_string n
+    | Ast.Float x -> Printf.sprintf "%g" x
+    | Ast.Byte b -> Printf.sprintf "\\%c" (Char.chr b)
+    | Ast.Call (_, [ { Ast.e = Ast.Int n; _ } ]) -> Int64.to_string (Int64.neg n)
+    | Ast.Call (_, [ { Ast.e = Ast.Float x; _ } ]) -> Printf.sprintf "%g" (-.x)
+    | _ -> "..."
+  in
+  (* %g drops the point from a whole float; put it back so the fix reads as
+     a float literal. 1e+20 already does. *)
+  let whole = lit <> "" && String.for_all (fun c -> (c >= '0' && c <= '9') || c = '-') lit in
+  let lit = if whole && lit_kind k = Some `Float then lit ^ ".0" else lit in
+  let fix =
+    if fln_source k.Ast.loc then Printf.sprintf "let %s: %s = %s" name (tyname l1 t1) lit
+    else Printf.sprintf "(%s %s)" (tyname l1 t1) lit
+  in
+  Loc.failk "check/literal-uses" k.Ast.loc
+    ~notes:[ Loc.note l1 (Printf.sprintf "%s is used as %s here" name (tyname l1 t1));
+             Loc.note l2 (Printf.sprintf "and as %s here" (tyname l2 t2)) ]
+    "%s is used as %s and as %s, and %s can have only one type. Write the \
+     one it should have: %s"
+    name (tyname l1 t1) (tyname l2 t2) lit fix
+
 and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
+  with_lits ctx loc
+    (List.filter_map
+       (fun (b : Ast.binding) -> if b.Ast.bty = None then Some b.Ast.bval else None)
+       bs)
+  @@ fun () ->
   scoped ctx (fun () ->
     let bs =
       map_lr
         (fun (b : Ast.binding) ->
            let want = Option.map (resolve ctx.env) b.Ast.bty in
-           let v = check ctx ?want b.Ast.bval in
+           let lit = if b.Ast.bty = None then lit_local ctx b.Ast.bname b.Ast.bval else None in
+           let v =
+             match lit with
+             | Some t -> lit_init ctx t b.Ast.bval
+             | None -> check ctx ?want b.Ast.bval
+           in
            (match v.Tast.ty with
             (* A refused initialiser, already reported: the name is bound to
                the poison so that what follows is still checked. *)
@@ -7165,7 +7789,10 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
                 b.Ast.bname (tyname loc v.Tast.ty)
             | _ -> ());
            (* Locals are assignable places; parameters are not. *)
-           let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
+           let slot =
+             bind ctx b.Ast.bname v.Tast.ty ~assignable:true
+               ?lit:(Option.map (fun _ -> b.Ast.bval) lit)
+           in
            (slot, v))
         bs
     in
@@ -7380,6 +8007,7 @@ and check_dotimes ctx ~want loc label name (b : Ast.bounds) body =
    below and every [continue] a [recur] mints count from the same stack [emit]
    indexes. *)
 and check_loop ctx ?want loc bs body =
+  with_lits ctx loc (List.map snd bs) @@ fun () ->
   scoped ctx (fun () ->
     (* Each initial value is evaluated once, before the loop, exactly as a
        [let]'s is and as [dotimes]'s bound is — and bound before the next is
@@ -7387,8 +8015,11 @@ and check_loop ctx ?want loc bs body =
        name. *)
     let binds =
       map_lr
-        (fun (n, v) ->
-           let v = check ctx v in
+        (fun (n, v0) ->
+           let lit = lit_local ctx n v0 in
+           let v =
+             match lit with Some t -> lit_init ctx t v0 | None -> check ctx v0
+           in
            (match v.Tast.ty with
             (* A refused initialiser, already reported: the name is bound to
                the poison so that what follows is still checked. *)
@@ -7397,7 +8028,8 @@ and check_loop ctx ?want loc bs body =
               fail v.Tast.loc "%s would be bound to %s, which is not a value" n
                 (tyname loc v.Tast.ty)
             | _ -> ());
-           (bind ctx n v.Tast.ty ~assignable:true, v))
+           (bind ctx n v.Tast.ty ~assignable:true
+              ?lit:(Option.map (fun _ -> v0) lit), v))
         bs
     in
     let names = List.map (fun (slot, v) -> (slot, v.Tast.ty)) binds in
@@ -7470,7 +8102,18 @@ and check_recur ctx ~tail loc args =
   if want <> got then
     fail loc "this loop binds %d name%s and this recur passes %d" want
       (if want = 1 then "" else "s") got;
-  let vals = List.map2 (fun a (_, ty) -> check ctx ~want:ty a) args names in
+  let vals =
+    List.map2
+      (fun a (slot, ty) ->
+         match
+           List.find_opt (fun (_, (b : binding)) -> b.slot = slot) ctx.scope
+         with
+         | Some (_, { blit = Some key; _ })
+           when (match ctx.lits with Some s -> s.recording | None -> false) ->
+           lit_down ctx key ty a
+         | _ -> check ctx ~want:ty a)
+      args names
+  in
   (* Every name is rebound at once. The new values go into temporaries first,
      so that (recur y x) swaps rather than writing y over x and then reading it
      back — the same reason Clojure's recur is simultaneous. *)
@@ -7585,7 +8228,7 @@ and check_truthy ctx c =
       (fun () ->
          try check_truthy_once ctx c
          with Loc.Error d as ex ->
-           truthy_failed := (c, scope, ctx.ret, d) :: !truthy_failed;
+           if !lit_recording = 0 then truthy_failed := (c, scope, ctx.ret, d) :: !truthy_failed;
            raise ex)
 
 and check_truthy_once ctx c =
@@ -7663,7 +8306,7 @@ and check_if ctx ?(tail = false) ?want loc c t e =
       (fun () ->
          try check_if_once ctx ~tail ?want loc c t e
          with Loc.Error d as ex ->
-           Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), want, d);
+           if !lit_recording = 0 then Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), want, d);
            raise ex)
 
 and check_if_once ctx ~tail ?want loc c t e =
@@ -7752,7 +8395,7 @@ and check_if_once ctx ~tail ?want loc c t e =
             with
             | Ok v -> Ok v
             | Error d ->
-              Hashtbl.add arm_failed e.Ast.loc (e, key, t.Tast.ty, d);
+              if !lit_recording = 0 then Hashtbl.add arm_failed e.Ast.loc (e, key, t.Tast.ty, d);
               Error d
         in
         let meet v =
@@ -7881,7 +8524,7 @@ and literal_join ctx (a : Ast.expr) (b : Ast.expr) =
     | _ -> probe ctx x.Ast.loc (fun () -> (check ctx x).Tast.ty)
   in
   match own a, own b with
-  | Some x, Some y -> Types.join x y
+  | Some x, Some y -> literal_meet x y
   | _ -> None
 
 (* Whether a name would reach a callee if it were called — a global function, a
@@ -7942,7 +8585,7 @@ and generic_ctor ctx ~want loc name given =
     (* A literal's own type, the one it has with nothing expected of it. *)
     let literal_type (a : Ast.expr) =
       match a.Ast.e with
-      | Ast.Float _ -> Types.Float Types.F64
+      | Ast.Float _ -> Types.Float (float_default ())
       | Ast.UInt _ -> Types.Int Types.U64
       | Ast.Byte _ -> Types.Int Types.U8
       | _ -> Types.Int Types.I32
@@ -7991,7 +8634,7 @@ and generic_ctor ctx ~want loc name given =
            (match List.assoc_opt v !subst with
             | None -> subst := (v, t) :: !subst; lit_only := v :: !lit_only
             | Some b ->
-              (match Types.join b t with
+              (match literal_meet b t with
                | Some j -> subst := (v, j) :: List.remove_assoc v !subst
                | None ->
                  fail a.Ast.loc "%s's .%s is %s here, and this is %s"
@@ -8459,12 +9102,13 @@ and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
     List.filter (fun t -> t <> Types.Never) (List.map snd typed)
   in
   let lit_tys = List.filter_map natural lits in
-  let join_all = function
+  let join_with meet = function
     | [] -> None
     | t :: ts ->
       List.fold_left
-        (fun acc t -> Option.bind acc (fun a -> Types.join a t)) (Some t) ts
+        (fun acc t -> Option.bind acc (fun a -> meet a t)) (Some t) ts
   in
+  let join_all = join_with Types.join in
   let mixed_dyn =
     List.mem Types.Dyn tys
     && (List.exists (fun t -> t <> Types.Dyn) tys || lits <> [])
@@ -8480,7 +9124,8 @@ and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
         List.fold_left
           (fun acc i ->
              if fits t i then acc
-             else Option.bind acc (fun a -> Option.bind (natural i) (Types.join a)))
+             else
+               Option.bind acc (fun a -> Option.bind (natural i) (Types.join a)))
           (Some t) lits
       in
       (match t' with
@@ -8489,7 +9134,7 @@ and arr_elem_type ctx (items : Ast.expr list) : Types.t option =
   in
   let candidates =
     if tys <> [] then [ join_all tys ]
-    else join_all lit_tys :: List.map Option.some lit_tys
+    else join_with literal_meet lit_tys :: List.map Option.some lit_tys
   in
   if mixed_dyn then None
   else if tys = [] && lits = [] then
@@ -9263,7 +9908,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
          List.fold_left
            (fun acc x ->
               Option.bind acc (fun a ->
-                Option.bind (literal_join ctx first x) (Types.join a)))
+                Option.bind (literal_join ctx first x) (literal_meet a)))
            (literal_join ctx first first) rest
        in
        (match j with
@@ -9340,7 +9985,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
                    (match trial ctx (at (Some w)) with
                     | Ok b -> Ok b
                     | Error d ->
-                      Hashtbl.add arm_failed head.Ast.loc
+                      if !lit_recording = 0 then Hashtbl.add arm_failed head.Ast.loc
                         (head, (ctx.scope, ctx.ret), w, d);
                       Error d)
                in
@@ -11449,6 +12094,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          { Ast.e = Ast.Int i; _ }; { Ast.e = Ast.Int n; _ };
          { Ast.e = Ast.Int exact; _ } ] ->
        let plural k = if Int64.equal k 1L then "" else "s" in
+       lit_typed_use ctx target;
        let target = check ctx target in
        (match target.Tast.ty with
         | Types.Array (m, elem) ->
@@ -11930,6 +12576,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
   | "clone" ->
     (match args with
      | target :: rest when List.length rest <= 1 ->
+       lit_typed_use ctx target;
        (* Checked once, then dispatched on what it turned out to be: checking
           it inside a guard as well would allocate the target's slots twice and
           evaluate whatever it was written as twice. *)
@@ -12676,6 +13323,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          "slice is (slice a), (slice a lo) or (slice a lo hi) — given %d \
           arguments" (List.length args)
      | target :: bounds ->
+       lit_typed_use ctx target;
        let target = check_target ctx target in
        let ty = target.Tast.ty in
        match ty with
@@ -12879,6 +13527,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
   | "addr" ->
     arity ctx loc name 1 args;
     let a = List.hd args in
+    lit_typed_use ctx a;
     (match place_of_expr a with
      | None ->
        fail a.Ast.loc
@@ -13387,6 +14036,11 @@ and named_call ?(qualified = false) ctx ~want loc name args =
         when Int64.compare n (-2147483648L) < 0
              || Int64.compare n 2147483647L > 0 -> Some target
       | Ast.UInt _, (Types.Int _ | Types.Float _) -> Some target
+      (* A float literal likewise: (f64 0.1) is the f64 nearest 0.1 and not
+         the f32 one widened, and (u64 1.8e19) converts the f64 it says. *)
+      | _, Types.Float _ when lit_kind (List.hd args) = Some `Float -> Some target
+      | _, Types.Int _ when lit_kind (List.hd args) = Some `Float ->
+        Some (Types.Float Types.F64)
       | _ -> None
     in
     let a = check ctx ?want (List.hd args) in
@@ -14400,7 +15054,7 @@ and trial ctx f =
      Only [Loc.Error] is caught. A timeout or a stack overflow is not a
      refusal to reconsider, and silently continuing past one would turn a
      resource failure into a wrong answer. *)
-  let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
+  let[@warning "+9"] { env = _; ret = _; lits = _; slots; slot_tys; slot_names; scope;
                        defers; defer_slot; defer_ok; defer_block; outer = _;
                        outer_what; caught; place_ok; envslot; parent = _;
                        in_frames; loops; tail; in_defer;
@@ -14463,12 +15117,58 @@ and trial_at ctx (y : Ast.expr) (w : Types.t) =
     (match trial ctx (fun () -> check ctx ~want:w y) with
      | Ok b -> Ok b
      | Error d ->
-       Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d);
+       if !lit_recording = 0 then Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d);
        Error d)
 
 and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
   match args with
-  | [ x; y ] ->
+  | [ 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
@@ -14579,7 +15279,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]
@@ -15144,7 +15843,9 @@ let check_parents env =
    that still does not check once no progress is left has a real error, so
    the last round is run without swallowing it. *)
 let settle_consts env consts =
-  let infer (_, v) = (check (invented_ctx env Types.Unit) v).Tast.ty in
+  let infer (_, v) =
+    with_typed_literals (fun () -> (check (invented_ctx env Types.Unit) v).Tast.ty)
+  in
   let pending = ref consts in
   let rec settle () =
     let left =
@@ -16184,12 +16885,12 @@ and read_return env (fn : Ast.fn) params =
   | (t0, l0, _) :: _ ->
     (* Where no join exists the first typed exit's type is the one checked
        against, so the refusal is the one [if] gives its else arm. *)
-    let meet = function
+    let meet ?(join = arm_join) = function
       | [] -> None
       | ((t, l, _) :: _) as xs ->
         let j =
           List.fold_left
-            (fun acc (u, _, _) -> Option.bind acc (fun a -> arm_join a u))
+            (fun acc (u, _, _) -> Option.bind acc (fun a -> join a u))
             (Some t) xs
         in
         let at =
@@ -16205,7 +16906,9 @@ and read_return env (fn : Ast.fn) params =
     let decided =
       match meet (List.filter (fun (_, _, lit) -> not lit) arrive) with
       | Some d -> d
-      | None -> Option.value (meet arrive) ~default:(t0, l0)
+      | None ->
+        (* Every exit a literal: they meet as two literals do. *)
+        Option.value (meet ~join:literal_meet arrive) ~default:(t0, l0)
     in
     ignore (attempt (fst decided));
     decided
@@ -16784,7 +17487,7 @@ let check_global env (d : Ast.decl) : Tast.global option =
                  ~pattern:(match v.Ast.e with Ast.Int _ -> false | _ -> true)
                  v.Ast.loc kind k, kind); ty;
           loc = d.Ast.dloc }
-      | _ -> check (ctx ()) ~want:ty v
+      | _ -> with_typed_literals (fun () -> check (ctx ()) ~want:ty v)
     in
     no_union_const env d.Ast.dloc n ginit;
     (* After the union's own refusal, so a computed union member keeps the
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 59cd0d2a..d4f500d7 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -1125,13 +1125,86 @@ _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;
+  }
+  /* An argument the compiler could not spell is an ellipsis, and a fix with
+   * a hole in it is a conversion to make, not code to paste. */
+  int holed = strstr(fix, "\xe2\x80\xa6") != NULL;
+  if (ok && used > 0)
+    flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s. %s %s",
+             (int)namelen, (const char *)name, (int)wantlen, (const char *)want,
+             (int)plen[0], (const char *)part[0],
+             holed ? "Convert the argument with" : "Write", 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
new file mode 100644
index 00000000..71aefc48
--- /dev/null
+++ b/test/programs/literal-locals.flan
@@ -0,0 +1,82 @@
+;;;; A number literal bound by let or loop takes its type from its uses in
+;;;; the function. Each line's expected output is beside it.
+
+;; A set of an i64 sum makes the accumulator an i64.
+(defn total [xs [i64]] i64
+  (let [t 0]
+    (dotimes [i (length xs)]
+      (set t (+ t (at xs i))))
+    t))
+
+;; The operand beside it: an f64 accumulator from a float literal.
+(defn mean [xs [f64]] f64
+  (let [s 0.0]
+    (dotimes [i (length xs)]
+      (set s (+ s (at xs i))))
+    (/ s (f64 (length xs)))))
+
+;; A counter compared with an i64 bound counts past i32.
+(defn count-to [n i64] i64
+  (let [i 0]
+    (while (< i n)
+      (set i (+ i 1000000000)))
+    i))
+
+;; A set of one literal local into another links them: b holds a value past
+;; i32, so a is an i64 too.
+(defn linked [] i64
+  (let [a 0 b 0]
+    (set b 3000000000)
+    (set a b)
+    a))
+
+;; Two locals fed from each other: i is counted against an i64, and acc
+;; sums a literal past i32.
+(defn sum-to [n i64] i64
+  (let [i 0 acc 0]
+    (while (< i n)
+      (set acc (+ acc 1000000000))
+      (set i (+ i 1)))
+    acc))
+
+;; Inside a generic body the literal takes the type variable.
+(defn sum-of [xs [$t]] $t {:where (numeric? $t)}
+  (let [acc 0]
+    (dotimes [i (length xs)]
+      (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])
+        gs (the [2 u8] [200 50])]
+    (println (total (slice xs 0 3)))               ; 3000000009
+    (println (mean (slice fs 0 2)))                ; 0.375
+    (println (count-to 5000000000))                ; 5000000000
+    (println (linked))                             ; 3000000000
+    (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
+  0)
diff --git a/test/programs/restarts.flan b/test/programs/restarts.flan
index 961c079f..cc799dc5 100644
--- a/test/programs/restarts.flan
+++ b/test/programs/restarts.flan
@@ -101,6 +101,15 @@
   (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 doubled [n i32] i32
+  (handler-bind [(AssetMissing [c] (let [big (i64 7)] (invoke-restart 'use-value (* big 2))))]
+    (supplied n)))
+
 (defn main [args [str]] i32
   ;; One argument selects a trap; none runs the table's case.
   (if (> (length args) 1)
@@ -110,6 +119,8 @@
         (= k 2) (print (mistyped 91))
         (= k 3) (print (overfull 92))
         (= k 4) (print (mislaid 93))
+        (= k 5) (print (widened 94))
+        (= k 6) (print (doubled 95))
         :else (println "?"))
       (return 0)))
 
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index d5591101..0e71bb29 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -389,6 +389,14 @@ let () =
     outputs "value semantics" "programs/values.flan" values_out;
     outputs "machine surface" "programs/machine.flan" machine_out;
     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\n3000000005\n0.1 5000000000\ntrue\n7 1.5\n"
+    in
+    outputs "literal locals take their uses' type" "programs/literal-locals.flan"
+      literal_locals_out;
+    outputs ~x86:true "literal locals take their uses' type, --x86"
+      "programs/literal-locals.flan" literal_locals_out;
     (* Comparisons over three operands and more. The lines that carry the
        whole claim are the tag transcripts: [abc -> false] is a chain whose
        *first* link already decided the answer and whose middle operand —
@@ -1467,6 +1475,10 @@ 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)";
+      refuses "and the argument as it was written when it is an expression" "6"
+        "restart use-value takes (i32), given (i64). Write (i32 (* big 2))";
       (try Sys.remove exe with Sys_error _ -> ())
     in
     restart_mismatch ();
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 3655f7fb..1dedf61e 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1086,6 +1086,53 @@ let () =
      two [infers] above still hold — and this is the position that had no way
      to say it. *)
   infers "array constructor"     "(array 4 f32)" "[4 f32]";
+  (* A literal bound by a let takes its type from its uses in the function,
+     and two uses no one type satisfies are refused with the annotation. *)
+  accepts "a literal local takes the type set into it"
+    "(defn f [x i64] i64 (let [t 0] (set t (+ t x)) t))";
+  accepts "a literal local takes an operand's type"
+    "(defn f [x f64] f64 (let [s 0.0] (set s (+ s x)) s))";
+  accepts "recur rebinds a literal local at the type it brings"
+    "(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))";
+  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)";
+  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";
+  (* Chains through a second round, and through do, let and if arms that
+     merge without one. *)
+  accepts "a literal local fed through do, however long the chain"
+    "(defn f [x i64] i64 (let [a0 0 a1 0 a2 0 a3 0 a4 0 a5 0 a6 0 a7 0 a8 0 a9 0 a10 0 \
+     a11 0 a12 0] (set a0 x) (set a1 (do a0)) (set a2 (do a1)) (set a3 (do a2)) \
+     (set a4 (do a3)) (set a5 (do a4)) (set a6 (do a5)) (set a7 (do a6)) \
+     (set a8 (do a7)) (set a9 (do a8)) (set a10 (do a9)) (set a11 (do a10)) \
+     (set a12 (do a11)) a12))";
+  accepts "a literal local fed through a let"
+    "(defn f [x i64] i64 (let [a0 0 a1 0 a2 0] (set a0 x) (set a1 (let [t a0] t)) \
+     (set a2 (let [t a1] t)) a2))";
+  accepts "a literal local fed through both arms of an if"
+    "(defn f [x i64] i64 (let [a0 0 a1 0] (set a0 x) (set a1 (if true a0 a0)) a1))";
+  accepts "a literal local fed through a generic call settles in rounds"
+    "(defn same [x $t] $t x) (defn f [x i64] i64 (let [a0 0 a1 0 a2 0] (set a0 x) \
+     (set a1 (same a0)) (set a2 (same a1)) a2))";
+  rejects_check "a chain the rounds cannot follow names the local to annotate"
+    ~needle:"the type of a7 depends on too long a chain of the values stored into \
+             it to be read off them. Write the type it should have: (i64 0)"
+    "(defn same [x $t] $t x) (defn f [x i64] i64 (let [a0 0 a1 0 a2 0 a3 0 a4 0 a5 0 \
+     a6 0 a7 0 a8 0 a9 0 a10 0] (set a0 x) (set a1 (same a0)) (set a2 (same a1)) \
+     (set a3 (same a2)) (set a4 (same a3)) (set a5 (same a4)) (set a6 (same a5)) \
+     (set a7 (same a6)) (set a8 (same a7)) (set a9 (same a8)) (set a10 (same a9)) a10))";
+  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)"
+    "(defn u [x u32] u32 x) (defn i [x i32] i32 x) \
+     (defn f [] i32 (let [x 0] (u x) (i x)) 0)";
   infers "array of a struct"     "(array 2 i32)" "[2 i32]";
   infers "array of an array"     "(array 2 [3 u8])" "[2 [3 u8]]";
   (* (array-fill [r c] v): the same type at any rank, with the element type