diff --git a/TODO.org b/TODO.org
index a1d37892..6bdf7bdc 100644
--- a/TODO.org
+++ b/TODO.org
@@ -628,51 +628,32 @@ awaiting confirmation, and the build order. Rules out Parinfer, wisp and
 sweet-expressions, and a simplified in-paren syntax — all thin the parens
 without removing them.
 
-** TODO A one-line if cannot take its else on the next line
-=if c then a= then =else b= under it is refused. Proposal: an =else=/=elif= at
-the if's column continues a one-line if, as F#'s does.
-
-** TODO A lambda with a block cannot be a call's argument
-=sort-by(xs, fn(a, b)= plus a block is refused; the lambda has to be bound first,
-with its type written. Proposal: a call ending in =fn(...)= and a trailing =:=
+** WAIT A lambda with a block cannot be a call's argument
+On the author's decision. =sort-by(xs, fn(a, b)= plus a block is refused; the
+lambda has to be bound first with =let=. Proposal: a call ending in =fn(...)= and a trailing =:=
 hands the block to that lambda: =sort-by(xs, fn(a, b)):=.
 
-** TODO A lambda's parameters cannot be typed
-=fn(a, b)= takes bare names, so a lambda bound by =let= needs
-=let f: Fn(C, C) -> bool = fn(a, b)=. Proposal: =fn(a: C, b: C)= as in a
-=fn= definition.
-
-** TODO A condition struct with a parent has no sugar
-=defstruct(DiskFull, :parent, IoError, [free i64])= is the fallback, with a
+** WAIT A condition struct with a parent has no sugar
+On the author's decision. =defstruct(DiskFull, :parent, IoError, [free i64])= is the fallback, with a
 paren field vector. Proposal: =struct DiskFull :parent IoError= plus field lines.
 
-** TODO defmacro has no sugar
-=defmacro(repeat, [i n & body]):= with a space-separated parameter vector.
+** WAIT defmacro has no sugar
+On the author's decision. =defmacro(repeat, [i n & body]):= with a space-separated parameter vector.
 Proposal: =macro repeat(i, n, & body)= plus a block.
 
-** TODO loop/recur has no sugar
-=loop([x a y b]):=. Proposal: =loop x = a, y = b= plus a block; =recur(...)=
+** WAIT loop/recur has no sugar
+On the author's decision. =loop([x a y b]):=. Proposal: =loop x = a, y = b= plus a block; =recur(...)=
 stays a call.
 
-** TODO A restart's report string is a body line
-=:report= and its string sit as two statements under =restart name()=.
-Proposal: =restart name() "report text"= on the header line.
+** TODO Hard-coded code in messages is still paren syntax in a .fln file
+Types follow the code's syntax now (=Types.spell=). Hints written into a message's
+text — =(Ptr %s)=, =(clone v)=, =(the T x)= in most of =check.ml= and =parse.ml=, the
+runtime's =(get 0 :body)= and =(/ x 0)= — still print parens; each is fixed per
+message as it is met.
 
-** TODO An enum member has only a keyword spelling
-=:north= works, =Dir.north= is an unknown name, while a data case is
-=Shape.Rect=. Proposal: accept =Dir.north= as the member.
-
-** TODO Checker and runtime messages print types and fixes in parens
-In a .fln file, =(Fn [A] R)=, =(Option i32)=, =(get 0 :body)=, =(/ x 0)= and most
-usage hints still print paren syntax; a handful now print .fln spellings.
-Proposal: =Types.to_string= and the hints take the syntax of the location's file.
-
-** TODO flan convert separates adjacent one-line globals with blank lines
-=once a: i32= on consecutive lines come back one blank line apart.
-
-** TODO A bad map key type is followed by unknown-name errors for its parts
-=map-new([const u8], i32)= reports the key, then "unknown name const" and
-"unknown name i32" — in both syntaxes.
+** CANCELLED Sugar for defclass, defgeneric, defmulti and defmethod
+CLOSED: [2026-09-26]
+The fallback, =defmethod(area, point, [p]):=, reads well enough.
 
 ** TODO The shims in sand.flan can go
 =sand.flan= defines =dyn->f64= and =dyn->u32=, one-line functions whose only job
diff --git a/lib/check.ml b/lib/check.ml
index 6e093a0d..b0fa4688 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -20,6 +20,9 @@
 
 let fail = Loc.fail
 
+(* A type in a message about the code at [loc], in that code's syntax. *)
+let tyname (loc : Loc.t) t = Types.spell ~indented:(Source.indented_at loc) t
+
 (* "A literal could not be built at the type this site asked for": 300 at a u8,
    1.5 at an i32, 3000000000 at the i32 an unconstrained integer defaults to.
 
@@ -1064,6 +1067,17 @@ let one_edit a b =
     else ta a (!i + 1) = ta b !i
   end
 
+(* [Dir.north] as the enum and the member's value, when [Dir] is an enum
+   with a member [north]. *)
+let enum_member env name =
+  match String.rindex_opt name '.' with
+  | Some i when i > 0 && i < String.length name - 1 ->
+    let e = String.sub name 0 i and m = String.sub name (i + 1) (String.length name - i - 1) in
+    (match Hashtbl.find_opt env.enums e with
+     | Some members -> Option.map (fun v -> (e, v)) (List.assoc_opt m members)
+     | None -> None)
+  | _ -> None
+
 (* The enum members' own near miss. One edit away is the usual typo; the
    second rule is for a package whose members carry a disambiguating prefix —
    raylib's Key spells them [key-r], [key-space] — where the natural mistake
@@ -1207,7 +1221,7 @@ let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
   if Types.equal v Types.Unit then
     fail loc
       "a map value cannot be () — write (Map %s bool) and ignore the value"
-      (Types.to_string k);
+      (tyname loc k);
   if Types.equal k Types.Unit then
     fail loc "a map key cannot be () — every key would be the same key";
   (* The key, as far as the type alone can say. A struct passes here and is
@@ -1225,7 +1239,7 @@ let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
     fail loc
       "%s is not a map key. A key is an integer, an enum, a bool, a string, a \
        fixed array of those, or a struct of those"
-      (Types.to_string k);
+      (tyname loc k);
   Types.Map (k, v)
 
 (* The positions a function value may not be written in, and the one reason
@@ -1265,12 +1279,12 @@ let callable_ty t = fn_sig t <> None
    field that holds one. *)
 let rec no_zeroed_fn loc what (t : Types.t) =
   match t with
-  | Types.Fn _ ->
+  | Types.Fn (ps, r) ->
     fail loc
       "%s cannot be %s — it would be zeroed, and a zeroed function value is a \
        null pointer. Pass it as a parameter, hold it in a let, or store a \
-       (CFn ...) if it captures nothing"
-      what (Types.to_string t)
+       %s if it captures nothing"
+      what (tyname loc t) (tyname loc (Types.CFn (ps, r)))
   | Types.Array (_, e) -> no_zeroed_fn loc what e
   | _ -> ()
 
@@ -1404,7 +1418,8 @@ let struct_app g args =
     Hashtbl.replace struct_apps key (g, args);
     Hashtbl.replace Types.display key
       (Printf.sprintf "(%s %s)" g
-         (String.concat " " (List.map Types.to_string args)))
+         (String.concat " " (List.map Types.to_string args)));
+    Hashtbl.replace Types.display_app key (g, args)
   end;
   key
 
@@ -1655,7 +1670,7 @@ and struct_copy ?(at_definition = false) env loc name targs =
         (List.map
            (fun (h, a) ->
               Printf.sprintf "(%s %s)" h
-                (String.concat " " (List.map Types.to_string a)))
+                (String.concat " " (List.map (tyname loc) a)))
            (env.schain @ [ (name, targs) ]))
     in
     if List.exists
@@ -1716,7 +1731,7 @@ and struct_copy ?(at_definition = false) env loc name targs =
              Loc.notes =
                d.Loc.notes
                @ [ Loc.note loc
-                     (Types.to_string (Types.Named key) ^ " is made here") ] }
+                     (tyname loc (Types.Named key) ^ " is made here") ] }
        | e -> raise e)
   end
 
@@ -1917,7 +1932,7 @@ and array_len env loc = function
      | Some (Types.Var _) -> abstract_len
      | Some t ->
        fail loc "%s is the type %s here, and an array length is an integer, a \
-                 constant or a length variable" n (Types.to_string t)
+                 constant or a length variable" n (tyname loc t)
      | None when List.mem bare env.lenvars -> abstract_len
      | None when List.mem bare env.tyvars ->
        fail loc "%s is a type variable, and an array length is an integer, a \
@@ -2767,8 +2782,8 @@ let unconstrained env loc op ~needs (t : Types.t) =
         "%s over the type variable %s: nothing declares %s %s. Write \
          {:where (%s %s)} at the head of the body, or take the operation as \
          a parameter, a (Fn [%s %s] ...), and call it here"
-        op (Types.to_string t) (Types.to_string t) needs needs
-        (Types.to_string t) (Types.to_string t) (Types.to_string t)
+        op (tyname loc t) (tyname loc t) needs needs
+        (tyname loc t) (tyname loc t) (tyname loc t)
 
 
 (* ── The runaway instantiation, refused by name rather than by depth ────
@@ -2803,7 +2818,7 @@ let runaway env loc gname cparams =
       (List.map
          (fun (g, ps, l) ->
             Printf.sprintf "%s at (%s), asked for at %s" g
-              (String.concat " " (List.map Types.to_string ps))
+              (String.concat " " (List.map (tyname loc) ps))
               (Loc.to_string l))
          (env.chain @ [ (gname, cparams, loc) ]))
   in
@@ -3046,19 +3061,19 @@ let refuse_const_place env loc (view : Types.t) =
     Loc.failk "check/store-through-const" loc
       "this changes the %s behind a %s, which can only be read through. A \
        container that has to change is handed over as a (Ptr %s)"
-      (Types.to_string t) (Types.to_string view) (Types.to_string t)
+      (tyname loc t) (tyname loc view) (tyname loc t)
   | Types.Ptr (_, t) ->
     Loc.failk "check/store-through-const" loc
       "this writes through a %s, which can only be read, so what it points at \
        is a value and not a place. (deref p) copies the %s out, and the copy \
        can be written"
-      (Types.to_string view) (Types.to_string t)
+      (tyname loc view) (tyname loc t)
   | _ ->
     let elem = match view with Types.Slice (_, t) -> t | t -> t in
     Loc.failk "check/store-through-const" loc
       "this writes through a %s, which can only be read, so the element is a \
        value and not a place. %s"
-      (Types.to_string view)
+      (tyname loc view)
       (match const_copy env elem with
        | Some c ->
          Printf.sprintf
@@ -3066,7 +3081,7 @@ let refuse_const_place env loc (view : Types.t) =
             into one" c
        | None ->
          Printf.sprintf "Where it has to be written, take it as a [%s] instead"
-           (Types.to_string elem))
+           (tyname loc elem))
 
 (* A runtime call, with the result type spelled at the site. *)
 let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
@@ -3433,7 +3448,7 @@ let widen loc (want : Types.t) (e : Tast.expr) =
 let no_dyn_yet loc ~into t extra =
   Loc.failk "check/dyn-not-yet" loc
     "%s does not cross into %s yet%s"
