diff --git a/TODO.org b/TODO.org
index b1169f74..3bd9439b 100644
--- a/TODO.org
+++ b/TODO.org
@@ -33,9 +33,10 @@ disagree are refused with a request for an annotation. Vector, map and text lite
 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.
-Local inference is in (check.ml [lit_session]). The f32 default and dyn text and vector
-literals wait on the author's answers to the phase-1 measurements; =FLAN_LIT=f32,dyn= in
-check.ml is the measuring switch, to be deleted with them.
+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
+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/emacs/test-flan.el b/emacs/test-flan.el
index 7712e455..39fd3406 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 = f64$" text)
+                                 (string-match-p "^;; selection-sort at \\$t = f32$" text)
                                  (string-match-p "^define .*flan\\.selection-sort-i32" text)
-                                 (string-match-p "^define .*flan\\.selection-sort-f64" text)))
+                                 (string-match-p "^define .*flan\\.selection-sort-f32" 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 62929a34..6ecc2894 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -769,6 +769,15 @@ let lit_recording = ref 0
    so its use is recorded as a [Hint] and not an [Up]. *)
 let lit_hint = 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 = {
@@ -3631,13 +3640,15 @@ let restart_sig tys =
 let dyn_i64 = Types.Int Types.I64
 let dyn_f64 = Types.Float Types.F64
 
-(* The switch the literal rules of TODO.org's "Dyn unless annotated" were
-   measured with: [f32] makes an unconstrained float literal f32, [dyn] makes
-   an unwanted text or vector literal dyn, [log] prints each literal local
-   inference moved off its default. Deleted once those rules are decided. *)
+(* 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)
-let float_default () = if lit_has "f32" then Types.F32 else Types.F64
+(* An unconstrained float literal is an f32, as an integer one is an i32. *)
+let float_default () = Types.F32
 
 (* ── Literal locals ([lit_session]) ────────────────────────────────── *)
 
@@ -3651,13 +3662,18 @@ let lit_kind (e : Ast.expr) =
   | 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 = 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
@@ -3669,6 +3685,7 @@ 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
 
 let lit_rounds = 3
@@ -3701,7 +3718,8 @@ let lit_solve (s : lit_session) =
     (fun (k, name) ->
        let members = List.filter (fun m -> List.exists (fun (k', _) -> k' == m) keys) (group k) in
        let kind =
-         if List.exists (fun m -> lit_kind m = Some `Float) members then `Float
+         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 =
@@ -3712,6 +3730,7 @@ let lit_solve (s : lit_session) =
          |> 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
@@ -4861,6 +4880,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]. *)
@@ -5870,8 +5899,14 @@ 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);
     mk loc (Types.Float k) (Tast.Float (x, k))
-  | Ast.Str s when want = None && lit_has "dyn" -> box loc (mk loc Types.String (Tast.Str s))
+  | 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
@@ -6171,7 +6206,7 @@ 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" ->
+  | 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
@@ -6536,7 +6571,8 @@ and var ctx ?(qualified = false) loc ~want name =
             | _ -> 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;
-      mk loc t (Tast.Local b.slot)
+      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)
     | 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:
@@ -7249,6 +7285,17 @@ 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 ->
+       s.cons <- (key, (Up, Types.Unit, e.Ast.loc)) :: s.cons
+     | _ -> ())
+  | _ -> ()
+
 (* The literal local [n] names, while its uses are being recorded. *)
 and lit_recorded ctx n =
   match ctx.lits, lookup ctx n with
@@ -7299,6 +7346,12 @@ and lit_local ctx name (e : Ast.expr) =
     Some (match List.assq_opt e s.decided with Some t -> t | None -> lit_default 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]. *)