-    (Types.to_string t) (if into then "dyn" else "a written type") extra
+    (tyname loc t) (if into then "dyn" else "a written type") extra
 
 (* M2 item 3: a typed container crossing into dyn as a view. The element set
    is exactly the unboxable scalars — i64, f64, bool — and that is not a smaller
@@ -3490,7 +3505,7 @@ let view_subject (e : Tast.expr) =
   | _ -> None
 
 let view_refusal kind loc (e : Tast.expr) reason =
-  let ty = Types.to_string e.Tast.ty in
+  let ty = tyname loc e.Tast.ty in
   let fln = fln_source loc in
   (* A parameter is made by the caller, so its fix is its declaration. The
      name is compared as well as the slot: a closure numbers its slots from
@@ -3539,7 +3554,7 @@ let view_not_yet loc (e : Tast.expr) (elem : Types.t) =
     (Printf.sprintf
        "A dyn value can see into a typed container only when its elements \
         are i64, f64 or bool, and these are %s"
-       (Types.to_string elem))
+       (tyname loc elem))
 
 (* M2 item 3's second guard, added on review: a view's descriptor holds an
    address into the container's own storage, chased fresh on every
@@ -3952,7 +3967,7 @@ let box loc (e : Tast.expr) : Tast.expr =
       "%s does not cross into dyn: a dyn view can be written through, and a \
        [const %s] can only be read. A dyn view is taken of the writable \
        storage it came from"
-      (Types.to_string e.Tast.ty) (Types.to_string elem)
+      (tyname loc e.Tast.ty) (tyname loc elem)
   | Types.Slice (Types.Mut, elem) ->
     (match view_elem elem with
      | None -> view_not_yet loc e elem
@@ -4123,7 +4138,7 @@ let box_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
     Loc.failk "check/option-nested-dyn" loc
       "(Option (Option %s)) does not cross into dyn — Some None and None \
        would both box as nil"
-      (Types.to_string inner)
+      (tyname loc inner)
   | _ ->
     (* A literal [Some]/[None] built right here skips the runtime check: the
        checker already knows which case it is, so there is nothing to test at
@@ -4159,7 +4174,7 @@ let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
     Loc.failk "check/option-nested-dyn" loc
       "(Option (Option %s)) does not cross from dyn — a dyn has one absence, \
        nil, which cannot tell None from Some None apart"
-      (Types.to_string inner)
+      (tyname loc inner)
   | _ when is_nil_lit got -> mk loc oty Tast.None_
   | _ ->
     let s = fresh_slot ctx Types.Dyn in
@@ -4309,16 +4324,16 @@ let declare_env ctx = function
 
 let numeric_note ?(fln = false) ~(want : Types.t) ~(got : Types.t) () =
   let cast =
-    if fln then Printf.sprintf "%s(x)" (Types.to_string want)
-    else Printf.sprintf "(%s x)" (Types.to_string want)
+    if fln then Printf.sprintf "%s(x)" (Types.spell ~indented:fln want)
+    else Printf.sprintf "(%s x)" (Types.spell ~indented:fln want)
   in
   if not (Types.is_numeric want && Types.is_numeric got) then ""
   else if Types.widens_to ~from:want ~into:got then
     Printf.sprintf
       " — %s into %s can lose, so it has to be written: %s. The other way \
        round, %s widens into %s by itself"
-      (Types.to_string got) (Types.to_string want) cast
-      (Types.to_string want) (Types.to_string got)
+      (Types.spell ~indented:fln got) (Types.spell ~indented:fln want) cast
+      (Types.spell ~indented:fln want) (Types.spell ~indented:fln got)
   else
     Printf.sprintf
       " — neither widens into the other, so the conversion has to be written: \
@@ -4326,30 +4341,32 @@ let numeric_note ?(fln = false) ~(want : Types.t) ~(got : Types.t) () =
       cast
 
 (* The rest of the sentence when a read-only slice meets a writable one. *)
-let const_note env ~(want : Types.t) ~(got : Types.t) =
+let const_note ?(fln = false) env ~(want : Types.t) ~(got : Types.t) =
   match want, got with
   | Types.Slice (Types.Mut, e), Types.Slice (Types.Const, e')
     when Types.equal e e' ->
-    let copy = const_copy env e in
+    let copy =
+      Option.map (fun c -> if fln then "clone(v)" else c) (const_copy env e) in
     Printf.sprintf
       " — a %s can only be read, and never becomes a %s that can be written \
        through. %sWhere nothing writes through it, the %s can be declared %s \
        instead"
-      (Types.to_string got) (Types.to_string want)
+      (Types.spell ~indented:fln got) (Types.spell ~indented:fln want)
       (match copy with
        | Some c ->
          Printf.sprintf "%s copies v into a %s of its own. " c
-           (Types.to_string want)
+           (Types.spell ~indented:fln want)
        | None -> "")
-      (Types.to_string want) (Types.to_string got)
+      (Types.spell ~indented:fln want) (Types.spell ~indented:fln got)
   | Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e')
     when Types.equal e e' ->
     Printf.sprintf
       " — a %s can only be read through, and never becomes a %s that can be \
-       written through. Copy the %s out with (deref p) and point at the copy; \
+       written through. Copy the %s out with %s and point at the copy; \
        where nothing writes through it, the %s can be declared %s instead"
-      (Types.to_string got) (Types.to_string want) (Types.to_string e)
-      (Types.to_string want) (Types.to_string got)
+      (Types.spell ~indented:fln got) (Types.spell ~indented:fln want) (Types.spell ~indented:fln e)
+      (if fln then "deref(p)" else "(deref p)")
+      (Types.spell ~indented:fln want) (Types.spell ~indented:fln got)
   | _ -> ""
 
 let expect ctx loc ~want (got : Tast.expr) =
@@ -4375,7 +4392,7 @@ let expect ctx loc ~want (got : Tast.expr) =
         fail loc
           "nil has no None to become at %s — nil only converts to (Option T) \
            or to dyn itself; wrap the type in Option, or keep the value dyn"
-          (Types.to_string w)
+          (tyname loc w)
       | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
       | _, Types.Dyn -> unbox loc w got
       (* Implicit widening, and this single arm is the whole of its surface.
@@ -4424,9 +4441,9 @@ let expect ctx loc ~want (got : Tast.expr) =
          reader who has just been told i64 and i32 are different types needs
          to be told, in the same breath, which direction needed nothing. *)
       Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s"
-        (Types.to_string w) (Types.to_string got.Tast.ty)
+        (tyname loc w) (tyname loc got.Tast.ty)
         (numeric_note ~fln:(Source.indented_at loc) ~want:w ~got:got.Tast.ty ())
-        (const_note ctx.env ~want:w ~got:got.Tast.ty)
+        (const_note ~fln:(Source.indented_at loc) ctx.env ~want:w ~got:got.Tast.ty)
 
 (* Something a [break] may not jump out of, named so the refusal can say which.
    See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@@ -4693,7 +4710,7 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
     fail loc
       "%s is not a map key. A key is an integer, an enum, a bool, a string, a \
        fixed array of those, or a struct of those"
-      (Types.to_string other)
+      (tyname loc other)
 
 and struct_key_pair env loc n =
   let hname = "map/hash/" ^ n and ename = "map/eq/" ^ n in
@@ -4821,7 +4838,7 @@ and array_key_pair env loc n e =
   if Int64.compare n 0L <= 0 then
     fail loc
       "%s has no elements, so it is not a map key — every value of it would be \
-       the same key" (Types.to_string (Types.Array (n, e)));
+       the same key" (tyname loc (Types.Array (n, e)));
   let aty = Types.Array (n, e) in
   (* The type's printed form, with what a symbol cannot hold replaced. *)
   let tag =
@@ -4829,7 +4846,7 @@ and array_key_pair env loc n e =
       (fun c -> match c with
          | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' | '-' -> c
          | _ -> '_')
-      (Types.to_string aty)
+      (tyname loc aty)
   in
   (* The mangle is many-to-one — [a+b] and [a_b] come out alike — so a digest
      of the printed type, which is an identity, keeps two such keys apart. *)
@@ -4964,7 +4981,7 @@ let deferred_key env loc what (k : Types.t) =
       Loc.failk "check/generic-map-key" loc
         "%s over a map keyed by the type variable %s needs %s to be hashable. \
          Write {:where (hashable? $%s)} at the head of the body"
-        what (Types.to_string k) (Types.to_string k) v;
+        what (tyname loc k) (tyname loc k) v;
     true
   | _ -> false
 
@@ -5235,7 +5252,7 @@ let note_grown ctx op loc (target : Tast.expr) =
               (List.exists
                  (fun (d : Loc.diag) -> d.Loc.dloc = p.Ast.floc)
                  !grow_warnings) ->
-       let ts = Types.to_string t in
+       let ts = tyname loc t in
        let msg =
          match target.Tast.e with
          | Tast.Local _ ->
@@ -5247,7 +5264,7 @@ let note_grown ctx op loc (target : Tast.expr) =
               container c"
              p.Ast.fname ts op (Loc.to_string loc) ts op p.Ast.fname
          | _ ->
-           let pt = Types.to_string (List.nth ctx.slot_tys (ctx.slots - 1 - s)) in
+           let pt = tyname loc (List.nth ctx.slot_tys (ctx.slots - 1 - s)) in
            Printf.sprintf
              "%s is a %s passed by value, a copy of the caller's, so the %s \
               at %s grows %s in this function's copy and the caller's never \
@@ -5294,6 +5311,12 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
            only what no expectation could change is kept: a name that is not
            there. *)
         match e.Ast.e with
+        (* A type written in a value position — [map-new([const u8], i32)] —
+           is not a value to look names up in. *)
+        | Ast.Call ({ Ast.e = Ast.Var ("map-new" | "builtin/map-new"); _ }, args) ->
+          recheck_args ctx (List.filteri (fun i _ -> i >= 2) args)
+        | Ast.Call ({ Ast.e = Ast.Var ("vec-new" | "builtin/vec-new"); _ }, args) ->
+          recheck_args ctx (List.filteri (fun i _ -> i >= 1) args)
         | Ast.Call (_, args) -> recheck_args ctx args
         | _ -> ()
       end;
@@ -5346,20 +5369,25 @@ and check_target ctx (e : Ast.expr) =
 and refuse_owned_copy ctx (r : Tast.expr) =
   match const_reached r with
   | Some view when owning ctx.env r.Tast.ty ->
-    let t = Types.to_string r.Tast.ty in
+    let fln = Source.indented_at r.Tast.loc in
+    let t = tyname r.Tast.loc r.Tast.ty in
     let fix =
       match r.Tast.ty with
       | (Types.Vec _ | Types.Map _) when not (region_only ctx.env r.Tast.ty) ->
-        Printf.sprintf "(clone v) copies it into a %s of its own" t
+        Printf.sprintf "%s copies it into a %s of its own"
+          (if fln then "clone(v)" else "(clone v)") t
       (* Nothing copies an array, an Option or a struct that owns storage,
          nor a container whose elements do: its address is the way to it. *)
-      | _ -> Printf.sprintf "(addr v) gives a (Ptr const %s) to read it through" t
+      | _ ->
+        Printf.sprintf "%s gives a %s to read it through"
+          (if fln then "addr(v)" else "(addr v)")
+          (tyname r.Tast.loc (Types.Ptr (Types.Const, r.Tast.ty)))
     in
     Loc.failk "check/const-owned-copy" r.Tast.loc
       "this copies a %s out of a %s, which can only be read, and the copy \
        would share its storage with the original. Use it where it stands — \
        index it, slice it or read its fields — or %s"
-      t (Types.to_string view) fix
+      t (tyname r.Tast.loc view) fix
   | _ -> ()
 
 and check_value ctx ?want (e : Ast.expr) : Tast.expr =
@@ -5390,14 +5418,14 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
     let gname, _, _ = List.nth ctx.env.chain (List.length ctx.env.chain - 1) in
     let var =
       match List.find_opt (fun (_, u) -> Types.equal u t) ctx.env.subst with
-      | Some (v, _) -> Printf.sprintf "$%s = %s" v (Types.to_string t)
-      | None -> Types.to_string t
+      | Some (v, _) -> Printf.sprintf "$%s = %s" v (tyname loc t)
+      | None -> tyname loc t
     in
     Loc.failk literal_at_want loc
       "%Ld does not fit in %s, which holds no negative number, and %s is called \
        at %s — the body has to work at every type it is called at, so write \
        it with no negative literal, as in (- x %Ld) in place of (+ x %Ld)"
-      n (Types.to_string t) gname var (Int64.neg n) n
+      n (tyname loc t) gname var (Int64.neg n) n
   | Ast.Int n -> int_literal loc ~want ~preds:ctx.env.tvpreds n
   | Ast.UInt (n, s) -> wide_literal loc ~want n s
   | Ast.Byte b ->
@@ -5444,7 +5472,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
              else Printf.sprintf "$%s" v)
       | Some other when other <> Types.Never ->
         Loc.failk literal_at_want loc "expected %s, found the float literal %g"
-          (Types.to_string other) x
+          (tyname loc other) x
       | _ -> Types.F64
     in
     mk loc (Types.Float k) (Tast.Float (x, k))
@@ -5486,7 +5514,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
        fail loc
          ":%s is an enum member where an enum is expected and a dyn keyword \
           elsewhere, but %s is expected here" k
-         (Types.to_string other))
+         (tyname loc other))
   (* {:a 1 :b s} — a dyn map, built where it stands. Always dyn: the
      runtime owns the storage the way (vec-new dyn) does, keys and values are
      both dyn words, and a typed want other than dyn refuses through [expect]
@@ -5603,7 +5631,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
       | None ->
         if not (Types.equal ctx.ret Types.Unit) then
           fail loc "this function returns %s, so return needs a value"
-            (Types.to_string ctx.ret);
+            (tyname loc ctx.ret);
         None
       | Some v -> Some (check ctx ~want:ctx.ret v)
     in
@@ -5679,7 +5707,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
       fail loc
         "(get m k) is a place only on a class instance, and this is %s. A \
          map's entries are written with put"
-        (Types.to_string target.Tast.ty);
+        (tyname loc target.Tast.ty);
     let k = check ctx ~want:Types.Dyn k in
     let v = check ctx ~want:Types.Dyn v in
     expect ctx loc ~want
@@ -5694,7 +5722,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
     (match Tast.field_index s name with
      | None ->
        Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname)
-         "%s has no field %s" (Types.to_string (Types.Named sname)) name
+         "%s has no field %s" (tyname loc (Types.Named sname)) name
      | Some i ->
        let fty = (List.nth s.Tast.fields i).Tast.fty in
        expect ctx loc ~want (mk loc fty (Tast.Field (target, i))))
@@ -5741,11 +5769,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
         | Types.Option t ->
           expect ctx loc ~want (mk loc t (Tast.UnwrapSome v))
         | other ->
-          fail loc "some takes an (Option T), found %s" (Types.to_string other))
+          fail loc "some takes an (Option T), found %s" (tyname loc other))
      | other ->
        fail loc
          "some early-returns None, so the enclosing function must return an \
-          Option; this one returns %s" (Types.to_string other))
+          Option; this one returns %s" (tyname loc other))
   | Ast.Unwrap (Ast.Utry, _) -> unimplemented loc "try (Result)" 6
   | Ast.Fn (params, body) -> check_fn ctx ~want loc params body
   | Ast.Dotimes (label, name, bounds, body) ->
@@ -5771,7 +5799,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
            condition's struct type, whose dyn fields are fine"
       | t ->
         fail c.Tast.loc
-          "a condition is a struct, not %s" (Types.to_string t)
+          "a condition is a struct, not %s" (tyname loc t)
     in
     (* A condition that *holds* a dyn is not refused. The condition crosses as
        a pointer to a value in the signalling frame, and that value is on the
@@ -5815,7 +5843,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
          | Types.Unit | Types.Never ->
            fail a.Tast.loc
              "a restart argument must be a value, and this one is %s"
-             (Types.to_string a.Tast.ty)
+             (tyname loc a.Tast.ty)
          | _ -> ())
       args;
     let sg = restart_sig (List.map (fun (a : Tast.expr) -> a.Tast.ty) args) in
@@ -5905,7 +5933,7 @@ and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n =
       n v v v
   | Some other when other <> Types.Never ->
     Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
-      (Types.to_string other) n
+      (tyname loc other) n
   | _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default))
 
 (* An integer written at or above 2^63, in decimal or in hex. Only a u64 holds
@@ -5920,7 +5948,7 @@ and wide_literal loc ~want n s =
     Loc.failk literal_at_want loc
       "%s is too large for any integer type but u64, and an integer literal \
        where %s is wanted is read as one — write (%s (u64 %s))"
-      s (Types.to_string t) (Types.to_string t) s
+      s (tyname loc t) (tyname loc t) s
   | Some Types.Never | None ->
     Loc.failk literal_at_want loc
       "%s does not fit in i32, the type an integer literal takes when nothing \
@@ -5935,7 +5963,7 @@ and wide_literal loc ~want n s =
   | Some other ->
     Loc.failk literal_at_want loc
       "expected %s, found the integer literal %s, which only a u64 holds"
-      (Types.to_string other) s
+      (tyname loc other) s
 
 (* Arithmetic wraps, but a literal that does not fit its type is a typo, not a
    wrap — 300 is never what someone meant by a u8. *)
@@ -5998,6 +6026,11 @@ and var ctx ?(qualified = false) loc ~want name =
      item 4. *)
   | "nil" ->
     expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_nil" [])
+  (* [Dir.north]: an enum's member named through its type, as a data case is
+     [Shape.Rect]; the same value as [:north] where a Dir is expected. *)
+  | _ when lookup ctx name = None && enum_member ctx.env name <> None ->
+    let e, v = Option.get (enum_member ctx.env name) in
+    expect ctx loc ~want (mk loc (Types.Enum e) (Tast.Int (v, Types.I32)))
   | "None" ->
     (match want with
      | Some (Types.Option t) -> mk loc (Types.Option t) Tast.None_
@@ -6006,7 +6039,7 @@ and var ctx ?(qualified = false) loc ~want name =
         absence and this is it, not an (Option T) that then gets boxed. *)
      | Some Types.Dyn -> rt loc Types.Dyn "flan_dyn_nil" []
      | Some other when other <> Types.Never ->
-       fail loc "expected %s, found None" (Types.to_string other)
+       fail loc "expected %s, found None" (tyname loc other)
      | _ ->
        fail loc
          "nothing here says what None is an Option of — use it where an \
@@ -6193,12 +6226,12 @@ and check_fn ctx ~want ?gen loc (params : string list) body =
           "this fn has %d parameter%s and %s was wanted here"
           (List.length params)
           (if List.length params = 1 then "" else "s")
-          (Types.to_string
+          (tyname loc
              (if bare then Types.CFn (ps, r) else Types.Fn (ps, r)))
       | _ ->
         match want with
         | Some other when other <> Types.Never ->
-          fail loc "expected %s, found an fn" (Types.to_string other)
+          fail loc "expected %s, found an fn" (tyname loc other)
         | _ ->
           if fln_source loc then
             fail loc
@@ -6246,7 +6279,7 @@ and check_fn ctx ~want ?gen loc (params : string list) body =
          fail loc
            "an fn with no body answers (), and this one is in a position \
             that wants %s — write the value it should answer"
-           (Types.to_string r)
+           (tyname loc r)
        | _ -> fbody, Types.Unit)
     | last :: rest ->
       (match ret0 with
@@ -6290,8 +6323,8 @@ and check_fn ctx ~want ?gen loc (params : string list) body =
        %s): a CFn is the bare address, one word, with nowhere for the \
        copies to live. Widen the position to Fn, or pass %s in as a parameter"
       (String.concat ", " names)
-      (String.concat " " (List.map Types.to_string pts)) (Types.to_string ret)
-      (String.concat " " (List.map Types.to_string pts)) (Types.to_string ret)
+      (String.concat " " (List.map (tyname loc) pts)) (tyname loc ret)
+      (String.concat " " (List.map (tyname loc) pts)) (tyname loc ret)
       (match names with [ n ] -> n | _ -> "them")
   end;
   (* An [Fn]-position literal declares the environment whether or not it
@@ -6365,7 +6398,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
            | Types.Named n -> n
            | t ->
              fail c.Ast.hloc
-               "a handler matches a struct type, not %s" (Types.to_string t)
+               "a handler matches a struct type, not %s" (tyname loc t)
          in
          (* Its own context: a fresh frame, an empty scope, and no way to reach
             the enclosing one. *)
@@ -6544,7 +6577,7 @@ and restart_clauses ctx ?want ?(hidden = false) ~what loc (tbody : Tast.expr)
                      | Types.Unit | Types.Never ->
                        fail p.Ast.floc
                          "%s would be a restart parameter of type %s, which is \
-                          not a value" p.Ast.fname (Types.to_string ty)
+                          not a value" p.Ast.fname (tyname loc ty)
                      | _ -> ());
                     (bind ctx p.Ast.fname ty ~assignable:false, ty))
                  c.Ast.rparams
@@ -6629,7 +6662,7 @@ and check_handler_case ctx ?want loc body clauses =
          | Types.Named n -> n
          | t ->
            fail c.Ast.hloc
-             "a handler matches a struct type, not %s" (Types.to_string t))
+             "a handler matches a struct type, not %s" (tyname loc t))
       clauses
   in
   (* Two clauses for one condition type: the first would take every one of
@@ -6769,7 +6802,7 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
             | Types.Never when is_poison v -> ()
             | Types.Unit | Types.Never ->
               fail b.Ast.bloc "%s would be bound to %s, which is not a value"
-                b.Ast.bname (Types.to_string v.Tast.ty)
+                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
@@ -7002,7 +7035,7 @@ and check_loop ctx ?want loc bs body =
             | Types.Never when is_poison v -> ()
             | Types.Unit | Types.Never ->
               fail v.Tast.loc "%s would be bound to %s, which is not a value" n
-                (Types.to_string v.Tast.ty)
+                (tyname loc v.Tast.ty)
             | _ -> ());
            (bind ctx n v.Tast.ty ~assignable:true, v))
         bs
@@ -7245,7 +7278,7 @@ and check_truthy_once ctx c =
     (try
        Loc.failk "check/condition-not-bool" loc
          "a condition is a bool or a dyn, and this is %s%s"
-         (Types.to_string c0.Tast.ty) how
+         (tyname loc c0.Tast.ty) how
      with Loc.Error d -> refuse_or_poison ctx.env loc d))
   | exception Loc.Error _ -> check ctx ~want:Types.Bool c
 
@@ -7383,7 +7416,7 @@ and check_if_once ctx ~tail ?want loc c t e =
            Loc.failk "check/shortcircuit-operand" t.Tast.loc
              "an and answers false or its last operand, so the two have to be \
               one type — this operand is %s, and false is a bool"
-             (Types.to_string t.Tast.ty)
+             (tyname loc t.Tast.ty)
          with Loc.Error d -> refuse_or_poison ctx.env e.Ast.loc d)
       | exception Loc.Error d when reworded -> refuse_or_poison ctx.env e.Ast.loc d
     in
@@ -7400,7 +7433,7 @@ and check_if_once ctx ~tail ?want loc c t e =
       else if Types.equal t.Tast.ty e.Tast.ty then t.Tast.ty
       else
         fail loc "the branches of this if have different types: %s and %s"
-          (Types.to_string t.Tast.ty) (Types.to_string e.Tast.ty)
+          (tyname loc t.Tast.ty) (tyname loc e.Tast.ty)
     in
     mk loc ty (Tast.If (c, t, e))
 
@@ -7507,13 +7540,13 @@ and generic_ctor ctx ~want loc name given =
                 | Some (fname, at) ->
                   [ Loc.note at
                       (Printf.sprintf ".%s is %s here, which decides $%s" fname
-                         (Types.to_string b) v) ]
+                         (tyname loc b) v) ]
                 | None -> []
               in
               Loc.failk "check/generic-struct-field" a.Ast.loc ~notes
                 "%s's .%s is $%s, which is %s here, and %g is a float literal. \
                  Write .%s as an integer, or give .%s a float type"
-                name f.Tast.fname v (Types.to_string b) x f.Tast.fname
+                name f.Tast.fname v (tyname loc b) x f.Tast.fname
                 (match List.assoc_opt v !decided_by with
                  | Some (fname, _) -> fname
                  | None -> f.Tast.fname)
@@ -7527,8 +7560,8 @@ and generic_ctor ctx ~want loc name given =
                | 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"
-                   (Types.to_string (Types.Named open_key)) f.Tast.fname
-                   (Types.to_string b) (Types.to_string t)))
+                   (tyname loc (Types.Named open_key)) f.Tast.fname
+                   (tyname loc b) (tyname loc t)))
          | _ ->
          if open_ty f.Tast.fty
             && not (literal a && subst_ty !subst f.Tast.fty |> open_ty |> not)
@@ -7555,9 +7588,9 @@ and generic_ctor ctx ~want loc name given =
                  !subst
              else
                fail a.Ast.loc "%s's .%s is %s here, and this is %s"
-                 (Types.to_string (Types.Named open_key)) f.Tast.fname
-                 (Types.to_string (subst_ty !subst f.Tast.fty))
-                 (Types.to_string t)
+                 (tyname loc (Types.Named open_key)) f.Tast.fname
+                 (tyname loc (subst_ty !subst f.Tast.fty))
+                 (tyname loc t)
          end)
       pairs;
     (match given with
@@ -7624,7 +7657,7 @@ and positional_struct ctx ~want loc name args =
     | Some (g, _) when Hashtbl.mem ctx.env.copies name -> g
     | _ -> name
   in
-  let shown = Types.to_string (Types.Named name) in
+  let shown = tyname loc (Types.Named name) in
   if given < n then begin
     let missing = List.nth fields given in
     Loc.failk "check/positional-too-few" loc ~notes:note
@@ -7709,7 +7742,7 @@ and check_bare ctx ~want loc kvs =
     Loc.failk "check/bare-struct-want" loc
       "%s is a struct field list and %s is expected here, which is not a \
        struct type"
-      written (Types.to_string other)
+      written (tyname loc other)
   | None ->
     Loc.failk "check/bare-struct-untyped" loc
       "%s does not say which struct it builds — the fields alone do not name \
@@ -7804,7 +7837,7 @@ and check_struct ctx ~want loc name kvs =
           if Tast.field_index s k = None then
             Loc.failk "check/unknown-field" v.Ast.loc
               ~notes:(declared_note ctx.env name)
-              "%s has no field %s" (Types.to_string (Types.Named name)) k)
+              "%s has no field %s" (tyname loc (Types.Named name)) k)
     in
     let fields = zii_fill ctx loc seen s.Tast.fields in
     expect ctx loc ~want (mk loc (Types.Named name) (Tast.Make (name, fields)))
@@ -7946,7 +7979,7 @@ and check_arr ctx ~want loc items =
     (fun (i : Tast.expr) ->
        if not (Types.fits ~expected:elem ~actual:i.Tast.ty) then
          fail i.Tast.loc "this array's elements are %s, but this one is %s"
-           (Types.to_string elem) (Types.to_string i.Tast.ty))
+           (tyname loc elem) (tyname loc i.Tast.ty))
     items;
   (match want with
    | Some (Types.Array (m, _)) when not (Int64.equal m n) ->
@@ -8095,15 +8128,15 @@ and numbers_disagree : 'a. ctx -> (Ast.expr * Types.t) list -> 'a =
       | _ -> t1, second, t2, first
     in
     ignore ctx;
-    let tn = Types.to_string target in
+    let tn = tyname moved.Ast.loc target in
     Loc.failk "check/array-numbers-disagree" moved.Ast.loc
       ~notes:[ Loc.note other.Ast.loc (Printf.sprintf "this element is %s" tn) ]
       "this array's elements are %s and %s, and neither holds every value of \
        the other — %s"
-      (Types.to_string moved_ty) tn
+      (tyname moved.Ast.loc moved_ty) tn
       (match spell_arg "" moved with
        | "" ->
-         Printf.sprintf "convert the %s element with the %s cast" (Types.to_string moved_ty) tn
+         Printf.sprintf "convert the %s element with the %s cast" (tyname moved.Ast.loc moved_ty) tn
        | x -> Printf.sprintf "convert one, as in (%s %s)" tn x)
 
 (* Elements that do not agree and cannot all become a dyn either: a struct
@@ -8284,6 +8317,15 @@ and array_build ctx loc ns elem ~pre ~element =
    [n T] the literal is, since an array literal is never a slice. *)
 and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
   let ty = resolve ctx.env t in
+  (* A typed .fln lambda, [fn(c: C) -> bool = ...], reads as [(the (Fn [C]
+     bool) (fn ...))]; where a CFn of the same signature is wanted, the
+     literal is that CFn, as an untyped one would be. *)
+  let ty =
+    match ty, v.Ast.e, want with
+    | Types.Fn (ps, r), Ast.Fn _, Some (Types.CFn (ps', r') as c)
+      when Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) -> c
+    | _ -> ty
+  in
   let is_nil = match v.Ast.e with Ast.Var "nil" -> true | _ -> false in
   if ty <> Types.Dyn && not is_nil
      && probe ctx loc (fun () -> (check ctx v).Tast.ty) = Some Types.Dyn
@@ -8291,7 +8333,7 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
         enum's type, not a dyn: [let d: Dir = :north]. *)
      && not (match ty, v.Ast.e with Types.Enum _, Ast.Kw _ -> true | _ -> false)
   then begin