@@ -7385,8 +7438,11 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
         (fun (b : Ast.binding) ->
            let want = Option.map (resolve ctx.env) b.Ast.bty in
            let lit = if b.Ast.bty = None then lit_local ctx b.Ast.bname b.Ast.bval else None in
-           let want = match lit with Some t -> Some t | None -> want in
-           let v = check ctx ?want b.Ast.bval 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. *)
@@ -7624,7 +7680,9 @@ and check_loop ctx ?want loc bs body =
       map_lr
         (fun (n, v0) ->
            let lit = lit_local ctx n v0 in
-           let v = check ctx ?want:lit 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. *)
@@ -8129,7 +8187,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
@@ -8239,7 +8297,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"
@@ -8707,12 +8765,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 <> [])
@@ -8728,7 +8787,13 @@ 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 ->
+                 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))
           (Some t) lits
       in
       (match t' with
@@ -8737,7 +8802,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
@@ -9511,7 +9576,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
@@ -11568,6 +11633,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) ->
@@ -12049,6 +12115,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. *)
@@ -12795,6 +12862,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
@@ -12998,6 +13066,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
@@ -13506,6 +13575,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
@@ -15269,7 +15343,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 =
@@ -16309,12 +16385,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 =
@@ -16330,7 +16406,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
@@ -16905,7 +16983,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/test/programs/x86-p12-handler-value.flan b/test/programs/x86-p12-handler-value.flan
index faa843a2..2bd60423 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 2.5))]
+  (handler-bind [(Oops [c] (invoke-restart 'use-value (f64 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 a0d42819..98661f13 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -3614,7 +3614,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 f64 {.a 1 .b 2.5})\n6\n\
+       (Pair i32 {.a 2 .b 1}) (Pair f32 {.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 +3791,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" "f64 is not hashable?";
+      "programs/generic-map-reject.flan" "f32 is not hashable?";
     refuses "and it names the type the call site asked for"
-      "programs/generic-map-reject.flan" "at $t = f64";
+      "programs/generic-map-reject.flan" "at $t = f32";
 
     (* 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 be21fb4e..dc32caec 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 f64: %s" backend (said r)
+        if status r <> "ok" then fail "%s: calling the generic at f32: %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 = f64" || types b <> "$t = i32" then
+              if types a <> "$t = f32" || 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 d8189f64..631c562a 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 f64" "0.5" "f64";
+  infers "float defaults to f32" "0.5" "f32";
   infers "byte is u8"            "\\space" "u8";
   infers "string"                "\"hi\"" "str";
   infers "bool"                  "true" "bool";
@@ -1096,6 +1096,13 @@ 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)"
+    "(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 "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)"
@@ -1108,7 +1115,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 f64]]";
+  infers "array-fill, rank 2"    "(array-fill [2 3] 0.5)" "[2 [3 f32]]";
   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. *)
@@ -1129,7 +1136,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)" "f64";
+  infers "int literal into a float" "(+ 1 0.5)" "f32";
   rejects_check "float literal into an int"
     "(defn f [] i32 (+ 1 0.5))" ~needle:"expected i32";
 
@@ -3828,7 +3835,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 f64";
+    ~needle:"expected u8, found f32";
   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 \
@@ -6718,7 +6725,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:"f64 is not integer?"
+    ~needle:"f32 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
@@ -7676,7 +7683,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 f64" "[1 2.5]" "[2 f64]";
+  infers "an int and a float literal meet at the float" "[1 2.5]" "[2 f32]";
   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";
@@ -7726,10 +7733,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 wider" "(if true 1 2.5)" "f64";
+  infers "two literal if arms meet at the float" "(if true 1 2.5)" "f32";
   infers "two integer if arms stay i32" "(if true 1 2)" "i32";
-  infers "two literal match arms meet at the wider"
-    "(match (Some 1) (Some v) 1 None 2.5)" "f64";
+  infers "two literal match arms meet at the float"
+    "(match (Some 1) (Some v) 1 None 2.5)" "f32";
   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"
@@ -7846,7 +7853,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] f64";
+     ("(defn f [c bool] _ (when c (return 1)) 2.5)" ^ main) "f" "f [bool] f32";
    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 328158fd..503dd716 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-f64" c.Session.fns) then
+     if not (List.mem "same-f32" 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-f64") then
+     if not (has e.Session.ir "pick-f32") 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-f64" ];
+       [ "hold-i32"; "hold-f32" ];
      (* 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-f64" ]
+       [ "put-at-i32"; "put-at-f32" ]
    | 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 f64, so [pick-f64] exists in no program
+     fixture never calls [pick] at f32, so [pick-f32] exists in no program
      anywhere; redefining the *caller* to ask for it has to build and install
-     it. Nothing in the form names [pick-f64] — it is found by being an
+     it. Nothing in the form names [pick-f32] — 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-f64" c.Session.fns) then
+     if not (List.mem "pick-f32" c.Session.fns) then
        fail "a redefinition needing a new instantiation did not install \
-             pick-f64; it installed %s" (String.concat " " c.Session.fns)
+             pick-f32; 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-f64") then
+     if not (has e.Session.ir "pick-f32") 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);