-    let tn = Types.to_string ty in
+    let tn = tyname loc ty in
     let numeric = match ty with Types.Int _ | Types.Float _ -> true | _ -> false in
     (* In a .fln file the user wrote [x: T = v], not [the]. *)
     let fln = fln_source loc in
@@ -8417,7 +8459,7 @@ and check_array_gen ctx ~want loc dims f =
            if not (Types.equal p index_ty) then
              fail f.Tast.loc
                "an index is an i32, and this generator's argument %d is %s"
-               (k + 1) (Types.to_string p))
+               (k + 1) (tyname loc p))
         ps;
       r
     | None ->
@@ -8425,7 +8467,7 @@ and check_array_gen ctx ~want loc dims f =
         "array-gen's second element is a function value, called once per \
          element with one i32 index per dimension, and this is %s — for one \
          value repeated, write array-fill"
-        (Types.to_string f.Tast.ty)
+        (tyname loc f.Tast.ty)
   in
   no_zeroed_fn loc "a fixed array's element" elem;
   let fs = fresh_slot ctx f.Tast.ty in
@@ -8475,7 +8517,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
       fail loc
         "match works on an Option, a data type, an enum, a bool, a number, a \
          string or a dyn, not on %s"
-        (Types.to_string other)
+        (tyname loc other)
   in
   (* A literal arm, spelled as it was written, for the refusals that name one. *)
   let spell (e : Ast.expr) =
@@ -8498,7 +8540,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
     | Ast.Var b -> b
     | _ -> "this literal"
   in
-  let what_ty t = match t with Types.Dyn -> "a dyn" | t -> Types.to_string t in
+  let what_ty t = match t with Types.Dyn -> "a dyn" | t -> tyname loc t in
   (* A literal match that compiles, over the scrutinee's own name where it
      has one, for the refusals that need to show the shape. *)
   let lit_arms_fix t =
@@ -8538,7 +8580,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
               an f64, and %s fits in neither. Change the arm to a value an \
               i64 holds, or remove it" (spell e)
          | _ -> ());
-        let tn = Types.to_string t in
+        let tn = tyname loc t in
         let an =
           match tn.[0] with
           | 'a' | 'e' | 'f' | 'i' | 'o' -> "an " ^ tn
@@ -8599,7 +8641,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
          (match t with
           | Types.Dyn -> "a dyn"
           | t ->
-            let tn = Types.to_string t in
+            let tn = tyname loc t in
             (match tn.[0] with
              | 'a' | 'e' | 'f' | 'i' | 'o' -> "an " ^ tn
              | _ -> "a " ^ tn))
@@ -8635,6 +8677,15 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
         | None -> fail a.Ast.aloc "%s has no member :%s — it has %s" n k all
       end;
       Some k, []
+    (* [Dir.north ->], the member named through its enum. *)
+    | `Enum (n, members), Ast.Pctor (c, [])
+      when String.length c > String.length n + 1
+           && String.sub c 0 (String.length n + 1) = n ^ "." ->
+      let k = String.sub c (String.length n + 1) (String.length c - String.length n - 1) in
+      if not (List.mem_assoc k members) then
+        fail a.Ast.aloc "%s has no member %s — it has %s" n k
+          (String.concat " " (List.map (fun (m, _) -> n ^ "." ^ m) members));
+      Some k, []
     | `Enum (n, members), Ast.Pctor (c, _) ->
       fail a.Ast.aloc
         "this match is over the enum %s, and %s is not one of its members. An \
@@ -8861,7 +8912,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
      Loc.failk "check/non-exhaustive-match" loc
        "this match is not exhaustive — its arms are literals, and no list of \
         them covers every %s. Add a _ arm for the rest, as in %s"
-       (match t with Types.Dyn -> "dyn value" | t -> Types.to_string t)
+       (match t with Types.Dyn -> "dyn value" | t -> tyname loc t)
        (lit_arms_fix t)
    | _ -> ());
   if not !saw_wild && missing <> [] then
@@ -9028,7 +9079,7 @@ and unknown_name : 'a. ?setting:bool -> ctx -> Loc.t -> string -> 'a =
         "unknown name %s — a dot is part of the name here, not field access. \
          A field is reached through an accessor, (.%s %s), and %s is %s, \
          which has no fields"
-        name field head head (Types.to_string t)
+        name field head head (tyname loc t)
     | None, None ->
       Loc.failk "check/unknown-name" loc
         "unknown name %s — nothing named %s is in scope either. A field is \
@@ -9087,7 +9138,7 @@ and check_arg ctx name i (want : Types.t) (a : Ast.expr) =
         let p = List.nth ps i in
         [ Loc.note p.Ast.floc
             (Printf.sprintf "%s's %s parameter %s is declared %s"
-               name which p.Ast.fname (Types.to_string want)) ]
+               name which p.Ast.fname (tyname p.Ast.floc want)) ]
       | _ -> []
     in
     refuse_or_poison ctx.env a.Ast.loc
@@ -9184,7 +9235,7 @@ and refuse_const_change _ctx loc (target : Tast.expr) =
   match const_reached target with
   | None -> ()
   | Some view ->
-    let t = Types.to_string target.Tast.ty in
+    let t = tyname loc target.Tast.ty in
     let holder =
       match view with Types.Slice (_, e) | Types.Ptr (_, e) -> e | t -> t
     in
@@ -9192,8 +9243,8 @@ and refuse_const_change _ctx loc (target : Tast.expr) =
       "this changes a %s reached through a %s, which can only be read. Where \
        it has to change, take the %s it lives in as a [%s] or a (Ptr %s) \
        instead"
-      t (Types.to_string view) (Types.to_string holder)
-      (Types.to_string holder) (Types.to_string holder)
+      t (tyname loc view) (tyname loc holder)
+      (tyname loc holder) (tyname loc holder)
 
 and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
   match p with
@@ -9244,7 +9295,7 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
     (match Tast.field_index s name with
      | None ->
        Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname)
-         "%s has no field %s" (Types.to_string (Types.Named sname)) name
+         "%s has no field %s" (tyname loc (Types.Named sname)) name
      | Some i ->
        if store then Option.iter (refuse_const_place ctx.env loc) (const_reached target);
        Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty)
@@ -9268,7 +9319,7 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
        refuse_const_place ctx.env loc view
      | Types.Ptr (_, t) -> Tast.Pderef target, t
      | other ->
-       fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))
+       fail loc "deref takes a (Ptr T), found %s" (tyname loc other))
   (* Only [set] writes a class slot, and it has its own arm above. A slot
      lives in a map the collector may move entries of, so it has no address
      to hand out. *)
@@ -9319,7 +9370,7 @@ and index_expr ctx (e : Ast.expr) =
       "an index is an i32, and %s is wider — write (i32 …)"
       (Types.ikind_name k)
   | other ->
-    fail e.Ast.loc "an index is an integer, found %s" (Types.to_string other)
+    fail e.Ast.loc "an index is an integer, found %s" (tyname e.Ast.loc other)
 
 (* [(at a i)] and [(at grid row col)]: one index per dimension.
 
@@ -9345,7 +9396,7 @@ and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list
           if store then Option.iter (fun l -> refuse_string_place l ty) place;
           Types.Int Types.U8
         | other ->
-          fail i.Ast.loc "%s cannot be indexed" (Types.to_string other)
+          fail i.Ast.loc "%s cannot be indexed" (tyname i.Ast.loc other)
       in
       let loc = i.Ast.loc in
       let i = index_expr ctx i in
@@ -9399,7 +9450,7 @@ and check_call ctx ~want loc (head : Ast.expr) (args : Ast.expr list) =
   | Ast.Call ({ Ast.e = Ast.Var "Ptr"; _ }, _)
     when (match type_of_expr head with Some _ -> true | None -> false) ->
     let target = resolve ctx.env (Option.get (type_of_expr head)) in
-    let spelled = Types.to_string target in
+    let spelled = tyname loc target in
     (match args with
      | [ a ] ->
        let a_loc = a.Ast.loc in
@@ -9410,8 +9461,8 @@ and check_call ctx ~want loc (head : Ast.expr) (args : Ast.expr list) =
           fail loc
             "%s is a %s, which cannot be written through, and %s would allow \
              writes. Write (%s %s)"
-            spelled_a (Types.to_string a.Tast.ty) spelled
-            (Types.to_string (Types.Ptr (Types.Const, u))) spelled_a
+            spelled_a (tyname loc a.Tast.ty) spelled
+            (tyname loc (Types.Ptr (Types.Const, u))) spelled_a
         | Types.Ptr _, _ ->
           expect ctx loc ~want
             (mk loc target (Tast.Prim (Tast.Cast target, [ a ])))
@@ -9419,12 +9470,12 @@ and check_call ctx ~want loc (head : Ast.expr) (args : Ast.expr list) =
           fail a_loc
             "%s converts a pointer, found %s. The address of the first \
              element is (addr (at %s 0)); write (%s (addr (at %s 0)))"
-            spelled (Types.to_string a.Tast.ty) spelled_a spelled spelled_a
+            spelled (tyname loc a.Tast.ty) spelled_a spelled spelled_a
         | Types.Int _, _ ->
           fail a_loc
             "%s converts a pointer, found %s. There is no conversion between \
              an integer and a pointer"
-            spelled (Types.to_string a.Tast.ty)
+            spelled (tyname loc a.Tast.ty)
         | Types.Dyn, _ ->
           fail a_loc
             "%s converts a pointer, found dyn. A dyn value never holds a \
@@ -9434,7 +9485,7 @@ and check_call ctx ~want loc (head : Ast.expr) (args : Ast.expr list) =
           fail a_loc
             "%s converts a pointer, found %s. The address of a place is \
              (addr %s); write (%s (addr %s))"
-            spelled (Types.to_string other) spelled_a spelled spelled_a)
+            spelled (tyname loc other) spelled_a spelled spelled_a)
      | _ ->
        fail loc "%s takes one pointer, given %d" spelled (List.length args))
   (* A computed head: ((choose k) 3). The head is an ordinary expression and
@@ -9459,7 +9510,7 @@ and call_value ctx ~want loc (callee : Tast.expr) args =
     expect ctx loc ~want (mk loc ret (Tast.CallPtr (callee, args)))
   | None ->
     fail loc "this is a %s and not a function, so it cannot be called"
-      (Types.to_string callee.Tast.ty)
+      (tyname loc callee.Tast.ty)
 
 (* A builtin's arity. The count is the builtin's and can only be the
    builtin's: a defn of the same name written in the program now takes the
@@ -9540,9 +9591,9 @@ and not_numeric name what (a : Tast.expr) =
     fail where
       "%s takes %s, and this is %s — there is no %s on text. The prelude \
        concatenates with concat and join"
-      name what (Types.to_string a.Tast.ty) name
+      name what (tyname where a.Tast.ty) name
   else
-    fail where "%s takes %s, found %s" name what (Types.to_string a.Tast.ty)
+    fail where "%s takes %s, found %s" name what (tyname where a.Tast.ty)
 
 (* ── A conversion whose operand is a type variable ─────────────────────
    [(i32 x)] where [x] is a [$t]. The concrete question — is this a number —
@@ -10018,7 +10069,7 @@ and type_of_expr ?(generic = fun _ -> false) (e : Ast.expr) : Ast.texpr option =
 and map_kv loc what (t : Types.t) =
   match t with
   | Types.Map (k, v) -> k, v
-  | other -> fail loc "%s takes a (Map K V), found %s" what (Types.to_string other)
+  | other -> fail loc "%s takes a (Map K V), found %s" what (tyname loc other)
 
 (* The key and value for [map-new]: two leading bare symbols naming types, or
    the expectation at the site. The same rule [vec-new] uses, with the same
@@ -10060,7 +10111,7 @@ and map_new_types ctx ~want loc args =
 and vec_elem loc what (t : Types.t) =
   match t with
   | Types.Vec e -> e
-  | other -> fail loc "%s takes a (Vec T), found %s" what (Types.to_string other)
+  | other -> fail loc "%s takes a (Vec T), found %s" what (tyname loc other)
 
 (* The allocator an operation uses: the one named at the site, or the current
    implicit one. spec-memory.md: an operation never falls back to a hidden
@@ -10392,11 +10443,11 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        | "=" | "!=" ->
          fail loc
            "%s compares numbers, enums, strings and bools, and %s is none \
-            of those" name (Types.to_string a.Tast.ty)
+            of those" name (tyname loc a.Tast.ty)
        | _ ->
          fail loc
            "%s orders machine numbers and enums, and %s is neither" name
-             (Types.to_string a.Tast.ty));
+             (tyname loc a.Tast.ty));
     match rest with
     | [] -> prim p Types.Bool [ a; b ]
     | _ ->
@@ -10449,7 +10500,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | t when generic_ty t ->
        unconstrained ctx.env loc name ~needs:"integer?" t
      | other -> fail loc "%s takes integers, found %s" name
-                  (Types.to_string other));
+                  (tyname loc other));
     (* A shift by the operand's own width or more is poison in LLVM, which at
        -O2 turns the whole function into an undefined value rather than into a
        wrong number. A literal count is rejected here — that is the typo — and
@@ -10461,7 +10512,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        if Int64.unsigned_compare n w >= 0 then
          fail loc
            "%s by %Ld is out of range for %s, which is %d bits wide" name n
-           (Types.to_string a.Tast.ty) (Types.bits k)
+           (tyname loc a.Tast.ty) (Types.bits k)
      | _ -> ());
     prim p a.Tast.ty [ a; b ]
   (* (min a b) and (max a b) evaluate each operand once — hence the slots —
@@ -10564,7 +10615,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
       | _ ->
         fail a.Ast.loc
           "%s takes a numeric? type, and %s is not one — as in (%s i32)" name
-          (Types.to_string ty) name
+          (tyname loc ty) name
     in
     expect ctx loc ~want v
   (* (zeroed) is the all-bytes-zero value of whatever it is being stored into,
@@ -10614,8 +10665,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
             "%s writes raw bytes over %s, and %s is not plain data — %s. \
              Fill only numbers and pointers, and structs, unions and fixed \
              arrays built out of them"
-            name (Types.to_string ty)
-            (if Types.equal bad ty then "it" else Types.to_string bad)
+            name (tyname loc ty)
+            (if Types.equal bad ty then "it" else tyname loc bad)
             (match bad with
              | Types.Dyn ->
                "a dyn is one word the collector walks by descriptor, and a \
@@ -10702,11 +10753,11 @@ and named_call ?(qualified = false) ctx ~want loc name args =
               "this pattern binds %Ld name%s, but %s has %Ld element%s — a \
                pattern over a fixed array names every element, or ends in \
                [& rest]"
-              n (plural n) (Types.to_string target.Tast.ty) m (plural m);
+              n (plural n) (tyname loc target.Tast.ty) m (plural m);
           if Int64.equal exact 0L && Int64.compare m n < 0 then
             fail loc
               "this pattern binds %Ld name%s before the &, but %s has only %Ld \
-               element%s" n (plural n) (Types.to_string target.Tast.ty) m
+               element%s" n (plural n) (tyname loc target.Tast.ty) m
               (plural m);
           prim Tast.At elem
             [ target; mk loc index_ty (Tast.Int (i, Types.I32)) ]
@@ -10722,13 +10773,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
             "a pattern cannot destructure %s — a slice's length is not known \
              until the program runs, so nothing here can check it has %Ld \
              element%s. Use %s and test %s yourself"
-            (Types.to_string target.Tast.ty) n (plural n)
+            (tyname loc target.Tast.ty) n (plural n)
             (if fln_source loc then "s[i]" else "(at s i)")
             (if fln_source loc then "length(s)" else "(length s)")
         | other ->
           fail loc
             "%s is not a fixed array, so [a b ...] cannot destructure it"
-            (Types.to_string other))
+            (tyname loc other))
      | _ ->
        fail loc
          "destructure~nth is written by the compiler and cannot be called")
@@ -11042,7 +11093,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        fail loc
          "a %s knows the allocator it came from, so free takes only the \
           container. Write (free %s)"
-         (Types.to_string target.Tast.ty) (spell_arg "v" (List.hd args))
+         (tyname loc target.Tast.ty) (spell_arg "v" (List.hd args))
      | _ -> ());
     (* A container of owning elements is refused here, and a reader will
        assume the opposite — that [free] recurses — so this says why it does
@@ -11074,7 +11125,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          "%s holds elements that own storage, and free releases only the \
           block those elements sit in. Write (free-all a) on the region it \
           was built against"
-         (Types.to_string target.Tast.ty)
+         (tyname loc target.Tast.ty)
      | Types.Vec elem ->
        expect ctx loc ~want
          (rt loc Types.Unit "flan_vec_free"
@@ -11093,10 +11144,10 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        fail loc
          "%s can only be read, so it cannot be freed. Free the [%s] it was \
           copied into"
-         (Types.to_string target.Tast.ty)
+         (tyname loc target.Tast.ty)
          (match target.Tast.ty with
-          | Types.Slice (_, e) -> Types.to_string e
-          | t -> Types.to_string t)
+          | Types.Slice (_, e) -> tyname loc e
+          | t -> tyname loc t)
      (* A view written right here — (slice ...) or (slice-from ...) —
         is storage something else owns, known without running anything. *)
      | Types.Slice (Types.Mut, _)
@@ -11118,7 +11169,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        fail loc
          "free takes a Vec, a Map, or a slice (bytes s) or (clone xs) made — \
           found %s"
-         (Types.to_string other))
+         (tyname loc other))
   (* Emitted by the prelude's [into] when no (map f) is in the chain, so that
      every element pushed is a source element as it stands. A push copies an
      element's header, and for an element that owns storage the copy and the
@@ -11141,7 +11192,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        (match elem with
         | Some e when owning ctx.env e ->
           let v = spell_arg "v" src in
-          let et = Types.to_string e in
+          let et = tyname loc e in
           let fix =
             if clone_accepts ctx.env e then
               match spell_form dst, List.map spell_form transforms with
@@ -11206,7 +11257,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           fail loc
             "%s cannot be cloned — its elements own storage, and nothing here \
              can walk one to copy what it owns. %s"
-            (Types.to_string target.Tast.ty)
+            (tyname loc target.Tast.ty)
             (insert_copies ctx.env target.Tast.ty)
         (* A slice's elements, copied into a block from the allocator and
            answered as a slice over it — what (bytes s) does for a string's
@@ -11216,7 +11267,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           fail loc
             "%s cannot be cloned — its elements own storage, and nothing here \
              can walk one to copy what it owns. %s"
-            (Types.to_string target.Tast.ty)
+            (tyname loc target.Tast.ty)
             (insert_copies ctx.env target.Tast.ty)
         (* The copy is a block from an allocator, which the collector does not
            walk, so a dyn in it would be a root nothing marks. *)
@@ -11225,7 +11276,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
             "%s cannot be cloned — its elements hold a dyn, and the copy would \
              live in allocator storage the collector does not look in. Build \
              a dyn vector from the elements instead"
-            (Types.to_string target.Tast.ty)
+            (tyname loc target.Tast.ty)
         | Types.Slice (_, elem) ->
           expect ctx loc ~want (dup_elems ctx loc elem target a)
         (* A map's clone reinserts rather than copying the block, because the
@@ -11403,7 +11454,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_kw" [ s ])
         | other ->
           fail loc "keyword takes a string or a [u8], found %s"
-            (Types.to_string other))
+            (tyname loc other))
      | _ -> assert false)
 
   (* (class-of v) -> the class's name as a keyword, or nil. It is the dyn
@@ -11870,7 +11921,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | other ->
        fail loc
          "length takes an array, a slice, a string, a Vec or a Map, found %s"
-         (Types.to_string other))
+         (tyname loc other))
   | "at" ->
     (match args with
      | target :: idx when idx <> [] ->
@@ -11957,7 +12008,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          | other ->
            fail loc
              "slice takes an array, a slice, a string or a Vec, found %s"
-             (Types.to_string other)
+             (tyname loc other)
        in
        (* An array that came back from a call is a value in a temporary this
           expression does not own: the slice would outlive it and view
@@ -12087,7 +12138,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
              "slice-from takes a (Ptr T) and the number of elements behind \
               it, found %s. A slice or an array already has a length; \
               (slice v lo hi) views part of one"
-             (Types.to_string other)
+             (tyname loc other)
        in
        let n_loc = n.Ast.loc in
        let spelled_n = spell_arg "n" n in
@@ -12101,7 +12152,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
           fail n_loc
             "slice-from counts elements with an integer, found %s. Write \
              (slice-from %s (i64 %s))"
-            (Types.to_string other) spelled_target spelled_n);
+            (tyname loc other) spelled_target spelled_n);
        (* A negative literal is a lie the checker can see, so it does not wait
           for the run-time test emit.ml plants beside it. *)
        (match literal n with
@@ -12139,7 +12190,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     (match a.Tast.ty with
      | Types.Ptr (_, t) -> expect ctx loc ~want (mk loc t (Tast.Deref a))
      | other -> fail loc "deref takes a (Ptr T), found %s"
-                  (Types.to_string other))
+                  (tyname loc other))
 
   (* ── Option ────────────────────────────────────────────────────── *)
   (* (Some nil) cannot be built. Some marks a value present; nil is dyn's own
@@ -12488,7 +12539,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
               Printf.sprintf
                 "%s has no rendering, so it cannot be watched — watch the \
                  values you want out of it instead"
-                (Types.to_string t))
+                (tyname loc t))
             (render_ctx ctx emitter) 0 value
       in
       let begin_ =
@@ -12569,7 +12620,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | other ->
        fail loc "%s converts an integer to an enum, found %s — an enum or a \
                  float goes through (i32 x) first" name
-         (Types.to_string other));
+         (tyname loc other));
     prim (Tast.Cast target) target [ a ]
   (* A cast to a *type variable*: [(t x)] or [($t x)] inside a generic body.
      The name is not one [is_cast] knows, because [is_cast] asks whether the
@@ -12618,7 +12669,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | Types.Var v ->
        cast_operand ctx loc name ~needs:"numeric?" ~also:("enum?", "an enum")
          ~what:"a number or an enum" ~is:"a number" v
-     | t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
+     | t -> fail loc "%s converts a number, found %s" name (tyname loc t));
     prim (Tast.Cast target) target [ a ]
   | _ when is_cast name && List.length args = 1 ->
     let target = resolve_name ctx.env ~seen:[] loc name in
@@ -12650,7 +12701,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | Types.Var v ->
        cast_operand ctx loc name ~needs:"numeric?" ~also:("enum?", "an enum")
          ~what:"a number or an enum" ~is:"a number" v
-     | t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
+     | t -> fail loc "%s converts a number, found %s" name (tyname loc t));
     (match a.Tast.ty with
      | Types.Dyn -> cast_dyn ctx loc target a
      | _ -> prim (Tast.Cast target) target [ a ])
@@ -13188,8 +13239,8 @@ and generic_call ctx ~want loc name vars pats pret args =
                    exactly — the pair cannot join at the wider type there. \
                    Write the conversion — (%s x) — or pass the arguments at \
                    one type"
-                  name v (Types.to_string p) (Types.to_string a.Tast.ty) v
-                  (Types.to_string p)
+                  name v (tyname loc p) (tyname loc a.Tast.ty) v
+                  (tyname loc p)
               | None ->
                 pending := (v, p, a.Tast.ty, a.Tast.loc) :: !pending;
                 true)
@@ -13199,13 +13250,13 @@ and generic_call ctx ~want loc name vars pats pret args =
             place a widening thunk can be built around it. See [bind_ty]. *)
          if (not handled) && not (bind_ty ~widen:true subst p a.Tast.ty) then
            fail a.Tast.loc "%s expects %s here, found %s%s" name
-             (Types.to_string p) (Types.to_string a.Tast.ty)
+             (tyname loc p) (tyname loc a.Tast.ty)
              (match p, a.Tast.ty with
               | Types.Slice (Types.Mut, _), Types.Slice (Types.Const, e) ->
                 Printf.sprintf
                   " — %s takes a slice it may write through, and a %s can \
                    only be read%s"
-                  name (Types.to_string a.Tast.ty)
+                  name (tyname loc a.Tast.ty)
                   (match const_copy ctx.env e with
                    | Some c ->
                      Printf.sprintf ". %s copies v into one that can be written" c
@@ -13239,7 +13290,7 @@ and generic_call ctx ~want loc name vars pats pret args =
            "this call binds %s's $%s to both %s and %s, and neither holds \
             every value of the other. Write the conversion you mean at one \
             of the arguments, or pass them at one type"
-           name v (Types.to_string t1) (Types.to_string t2))
+           name v (tyname loc t1) (tyname loc t2))
     !pending;
   (* The binding is final; the arguments it out-widened catch up. Only a bare
      [$t] parameter can be here — [bound_exactly] kept every container-bound
@@ -13288,8 +13339,8 @@ and generic_call ctx ~want loc name vars pats pret args =
                   (Tast.Thicken (thick_thunk ctx.env a.Tast.loc ps r, a))
               else
                 fail a.Tast.loc "%s expects %s here, found %s" name
-                  (Types.to_string (Types.Fn (ps, r)))
-                  (Types.to_string a.Tast.ty)
+                  (tyname loc (Types.Fn (ps, r)))
+                  (tyname loc a.Tast.ty)
             | _ -> a))
       pats targs
   in
@@ -13331,7 +13382,7 @@ and generic_call ctx ~want loc name vars pats pret args =
            "this call would instantiate %s at $%s = %s, and a type variable \
             is not instantiated at dyn. Write the type the value has, or use \
             a defgeneric with a defmethod per class"
-           name v (Types.to_string t))
+           name v (tyname loc t))
     !subst;
   let cparams = List.map (subst_ty !subst) pats in
   let cret = subst_ty !subst pret in
@@ -13369,7 +13420,7 @@ and generic_call ctx ~want loc name vars pats pret args =
               Loc.failk "check/predicate-unsatisfied" loc
                 "%s is written {:where (%s $%s)}, and this call passes %s, \
                  which is not %s"
-                name p.Ast.pname p.Ast.pvar (Types.to_string t) p.Ast.pname
+                name p.Ast.pname p.Ast.pvar (tyname loc t) p.Ast.pname
             | _ -> ())
          gfn.Ast.fwhere);
     expect ctx loc ~want (mk loc cret (Tast.Call (name, targs)))
@@ -13420,7 +13471,7 @@ and instantiate env loc gname vars subst cparams cret =
              Loc.failk "check/predicate-unsatisfied" loc
                "this call instantiates %s at $%s = %s, and %s is not %s. %s is \
                 written {:where (%s $%s)} — pass a type the predicate admits"
-               gname p.Ast.pvar (Types.to_string t) (Types.to_string t)
+               gname p.Ast.pvar (tyname loc t) (tyname loc t)
                p.Ast.pname gname p.Ast.pname p.Ast.pvar)
       fn.Ast.fwhere;
     if Hashtbl.mem env.fns sym then
@@ -13471,7 +13522,7 @@ and instantiate env loc gname vars subst cparams cret =
           String.concat ", "
             (List.map
                (fun v -> Printf.sprintf "$%s = %s" v
-                   (Types.to_string (List.assoc v subst)))
+                   (tyname loc (List.assoc v subst)))
                vars)
         in
         let in_prelude (l : Loc.t) = String.equal l.Loc.file Prelude.file in
@@ -14546,12 +14597,12 @@ let collect env (decls : Ast.decl list) =
                 which is what a C function pointer would need, and not about \
                 crossing today. Write the callback in C, or give the binding \
                 a (Ptr ()) and let the shim pass C's own"
-               what fn.Ast.name (Types.to_string t)
+               what fn.Ast.name (tyname loc t)
            | _ ->
              fail loc
                "%s of %s is %s, which cannot cross to C directly — pass \
                 (Ptr %s) and let the shim read it" what fn.Ast.name
-               (Types.to_string t) (Types.to_string t)
+               (tyname loc t) (tyname loc t)
          in
          List.iter (crossable "a parameter") params;
          crossable "the return type" ret;
@@ -14593,7 +14644,7 @@ let collect env (decls : Ast.decl list) =
                fail t.Ast.tloc
                  "%s names %s as its parent, and a parent is a condition \
                   struct, such as Error, the root every error descends from"
-                 n (Types.to_string pt)));
+                 n (tyname loc pt)));
          let fields = List.map field fs in
          (* Recorded before the refusal below rather than after it, because the
             refusal asks [region_only], which walks this very declaration: a
@@ -15251,7 +15302,7 @@ let container_global_init loc n (ty : Types.t) (init : Ast.init) =
       fail loc
         "the global %s is %s, and uninit on one is refused. Write (defonce \
          %s %s) with no initialiser — a zeroed %s is an empty one"
-        n (Types.to_string ty) n (Types.to_string ty) (Types.to_string ty)
+        n (tyname loc ty) n (tyname loc ty) (tyname loc ty)
     | _ -> ()
 
 (* A container global has to be a [defonce]. A [defconst] is not an assignable
@@ -15266,8 +15317,8 @@ let no_container_defconst loc n (ty : Types.t) =
       "the global %s is %s, and a %s global is a defonce, not a defconst — a \
        defconst would stay the empty %s it was declared as. Write (defonce %s \
        %s) and fill it in a function"
-      n (Types.to_string ty) (Types.to_string ty) (Types.to_string ty)
-      n (Types.to_string ty)
+      n (tyname loc ty) (tyname loc ty) (tyname loc ty)
+      n (tyname loc ty)
 
 (* A union member written into a *constant* would have to be encoded into the
    blob at link time, which is the byte-level encoder a data type case does not
@@ -16109,7 +16160,7 @@ let dyn_descriptors (p : Tast.program) =
           collector marks a struct's dyn fields by their byte offsets, which \
           %s does not have — its storage is not part of the value. Hold the \
           dyn in a struct field, or wait for the typed container view"
-         what (Types.to_string t) (Types.to_string at) (Types.to_string at)
+         what (tyname loc t) (tyname loc at) (tyname loc at)
      | None -> ());
     (* The count is saturated, so the message says more-than rather than a
        figure the reader could check — which is the honest thing to print,
@@ -16120,7 +16171,7 @@ let dyn_descriptors (p : Tast.program) =
          offsets of an array are flattened one element at a time, and %d is \
          the most this compiler will write out — the repeat form that would \
          avoid it arrives with the typed container view"
-        what (Types.to_string t) desc_offsets_max desc_offsets_max
+        what (tyname loc t) desc_offsets_max desc_offsets_max
   in
   (* The foreign boundary, which is the one place the note above admits an
      honest hole. Every slot, global and array this compiler hands out for a
diff --git a/lib/indent_printer.ml b/lib/indent_printer.ml
index 88b14e23..eab9fe7b 100644
--- a/lib/indent_printer.ml
+++ b/lib/indent_printer.ml
@@ -363,7 +363,7 @@ and head_text (h : Form.t) =
   | Form.Sym s -> fst (sym h s)
   | _ -> at 9 h
 
-and list _f h args =
+and list f h args =
   let call () = (head_text h ^ "(" ^ commas args ^ ")", 9) in
   match h.v, args with
   | Form.Sym "quote", [ x ] -> ("'" ^ Form.to_source x, 10)
@@ -418,6 +418,10 @@ and list _f h args =
     if glued then (tt ^ s, 9) else call ()
   | Form.Sym s, [ ({ v = Form.Map _; _ } as m) ] when name_ok s && R.capitalised s ->
     (s ^ fst (expr m), 9)
+  | Form.Sym "the", _ when (match typed_lambda f with Some (_, [ _ ]) -> true | _ -> false) ->
+    (match typed_lambda f with
+     | Some (head, [ body ]) -> (head ^ " = " ^ unit_text body, 0)
+     | _ -> assert false)
   | Form.Sym "fn", [ { v = Form.Vec ps; _ }; body ] when List.for_all sym_param ps ->
     ("fn(" ^ commas ps ^ ") = " ^ unit_text body, 0)
   | Form.Sym "if", [ c; a; b ] ->
@@ -463,6 +467,26 @@ and assign_text ?(lvl = 0) t v =
 and sym_param (p : Form.t) =
   match p.v with Form.Sym s -> name_ok s | _ -> false
 
+(* [(the (Fn [C dyn] R) (fn [a b] ...))] as [fn(a: C, b) -> R], the typed
+   lambda it reads from; [None] for any other shape. *)
+and typed_lambda (f : Form.t) =
+  let rec tyt (t : Form.t) =
+    match t.v with
+    | Form.List [ { v = Form.Sym (("Fn" | "CFn") as h); _ }; { v = Form.Vec ps; _ }; r ] ->
+      h ^ "(" ^ String.concat ", " (List.map tyt ps) ^ ") -> " ^ tyt r
+    | _ -> at 9 t
+  in
+  match f.v with
+  | Form.List [ { v = Form.Sym "the"; _ };
+                { v = Form.List [ { v = Form.Sym "Fn"; _ }; { v = Form.Vec ts; _ }; r ]; _ };
+                { v = Form.List ({ v = Form.Sym "fn"; _ } :: { v = Form.Vec ps; _ } :: body); _ } ]
+    when List.length ts = List.length ps && List.for_all sym_param ps && body <> [] ->
+    let one (n : Form.t) (t : Form.t) =
+      if is_sym "dyn" t then fst (expr n) else fst (expr n) ^ ": " ^ tyt t
+    in
+    Some ("fn(" ^ String.concat ", " (List.map2 one ps ts) ^ ") -> " ^ tyt r, body)
+  | _ -> None
+
 (* A type after [:] or [->]: the function-type arrow at the top, a postfix
    term below it. *)
 let rec ty (f : Form.t) =
@@ -750,6 +774,9 @@ and value_lines n prefix (v : Form.t) =
   else if n + String.length inline <= width then [ ind n ^ inline ]
   else
     match v.v with
+    | _ when typed_lambda v <> None ->
+      let head, body = Option.get (typed_lambda v) in
+      [ ind n ^ prefix ^ " = " ^ head ] @ block (n + 2) body
     | Form.List ({ v = Form.Sym "fn"; _ } :: { v = Form.Vec ps; _ } :: (_ :: _ as body))
       when List.for_all sym_param ps ->
       [ ind n ^ prefix ^ " = fn(" ^ commas ps ^ ")" ] @ block (n + 2) body
@@ -894,8 +921,14 @@ and sugar n (f : Form.t) : string list option =
       match c.v with
       | Form.List ({ v = Form.Sym r; _ } :: { v = Form.Vec ps; _ } :: (_ :: _ as b))
         when def_name r ->
+        let report, b =
+          match b with
+          | { v = Form.Kw "report"; _ } :: ({ v = Form.Str _; _ } as t) :: (_ :: _ as rest) ->
+            (" " ^ fst (expr t), rest)
+          | _ -> ("", b)
+        in
         Option.map
-          (fun pt -> (i ^ "restart " ^ r ^ "(" ^ pt ^ ")") :: block (n + 2) b)
+          (fun pt -> (i ^ "restart " ^ r ^ "(" ^ pt ^ ")" ^ report) :: block (n + 2) b)
           (params_text ps)
       | _ -> None
     in
@@ -1026,7 +1059,8 @@ and let_lines n prs body =
   (* [(let [x (the T v)])] is [let x: T = v]. *)
   let bind ((t : Form.t), (v : Form.t)) =
     match t.v, v.v with
-    | Form.Sym x, Form.List [ { v = Form.Sym "the"; _ }; ty_; w ] when def_name x ->
+    | Form.Sym x, Form.List [ { v = Form.Sym "the"; _ }; ty_; w ]
+      when def_name x && typed_lambda v = None ->
       ("let " ^ x ^ ": " ^ ty ty_, w)
     | _ -> ("let " ^ guard (at 8 t), v)
   in
@@ -1063,11 +1097,11 @@ let program ?source ?macros:m (fs : Form.t list) : string =
   in
   let rec go = function
     | [] -> []
-    | [ x ] -> [ top x ]
-    | x :: rest -> top (if let_sugar x then in_do x else x) :: go rest
+    | [ x ] -> [ (x, top x) ]
+    | x :: rest -> (x, top (if let_sugar x then in_do x else x)) :: go rest
   in
   let text =
-    try String.concat "\n\n" (go fs) ^ "\n"
+    try Source_text.join_top (go fs) ^ "\n"
     with e -> spelling := (fun _ -> None); inside := (fun _ -> false); raise e
   in
   spelling := (fun _ -> None);
diff --git a/lib/indent_reader.ml b/lib/indent_reader.ml
index 0b3be79e..d2e7e675 100644
--- a/lib/indent_reader.ml
+++ b/lib/indent_reader.ml
@@ -386,6 +386,9 @@ let layout ?(snippet = false) ?(base = 1) ?indent (toks : token list) : token ar
 
 type p = { toks : token array; mutable i : int }
 
+(* Set below [params] and [ty], which the expression parser comes before. *)
+let typed_fn_expr : (p -> Form.t * int) ref = ref (fun _ -> assert false)
+
 let peek p = p.toks.(p.i)
 let peek_at p k = p.toks.(min (p.i + k) (Array.length p.toks - 1))
 let advance p =
@@ -785,6 +788,7 @@ and inline_stmt p : Form.t =
 (* [fn(a, b) = body] is a lambda; [fn(...)] followed by anything else is the
    fallback call spelling of [(fn ...)]. *)
 and fn_expr p =
+  if typed_lambda p then !typed_fn_expr p else
   let t = advance p in
   let lp = advance p in
   let args = items p RP lp.loc ~what:"parameters" in
@@ -801,6 +805,21 @@ and fn_expr p =
      0)
   | _ -> (mk p t.loc (Form.List (sym t.loc "fn" :: args)), 9)
 
+(* Whether the [fn(] at point has a [:] among its parameters or a [->]
+   after them: a lambda that states its types. *)
+and typed_lambda p =
+  let rec go k depth =
+    let t = peek_at p k in
+    match t.tok with
+    | EOF -> false
+    | COLON when depth = 1 -> true
+    | LP | LB | LC -> go (k + 1) (depth + 1)
+    | RP when depth = 1 -> (peek_at p (k + 1)).tok = NAME "->"
+    | RP | RB | RC -> go (k + 1) (depth - 1)
+    | _ -> go (k + 1) depth
+  in
+  go 1 0
+
 and span_of_list l args =
   match List.rev args with
   | [] -> l
@@ -1068,6 +1087,49 @@ let params p (lp : token) =
   in
   go []
 
+(* [fn(a: C, b) -> R = body] is [(the (Fn [C dyn] R) (fn [a b] body))]: the
+   paren [fn] takes its parameters' types from where it is written, and [the]
+   is the form that says what a value is, as in [let x: T = v]. An untyped
+   parameter is dyn, as in a definition, and the return type is required. A
+   block body is added by [lambda_block]. *)
+let () = typed_fn_expr := fun p ->
+  let t = advance p in
+  let lp = advance p in
+  let ps = params p lp in
+  let rec split = function
+    | n :: ty :: rest -> let ns, ts = split rest in (n :: ns, ty :: ts)
+    | _ -> ([], [])
+  in
+  let names, tys = split ps in
+  let r =
+    match (peek p).tok with
+    | NAME "->" -> ignore (advance p); ty p
+    | _ ->
+      failk "lambda-return" (where_ p)
+        "a lambda that states its parameters' types states its return type \
+         too: fn(%s) -> R = value"
+        (String.concat ", "
+           (List.map2 (fun n (ty : Form.t) ->
+                if ty.v = Form.Sym "dyn" then text_of n else text_of n ^ ": " ^ text_of ty)
+               names tys))
+  in
+  let fty = mk p lp.loc (Form.List [ sym t.loc "Fn"; Form.make (Form.Vec tys) lp.loc; r ]) in
+  let vec = Form.make (Form.Vec names) lp.loc in
+  let wrap body =
+    mk p t.loc (Form.List [ sym t.loc "the"; fty;
+                            mk p t.loc (Form.List (sym t.loc "fn" :: vec :: body)) ])
+  in
+  match (peek p).tok with
+  | NAME "=" ->
+    ignore (advance p);
+    let i0 = p.i and t0 = peek p in
+    let body, _ = expr p in
+    (wrap [ unit_slot p i0 t0 body ], 0)
+  | NEWLINE when (peek_at p 1).tok = INDENT -> (wrap [], 0)
+  | _ ->
+    failk "lambda-body" (where_ p)
+      "a lambda's body follows = on its line, or is the block under it"
+
 let rec stmts (s : st) : Form.t list =
   let p = s.p in
   match (peek p).tok with
@@ -1143,6 +1205,15 @@ and then_on_line p =
 
 and lambda_block ?(block_ok = false) (s : st) (e : Form.t) ~after =
   let p = s.p in
+  match e.v with
+  (* A typed lambda waiting for its block, from [typed_fn_expr]. *)
+  | Form.List [ ({ v = Form.Sym "the"; _ } as th); fty;
+                ({ v = Form.List [ ({ v = Form.Sym "fn"; _ } as fh); ({ v = Form.Vec _; _ } as vec) ]; _ } as fn_) ]
+    when (peek p).tok = NEWLINE && (peek_at p 1).tok = INDENT ->
+    ignore (advance p);
+    let body = block s ~after in
+    mk p e.loc (Form.List [ th; fty; { fn_ with v = Form.List (fh :: vec :: body) } ])
+  | _ ->
   if is_lambda_candidate e && (last p).tok = RP && (peek p).tok = NEWLINE
      && (peek_at p 1).tok = INDENT
   then begin
@@ -1216,11 +1287,9 @@ and stmt (s : st) : Form.t =
   | NAME w when header_follow p w -> header s w
   | NAME (("else" | "elif") as w) when one_line_if_above p t ->
     failk "orphan-else" t.loc
-      "the if above is a one-line if, which ends with its line, so this %s \
-       has no if to belong to. Keep the one-line form on one line:\n\n\
-      \    if c then a else b\n\n\
-       or give each branch a block:\n\n\
-      \    if c\n      a\n    else\n      b"
+      "this %s is not at the column of the one-line if above it. An else or \
+       elif that continues a one-line if goes at the if's column:\n\n\
+      \    if c then a\n    else b"
       w
   | NAME (("else" | "elif") as w) ->
     failk "orphan-else" t.loc
@@ -1455,72 +1524,88 @@ and header (s : st) w : Form.t =
     form [ alias; path ]
   | "if" ->
     let c, _ = binary p 1 in
+    (* The elif and else clauses at the if's column, then the whole form.
+       [oneline] when the if was [if c then a]: its clauses may then be
+       one-line too, [elif c then x] and [else y], or take blocks. *)
+    let clauses ~oneline body =
+      let rec elifs acc =
+        match (peek p).tok with
+        | NAME "elif" ->
+          ignore (advance p);
+          let c, _ = binary p 1 in
+          (match (peek p).tok with
+           | NAME "then" when oneline ->
+             ignore (advance p);
+             let x = inline_stmt p in
+             expect_eol p ~after:(text_of x);
+             elifs ((c, [ x ]) :: acc)
+           | NAME "then" ->
+             failk "elif-then" (peek p).loc
+               "elif takes its block on the indented lines under it, with no \
+                then. Put the branch on the next line, indented"
+           | _ ->
+             expect_line_end p ~after:("elif " ^ text_of c);
+             let b = block s ~after:"elif" in
+             elifs ((c, b) :: acc))
+        | _ -> List.rev acc
+      in
+      let els_ = elifs [] in
+      let else_ =
+        match (peek p).tok with
+        | NAME "else" ->
+          let et = advance p in
+          (match (peek p).tok with
+           | NEWLINE -> ignore (advance p); Some (et.loc, block s ~after:"else")
+           | NAME "if" when not oneline ->
+             failk "else-if" (where_ p)
+               "else takes its block on the lines under it. For another test \
+                at this level, write elif c"
+           | _ when oneline ->
+             let x = inline_stmt p in
+             expect_eol p ~after:(text_of x);
+             Some (et.loc, [ x ])
+           | _ -> stray p ~after:"else")
+        | _ -> None
+      in
+      match els_, else_ with
+      | [], None -> named "when" (c :: body)
+      | [], Some (el, e) -> form [ c; blk s l0 body; blk s el e ]
+      | _ ->
+        let pairs =
+          List.concat_map (fun (c, b) -> [ c; blk s c.Form.loc b ]) ((c, body) :: els_)
+        in
+        let tail =
+          match else_ with
+          | Some (el, e) -> [ Form.make (Form.Kw "else") el; blk s el e ]
+          | None -> []
+        in
+        named "cond" (pairs @ tail)
+    in
     (match (peek p).tok with
      | NAME "then" ->
        ignore (advance p);
        let a = inline_stmt p in
-       let f =
-         match (peek p).tok with
-         | NAME "else" ->
-           ignore (advance p);
-           let b = inline_stmt p in
-           form [ c; a; b ]
-         | NAME "elif" ->
-           failk "one-line-elif" (peek p).loc
-             "a one-line if has then and else and no elif. Chain another if \
-              after the else — if a then x else if b then y else z — or write \
-              the if over several lines, where elif goes"
-         | _ -> named "when" [ c; a ]
-       in
-       expect_eol p ~after:(text_of f);
-       f
+       (match (peek p).tok with
+        | NAME "else" ->
+          ignore (advance p);
+          let b = inline_stmt p in
+          let f = form [ c; a; b ] in
+          expect_eol p ~after:(text_of f);
+          f
+        | NAME "elif" ->
+          failk "one-line-elif" (peek p).loc
+            "a one-line if has then and else and no elif. Chain another if \
+             after the else — if a then x else if b then y else z — or write \
+             the if over several lines, where elif goes"
+        | _ ->
+          expect_eol p ~after:(text_of (named "when" [ c; a ]));
+          (* An else or elif on the next line, at the if's column,
+             continues it. *)
+          clauses ~oneline:true [ a ])
      | _ ->
        expect_line_end p ~after:("if " ^ text_of c);
        let body = block s ~after:("if " ^ text_of c) in
-       let rec elifs acc =
-         match (peek p).tok with
-         | NAME "elif" ->
-           ignore (advance p);
-           let c, _ = binary p 1 in
-           (match (peek p).tok with
-            | NAME "then" ->
-              failk "elif-then" (peek p).loc
-                "elif takes its block on the indented lines under it, with no \
-                 then. Put the branch on the next line, indented"
-            | _ -> ());
-           expect_line_end p ~after:("elif " ^ text_of c);
-           let b = block s ~after:"elif" in
-           elifs ((c, b) :: acc)
-         | _ -> List.rev acc
-       in
-       let els_ = elifs [] in
-       let else_ =
-         match (peek p).tok with
-         | NAME "else" ->
-           let et = advance p in
-           (match (peek p).tok with
-            | NEWLINE -> ignore (advance p)
-            | NAME "if" ->
-              failk "else-if" (where_ p)
-                "else takes its block on the lines under it. For another test \
-                 at this level, write elif c"
-            | _ -> stray p ~after:"else");
-           Some (et.loc, block s ~after:"else")
-         | _ -> None
-       in
-       (match els_, else_ with
-        | [], None -> named "when" (c :: body)
-        | [], Some (el, e) -> form [ c; blk s l0 body; blk s el e ]
-        | _ ->
-          let pairs =
-            List.concat_map (fun (c, b) -> [ c; blk s c.Form.loc b ]) ((c, body) :: els_)
-          in
-          let tail =
-            match else_ with
-            | Some (el, e) -> [ Form.make (Form.Kw "else") el; blk s el e ]
-            | None -> []
-          in
-          named "cond" (pairs @ tail)))
+       clauses ~oneline:false body)
   | "while" | "until" ->
     let label =
       match (peek p).tok, (peek_at p 1).tok with
@@ -1639,10 +1724,19 @@ and header (s : st) w : Form.t =
         let name = name_tok p ~what:"the restart's name" in
         let lp = glued_lp p ~what:"the restart's parameters in parentheses" in
         let ps = params p lp in
+        (* [restart name() "text"]: the report the break loop shows,
+           [:report "text"] in the clause. *)
+        let report =
+          match (peek p).tok with
+          | ATOM (Form.Str _ as v) ->
+            let st = advance p in
+            [ Form.make (Form.Kw "report") st.loc; Form.make v st.loc ]
+          | _ -> []
+        in
         clause_end p ("restart " ^ text_of name ^ "(...)");
         let b = block s ~after:"restart" in
         let c =
-          mk p name.loc (Form.List (name :: Form.make (Form.Vec ps) lp.loc :: b))
+          mk p name.loc (Form.List (name :: Form.make (Form.Vec ps) lp.loc :: (report @ b)))
         in
         clauses (c :: acc)
       | _ -> List.rev acc
diff --git a/lib/paren_printer.ml b/lib/paren_printer.ml
index 78df2da9..fd32ae83 100644
--- a/lib/paren_printer.ml
+++ b/lib/paren_printer.ml
@@ -327,13 +327,13 @@ let program ?source (fs : Form.t list) : string =
       cs
   in
   let text =
-    String.concat "\n\n"
+    Source_text.join_top
       (List.map
          (fun (f : Form.t) ->
-            String.concat "\n"
-              (match layout ~inside spell 0 f with
-               | first :: rest -> Source_text.tag f.loc.Loc.line first :: rest
-               | [] -> []))
+            (f, String.concat "\n"
+               (match layout ~inside spell 0 f with
+                | first :: rest -> Source_text.tag f.loc.Loc.line first :: rest
+                | [] -> [])))
          fs)
     ^ "\n"
   in
diff --git a/lib/source_text.ml b/lib/source_text.ml
index e876f58f..16617d1a 100644
--- a/lib/source_text.ml
+++ b/lib/source_text.ml
@@ -206,3 +206,23 @@ let weave ?(starts = []) (cs : comment list) (text : string) : string =
     else s
   in
   trim s
+
+(** Top-level forms' printed texts joined with a blank line between them,
+    except that one-line globals written on adjacent lines stay adjacent. *)
+let join_top (items : (Form.t * string) list) : string =
+  let global (f : Form.t) =
+    match f.v with
+    | Form.List ({ v = Form.Sym ("def" | "defonce" | "defconst"); _ } :: _) -> true
+    | _ -> false
+  in
+  let rec go = function
+    | [] -> []
+    | [ (_, t) ] -> [ t ]
+    | ((a : Form.t), ta) :: (((b : Form.t), tb) :: _ as rest) ->
+      let tight =
+        global a && global b && (not (String.contains ta '\n'))
+        && (not (String.contains tb '\n')) && b.loc.Loc.line = a.loc.Loc.eline + 1
+      in
+      ta :: (if tight then "\n" else "\n\n") :: go rest
+  in
+  String.concat "" (go items)
diff --git a/lib/types.ml b/lib/types.ml
index 37162cd5..7ba99ed4 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -229,6 +229,10 @@ let rec equal a b =
    and then only in how a message spells it. *)
 let display : (string, string) Hashtbl.t = Hashtbl.create 16
 
+(* The same copies as the template and its arguments, for [spell] to write
+   in either syntax. *)
+let display_app : (string, string * t list) Hashtbl.t = Hashtbl.create 16
+
 (* A struct's name as a printed value's head: its own name, or for a generic
    struct's copy the template and its arguments, [Pair i32] — so a value
    prints as [(Pair i32 {.a 1 .b 2})], the way its type is written. *)
@@ -238,7 +242,33 @@ let struct_head n =
     String.sub d 1 (String.length d - 2)
   | _ -> n
 
-let rec to_string = function
+(* A type as the code it is written in spells it: [(Fn [i32] bool)] in a
+   .flan file, [Fn(i32) -> bool] in a .fln one. Messages use it; a spelling
+   that is a key, a symbol or a runtime string stays [to_string]'s. *)
+let rec spell ~indented t =
+  if not indented then to_string t
+  else
+    let sp = spell ~indented in
+    let call h args = h ^ "(" ^ String.concat ", " args ^ ")" in
+    match t with
+    | Named n ->
+      (match Hashtbl.find_opt display_app n with
+       | Some (g, args) -> call g (List.map sp args)
+       | None -> to_string t)
+    | Slice (Mut, t) -> "[" ^ sp t ^ "]"
+    | Slice (Const, t) -> "[const " ^ sp t ^ "]"
+    | Array (n, t) -> Printf.sprintf "[%Ld %s]" n (sp t)
+    | LArray (n, t) -> Printf.sprintf "[$%s %s]" n (sp t)
+    | Map (k, v) -> call "Map" [ sp k; sp v ]
+    | Ptr (Mut, t) -> call "Ptr" [ sp t ]
+    | Ptr (Const, t) -> call "Ptr" [ "const " ^ sp t ]
+    | Vec t -> call "Vec" [ sp t ]
+    | Option t -> call "Option" [ sp t ]
+    | Fn (ps, r) -> call "Fn" (List.map sp ps) ^ " -> " ^ sp r
+    | CFn (ps, r) -> call "CFn" (List.map sp ps) ^ " -> " ^ sp r
+    | _ -> to_string t
+
+and to_string = function
   | Int k -> ikind_name k
   | Float k -> fkind_name k
   | Bool -> "bool"
diff --git a/spec-syntax.md b/spec-syntax.md
index 22218f78..bb6bac9f 100644
--- a/spec-syntax.md
+++ b/spec-syntax.md
@@ -88,9 +88,10 @@ reads as `(rl/with-drawing (rl/clear-background rl/black) (game-draw))`.
 Replacing macros with built-in constructs is **not** part of this work.
 
 **Diagnostics may print paren syntax** during the test drive. `Form.to_string`,
-`Types.to_string`, the usage strings in `parse.ml` and `check.ml`, and
-`Render` all print parens today (inventory in section 5). Fixing that waits on
-the author deciding to switch.
+the usage strings in `parse.ml` and `check.ml`, and `Render` print parens
+today (inventory in section 5). Types in `check.ml`'s messages do not: they
+are spelled by `Types.spell`, in the syntax of the code the message is about
+(section 3, item 9).
 
 ## 2. Proposed (confirm before building the piece it governs)
 
@@ -201,7 +202,10 @@ Each item: the proposal, then the reason in one line.
 - **`if`/`elif`/`else`.** `else` and `elif` sit at the `if`'s column. No `elif`
   reads as `if` (with else) or `when` (without); with `elif` it reads as `cond`.
   One-line form: `if c then a else b`, for use in a `let`. **Built** (a block
-  of one line is that line; of more, `(do …)`).
+  of one line is that line; of more, `(do …)`). An `else` or `elif` on the
+  line after a one-line `if c then a`, at its column, continues it (section
+  3, item 6); each such clause is one-line (`elif c then x`, `else y`) or
+  takes a block.
 - **`while c`, `until c`**, optional label first: `while :outer c`. **Built.**
 - **`for i in range(n)`**, `range(a, b)`, `range(a, b, step)` read as
   `dotimes`. `range` here is syntax, not a function. `..` is avoided because
@@ -253,14 +257,17 @@ Each item: the proposal, then the reason in one line.
     v * 2
   ```
   `handler-bind` takes the same `on` clauses; the reader moves them in front of
-  the body, where the form wants them. **Built.**
+  the body, where the form wants them. **Built.** A restart's report text goes
+  on its header, `restart retry() "Try the load again"`, and reads
+  `(retry [] :report "Try the load again" …)`.
 - **Unit:** `()` as a statement reads `(do)`; in a type it is `()`. **Built**;
   inside an expression `()` stays `()`, and the printer writes a lone `()`
   statement as `(())`. A bare `()` in a one-line body slot (`fn f() -> () = ()`,
   `_ -> ()`, `fn() = ()`, `then ()`) is a statement too, and reads `(do)`.
 - **Lambda:** `fn(i, j) = i * 10 + j`, or `fn(i, j)` plus a block. **Built**;
   its parameters are bare names, as `(fn [i j] …)` wants, with no `dyn`.
-  `fn(…)` followed by anything else is the fallback call.
+  `fn(…)` followed by anything else is the fallback call. A lambda may state
+  its types, `fn(a: C, b) -> bool = …` or plus a block (section 3, item 7).
 
 ### Definitions
 
@@ -274,10 +281,14 @@ Each item: the proposal, then the reason in one line.
 - `struct Cell` with a `name: Type` line per field. `data Shape` with a line per
   case: `Circle(r: f32)`, `Empty`. `enum K` with `lo = -1`, `mid`. `union U` like
   `struct`. **Built** (an untyped field is `dyn`; `Empty()` is `(Empty [])`).
+  A member is `:mid` or `K.mid`, in a value and in a match arm, in both
+  syntaxes (section 3, item 8).
 - `import rl "vendor:raylib"`. **Built.**
 - **Every other form uses the fallback** (next item) until someone asks for
   sugar: `defclass`, `defgeneric`, `defmulti`, `defmethod`, `declare`,
   `declare-c`, `defalias`, `defmacro`, `loop`/`recur`, `array-fill`. **Built.**
+  The class forms keep the fallback for good (2026-09-26):
+  `defmethod(area, point, [p]):` reads well enough.
 
 ### The fallback
 
@@ -341,6 +352,27 @@ after it, so `~name(x)` is `((unquote name) x)`, and `~(f(x))` unquotes a call.
    omitted. `_` in type position means "fill this in" in Rust and OCaml too,
    and no type can be named `_`.
 
+Settled 2026-09-26, after writing programs by hand (`test/syntax/handwritten/`):
+
+6. **A one-line if continues on the next line.** `if c then a` followed by
+   `else b` (or `elif c2 then d`, or either with a block) at the if's column
+   is one if. An `else` left of that column is refused.
+7. **Typed lambdas.** `fn(a: C, b) -> R = body`, or plus a block, reads
+   `(the (Fn [C dyn] R) (fn [a b] body))`: the paren `fn` has no typed
+   parameters, and `the` is how a value states its type, as in
+   `let x: T = v`. An untyped parameter is `dyn`; the return type is
+   required. Where a `CFn` of the same signature is wanted, the literal is
+   that `CFn`. The printer writes that form back as the typed lambda.
+8. **`Dir.north` is the enum member `:north`**, in a value and in a match
+   pattern, in both syntaxes. `:north` stays.
+9. **Types in messages follow the code's syntax.** `Types.spell ~indented` is
+   the one printer, `Fn(A) -> R`, `Option(i32)`, `Small(4, i32)` for a .fln
+   location and `(Fn [A] R)` for a .flan one; `Types.to_string` stays the
+   spelling for keys, symbols and runtime strings. Hard-coded code in a hint
+   is written per message.
+10. **`flan convert` keeps adjacent one-line globals adjacent**, in both
+    directions.
+
 ## 4. Build order
 
 Each step lands on its own, with `dune test --root .` green.
diff --git a/test/syntax/handwritten/csv.fln b/test/syntax/handwritten/csv.fln
index 2c63edc6..bb1a54cb 100644
--- a/test/syntax/handwritten/csv.fln
+++ b/test/syntax/handwritten/csv.fln
@@ -26,7 +26,7 @@ fn flush(field: Ptr(Vec(u8)), row: Ptr(Vec(string))) -> ()
 fn parse-line(line: [const u8]) -> Vec(string)
   let row = vec-new(string)
   let field = vec-new(u8)
-  let state: State = :start
+  let state = State.start
   for i in range(length(line))
     let c = line[i]
     match state
@@ -38,7 +38,7 @@ fn parse-line(line: [const u8]) -> Vec(string)
         else
           push(field, c)
           state = :bare
-      :bare ->
+      State.bare ->
         if c == separator
           flush(addr(field), addr(row))
           state = :start
diff --git a/test/syntax/handwritten/traffic.fln b/test/syntax/handwritten/traffic.fln
index e0b56b23..efcf64fa 100644
--- a/test/syntax/handwritten/traffic.fln
+++ b/test/syntax/handwritten/traffic.fln
@@ -18,10 +18,8 @@ const red-time = 3
 fn next(l: Light, pressed: bool) -> Light
   match l
     Green(left) ->
-      if left > 1 and not pressed
-        Light.Green{.left left - 1}
-      else
-        Light.Yellow{.left yellow-time, .walk pressed}
+      if left > 1 and not pressed then Light.Green{.left left - 1}
+      else Light.Yellow{.left yellow-time, .walk pressed}
     Yellow(left, walk) ->
       if left > 1
         Light.Yellow{.left left - 1, .walk walk}
@@ -53,9 +51,7 @@ fn run(ticks: i32, presses: [const i32], fault-at: i32) -> ()
       l = restart-case
         error(Fault{.tick t})
         l
-      restart reset()
-        :report
-        "Put the light back to red and carry on"
+      restart reset() "Put the light back to red and carry on"
         Light.Red{.left red-time, .walk false}
       restart flash()
         Light.Flashing{}
diff --git a/test/syntax/handwritten/words.fln b/test/syntax/handwritten/words.fln
index 65d3773f..e090d550 100644
--- a/test/syntax/handwritten/words.fln
+++ b/test/syntax/handwritten/words.fln
@@ -58,7 +58,7 @@ fn main() -> i32
   let text = "The cat saw the dog. The dog didn't see the cat, but the bird saw both!"
   let ws = words(bytes-view(text))
   let counts = tally(slice(ws))
-  let by-count: Fn(Count, Count) -> bool = fn(a, b)
+  let by-count = fn(a: Count, b: Count) -> bool
     if a.n != b.n
       return a.n > b.n
     bytes<?(a.word, b.word)
diff --git a/test/test_syntax.ml b/test/test_syntax.ml
index 0602f8f0..d54d3284 100644
--- a/test/test_syntax.ml
+++ b/test/test_syntax.ml
@@ -592,8 +592,21 @@ let () =
     "indent/lambda-block-in-brackets" "let f = fn(a, b)";
   refuses "an unclosed call swallows the next line" "fn f() -> ()\n  push(v, 1\n  g()"
     "indent/missing-comma" "If the ( on line 2 was meant to close";
-  refuses "else under a one-line if" "if a then b\nelse c"
-    "indent/orphan-else" "one-line if";
+  reads "else on the line after a one-line if" "if a then b\nelse c" "(if a b c)";
+  reads "elif and else continuing a one-line if"
+    "if a then b\nelif c then d\nelif e\n  f()\n  g()\nelse\n  h()"
+    "(cond a b c d e (do (f) (g)) :else (h))";
+  refuses "else left of a one-line if" "while x\n  if a then b\nelse c"
+    "indent/orphan-else" "goes at the if's column";
+  reads "a typed lambda" "f = fn(a: C, b) -> bool = a.n < b"
+    "(set f (the (Fn [C dyn] bool) (fn [a b] (< (.n a) b))))";
+  reads "a typed lambda with a block" "let f = fn(x: i32) -> i32\n  let y = x + 1\n  y\ng(f)"
+    "(let [f (the (Fn [i32] i32) (fn [x] (let [y (+ x 1)] y)))] (g f))";
+  refuses "a typed lambda states its return type" "f = fn(a: C) = a"
+    "indent/lambda-return" "fn(a: C) -> R = value";
+  reads "a restart's report on its header"
+    "restart-case\n  go()\nrestart retry(n: i32) \"Try again\"\n  n"
+    "(restart-case (go) (retry [n i32] :report \"Try again\" n))";
   reads "a bare () in a body slot does nothing"
     "fn f() -> () = ()\nfn g(x) -> ()\n  match x\n    1 -> h()\n    _ -> ()\n  k = fn() = ()"
     "(defn f [] () (do))\n(defn g [x dyn] () (match x 1 (h) _ (do)) (set k (fn [] (do))))";
@@ -763,6 +776,18 @@ let () =
     "(defn f [] () (if (> a 1) (let [k 2] (g k))))" "  if(a > 1):\n    let k = 2";
   prints "and inside or keeps its parentheses"
     "(defn f [a bool b bool c bool] bool (or (and a b) c))" "= (a and b) or c";
+  prints "a typed lambda prints as one"
+    "(defn f [] () (let [g (the (Fn [C] bool) (fn [c] (> (.n c) 3)))] (h g)))"
+    "let g = fn(c: C) -> bool = c.n > 3";
+  prints "a restart's report goes on its header"
+    "(defn f [] i32 (restart-case (go) (retry [] :report \"Try again\" 7)))"
+    "restart retry() \"Try again\"\n    7";
+  prints "adjacent one-line globals stay adjacent"
+    "(defonce a i32)\n(def b i32 2)\n\n(defconst c 3)\n"
+    "once a: i32\ndef b: i32 = 2\n\nconst c = 3";
+  back "adjacent one-line globals stay adjacent in parens"
+    "once a: i32\ndef b: i32 = 2\n\nconst c = 3\n"
+    "(defonce a i32)\n(def b i32 2)\n\n(defconst c 3)";
   prints "a field of a field chains" "(defn f [] () (g (.count (.x w))))" "g(w.x.count)";
   prints "an else-if chain on one line"
     "(defn f [r] dyn (if (> r 7) :rich (if (> r 4) :fair :poor)))"
@@ -983,6 +1008,31 @@ let () =
     [ "write ++(x) or x += 1" ];
   refused "plusplus-global.fln" "once g = 0\n\nfn main() -> i32\n  g--\n  0\n"
     [ "write --(g) or g -= 1" ];
+  (* Types in a message are in the syntax of the code it is about. *)
+  refused "types.fln" "fn g(x: Option(i32)) -> i32 = 0\n\nfn main() -> i32\n  let v = vec-new(i32)\n  g(v)\n"
+    [ "expected Option(i32), found Vec(i32)" ];
+  refused "types.flan" "(defn g [x (Option i32)] i32 0)\n(defn main [] i32 (let [v (vec-new i32)] (g v)))\n"
+    [ "expected (Option i32), found (Vec i32)" ];
+  refused "fn-field.fln" "struct R\n  f: Fn(i32) -> bool\n\nfn main() -> i32 = 0\n"
+    [ "cannot be Fn(i32) -> bool"; "store a CFn(i32) -> bool" ];
+  refused "generic-struct.fln"
+    "struct Small\n  items: [$n $t]\n\nfn main() -> i32\n  let s: Small(4, i32) = zeroed()\n  let q: i32 = s\n  0\n"
+    [ "found Small(4, i32)" ];
+  (* Dir.north is the member :north. *)
+  checks "enum-qualified.fln"
+    ("enum Dir\n  north\n  south\n\nfn name(d: Dir) -> i32\n  match d\n    Dir.north -> 1\n    :south -> 2\n\n"
+     ^ "fn main() -> i32\n  let d = Dir.north\n  let e: Dir = Dir.south\n  name(d) + name(e)\n");
+  refused "enum-qualified-miss.fln"
+    "enum Dir\n  north\n\nfn f(d: Dir) -> i32\n  match d\n    Dir.west -> 1\n    _ -> 0\n\nfn main() -> i32 = 0\n"
+    [ "Dir has no member west — it has Dir.north" ];
+  (* A bad key type is one error, not three. *)
+  refused "map-key.fln" "fn main() -> i32\n  let m = map-new([const u8], i32)\n  0\n"
+    [ "[const u8] is not a map key" ];
+  (match Front.checked (Filename.concat scratch "map-key.fln") with
+   | exception Loc.Errors (_ :: _ :: _ as ds) ->
+     fail "map-key.fln: %d errors, wanted one" (List.length ds)
+   | exception _ -> ()
+   | _ -> ());
   refused "defvar.fln" "defvar(x, 1)\n\nfn main() -> i32 = 0\n"
     [ "once x = 1 initialises once"; "def x = 1 re-initialises" ]