diff --git a/FIX.org b/FIX.org
index 0621920..4649ca5 100644
--- a/FIX.org
+++ b/FIX.org
@@ -5468,3 +5468,77 @@ that is a session of its own.
 The four-green result is measured against that base. dev-loop has moved since
 — runtime/flan_rt.c, vendor/agent/flan_agent.c and lib/dev.ml among others —
 and those belong to the next batch, not to this one.
+
+* Diagnostics reworded, 2026-09-21
+The author, on a message that ran three lines to explain a naming decision:
+
+#+begin_quote
+go through all compiler messages and rewrite them plainly to state what they
+mean, I don't need this verbosity, it's too much
+#+end_quote
+
+And, correcting the example he gave for it:
+
+#+begin_quote
+it should say that defvar doesn't exist. You shouldn't write compiler errors
+that report design decisions we've made, but should report errors to use[rs]
+who have never used this language and have no idea that defvar even existed
+#+end_quote
+
+So the standard is two rules, not one. A message says what is wrong and what
+to write, and stops. And it says it to someone holding this compiler and
+nothing else: no prior spelling, no milestone number, no plan.org, no
+rename framed as a rename. defunion's refusal now states what defunion is and
+what to write for a tagged sum, rather than announcing that the tagged sum
+"is defdata now".
+
+The headline case is the one the author quoted. It said defvar was renamed
+and then explained the choice of name; it now says:
+
+  there is no defvar.
+    Did you mean defonce? (defonce gravity float 0.1) initialises once and
+    keeps its value. (def gravity float 0.1) re-initialises on every re-run.
+
+Both spellings in it compile as written, which is the standing rule for a
+suggestion and was checked by building them.
+
+About 130 messages rewritten across lib/check.ml, lib/parse.ml,
+lib/session.ml, lib/load.ml, lib/shim.ml, lib/macro.ml, lib/expand.ml,
+lib/cimport.ml, lib/dev.ml, lib/render.ml, lib/build.ml, lib/emit.ml,
+lib/x86.ml, runtime/flan_rt.c and vendor/agent/flan_agent.c. lib/reader.ml
+was already right and was not touched, nor were parse.ml's "X is (X ...)"
+usage lines, which are the shape everything else was moved towards.
+
+emit.ml's thirty assertions are not diagnostics — each one says the checker
+admitted something it refuses, so no program text reaches one. They now go
+through [Emit.internal], which prefixes "internal:" and says the message is a
+compiler bug, so the one person who ever sees one is told what it is instead
+of reading "no layout for t" as a statement about their own code. x86.ml's
+[unsupported] strings stay as they are: they name the missing feature and
+session.ml already wraps them in the sentence with the fix in it.
+
+Review follow-ups. One rewrite had turned descriptive prose into an
+imperative that does not compile: the Map-into-dyn refusal said "Write
+(map-new dyn) for a dyn map", and there is no such call — map-new wants a key
+and a value, and dyn is refused as a key. A dyn map is the map literal, so
+that is what it names now. Two more of the same class: shim.ml offered
+(as-slice v), a spelling this branch retired in favour of (slice v), and the
+defvar refusal echoed the old form's arguments back inside the new spelling
+even when there were too few to make a valid one — (defvar x) was answered
+with (defonce x), which does not compile. Fewer than two arguments now gets
+the shapes rather than an echo.
+
+Trimming went one word too far in one place: the defer refusal ended "or in a
+let that is", whose antecedent had been inside the parenthetical that was
+cut. And view_not_yet was missed by the sweep entirely — it still carried
+five lines about what the collector does and does not scan.
+
+Test needles followed the wording, each one picked to stay specific to the
+message it is about. Two rows had to be re-pinned after review: both asserted
+"uninit on one is refused", which matches the container-global arm and the
+data-type arm alike, so each now names something only its own arm says. One
+test was asserting the wrong thing: "a dyn in a
+condition's payload" reached the struct-field refusal that fired first, never
+the condition arm it was named for. The struct refusal is gone since the
+descriptors landed, so the row is an [accepts] now and a new [rejects_check]
+signals a dyn directly to reach the arm that is still there.
diff --git a/lib/build.ml b/lib/build.ml
index e0628e0..73098ee 100644
--- a/lib/build.ml
+++ b/lib/build.ml
@@ -747,7 +747,7 @@ let executable ?(opts = default) ?(csrcs = []) ?(lflags = []) ?(pnames = [])
     if opts.sanitize then
       failwith "js: --sanitize is native only";
     if opts.x86 then
-      failwith "js: --x86 and --target=js are two different backends";
+      failwith "js: --x86 and --target=js are two different backends — pick one";
     write out (Js.program ~checks:opts.checks p);
     out
   end
diff --git a/lib/check.ml b/lib/check.ml
index fee22ed..34a1953 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -576,14 +576,12 @@ let captured ctx loc name =
   | Some what when List.mem_assoc name ctx.outer ->
     let why =
       if String.equal what "a handler" then
-        "a handler runs from wherever the signal was. Use a global, or pass \
-         it on the condition"
+        "Use a global, or pass it on the condition"
       else
-        "an fn is lifted into a function of its own and is handed nothing but \
-         its parameters. Pass it in, or use a global"
+        "Pass it in, or use a global"
     in
     Loc.failk "check/capture" loc
-      "%s cannot see %s: it is a local of the enclosing function, and %s."
+      "%s cannot see %s — it is a local of the enclosing function. %s"
       what name why
   | _ -> ()
 
@@ -611,11 +609,11 @@ let branch ctx f =
 (* ── Type resolution ───────────────────────────────────────────────── *)
 
 let unimplemented loc what milestone =
-  (* No repo filename in a message. Somebody meeting this wants to know that
-     the thing is not there yet and roughly how far off it is; where the
-     schedule is written down is the compiler's business, not theirs. *)
-  fail loc "%s is not implemented yet — it is milestone %d work"
-    what milestone
+  (* No repo filename in a message, and no milestone number either: neither
+     means anything to somebody who has this compiler and nothing else. What
+     they need is that the thing is not there yet. *)
+  ignore milestone;
+  fail loc "%s is not implemented yet" what
 
 (* Four names the randomness functions do not have, each with the name that
    does and a call that compiles. A reader who has never seen this language
@@ -832,8 +830,7 @@ let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
      someone will write it, so it is refused by name rather than by a crash. *)
   if Types.equal v Types.Unit then
     fail loc
-      "a map value cannot be () — there is nothing to store. A set of keys \
-       is not built yet; use (Map %s bool) and ignore the value"
+      "a map value cannot be () — write (Map %s bool) and ignore the value"
       (Types.to_string k);
   if Types.equal k Types.Unit then
     fail loc "a map key cannot be () — every key would be the same key";
@@ -850,11 +847,8 @@ let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
           | Types.Var v -> declares preds v "hashable?"
           | k -> Types.keyable k) then
     fail loc
-      "%s is not a map key. The first implementation takes integers, enums, \
-       bools, strings, fixed arrays of those, and value structs composed of \
-       those (spec-memory.md, \"Maps — first implementation\"). A float has \
-       no usable equality — NaN is not equal to itself — and a Ptr, a slice, \
-       a Vec or a Map would hash an address rather than what it points at"
+      "%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);
   Types.Map (k, v)
 
@@ -875,9 +869,8 @@ let rec no_zeroed_fn loc what (t : Types.t) =
   match t with
   | Types.Fn _ ->
     fail loc
-      "%s cannot be %s: it would be zeroed, and a zeroed function value is \
-       a null pointer — every other type's zero is a value it can have, and \
-       this one is not. Pass it as a parameter, or hold it in a let"
+      "%s cannot be %s — it would be zeroed, and a zeroed function value is a \
+       null pointer. Pass it as a parameter, or hold it in a let"
       what (Types.to_string t)
   | Types.Array (_, e) -> no_zeroed_fn loc what e
   | _ -> ()
@@ -1024,10 +1017,9 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
           [Render] and the DWARF path. docs/SPIKE-GENERICS.md, question 4,
           prices it and leaves it out. *)
        fail loc
-         "%s takes no type arguments. A generic *function* is written with \
-          [$t] in its parameter vector and copied per call site; a generic \
-          *type* — (%s ...) — is not there yet"
-         name name)
+         "%s takes no type arguments. A generic function is written with $t \
+          in its parameter vector; a generic type is not there yet"
+         name)
 
 (* One edit away from a type that exists — a substitution, an insertion, a
    deletion or a transposition of neighbours. Bounded at one, because two edits
@@ -1266,16 +1258,16 @@ let dyn_param_or_typo env n loc =
   match suggestion with
   | Some m ->
     Loc.failk "check/unknown-type" loc
-      "unknown type %s — did you mean %s? A parameter with no type is dyn, so \
-       this would otherwise be read as a second parameter called %s"
+      "unknown type %s — did you mean %s? Otherwise %s reads as a second \
+       parameter, because a parameter with no type is dyn"
       n m n
   | None ->
     if n <> "" && n.[0] = Char.uppercase_ascii n.[0]
        && n.[0] <> Char.lowercase_ascii n.[0]
     then
       Loc.failk "check/unknown-type" loc
-        "unknown type %s. A capitalised name in a parameter vector is a type — \
-         a parameter with no type is dyn, and parameters are lowercase"
+        "unknown type %s. A capitalised name in a parameter vector is a type; \
+         parameters are lowercase"
         n
 
 let pair_params env (items : Ast.pitem list) : Ast.field list =
@@ -1284,14 +1276,13 @@ let pair_params env (items : Ast.pitem list) : Ast.field list =
     | [] -> []
     | Ast.Ptype t :: _ ->
       Loc.failk "check/parameter-name-expected" t.Ast.tloc
-        "a parameter's name was expected here, and this is a type. \
-         Parameters are [name Type ...], and a name with no type is dyn"
+        "a parameter's name was expected here, and this is a type. Parameters \
+         are [name Type ...]"
     | Ast.Pname (n, loc) :: rest when is_type_name env n ->
       ignore rest;
       Loc.failk "check/parameter-named-type" loc
-        "%s names a type, so it cannot also be this parameter's name. If the \
-         pair was written backwards it is [name %s]; otherwise rename the \
-         parameter" n n
+        "%s names a type, so it cannot also be this parameter's name. Write \
+         [name %s], or rename the parameter" n n
     | Ast.Pname (n, loc) :: Ast.Ptype t :: rest ->
       { Ast.fname = n; fty = t; floc = loc } :: go rest
     | Ast.Pname (n, loc) :: Ast.Pname (t, tloc) :: rest when is_type_name env t ->
@@ -1629,10 +1620,9 @@ let unconstrained env loc op ~needs (t : Types.t) =
     | Some v when declares env.tvpreds v needs -> ()
     | _ ->
       Loc.failk "check/unconstrained-type-variable" loc
-        "%s over the type variable %s is refused: a type variable supports \
-         only what it is declared to support, and nothing here says %s is \
-         %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"
+        "%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)
 
@@ -1717,11 +1707,9 @@ let runaway env loc gname cparams =
   (match earlier with
    | Some _ ->
      Loc.failk "check/runaway-instantiation" loc
-       "%s instantiates itself without end. Each copy asks for another at a \
-        type built around the one before, so there is no last copy to \
-        generate:\n  %s\nA generic function may call itself, but not at a \
-        type built out of its own type variable — the argument has to get \
-        smaller, or stay the same"
+       "%s instantiates itself without end — each copy asks for another at a \
+        type built around the one before:\n  %s\nRecur at the same type, or \
+        at a smaller one"
        gname (chain_text ())
    | None -> ());
   (* The backstop. Nothing known reaches it; it exists so that a growth the
@@ -1821,8 +1809,7 @@ let embed_path loc (p : Ast.expr) =
   | Ast.Str s -> s
   | _ ->
     Loc.fail p.Ast.loc
-      "an embedded path must be a literal string — the bytes are read at \
-       compile time, so there is nothing here to compute it from"
+      "an embedded path must be a literal string"
 
 (* The whole read is guarded, not only the open. On Linux [open_in_bin] on a
    *directory* succeeds and [in_channel_length] answers a number; the read is
@@ -1841,8 +1828,7 @@ let read_embed_file path loc =
     if Sys.file_exists path && (try Sys.is_directory path with Sys_error _ -> false)
     then
       Loc.fail loc
-        "cannot embed %s: it is a directory — (embed-dir \"...\") embeds one \
-         of those, as a [n EmbedFile]"
+        "cannot embed %s: it is a directory — use embed-dir for one of those"
         path
     else Loc.fail loc "cannot embed %s: %s" path msg
   | exception End_of_file ->
@@ -2093,14 +2079,8 @@ let view_elem_lit loc (k : int64) =
 let view_not_yet loc (container : Types.t) (elem : Types.t) =
   no_dyn_yet loc ~into:true container
     (Printf.sprintf
-       ". A container view at this milestone holds i64, f64 or bool \
-        elements only, and %s is not one of the three. The restriction \
-        exists for the string case: a dyn string's form is a pointer into \
-        the collector's heap, and a typed container's storage is memory the \
-        collector never scans, so a write through a view over strings could \
-        plant a pointer where nothing will ever trace it. Every other \
-        element type is refused with it rather than admitted one width at a \
-        time"
+       ". A container view carries i64, f64 or bool elements, and %s is not \
+        one of them"
        (Types.to_string elem))
 
 (* M2 item 3's second guard, added on review: a view's descriptor holds an
@@ -2219,9 +2199,7 @@ let box loc (e : Tast.expr) : Tast.expr =
      two get confused if unit is allowed to become one. *)
   | Types.Unit ->
     Loc.failk "check/dyn-unit" loc
-      "() does not box into dyn — a value of the zero-sized type carries \
-       nothing a dyn could hold. The absent dyn value is nil, which is a \
-       literal here: write nil"
+      "() does not box into dyn. The absent dyn value is nil — write nil"
   | Types.Never -> e
   (* A view, not a copy: the box holds one word naming where the elements
      live and what one of them is, and every read or write goes straight
@@ -2259,11 +2237,13 @@ let box loc (e : Tast.expr) : Tast.expr =
        else
          dyn "flan_dyn_view_flat"
            [ e; mk loc dyn_i64 (Tast.Int (n, Types.I64)); view_elem_lit loc k ])
+  (* No view for a map yet, and the suggestion is the *literal* rather than a
+     constructor call: there is no [(map-new dyn)] — [map_new_types] wants a
+     key and a value, and [map_type] refuses dyn as a key — so naming one
+     would be advice that does not compile. A dyn map is written {:k v}. *)
   | Types.Map _ ->
     no_dyn_yet loc ~into:true e.Tast.ty
-      ". The dyn container at this milestone is the runtime's own, from \
-       (map-new dyn); a typed (Map K V) has a representation the dyn \
-       runtime cannot walk"
+      ". A dyn map is written as a literal, {:key value ...}"
   (* [Option] is on this list in name only: [expect] intercepts it before
      [box] ever sees one — [box_option] is the real answer, M2 item 4 — so
      this arm only fires for a direct caller that hands [box] an Option
@@ -2301,8 +2281,7 @@ let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
   | Types.Int _ | Types.Float _ ->
     no_dyn_yet loc ~into:false want
       (Printf.sprintf
-         " — the dyn runtime carries integers as i64 and floats as f64, so \
-          take it as %s and convert"
+         " — take it as %s and convert"
          (if Types.is_numeric want && (match want with Types.Float _ -> true | _ -> false)
           then "f64" else "i64"))
   | _ -> no_dyn_yet loc ~into:false want ""
@@ -2407,9 +2386,8 @@ let box_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
   match t with
   | Types.Option inner ->
     Loc.failk "check/option-nested-dyn" loc
-      "(Option (Option %s)) does not cross into dyn — boxing Some of an \
-       inner None would box it as nil, the same nil an outer None becomes, \
-       which is the ambiguity (Some nil) is refused for"
+      "(Option (Option %s)) does not cross into dyn — Some None and None \
+       would both box as nil"
       (Types.to_string inner)
   | _ ->
     (* A literal [Some]/[None] built right here skips the runtime check: the
@@ -2439,8 +2417,8 @@ let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
   match t with
   | Types.Option inner ->
     Loc.failk "check/option-nested-dyn" loc
-      "(Option (Option %s)) does not cross from dyn — a dyn value is nil or \
-       it is not, one absence, and that cannot tell None from Some None apart"
+      "(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)
   | _ when is_nil_lit got -> mk loc oty Tast.None_
   | _ ->
@@ -2645,12 +2623,9 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
      to that is still a refusal rather than a guessed pair. *)
   | Types.Var v ->
     Loc.failk "check/generic-map-key" loc
-      "a map keyed by the type variable %s has no hash and no equality here: \
-       both are emitted as concrete symbols chosen from the concrete key \
-       type, and there is none until this generic is instantiated. The map \
-       operations are deferred to the instantiation when {:where (hashable? \
-       $%s)} is declared — declare it, or write the operation in a function \
-       over the concrete key type and call that" v v
+      "a map keyed by the type variable %s has no hash and no equality here. \
+       Write {:where (hashable? $%s)} at the head of the body, or write the \
+       operation in a function over the concrete key type and call that" v v
   | Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str"
   | t when bytewise_key t ->
     Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"
@@ -2663,10 +2638,8 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
      nothing has yet wanted. Refused by name rather than written untested. *)
   | Types.Named n when Hashtbl.mem env.datas n ->
     fail loc
-      "%s is a data type, and a data type is not a map key: the payload past \
-       the case in hand is indeterminate, so hashing the bytes would make two equal \
-       values hash differently. Hashing one needs a per-case walk, which is \
-       not written — key on the tag, or on a struct holding what you meant" n
+      "%s is a data type, and a data type is not a map key — key on the tag, \
+       or on a struct holding what you meant" n
   (* And an untagged union is refused for the half of that reason which has
      nothing to do with a tag: a member smaller than the union leaves the rest
      of the storage indeterminate, so two values that agree about every byte
@@ -2674,20 +2647,15 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
      either — nothing records which member was written, which is the type. *)
   | Types.Named n when Hashtbl.mem env.unions n ->
     fail loc
-      "%s is a union, and a union is not a map key: a member narrower than \
-       the union leaves the rest of the bytes indeterminate, so two values \
-       that agree about everything written would still hash differently. Key \
-       on the member you meant" n
+      "%s is a union, and a union is not a map key — key on the member you \
+       meant" n
   | Types.Array (_, e) ->
     (* A fixed array of a struct or of strings would need the same per-element
        walk a struct key gets, driven by a loop rather than by a field list.
        Nothing has wanted one, so it is refused by name rather than written
        untested — and refused with the shape that does work named beside it. *)
     fail loc
-      "a fixed array is a map key only when its elements are compared \
-       bytewise, and %s is not — a struct or a string element needs a \
-       per-element walk that is not written. A struct key holding the array \
-       works, because a struct key is walked field by field"
+      "a fixed array of %s is not a map key — a struct holding the array is"
       (Types.to_string e)
   | Types.Float _ ->
     (* Not a milestone question, which is why it is said separately: NaN is not
@@ -2695,16 +2663,12 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
        float key therefore has no equality for a hash map to use, whatever the
        implementation does. *)
     fail loc
-      "a float is not a map key: NaN is not equal to itself, and 0.0 and -0.0 \
-       are equal but differ bytewise, so there is no equality here for a map \
-       to hash. Key on an integer, or on a quantised integer of your choosing"
+      "a float is not a map key — NaN is not equal to itself. Key on an \
+       integer instead"
   | other ->
     fail loc
-      "%s is not a map key. The first implementation takes integers, enums, \
-       bools, strings, fixed arrays of those, and value structs composed of \
-       those (spec-memory.md, \"Maps — first implementation\"). A Ptr, a \
-       slice, a Vec or a Map would hash an address rather than what it points \
-       at, which is a different operation"
+      "%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)
 
 and struct_key_pair env loc n =
@@ -2718,8 +2682,8 @@ and struct_key_pair env loc n =
     let fields = (Hashtbl.find env.structs n).Tast.fields in
     if fields = [] then
       fail loc
-        "%s has no fields, so every value of it is equal to every other — a \
-         map keyed on it holds at most one entry, which is not a map" n;
+        "%s has no fields, so it is not a map key — every value of it would \
+         be the same key" n;
     let hparams = [ Types.Ptr sty; hash_ty; Types.Int Types.I64 ] in
     let eparams = [ Types.Ptr sty; Types.Ptr sty; Types.Int Types.I64 ] in
     (* Registered before the fields are walked, so a struct reached twice
@@ -2852,13 +2816,8 @@ let deferred_key env loc what (k : Types.t) =
   | Types.Var v ->
     if not (declares env.tvpreds v "hashable?") then
       Loc.failk "check/generic-map-key" loc
-        "%s over a map keyed by the type variable %s is refused: the hash and \
-         the equality are emitted as concrete symbols chosen from the \
-         concrete key type, and nothing here declares %s hashable. Write \
-         {:where (hashable? $%s)} at the head of the body — then the \
-         operation is deferred to each instantiation, and a call site that \
-         asks for a key type that cannot be hashed is refused there, against \
-         the clause"
+        "%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;
     true
   | _ -> false
@@ -2967,23 +2926,20 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
            at *any* type the variable can become, not merely at some. *)
         if declares ctx.env.tvpreds v "integer?" then
           Loc.failk literal_at_want loc
-            "the float literal %g cannot stand where $%s is wanted: \
-             {:where (integer? $%s)} admits no float type, so there is no \
-             instantiation at which this literal means anything. Write an \
-             integer literal, or take the value as a parameter"
+            "the float literal %g cannot stand where $%s is wanted — \
+             {:where (integer? $%s)} admits no float type. Write an integer \
+             literal, or take the value as a parameter"
             x v v
         else
           Loc.failk literal_at_want loc
-            "the float literal %g cannot stand where $%s is wanted: %s may be \
-             instantiated at an integer type, and a float literal is never \
-             usable where an integer is wanted. Write the constant as an \
-             integer literal — that one is admitted under {:where (numeric? \
-             $%s)} at every numeric type — or take the value as a parameter"
+            "the float literal %g cannot stand where $%s is wanted — %s may \
+             be instantiated at an integer type. Write an integer literal, \
+             which is admitted at every numeric type, or take the value as a \
+             parameter"
             x v
             (if declares ctx.env.tvpreds v "numeric?" then
                Printf.sprintf "{:where (numeric? $%s)} admits integers too, so $%s" v v
              else Printf.sprintf "$%s" v)
-            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
@@ -3101,8 +3057,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
        has gone. Rejected rather than left to corrupt it, the same rule as
        defer inside a block. *)
     fail loc
-      "return is not allowed inside %s yet — the frames it established are \
-       popped on the way out and an early exit would leave them on the stack"
+      "return is not allowed inside %s yet"
       (match ctx.in_frames with Some n -> n | None -> assert false)
 
   | Ast.Return v ->
@@ -3226,25 +3181,22 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     let name =
       match c.Tast.ty with
       | Types.Named n -> n
-      (* Its own arm ahead of the general one, because "a condition is a
-         struct, not dyn" would read as a rule about shape when the answer is a
-         milestone. A condition crosses a handler boundary as a pointer to a
-         frame that is still alive, and a dyn payload has to stay rooted across
-         that transfer — which is the collector's question, not this one's, and
-         it is milestone 2's. *)
+      (* Its own arm ahead of the general one. "A condition is a struct, not
+         dyn" is true and useless here: a dyn holding a condition struct is
+         one edit away from working, and the edit is naming the struct type.
+         Since the descriptors landed, the fields inside it may be dyn — which
+         is the half of the answer the general sentence would have hidden. *)
       | Types.Dyn ->
         fail c.Tast.loc
           "a condition is matched by its type and dyn is not one — write the \
            condition's struct type, whose dyn fields are fine"
       | t ->
         fail c.Tast.loc
-          "a condition is a struct, not %s — matching is by type and there is \
-           no condition hierarchy"
-          (Types.to_string t)
+          "a condition is a struct, not %s" (Types.to_string t)
     in
-    (* A condition that *holds* a dyn used to be refused here for the same
-       reason. It is not any more: the condition crosses as a pointer to a
-       value in the signalling frame, and that value is on the collector's
+    (* 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
+       collector's
        root stack with its type's descriptor beside it — which is exactly the
        shape the transfer needed and could not have. Where the condition is
        not a place, the backends evaluate it into a rooted slot rather than a
@@ -3275,10 +3227,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
        check that these arguments are the ones the clause takes (§3). *)
     if ctx.in_defer then
       fail loc
-        "invoke-restart is not allowed inside a defer — a defer is the cleanup \
-         a transfer runs on its way out, so starting one there would leave \
-         this function's defers half run with two targets and no way to \
-         choose";
+        "invoke-restart is not allowed inside a defer";
     let args = map_lr (fun a -> check ctx a) args in
     List.iter
       (fun (a : Tast.expr) ->
@@ -3321,11 +3270,9 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
        construct it was written in, so it is refused, and named. *)
     if not defer_ok then
       fail loc
-        "defer is not allowed inside %s — a defer is copied into every exit \
-         path of the function, so it always registers and always runs at \
-         function exit. Write it at the top level of the function body, or in \
-         a let that is (a let has the function's extent, because nothing is \
-         released at scope exit)"
+        "defer is not allowed inside %s — a defer always runs at function \
+         exit. Write it at the top level of the function body, or in a let \
+         that is itself at the top level"
         ctx.defer_block;
     register_defer ctx loc forms
 
@@ -3372,10 +3319,9 @@ and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n =
      mismatch the programmer cannot act on. *)
   | Some (Types.Var v) ->
     Loc.failk literal_at_want loc
-      "the integer literal %Ld cannot stand where $%s is wanted: an \
-       unconstrained type variable may be instantiated at a type that holds \
-       no number. Declare the bound — {:where (numeric? $%s)} — and the \
-       literal is admitted at every type $%s can then be"
+      "the integer literal %Ld cannot stand where $%s is wanted — nothing \
+       declares $%s numeric. Write {:where (numeric? $%s)} at the head of \
+       the body"
       n v v v
   | Some other when other <> Types.Never ->
     Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
@@ -3498,8 +3444,8 @@ and var ctx ?(qualified = false) loc ~want name =
                (Tast.MakeCase (dname, c.Tast.vname, [])))
         | Some (dname, c) ->
           fail loc
-            "%s is a case of the data type %s, and a data type value names both — \
-             write %s.%s" name dname dname c.Tast.vname
+            "%s is a case of the data type %s — write %s.%s"
+            name dname dname c.Tast.vname
         | None ->
           (* A bare function name *is* the function. This is a Lisp-1 — one
              top-level namespace, enforced, so a defn and a defonce cannot share
@@ -3516,9 +3462,7 @@ and var ctx ?(qualified = false) loc ~want name =
              if Hashtbl.mem ctx.env.externs name then
                fail loc
                  "%s is a foreign function, and its address is not a Flan \
-                  function value: a Flan function's signature ends with the \
-                  transfer channel and a C one does not. Wrap it in a defn \
-                  and pass that" name;
+                  function value. Wrap it in a defn and pass that" name;
              expect ctx loc ~want
                (mk loc (Types.Fn (params, ret)) (Tast.FnAddr (Tast.Fnval name)))
            | None -> captured ctx loc name; unknown_name ctx loc name)
@@ -3609,9 +3553,8 @@ and check_fn ctx ~want ?gen loc (params : string list) body =
       | _ ->
         fail loc
           "nothing here says what this fn's parameters are — an fn takes its \
-           types from the position it is written in, so it goes in an argument \
-           whose parameter is a (Fn [T ...] R), and a name already written as \
-           a defn goes anywhere"
+           types from the position it is written in. Write it as an argument \
+           whose parameter is a (Fn [T ...] R)"
   in
   (* Its own frame and its own empty scope, with [outer] kept only so that a
      reference to the enclosing function's locals is refused for the reason it
@@ -4128,9 +4071,8 @@ and loop_target ctx loc verb label =
          fail loc "%s is only allowed inside a loop" verb
        | Some l ->
          fail loc
-           "no loop named :%s encloses this %s. A label names one of the loops \
-            this form is written inside — it is not a goto, so it cannot name a \
-            loop somewhere else" l verb)
+           "no loop named :%s encloses this %s — a label names one of the \
+            loops this form is written inside" l verb)
     | Lloop name :: rest ->
       (match label with
        | None -> depth
@@ -4144,15 +4086,13 @@ and loop_target ctx loc verb label =
       (match label with
        | None ->
          fail loc
-           "%s is not allowed here: the nearest loop is a (loop ...), which \
-            answers with the value of its body, so leaving it this way would \
-            have no value to give. Answer with the value, or use a while"
+           "%s cannot leave a (loop ...), and that is the nearest loop. \
+            Answer with the value, or use a while"
            verb
        | Some l ->
          fail loc
-           "%s :%s would leave a (loop ...), which it may not: a loop answers \
-            with the value of its body and a jump out of one has no value to \
-            give" verb l)
+           "%s :%s would leave a (loop ...), and it may not. Answer with the \
+            value, or use a while" verb l)
     | Lbarrier what :: rest ->
       (* Crossing it would skip whatever the construct does on the way out —
          the handler or restart frames it pushed, or, for a defer, would jump
@@ -4163,16 +4103,13 @@ and loop_target ctx loc verb label =
       (match label with
        | None ->
          fail loc
-           "%s is not allowed here: the nearest loop is outside %s, and leaving \
-            it that way would skip what %s does on the way out. Write the loop \
-            inside it, or leave with a value and test that after"
+           "%s cannot leave %s, and the nearest loop is outside it. Write the \
+            loop inside %s, or leave with a value and test that after"
            verb what what
        | Some l ->
          fail loc
-           "%s :%s would leave %s, which it may not: whatever %s does on the way \
-            out would be skipped. A break may only leave loops that are inside \
-            the same %s it is"
-           verb l what what what)
+           "%s :%s would leave %s, and it may not. Name a loop inside %s"
+           verb l what what)
   in
   go 0 ctx.loops
 
@@ -4219,9 +4156,8 @@ and check_dotimes ctx ~want loc label name (b : Ast.bounds) body =
   (match literal, step with
    | Some 0L, Some s ->
      fail s.Tast.loc
-       "a step of 0 never moves the counter, so this loop would never end. \
-        Give it a step that moves, as in (dotimes [i 0 10 2] (print i)). \
-        Left out, the step is 1"
+       "a step of 0 never moves the counter. Give it a step that moves, as \
+        in (dotimes [i 0 10 2] ...); left out, the step is 1"
    | _ -> ());
   scoped ctx (fun () ->
     let i = bind ctx name index_ty ~assignable:false in
@@ -4366,10 +4302,8 @@ and recur_target ctx loc =
   let rec go depth = function
     | [] ->
       fail loc
-        "recur is only allowed inside a (loop ...). There are no tail calls in \
-         this compiler, so a function cannot recur into itself and two \
-         functions cannot recur into each other — write the repetition as a \
-         loop with a recur in its tail"
+        "recur is only allowed inside a (loop ...) — write the repetition as \
+         a loop with a recur in its tail"
     | Lrecur names :: _ -> (depth, names)
     (* Unreachable while the tail rule holds — a loop body is not a tail
        position, so no [recur] is ever written inside one — but the depth is
@@ -4377,9 +4311,7 @@ and recur_target ctx loc =
     | Lloop _ :: rest -> go (depth + 1) rest
     | Lbarrier what :: _ ->
       fail loc
-        "recur would leave %s, which it may not: whatever %s does on the way \
-         out would be skipped. Write the loop inside it, or leave with a value \
-         and test that after"
+        "recur would leave %s, and it may not. Write the loop inside %s"
         what what
   in
   go 0 ctx.loops
@@ -4393,8 +4325,7 @@ and check_recur ctx ~tail loc args =
     fail loc
       "recur must be in the tail position of its loop — the last thing the \
        body does, or the last thing in an if, match or let arm that is itself \
-       in the tail. Here something would still have to run afterwards, and a \
-       recur is a jump back to the top, not a call that returns";
+       in the tail. Something here would still run afterwards";
   let want = List.length names and got = List.length args in
   if want <> got then
     fail loc "this loop binds %d name%s and this recur passes %d" want
@@ -4588,9 +4519,8 @@ and check_if ctx ?(tail = false) ?want loc c t e =
         when want = None && and_sentinel e
              && String.equal d.Loc.kind "check/type-mismatch" ->
         Loc.failk "check/shortcircuit-operand" t.Tast.loc
-          "an and answers false when it stops early and its last operand \
-           otherwise, so the two have to be one type — this operand is %s, \
-           and false is a bool"
+          "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)
     in
     let ty =
@@ -4756,14 +4686,14 @@ and check_struct ctx ~want loc name kvs =
         misspelling. It can now, so it says what was meant. *)
      | Some (dname, c) ->
        fail loc
-         "%s is a case of the data type %s, not a struct — a data type value names \
-          both, as (%s.%s {.field value ...})"
+         "%s is a case of the data type %s, not a struct — write (%s.%s \
+          {.field value ...})"
          name dname dname c.Tast.vname
      | None ->
        if Hashtbl.mem ctx.env.datas name then
          fail loc
-           "%s is a data type, and a data type value names the case as well as the \
-            type — write (%s.%s {.field value ...}) for one of %s"
+           "%s is a data type, so a value of it names a case — write (%s.%s \
+            {.field value ...}), for one of %s"
            name name (first_case_name ctx.env name) (case_list ctx.env name)
        (* [is_struct_map] (parse.ml) has two blind spots, not one: [(name
           {})] reads as a struct literal with no fields regardless of what
@@ -4856,9 +4786,8 @@ and check_union ctx ~want loc name kvs =
   (match kvs with
    | (a, _) :: (b, (second : Ast.expr)) :: _ ->
      Loc.failk "check/union-two-members" second.Ast.loc
-       "%s is a union, so %s and %s are the same bytes and only one of them \
-        can be written — give the one this value is, and read the other \
-        member when you want to see those bytes that way"
+       "%s is a union, so only one member can be written — give %s or %s, not \
+        both"
        name a b
    | _ -> ());
   match kvs with
@@ -5170,9 +5099,8 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
        milestone answer below, because the milestone is not the reason. *)
     | Types.Enum n ->
       fail loc
-        "match over the enum %s is not implemented — the lowering is a chain \
-         of (= k :member), but a keyword has no case in the pattern type yet. \
-         Use cond" n
+        "match over the enum %s is not implemented — use cond with \
+         (= k :member)" n
     (* An untagged union has nothing for the arms to be alternatives over.
        This is not a milestone and not a missing lowering: [match] reads a tag
        and decides, and the absence of a tag is the whole definition of this
@@ -5180,11 +5108,9 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
        apart in the source and someone will write it. *)
     | Types.Named n when Hashtbl.mem ctx.env.unions n ->
       fail loc
-        "%s is a union, and there is nothing in one to match on: its members \
-         overlay the same bytes and nothing records which was written. Read \
-         the member you mean with (.member u), or keep a tag of your own \
-         beside it in a struct and match on that. A tagged alternative is \
-         what defdata is" n
+        "%s is a union, and nothing in one records which member was written, \
+         so there is nothing to match on. Read the member you mean with \
+         (.member u), or use a defdata" n
     | other ->
       fail loc "match works on an Option or a data type, not on %s"
         (Types.to_string other)
@@ -5483,9 +5409,8 @@ and struct_target ctx (target : Ast.expr) : Tast.expr * string =
   | (Types.Named n | Types.Ptr (Types.Named n))
     when Hashtbl.mem ctx.env.datas n ->
     fail target.Ast.loc
-      "%s is a data type, and a data type's fields belong to a case — which \
-       one it is holding is what the tag says, so they are reached by (match ...), \
-       whose arms bind the fields of the case they matched"
+      "%s is a data type, and its fields belong to a case — reach them with \
+       (match ...), whose arms bind the fields of the case they matched"
       n
   | other ->
     (* The pattern bound this, and it looks like a destructuring that did not
@@ -5519,9 +5444,8 @@ and struct_target ctx (target : Ast.expr) : Tast.expr * string =
 and refuse_string_place loc (ty : Types.t) =
   if Types.equal ty Types.String then
     fail loc
-      "a string is a read-only view of bytes it does not own, so (at s i) is \
-       a value and not a place — there is nothing to assign into or take the \
-       address of. Copy the bytes into a buffer you own and use that"
+      "a string is read-only, so (at s i) is a value and not a place. Copy \
+       the bytes into a buffer you own and write that"
 
 and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
   match p with
@@ -5530,8 +5454,8 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
      | Some b ->
        if not b.assignable then
          fail loc
-           "%s is a parameter, and a parameter is not a place you can assign \
-            to — bind a local with let" name;
+           "%s is a parameter, and a parameter is not assignable — bind a \
+            local with let" name;
        Tast.Plocal b.slot, b.bty
      | None ->
        match Hashtbl.find_opt ctx.env.globals name with
@@ -5547,9 +5471,8 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
            | None -> []
          in
          Loc.failk "check/set-constant" loc ~notes
-           "%s is a constant, and a constant is not assignable — it is written \
-            into the image and there is nothing to assign to. Declare it with \
-            defonce if it has to change" name
+           "%s is a constant, and a constant is not assignable. Declare it \
+            with defonce if it has to change" name
        | Some (ty, false) -> Tast.Pglobal name, ty
        | None -> captured ctx loc name; unknown_name ~setting:true ctx loc name)
   | Ast.Pfield (target, name) ->
@@ -5619,9 +5542,8 @@ and index_expr ctx (e : Ast.expr) =
              Tast.e = Tast.Prim (Tast.Cast index_ty, [ v ]) }
   | Types.Int k ->
     fail e.Ast.loc
-      "an index is an i32, and %s is wider — write (i32 …), because a value \
-       that does not fit truncates to one that does and would read the wrong \
-       element without tripping the bounds check" (Types.ikind_name k)
+      "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)
 
@@ -5723,7 +5645,7 @@ and fold_arity loc name args =
   | [ _ ] when String.equal name "-" ->
     fail loc
       "- takes two arguments or more, given 1 — there is no unary minus; \
-       write (- 0 x) to negate, which is what the prelude does"
+       write (- 0 x) to negate"
   | [ _ ] when String.equal name "/" ->
     fail loc
       "/ takes two arguments or more, given 1 — there is no reciprocal; \
@@ -6212,8 +6134,7 @@ and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
       [ target; i; size_of loc elem; here loc ], elem
   | _ ->
     fail loc
-      "a Vec takes exactly one index — (at v i) — and its element is indexed \
-       separately"
+      "a Vec takes exactly one index, as (at v i)"
 
 (* [(slice v)], [(slice v lo)] and [(slice v lo hi)] over a Vec — the arm for
    it is in [slice], and this is the half that differs from an array's.
@@ -6720,9 +6641,9 @@ and named_call ?(qualified = false) ctx ~want loc name args =
            trade this language does not make. *)
         | Types.Slice _ ->
           fail loc
-            "a pattern cannot destructure %s: a slice's length is a runtime \
-             value, so nothing here can check that it has %Ld element%s. Use \
-             (at s i) and test (len s) yourself"
+            "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 (at s i) and test (len s) yourself"
             (Types.to_string target.Tast.ty) n (plural n)
         | other ->
           fail loc
@@ -6745,17 +6666,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      symbols the emitter names, and no Flan type mentions them. *)
   | "make-allocator" | "allocator-from" | "allocator" ->
     fail loc
-      "a user-written allocator is not implemented yet, and a defn's name in \
-       value position — which is what this used to wait for — is no longer \
-       what is missing. Two things are. The runtime calls an allocator as \
-       proc(a, mode, p, old, size, align): six C arguments and no transfer \
-       channel, and every Flan function value's signature ends with one, so \
-       the pointer would be called with the wrong shape (the same mismatch a \
-       foreign function's address is refused for). And Allocator is opaque \
-       and pointer-width, so there is nowhere for a program to put the \
-       flan_allocator the pointer would have to point at. Use \
-       (arena-new ...) with a backing buffer, which is the parameterised \
-       allocator that does exist"
+      "a user-written allocator is not implemented yet — use (arena-new ...) \
+       with a backing buffer"
   | "heap-allocator" ->
     arity ctx loc name 0 args;
     expect ctx loc ~want
@@ -6908,9 +6820,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     if elem = Types.Dyn then begin
       if args <> [] then
         fail loc
-          "(vec-new dyn) takes no allocator — the dyn container's storage is \
-           the dyn runtime's, which is what lets the collector find the values \
-           inside it";
+          "(vec-new dyn) takes no allocator — its storage is the dyn \
+           runtime's";
       expect ctx loc ~want (rt loc Types.Dyn "flan_dyn_vec_new" [])
     end else begin
     let a = allocator_arg ctx loc args in
@@ -7046,12 +6957,9 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | (Types.Vec _ | Types.Map _)
        when region_only ctx.env target.Tast.ty ->
        fail loc
-         "%s holds elements that own storage, and free releases the block \
-          those elements sit in — not the blocks they point at, which nothing \
-          type-erased can reach. This container was built against a region \
-          allocator, because the guard at its construction admits no other, so \
-          release the region: (free-all a) takes it and everything its \
-          elements own, in one operation and with no per-element teardown"
+         "%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)
      | Types.Vec elem ->
        expect ctx loc ~want
@@ -7065,8 +6973,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        (* A field is never freed on its own: it would leave its owner partly
           dead with no way to say so. *)
        fail loc
-         "free takes an owning container — a Vec or a Map — found %s. A \
-          resource type with a drop hook is step 5 and does not exist yet"
+         "free takes an owning container — a Vec or a Map — found %s"
          (Types.to_string other))
   (* (clone v) uses the current allocator, (clone v a) names one. A deep,
      independent copy: spec-memory.md's "copying is always explicit". *)
@@ -7102,13 +7009,9 @@ and named_call ?(qualified = false) ctx ~want loc name args =
            where the promise is made. *)
         | (Types.Vec _ | Types.Map _) when region_only ctx.env target.Tast.ty ->
           fail loc
-            "%s cannot be cloned: clone is a deep, independent copy, and the \
-             type-erased runtime copies slots bytewise — so the copy's \
-             elements would still point at the original's blocks, which is an \
-             alias under a name that promises the opposite. Nothing here can \
-             walk an element to copy what it owns. Build a second container \
-             and insert into it, or keep the one you have — a region makes \
-             sharing safe, not copying"
+            "%s cannot be cloned — its elements own storage, and nothing here \
+             can walk one to copy what it owns. Build a second container and \
+             insert into it"
             (Types.to_string target.Tast.ty)
         (* A map's clone reinserts rather than copying the block, because the
            seed is derived from the block's address — see flan_rt.c. That is
@@ -7458,8 +7361,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
         | [ _; { Ast.e = Ast.Var "string"; _ } ] | [ _ ] -> ()
         | [ _; t ] ->
           fail t.Ast.loc
-            "embed's second argument is the type to read the file as, and \
-             `string` is the only one — (embed \"p\") is the [u8]"
+            "embed's second argument is string, or nothing for a [u8]"
         | _ -> ());
        let data = read_embed_file (embed_path loc p) p.Ast.loc in
        let as_string () = mk loc Types.String (Tast.Str data) in
@@ -7518,18 +7420,14 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      | Ast.Str s -> fail loc "%s" s
      | _ ->
        fail (List.hd args).Ast.loc
-         "compile-error takes a literal string — it is reported while the \
-          program is being checked, so there is nothing here to build one \
-          from. A macro that has to refuse builds the sentence as it expands \
-          and puts it in the form")
+         "compile-error takes a literal string")
   | "embed-dir" ->
     arity ctx loc name 1 args;
     let arg = List.hd args in
     let entries = read_embed_dir (embed_path loc arg) arg.Ast.loc in
     if not (Hashtbl.mem ctx.env.structs "EmbedFile") then
       fail loc
-        "embed-dir answers a [n EmbedFile] and EmbedFile is not in scope — it \
-         is a prelude type and something has replaced the prelude";
+        "embed-dir answers a [n EmbedFile], and EmbedFile is not in scope";
     let ety = Types.Named "EmbedFile" in
     let elems =
       List.map
@@ -7749,8 +7647,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
                (rt loc Types.Dyn "flan_dyn_at" [ target; check ctx ~want:Types.Dyn i ])
            | _ ->
              fail loc
-               "(at ...) over a dyn takes one index — the compiler cannot see \
-                the shape of a dyn container, so write (at (at x i) j)")
+               "(at ...) over a dyn takes one index — write (at (at x i) j)")
         | _ ->
           let idx, ty = indexed ctx target idx in
           prim Tast.At ty (target :: idx))
@@ -7808,9 +7705,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        (match ty, target.Tast.e with
         | Types.Array _, (Tast.Call _ | Tast.CallPtr _) ->
           fail loc
-            "this slices an array a call returned, and a returned array is a \
-             temporary — the slice would outlive it and view storage the \
-             frame has reused. Bind it first: (let [a (…)] (slice a …))"
+            "this slices an array a call returned, which is a temporary the \
+             slice would outlive. Bind it first: (let [a (…)] (slice a …))"
         | _ -> ());
        let int k = mk loc index_ty (Tast.Int (k, Types.I32)) in
        (* [hi] is wanted twice only when it is the implicit length of
@@ -7906,8 +7802,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
          | other ->
            fail loc
              "slice-from-ptr takes a (Ptr T) and the number of elements behind \
-              it, found %s. It is for a pointer that came back from C, whose \
-              length only the caller knows"
+              it, found %s"
              (Types.to_string other)
        in
        let n_loc = n.Ast.loc in
@@ -7917,9 +7812,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        (match literal n with
         | Some k when k < 0L ->
           fail n_loc
-            "slice-from-ptr length %Ld is negative — the length is what the \
-             caller promises the pointer addresses, and no pointer addresses \
-             fewer than zero elements" k
+            "slice-from-ptr length %Ld is negative" k
         | _ -> ());
        prim Tast.SliceFromPtr (Types.Slice elem) [ target; n ]
      | _ -> assert false)
@@ -7970,9 +7863,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
       else if is_nil_lit a then
         Loc.failk "check/some-nil" loc
           "(Some nil) cannot be built — Some marks a value present, and nil \
-           is dyn's own absence, so a present nil would make nil and None \
-           the same case of an (Option dyn), which nil <-> None at the \
-           boundary depends on staying apart. Use None instead"
+           is dyn's absence. Use None instead"
       else rt loc Types.Dyn "flan_dyn_need_not_nil" [ a ]
     in
     expect ctx loc ~want (mk loc (Types.Option a.Tast.ty) (Tast.Some_ a))
@@ -8431,7 +8322,7 @@ and ordinary_call ctx ~want loc name args =
     | None ->
       if Hashtbl.mem ctx.env.datas name then
         fail loc
-          "%s is a data type — a data type value names the case too, as \
+          "%s is a data type, so a value of it names a case — write \
            (%s.%s {.field value ...})"
           name name (first_case_name ctx.env name)
       else if Hashtbl.mem ctx.env.cases name then
@@ -8519,10 +8410,9 @@ and ordinary_call ctx ~want loc name args =
                same thing here so the answer does not depend on which side of
                the fork the form fell down. *)
             Loc.failk "check/unknown-function" loc
-              "unknown function %s. A capitalised name is a type, and a type \
-               given type arguments — (%s ...) — is a generic type, which is \
-               not there yet. A generic *function* is: it is written with \
-               [$t] in its parameter vector and copied per call site"
+              "unknown function %s. A capitalised name is a type, and (%s \
+               ...) is a generic type, which is not there yet — a generic \
+               function is, written with $t in its parameter vector"
               name name
           else Loc.failk "check/unknown-function" loc "unknown function %s" name
 
@@ -8735,9 +8625,7 @@ and generic_call ctx ~want loc name vars pats pret args =
     (fun v ->
        if not (List.mem_assoc v !subst) then
          fail loc
-           "%s's type variable $%s is not determined by any argument — a \
-            generic function is instantiated from its call site, and there is \
-            no syntax for naming the type" name v)
+           "%s's type variable $%s is not determined by any argument" name v)
     vars;
   (* The pairs that met no join, re-asked now that every argument has spoken.
      A later, wider argument dissolves one — u32 and i32 both widen into an
@@ -8751,11 +8639,9 @@ and generic_call ctx ~want loc name vars pats pret args =
        in
        if not (fits t1 && fits t2) then
          Loc.failk "check/tyvar-no-join" ploc
-           "this call binds %s's $%s to both %s and %s, and the two meet at \
-            no type: implicit widening only ever widens — every value kept, \
-            no sign lost — and neither of these holds every value of the \
-            other. Write the conversion you mean at one of the arguments, or \
-            pass them at one type"
+           "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))
     !pending;
   (* The binding is final; the arguments it out-widened catch up. Only a bare
@@ -8813,12 +8699,8 @@ and generic_call ctx ~want loc name vars pats pret args =
        if reaches_dyn t && not (clause_on v) then
          Loc.failk "check/tyvar-at-dyn" loc
            "this call would instantiate %s at $%s = %s, and a type variable \
-            is not instantiated at dyn: a copy is made per *written* type, \
-            and dyn is the one type whose own type is not known until it \
-            runs. One value, two models — a defgeneric with a defmethod per \
-            class dispatches on what the value turns out to be, which is the \
-            question a dyn argument is asking. Write the type the value has, \
-            or reach for the dyn side"
+            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))
     !subst;
   let cparams = List.map (subst_ty !subst) pats in
@@ -8850,9 +8732,7 @@ and generic_call ctx ~want loc name vars pats pret args =
               Loc.failk "check/predicate-not-carried" loc
                 "%s is written {:where (%s $%s)}, and this call passes the \
                  type variable %s, which nothing here declares %s. Add \
-                 {:where (%s $%s)} to this function's own clause — a \
-                 predicate a body relies on has to be carried by every \
-                 signature between it and the call site"
+                 {:where (%s $%s)} to this function's own clause"
                 name p.Ast.pname p.Ast.pvar v p.Ast.pname p.Ast.pname v
             | Some t when not (generic_ty t) && not (pred_holds p.Ast.pname t) ->
               Loc.failk "check/predicate-unsatisfied" loc
@@ -8907,18 +8787,15 @@ and instantiate env loc gname vars subst cparams cret =
          | Some t ->
            if not (pred_holds p.Ast.pname t) then
              Loc.failk "check/predicate-unsatisfied" loc
-               "this call instantiates %s at $%s = %s, and %s does not \
-                answer %s — which %s requires, being written {:where (%s \
-                $%s)}. The requirement is the signature's, so the refusal is \
-                here, at the call that asked for the type: pass one the \
-                predicate admits"
+               "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)
                p.Ast.pname gname p.Ast.pname p.Ast.pvar)
       fn.Ast.fwhere;
     if Hashtbl.mem env.fns sym then
       fail loc
         "%s at these types is called %s, and %s is already defined — rename \
-         one of them" gname sym sym;
+         one" gname sym sym;
     runaway env loc gname cparams;
     (* The entry goes in *before* the body is checked, which is what makes a
        recursive generic function terminate: the call to itself at the same
@@ -9495,8 +9372,8 @@ let builtins : (string * string * string) list =
     ("false", "false bool", "The false boolean literal.");
     ("nil", "nil dyn",
      "The absent dyn value: what (get m k) answers for a key a dyn map does \
-      not hold, and always dyn — what a nil does at an (Option T) boundary \
-      is a later milestone's question.");
+      not hold. It becomes None where an (Option T) is wanted, and stays dyn \
+      everywhere else.");
     ("None", "None (Option T)",
      "The absent Option. It takes its type from its context — a return type \
       or an annotated binding — because nothing about the word says what it \
@@ -9801,10 +9678,8 @@ let collect env (decls : Ast.decl list) =
               Refused by name rather than let through as an integer. *)
            | Types.Dyn ->
              fail loc
-               "%s of %s is dyn, which does not cross to C. A dyn is one word \
-                and would pass as an integer, but what the word means is the \
-                dyn runtime's and there is nothing on the C side that can ask \
-                — take the value at a written type and pass that"
+               "%s of %s is dyn, which does not cross to C — take the value \
+                at a written type and pass that"
                what fn.Ast.name
            | _ ->
              fail loc
@@ -9864,8 +9739,8 @@ let collect env (decls : Ast.decl list) =
             layout with a tag and no case for the tag to name. *)
          if vs = [] then
            fail loc
-             "%s declares no cases, so no value of it can exist — a data type is \
-              (defdata %s [(Case [field Type ...]) ...])" n n;
+             "%s declares no cases — a data type is (defdata %s [(Case [field \
+              Type ...]) ...])" n n;
          let cnames = List.map (fun (v : Ast.variant) -> v.Ast.vname) vs in
          if List.length (List.sort_uniq compare cnames) <> List.length cnames
          then fail loc "%s declares the same case twice" n;
@@ -9910,8 +9785,8 @@ let collect env (decls : Ast.decl list) =
           tag the program keeps beside the union, as C does. *)       | Ast.Defunion (n, ms) ->
          if ms = [] then
            fail loc
-             "%s declares no members, so it has no size and nothing could be \
-              read out of it — a union is (defunion %s [member Type ...])" n n;
+             "%s declares no members — a union is (defunion %s [member Type \
+              ...])" n n;
          let names = List.map (fun (f : Ast.field) -> f.Ast.fname) ms in
          if List.length (List.sort_uniq compare names) <> List.length names then
            fail loc "%s declares the same member twice" n;
@@ -9935,12 +9810,11 @@ let collect env (decls : Ast.decl list) =
                   p.Ast.pname (String.concat ", " predicate_names);
               if not (List.mem p.Ast.pvar vars) then
                 Loc.failk "check/unbound-predicate-variable" p.Ast.ploc
-                  "$%s is not a type variable of %s — a where clause \
-                   constrains the variables the signature binds%s"
+                  "$%s is not a type variable of %s%s"
                   p.Ast.pvar fn.Ast.name
-                  (if vars = [] then ", and this signature binds none"
+                  (if vars = [] then " — it binds none"
                    else
-                     ", which here are "
+                     " — it binds "
                      ^ String.concat ", " (List.map (fun v -> "$" ^ v) vars)))
            fn.Ast.fwhere;
          env.tyvars <- vars;
@@ -10074,10 +9948,8 @@ let check_union_members env =
     match t with
     | Types.Bool ->
       fail (Option.value (Hashtbl.find_opt env.locs uname) ~default:Loc.unknown)
-        "%s is a bool, and a union may not hold one at any depth: writing a \
-         member that overlays it leaves a byte that is neither 0 nor 1, and \
-         an i1 with that byte in it is a value the optimiser is entitled to \
-         assume cannot exist. Hold a u8 in the union and compare it yourself"
+        "%s is a bool, and a union may not hold one at any depth — hold a u8 \
+         in the union and compare it yourself"
         where
     (* An [Option] is deliberately not on this list, and the difference is
        worth stating because a reader will ask. Its [match] lowers to a test of
@@ -10088,13 +9960,8 @@ let check_union_members env =
     | Types.Array (_, e) | Types.Option e -> walk uname where e
     | Types.Named n when Hashtbl.mem env.datas n ->
       fail (Option.value (Hashtbl.find_opt env.locs uname) ~default:Loc.unknown)
-        "%s is %s, a data type, and a union may not hold one at any depth: a \
-         data type's tag steers every match over it, and overlaying another \
-         member leaves that tag arbitrary — a tag no case names falls past \
-         every comparison into a block the optimiser may treat as \
-         unreachable. This is the same refusal uninit on a data type gets, \
-         and it arrives here because a union is the other way to hand one \
-         bytes nobody wrote. Hold the %s beside the union"
+        "%s is %s, a data type, and a union may not hold one at any depth — \
+         hold the %s beside the union"
         where n n
     | Types.Named n ->
       (match Hashtbl.find_opt env.structs n with
@@ -10299,10 +10166,8 @@ let container_global_init loc n (ty : Types.t) (init : Ast.init) =
     match init with
     | Ast.Uninit ->
       fail loc
-        "the global %s is %s, and uninit on one is refused: its block pointer \
-         steers every read of it, and garbage there is not a garbage number \
-         the way it is for an f64. Write (defonce %s %s) with no initialiser — \
-         a zeroed %s is an empty one, and that is a value, not a placeholder"
+        "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)
     | _ -> ()
 
@@ -10315,10 +10180,9 @@ let container_global_init loc n (ty : Types.t) (init : Ast.init) =
 let no_container_defconst loc n (ty : Types.t) =
   if zero_only ty then
     fail loc
-      "the global %s is %s, and a %s global is a defonce and not a defconst: \
-       a constant is not an assignable place, so nothing could ever load \
-       this one — it would stay the empty %s it was declared as. Write \
-       (defonce %s %s) and fill it in a function"
+      "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)
 
@@ -10343,9 +10207,7 @@ let no_union_const env loc n (v : Tast.expr) =
   | Types.Named un, _ when Hashtbl.mem env.unions un ->
     fail loc
       "the constant %s is the union %s, and a union member cannot be written \
-       into a constant: a constant is what the linker writes into the image \
-       and storing a member is a store. Leave it zeroed, or make it a defonce \
-       and let its initialiser run at startup"
+       into a constant. Leave it zeroed, or make it a defonce"
       n un
   | _ -> ()
 
@@ -10397,11 +10259,8 @@ let const_defconst_init env loc n (v : Tast.expr) =
   | None -> ()
   | Some { Tast.e = Tast.MakeCase (dname, case, _); _ } ->
     fail loc
-      "a constant cannot be %s.%s — a data type's payload is a blob, and \
-       writing a case into one at link time needs a byte-level encoder that \
-       does not exist (a string field could not be encoded at all). Make it a \
-       defonce, whose initialiser runs at startup and stores the case, or \
-       declare it zeroed, which is %s.%s"
+      "a constant cannot be %s.%s. Make it a defonce, or declare it zeroed, \
+       which is %s.%s"
       dname case dname
       (match Hashtbl.find_opt env.datas dname with
        | Some { Tast.cases = c :: _; _ } -> c.Tast.vname
@@ -10469,11 +10328,8 @@ let no_transfer_in_init n (v : Tast.expr) =
        let bad what can =
          fail e.Tast.loc
            "%s in the initialiser of the global %s, with no handler-bind or \
-            restart-case around it: an initialiser runs at startup, before the \
-            program has a caller that could have established one, so this can \
-            only %s. Write one inside the initialiser — they run there like \
-            anywhere else — or move the whole thing into a function the \
-            program calls"
+            restart-case around it, can only %s. Write one inside the \
+            initialiser, or move the whole thing into a function"
            what n can
        in
        if List.memq e !covered then ()
@@ -10567,9 +10423,8 @@ let check_global env (d : Ast.decl) : Tast.global option =
         (match ty with
          | Types.Named un when Hashtbl.mem env.datas un ->
            fail d.Ast.dloc
-             "%s is a data type, and uninit on one is refused: its tag steers \
-              every match, and a tag no case names has no arm to reach. Drop \
-              the uninit — a zeroed %s is %s, which is a real case"
+             "%s is a data type, and uninit on one is refused. Drop the \
+              uninit — a zeroed %s is %s"
              (Types.to_string ty) un
              (match Hashtbl.find_opt env.datas un with
               | Some { Tast.cases = c :: _; _ } -> un ^ "." ^ c.Tast.vname
@@ -10762,9 +10617,8 @@ let init_order (globals : Tast.global list) (fns : Tast.fn list) =
       Reach.expr_refs note g.Tast.ginit;
       if List.mem g.Tast.gname !acc then
         fail g.Tast.ginit.Tast.loc
-          "the global %s is initialised from itself: its own value is what the \
-           initialiser is producing, so there is nothing there to read but the \
-           zero it starts as. Leave it zeroed and load it in a function"
+          "the global %s is initialised from itself — leave it zeroed and \
+           load it in a function"
           g.Tast.gname;
       !acc
     in
@@ -10821,9 +10675,8 @@ let init_order (globals : Tast.global list) (fns : Tast.fn list) =
            r
        in
        fail g.Tast.ginit.Tast.loc
-         "the globals %s initialise each other: %s. One of them has to start \
-          without the other — leave it zeroed and load it in a function that \
-          runs once, where the order is yours to write"
+         "the globals %s initialise each other: %s. Leave one zeroed and load \
+          it in a function"
          (String.concat " and " r) (String.concat ", " edges));
     (* The sorted sequence, dropped back into the slots the computed globals
        already occupied. Everything else — a constant, a zeroed container —
diff --git a/lib/cimport.ml b/lib/cimport.ml
index 8d8473e..6a7f1da 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -192,8 +192,7 @@ let run_clang ~loc ~header ~flags =
     with Unix.Unix_error _ ->
       List.iter Unix.close [ out_r; out_w; err_r; err_w ];
       fail loc
-        "clang is not on PATH, and reading a C header is done by running it \
-         (%s)"
+        "clang is not on PATH, and reading a C header runs it (%s)"
         (String.concat " " argv)
   in
   Unix.close out_w;
diff --git a/lib/dev.ml b/lib/dev.ml
index ab8f649..b2bad53 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -1515,7 +1515,7 @@ let layout t ~ty =
          `C-x C-e' with its case and that case's fields. *)
       error
         (ty
-         ^ " is a data type, not a struct; a data type is a tag and one payload per case, so it has no single field list for this op to answer with. Its value renders with its case and fields in a frame's locals and at C-x C-e")
+         ^ " is a data type, not a struct, so it has no one field list to answer with. Its value renders with its case and fields in a frame's locals and at C-x C-e")
     else
       let suffix = "/" ^ ty in
       let candidates =
@@ -1901,7 +1901,7 @@ let stopped_frame t ~frame ~what : (string * Tast.fn, string) result =
             if not mine then
               Error
                 (name
-                 ^ " is a frame of the expression this break is inside, not of the program; its thunk is not part of the session, so there is no record of what its slots are called")
+                 ^ " is a frame of the expression this break is inside, not of the program, so there is no record of what its slots are called")
             else
               match find_fn t name with
               | None ->
@@ -1917,7 +1917,7 @@ let stopped_frame t ~frame ~what : (string * Tast.fn, string) result =
                 if nslots <> Array.length fn.Tast.slots then
                   Error
                     (Printf.sprintf
-                       "%s on the stack has %d slots and the %s this session holds has %d: the frame is running a body that has been redefined since, so every slot index here would be a guess"
+                       "%s on the stack has %d slots and the %s this session holds has %d — the frame is running a body that has been redefined since"
                        name nslots name (Array.length fn.Tast.slots))
                 else if sig_ <> Emit.slot_fingerprint fn then
                   (* The count matching is not the same as the body matching.
@@ -1930,7 +1930,7 @@ let stopped_frame t ~frame ~what : (string * Tast.fn, string) result =
                      cannot be trusted are different facts. *)
                   Error
                     (Printf.sprintf
-                       "%s on the stack was compiled from a different body than the %s this session holds: this frame's body was redefined since it was entered, so its names no longer describe its values"
+                       "%s on the stack was compiled from a different body than the %s this session holds — it was redefined after this frame was entered, so its names no longer describe its values"
                        name name)
                 else Ok (name, fn)))
 
@@ -5086,10 +5086,9 @@ let start ?(debug = false) ?(merged = true) ?(x86 = true) ~file ~sock () =
      and it is still refused. *)
   if x86 && debug then
     failwith
-      "flan dev --x86 --debug: the dev backend emits DWARF for a whole program \
-       but not yet for a redefinition module, so a breakpoint set on a line \
-       would stop firing at the first C-c C-c. Drop --x86 and --debug will \
-       build this session with LLVM, which has both.";
+      "flan dev --x86 --debug: the dev backend emits no DWARF for a \
+       redefinition module, so a breakpoint would stop firing at the first \
+       C-c C-c. Drop --x86 to build this session with LLVM.";
   (* The merged daemon used to be refused here for [--x86] and no longer is,
      and what made the combination safe is worth stating where the refusal
      stood. A merged build is the program and the compiler in one process, and
diff --git a/lib/emit.ml b/lib/emit.ml
index 2f48dac..215cfb0 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -37,6 +37,19 @@
 
 let fail = Loc.fail
 
+(* The assertions below this line are not diagnostics. Every one of them says
+   the checker admitted something it refuses — a type with no layout, a case
+   that is not a case of its data type, arithmetic on a struct — so no program
+   text reaches one and there is no fix to name. They are still worded for a
+   reader, because the one way to see one is a compiler bug and the person who
+   sees it should be told that rather than left reading "no layout for t" as a
+   statement about their own code. [internal] is the whole of the treatment
+   they get: the prefix check.ml already uses, and the sentence that says who
+   the message is for. *)
+let internal fmt =
+  Printf.ksprintf
+    (fun m -> failwith ("internal: " ^ m ^ " — this is a compiler bug")) fmt
+
 (* [List.map]'s evaluation order is unspecified, and so is [let ... and ...].
    Emission is all side effect — instructions, calls, branches to a [ret] — so
    left-to-right is required, not a preference. Same rule as in Check. *)
@@ -163,13 +176,13 @@ module Rt = struct
   let field s n =
     match List.assoc_opt n (snd (layout s)) with
     | Some o -> o
-    | None -> failwith (Printf.sprintf "no field %s in %%%s" n s.sname)
+    | None -> internal "no field %s in %%%s" n s.sname
 
   (* The [getelementptr] index of a field, which is this backend's handle on
      it — LLVM counts fields where the assembler counts bytes. *)
   let index s n =
     let rec go i = function
-      | [] -> failwith (Printf.sprintf "no field %s in %%%s" n s.sname)
+      | [] -> internal "no field %s in %%%s" n s.sname
       | (f, _) :: rest -> if String.equal f n then i else go (i + 1) rest
     in
     go 0 s.fields
@@ -260,7 +273,7 @@ let rec ll (t : Types.t) =
   | Types.Dyn -> "i64"
   | Types.Var _ ->
     (* The checker rejects it by name — nothing reaches here. *)
-    failwith ("no layout for " ^ Types.to_string t)
+    internal "no layout for %s" (Types.to_string t)
 
 let is_void (t : Types.t) = match t with Types.Unit | Types.Never -> true | _ -> false
 
@@ -472,9 +485,9 @@ let rec lay m (t : Types.t) : int * int =
        | None ->
          match Hashtbl.find_opt m.unions n with
          | Some u -> union_lay m u
-         | None -> failwith ("no layout for struct " ^ n))
+         | None -> internal "no layout for struct %s" n)
   | Types.Dyn -> 8, 8
-  | Types.Var _ -> failwith ("no layout for " ^ Types.to_string t)
+  | Types.Var _ -> internal "no layout for %s" (Types.to_string t)
 
 (* Size, alignment, and the offset of every member. *)
 and lay_fields m tys =
@@ -527,7 +540,7 @@ and payload_lay m (u : Tast.data) : int * int =
 (* The integer kind of a given width, for the payload blob's element type. *)
 and int_kind = function
   | 8 -> Types.I8 | 16 -> Types.I16 | 32 -> Types.I32 | 64 -> Types.I64
-  | n -> failwith ("no integer type of " ^ string_of_int n ^ " bits")
+  | n -> internal "no integer type of %d bits" n
 
 (* ── Per-type dyn descriptors ────────────────────────────────────────
  *
@@ -774,7 +787,7 @@ let rec dty m d (t : Types.t) : int =
                     (String.concat ", "
                        (List.map (fun i -> Printf.sprintf "!%d" i) ms)));
                id
-             | None -> failwith ("no debug type for struct " ^ sn))
+             | None -> internal "no debug type for struct %s" sn)
       (* An opaque pointer under lldb, which is the truth: the allocator's
          fields are the runtime's C and lldb already has that type from
          flan_rt.c's own debug info. *)
@@ -820,7 +833,7 @@ let rec dty m d (t : Types.t) : int =
          runtime's own printer. *)
       | Types.Dyn -> basic "dyn" 64 "DW_ATE_unsigned"
       | Types.Var _ ->
-        failwith ("no debug type for " ^ Types.to_string t)
+        internal "no debug type for %s" (Types.to_string t)
     in
     Hashtbl.replace d.dtys key n;
     n
@@ -2006,7 +2019,7 @@ and field_addr f (target : Tast.expr) i =
   let sty = match target.Tast.ty with
     | Types.Named n -> sname n
     | Types.Option _ as t -> ll t
-    | t -> failwith ("field of " ^ Types.to_string t)
+    | t -> internal "field of %s" (Types.to_string t)
   in
   let p = fresh f in
   ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d" p sty base i;
@@ -2044,7 +2057,7 @@ and element_addr f (target : Tast.expr) idx =
          let p = fresh f in
          ins f "%s = getelementptr inbounds %s, ptr %s, i64 %s" p (ll elem) base i64;
          go p elem rest
-       | t -> failwith ("index into " ^ Types.to_string t))
+       | t -> internal "index into %s" (Types.to_string t))
   in
   go (addr f target) target.Tast.ty idx
 
@@ -2054,13 +2067,13 @@ and place f (p : Tast.place) : string * Types.t =
   | Tast.Pglobal n -> global_addr f n, Hashtbl.find f.md.globals n
   | Tast.Pfield (target, i) ->
     let sn = match target.Tast.ty with
-      | Types.Named n -> n | t -> failwith ("field of " ^ Types.to_string t)
+      | Types.Named n -> n | t -> internal "field of %s" (Types.to_string t)
     in
     field_addr f target i, field_ty f.md sn i
   | Tast.Pindex (target, idx) -> element_addr f target idx
   | Tast.Pderef target ->
     let t = match target.Tast.ty with
-      | Types.Ptr t -> t | t -> failwith ("deref of " ^ Types.to_string t)
+      | Types.Ptr t -> t | t -> internal "deref of %s" (Types.to_string t)
     in
     value f target, t
 
@@ -2077,7 +2090,7 @@ and emit_make_case f dname case fields =
   let u = Hashtbl.find f.md.datas dname in
   let tag = match Tast.case_index u case with
     | Some (i, _) -> i
-    | None -> failwith ("no case " ^ case ^ " of " ^ dname)
+    | None -> internal "no case %s of %s" case dname
   in
   let tmp = alloca f ty in
   ins f "store %s zeroinitializer, ptr %s" (ll ty) tmp;
@@ -2110,7 +2123,7 @@ and payload_addr f dname base =
 and case_field_addr f (target : Tast.expr) case i =
   let dname = match target.Tast.ty with
     | Types.Named n -> n
-    | t -> failwith ("case field of " ^ Types.to_string t)
+    | t -> internal "case field of %s" (Types.to_string t)
   in
   let base = addr f target in
   let pp = payload_addr f dname base in
@@ -2579,7 +2592,7 @@ and emit_match f ty scrut arms =
     match scrut.Tast.ty with
     | Types.Named n when Hashtbl.mem f.md.datas n -> Some n
     | Types.Option _ -> None
-    | t -> failwith ("match on " ^ Types.to_string t)
+    | t -> internal "match on %s" (Types.to_string t)
   in
   let tag, read_tag, bind_of =
     match dname with
@@ -2587,7 +2600,7 @@ and emit_match f ty scrut arms =
       let sv = value f scrut in
       let sty = ll scrut.Tast.ty in
       let payload_ty = match scrut.Tast.ty with
-        | Types.Option t -> t | t -> failwith ("match on " ^ Types.to_string t)
+        | Types.Option t -> t | t -> internal "match on %s" (Types.to_string t)
       in
       let tag = fresh f in
       ins f "%s = extractvalue %s %s, 0" tag sty sv;
@@ -2610,7 +2623,7 @@ and emit_match f ty scrut arms =
        (fun c ->
           match Tast.case_index u c with
           | Some (i, _) -> ("i32", i)
-          | None -> failwith ("no case " ^ c ^ " of " ^ n)),
+          | None -> internal "no case %s of %s" c n),
        fun case i slot ->
          let pp = payload_addr f n base in
          let fp = fresh f in
@@ -2619,7 +2632,7 @@ and emit_match f ty scrut arms =
          let fty =
            match Tast.case_index u case with
            | Some (_, c) -> (List.nth c.Tast.vfields i).Tast.fty
-           | None -> failwith ("no case " ^ case ^ " of " ^ n)
+           | None -> internal "no case %s of %s" case n
          in
          let v = load f fp fty in
          ins f "store %s %s, ptr %s" (ll fty) v f.slots.(slot);
@@ -2694,7 +2707,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
       | Types.Int _, Tast.Mul -> "mul"
       | Types.Int k, Tast.Div -> if Types.signed k then "sdiv" else "udiv"
       | Types.Int k, _ -> if Types.signed k then "srem" else "urem"
-      | t, _ -> failwith ("arithmetic on " ^ Types.to_string t)
+      | t, _ -> internal "arithmetic on %s" (Types.to_string t)
     in
     (* A divide or a remainder by zero, and the one division that overflows,
        signal ArithError. Integers only: IEEE says x / 0.0 is an infinity and
@@ -2735,7 +2748,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
         (runtime/flan_rt.c), bytewise with a length and a same-pointer fast
         path. [check.ml] only ever builds [Eq]/[Ne] here: [<] and friends are
         refused on a string before a Tast node exists (Types.is_comparable
-        says no), so the [failwith] below is unreachable except as a checker
+        says no), so the [internal] below is unreachable except as a checker
         bug, and stays as the same tripwire the Enum case above already is. *)
      | Types.String ->
        let ap = fresh f in
@@ -2751,10 +2764,10 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
          r ap al bp bl;
        let cc = match p with
          | Tast.Eq -> "ne" | Tast.Ne -> "eq"
-         | _ -> failwith ("comparison on " ^ Types.to_string x.Tast.ty)
+         | _ -> internal "comparison on %s" (Types.to_string x.Tast.ty)
        in
        ins f "%s = icmp %s i8 %s, 0" t cc r
-     | t' -> failwith ("comparison on " ^ Types.to_string t'));
+     | t' -> internal "comparison on %s" (Types.to_string t'));
     t
   | (Tast.BitAnd | Tast.BitOr | Tast.BitXor | Tast.Shl | Tast.Shr), [ x; y ] ->
     let a = value f x in
@@ -2763,7 +2776,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
       | _, Tast.BitAnd -> "and" | _, Tast.BitOr -> "or"
       | _, Tast.BitXor -> "xor" | _, Tast.Shl -> "shl"
       | Types.Int k, _ -> if Types.signed k then "ashr" else "lshr"
-      | t, _ -> failwith ("bitwise on " ^ Types.to_string t)
+      | t, _ -> internal "bitwise on %s" (Types.to_string t)
     in
     (* The count is masked to the operand's width. LLVM makes an over-wide
        shift poison, and a poison return at -O2 is a function that returns
@@ -2840,7 +2853,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
         let p = fresh f in
         ins f "%s = getelementptr inbounds i8, ptr %s, i64 %s" p q lo64;
         p
-      | t -> failwith ("slice of " ^ Types.to_string t)
+      | t -> internal "slice of %s" (Types.to_string t)
     in
     let d = fresh f in
     ins f "%s = sub i64 %s, %s" d hi64 lo64;
@@ -3010,7 +3023,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
   | Tast.AlignOf t, [] -> Printf.sprintf "%d" (snd (lay f.md t))
   | Tast.AddrOf, [ x ] -> addr_rooted f x
   | Tast.Cast target, [ x ] -> cast f ~guard:(fun () -> guard f) x target
-  | _ -> failwith "malformed primitive"
+  | _ -> internal "malformed primitive"
 
 (* A slice argument crosses to C as ptr+len, never as a struct by value. *)
 and explode f (x : Tast.expr) =
@@ -3096,7 +3109,7 @@ and cast f ~guard (x : Tast.expr) target =
          decided the value was a bool, so the discarded bits are zero. *)
       | Types.Bool, Types.Int _ -> "zext"
       | Types.Int _, Types.Bool -> "trunc"
-      | _ -> failwith "unsupported cast"
+      | _ -> internal "unsupported cast"
     in
     if op = "bitcast" then v
     else begin
@@ -3510,9 +3523,8 @@ let rec const m (e : Tast.expr) =
      diagnostic, and it fires only if that refusal and [Tast.const_init] stop
      agreeing about the same set. *)
   | _ ->
-    failwith
-      ("no constant image for " ^ Types.to_string e.Tast.ty ^ " at "
-       ^ Loc.to_string e.Tast.loc)
+    internal "no constant image for %s at %s"
+      (Types.to_string e.Tast.ty) (Loc.to_string e.Tast.loc)
 
 (* A dev build emits a [defconst] as a mutable [global]. Two things follow, and
    both are wanted: LLVM can no longer fold a read of it, and a redefinition
@@ -3845,9 +3857,9 @@ declare i64 @flan_dyn_map_get(i64, i64)
 declare void @flan_dyn_map_set(i64, i64, i64)
 declare i64 @flan_dyn_map_contains(i64, i64)
 ; The nine that trap carry the site as ptr+len, the way the bounds and
-; arithmetic traps in flan_rt.c do: a dyn type error IS the type error in a
-; dynamic program, and it used to print with no file and no line. [eq] never
-; traps, so it has nowhere to put one.
+; arithmetic traps do: a dyn type error IS the type error in a dynamic
+; program, and it used to print with no file and no line. [eq] never traps,
+; so it has nowhere to put one.
 declare i64 @flan_dyn_add(i64, i64, ptr, i64)
 declare i64 @flan_dyn_sub(i64, i64, ptr, i64)
 declare i64 @flan_dyn_mul(i64, i64, ptr, i64)
@@ -4363,11 +4375,9 @@ let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = [])
      that links, runs, and silently installs nothing. There is no such thing as
      a reloadable macro module, so nothing is lost by saying so out loud. *)
   if hidden && dev then
-    failwith
-      "Emit.program ~hidden ~dev: a dev build exports its cells so that a \
-       redefinition module can reach them, and hiding them would break every \
-       reload. [hidden] is the macro module's flag and a macro module is not a \
-       dev build.";
+    internal
+      "Emit.program was given ~hidden and ~dev together, and a dev build has \
+       to export its cells";
   let m = new_module ~checks ~dev ~known:(fun _ -> true) ~debug ~sanitize p in
   (* One cell per function, initialised to the function this build compiled.
      Nothing has been redefined yet, so a dev build starts out behaving exactly
@@ -4470,7 +4480,7 @@ let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = [])
     (fun n ->
        match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = n) p.Tast.fns with
        | Some fn -> macro_thunk m fn
-       | None -> failwith ("no such macro: " ^ n))
+       | None -> internal "no such macro %s" n)
     macros;
   finish m
 
@@ -4505,7 +4515,7 @@ let redefinition ?(checks = true) ?(dev = false) ?(debug = false)
   let target name =
     match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = name) p.Tast.fns with
     | Some f -> f
-    | None -> failwith (Printf.sprintf "no such function: %s" name)
+    | None -> internal "no such function %s" name
   in
   let targets = List.map target fns in
   (* A clause lifted out of one of these comes with it: its body may have
diff --git a/lib/expand.ml b/lib/expand.ml
index ddfe51b..15f74ef 100644
--- a/lib/expand.ml
+++ b/lib/expand.ml
@@ -192,9 +192,8 @@ let rec quote (f : Form.t) : Form.t =
       match f.Form.v with
       | Form.List ({ Form.v = Form.Sym "quasiquote"; _ } :: _) ->
         Loc.fail loc
-          "a quasiquote inside a quasiquote is not implemented: the reader does \
-           not count nesting levels and neither does this, so the inner one has \
-           no meaning to give. Build the inner form with form-cons"
+          "a quasiquote inside a quasiquote is not implemented — build the \
+           inner form with form-cons"
       | Form.Sym s -> node loc "Sym" "s" (Form.Str s)
       | Form.Kw s -> node loc "Kw" "s" (Form.Str s)
       | Form.Int i -> node loc "Int" "i" (Form.Int i)
diff --git a/lib/load.ml b/lib/load.ml
index c488e2d..0606298 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -1113,9 +1113,8 @@ let rec import ~seen ~open_ ~loc alias dir =
        List.map (fun (_, a) -> a) ring @ [ alias ]
      in
      fail loc
-       "%s imports itself round a ring: %s. Imports have to be acyclic — a \
-        definite package order is what lets a package be compiled before the \
-        ones that use it — so one of these imports has to go"
+       "%s imports itself round a ring: %s. Imports have to be acyclic, so \
+        one of these has to go"
        (snd (List.nth open_ i)) (String.concat " -> " names)
    | None -> ());
   match Hashtbl.find_opt seen dir' with
@@ -1130,8 +1129,8 @@ let rec import ~seen ~open_ ~loc alias dir =
     { decls = []; csrcs = []; lflags = []; pkgs = []; macros }
   | Some (previous, _) ->
     fail loc
-      "%s is imported as %s here and as %s elsewhere; one directory is one set \
-       of names, so the two cannot both be true" dir alias previous
+      "%s is imported as %s here and as %s elsewhere — one directory takes \
+       one alias" dir alias previous
   | None ->
     Hashtbl.replace seen dir' (alias, []);
     let open_ = open_ @ [ (dir', alias) ] in
diff --git a/lib/macro.ml b/lib/macro.ml
index 889895c..6d5a347 100644
--- a/lib/macro.ml
+++ b/lib/macro.ml
@@ -180,10 +180,8 @@ let reduce (forms : Form.t list) : Form.t list =
        match head_name f with
        | Some ("defmacro", n) when names_macro macros f ->
          Loc.fail f.Form.loc
-           "the prelude macro %s calls a macro, and a prelude macro may not: \
-            the module that expands it is compiled from the prelude, so the \
-            call would have to be expanded by a module that does not exist \
-            yet. Call a function instead"
+           "the prelude macro %s calls a macro, and a prelude macro may not. \
+            Call a function instead"
            n
        | _ -> ())
     forms;
@@ -412,8 +410,7 @@ and settle l first loc (f : Form.t) left =
     if left <= 0 then
       Loc.fail loc
         "expanding %s did not settle after %d rounds — a macro that expands \
-         into a call to a macro has to get smaller each time, and this one is \
-         not"
+         into a macro call has to get smaller each time"
         first fuel
     else begin
       let args = List.map (expand_form l) args in
@@ -450,10 +447,8 @@ let rounds ~(prelude : string list) (pending : (string * Form.t) list)
       in
       if now = [] then
         Loc.fail (snd (List.hd pending)).Form.loc
-          "these macros call each other and none can be compiled first: %s. A \
-           defmacro has to be compiled before the call it expands, so a ring \
-           has no order to be compiled in — one of them has to call a function \
-           instead"
+          "these macros call each other and none can be compiled first: %s. \
+           One of them has to call a function instead"
           (String.concat ", " waiting)
       else
         let taken = taken @ now in
diff --git a/lib/parse.ml b/lib/parse.ml
index 8dc6ad4..e1d5451 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -50,9 +50,8 @@ let no_pattern (f : Form.t) =
   match f.v with
   | Map _ | Vec _ ->
     fail f
-      "%s is a destructuring pattern, and a pattern binds only in let — this \
-       position takes a plain name. Take the value under a name and \
-       destructure it in the body"
+      "%s is a destructuring pattern, and this position takes a plain name. \
+       Take the value under a name and destructure it in the body"
       (Form.to_string f)
   | _ -> ()
 
@@ -96,8 +95,7 @@ let rec texpr (f : Form.t) : Ast.texpr =
      and with braces gone from type position there is nothing for it to be
      confused with. *)
   | Map _ ->
-    fail f "a map type is written (Map K V), not in braces — braces in type \
-            position are not a type" 
+    fail f "a map type is written (Map K V), not in braces"
   | List ({ v = Sym "Fn"; _ } :: rest) ->
     (match rest with
      | [ { v = Vec params; _ }; ret ] ->
@@ -163,10 +161,8 @@ and dyn_params which (items : Form.t list) : Ast.field list =
            floc = it.loc }
        | _ ->
          fail it
-           "a %s's parameter is a bare name, and found %s. Every parameter of \
-            a generic function is dyn — there is no type to write, and a \
-            method that wanted one could not be reached by a dispatch that \
-            does not know types either"
+           "a %s's parameter is a bare name, and found %s. Every parameter \
+            here is dyn, so there is no type to write"
            which (Form.to_string it))
     items
 
@@ -189,8 +185,7 @@ and dispatch (f : Form.t) : Ast.dispatch =
     fail f
       "a method's dispatch value is a class's name, a keyword, a string, an \
        integer, true, false, or :else for the one that answers when no other \
-       does — and found %s. It is matched at compile time as well as at run \
-       time, so it is written out rather than computed"
+       does — and found %s. It is written out, not computed"
       (Form.to_string f)
 
 (* ── The constraint map at the head of a defn body ──────────────────────
@@ -256,9 +251,8 @@ let constraints (body : Form.t list) : Ast.pred list * Form.t list =
           | _ -> rest <> []) ->
     if kvs = [] then
       Loc.fail loc
-        "an empty map literal here is discarded — the body has more after \
-         it, and its value going unused is almost always a typo for \
-         {:where ...}; write (do {} ...) if the empty map is deliberate"
+        "an empty map literal here is discarded — did you mean {:where ...}? \
+         Write (do {} ...) if the empty map is deliberate"
     else
     let pred (p : Form.t) =
       match p.Form.v with
@@ -530,9 +524,7 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
     (match args with
      | { v = Kw k; _ } :: _ ->
        fail f
-         ":%s — loop takes no label. break and continue may not leave a loop, \
-          because a loop answers with the value of its body; there is nothing \
-          for a label to name" k
+         ":%s — loop takes no label; break and continue may not leave a loop" k
      | { v = Vec bs; _ } :: body -> mk (Ast.Loop (loop_bindings f bs, body_of body))
      | _ -> fail f "loop is (loop [name value ...] body ...)")
 
@@ -691,9 +683,8 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
         | "defdata" | "defunion" | "defclass" | "defgeneric" | "defmulti"
         | "defmethod" | "defenum" | "defalias" | "import" as name) ->
     fail f
-      "%s is a top-level declaration, not an expression. A quasiquoted one is \
-       a value and a macro may answer with it; an evaluated one is not a thing \
-       anything can do" name
+      "%s defines a name at the top level, so it cannot be used as an \
+       expression here" name
 
   (* Recognised, deliberately unimplemented. Rejected rather than left to fall
      through to Call, where they would parse and mean nothing. *)
@@ -702,7 +693,7 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
   | Sym ("find-restart" | "compute-restarts"
         | "errdefer"
         | "await" as name) ->
-    fail f "%s is not implemented yet (see the build sequence in plan.org)" name
+    fail f "%s is not implemented yet" name
 
   (* ── field access: (.pos c) ────────────────────────────────────── *)
   | Sym s when String.length s > 1 && s.[0] = '.' ->
@@ -1190,9 +1181,8 @@ and pattern (f : Form.t) : Ast.pattern =
      spelled as a constructor it is not. *)
   | Kw member ->
     fail f
-      ":%s is not implemented as a pattern — match is over an Option here, \
-       and an enum member cannot be one until Ast.pattern can hold a keyword. \
-       Use cond with (= k :%s)" member member
+      ":%s is not implemented as a pattern — use cond with (= k :%s)"
+      member member
   | List ({ v = Sym ctor; _ } :: binds) ->
     List.iter no_pattern binds;
     Ast.Pctor (ctor, List.map sym binds)
@@ -1315,11 +1305,9 @@ let rec decl (f : Form.t) : Ast.decl =
             in
             if looks_tagged then
               Loc.failk "parse/defunion-renamed" f.loc
-                "the tagged sum is defdata now — (defdata Name [(Case [field \
-                 Type ...]) ...]) — and defunion is C's untagged union, whose \
-                 members overlay one storage: (defunion Name [member Type \
-                 ...]). This reads as the tagged one, so it is refused rather \
-                 than quietly given the other meaning")
+                "defunion is C's untagged union, written (defunion Name \
+                 [member Type ...]). This reads as a tagged sum — write \
+                 (defdata Name [(Case [field Type ...]) ...])")
          ms;
        mk (Ast.Defunion (sym n, fields f ms))
      | _ -> fail f "defunion is (defunion Name [member Type ...])")
@@ -1442,9 +1430,8 @@ let rec decl (f : Form.t) : Ast.decl =
                    | Sym name -> (name, s.loc)
                    | _ ->
                      fail s
-                       "a class slot is a name. Its value is dyn and there is \
-                        no type to write: an instance is a dyn map with a \
-                        shape tag on it, and (get p :%s) is how a slot is read"
+                       "a class slot is a name — its value is dyn, so there \
+                        is no type to write. Read one with (get p :%s)"
                        (Form.to_string s))
                 slots))
      | _ -> fail f "defclass is (defclass Name [slot ...])")
@@ -1569,16 +1556,15 @@ let rec decl (f : Form.t) : Ast.decl =
          else if explicit then
            Loc.failk "parse/enum-value-out-of-range" loc
              "the member %s of %s is %Ld, which does not fit i32 — an enum's \
-              discriminant is an i32, so its members run from -2147483648 to \
-              2147483647. Give %s a value in that range, or a defconst of a \
-              wider type if the number itself is what matters"
+              members run from -2147483648 to 2147483647. Give %s a value in \
+              that range, or use a defconst"
              m ename v m
          else
            Loc.failk "parse/enum-value-out-of-range" loc
              "the member %s of %s has no value of its own, so it \
               autoincrements to %Ld, which does not fit i32 — an enum's \
-              discriminant is an i32, so its members run from -2147483648 to \
-              2147483647. Write %s's value out, or lower the member above it"
+              members run from -2147483648 to 2147483647. Write %s's value \
+              out, or lower the member above it"
              m ename v m
        in
        (* Each member becomes its name, its value, whether that value was
@@ -1674,30 +1660,34 @@ let rec decl (f : Form.t) : Ast.decl =
           that is not a type is the value of a dyn global"
          form form form)
 
-  (* The old name of [defonce], refused by name rather than left to fall
-     through to "unknown function": every program written before the rename
-     spells it, and the message is the migration. *)
+  (* [defvar] is caught by name rather than left to fall through to "unknown
+     function", because two forms answer it and a did-you-mean over one name
+     could only ever offer one of them.
+
+     It says there is no defvar, not that defvar was renamed. The reader has
+     this compiler and nothing else: a rename is a fact about our history, and
+     what they need is the name that exists and what it does. *)
   | List ({ v = Sym "defvar"; _ } :: args) ->
     (* The rest of the form is echoed back inside the two spellings, so the
-       answer is a line that can be pasted. A form with nothing after the
-       keyword has nothing to paste, and echoing it would offer
-       [(defonce )] as the fix for [(defvar )] — a malformed old form
-       answered with a malformed new one. The names alone then, which is what
-       there is to say about a form that named nothing. *)
+       answer is a line that can be pasted. That only holds for a form long
+       enough to make a valid one: the shortest defonce is [(defonce name
+       value)], so an old form with fewer than two arguments has nothing to
+       paste and echoing it would answer [(defvar x)] with [(defonce x)] —
+       a malformed old form given a malformed new one, which is the standing
+       rule against a suggestion that does not compile. The shapes alone
+       then, which is what there is to say about a form that named too
+       little. *)
     (match args with
-     | [] ->
+     | [] | [ _ ] ->
        Loc.failk "parse/defvar-renamed" f.loc
-         "defvar is now called defonce — the name says what it does: it \
-          initialises once and keeps its value across re-runs. It is \
-          (defonce name Type value?), or (def name Type value?) if the value \
-          should follow the source on every re-run"
+         "there is no defvar. Did you mean defonce? \
+          (defonce name Type value?) initialises once and keeps its value; \
+          (def name Type value?) re-initialises on every re-run"
      | _ ->
        let rest = String.concat " " (List.map Form.to_string args) in
        Loc.failk "parse/defvar-renamed" f.loc
-         "defvar is now called defonce — the name says what it does: it \
-          initialises once and keeps its value across re-runs. Write (defonce \
-          %s), or (def %s) if the value should follow the source on every \
-          re-run"
+         "there is no defvar. Did you mean defonce? (defonce %s) initialises \
+          once and keeps its value; (def %s) re-initialises on every re-run"
          rest rest)
 
   | List ({ v = Sym "defconst"; _ } :: args) ->
@@ -1756,9 +1746,8 @@ let rec decl (f : Form.t) : Ast.decl =
      fault to guess at. *)
   | List ({ v = Sym "do"; _ } :: _) ->
     fail f
-      "a top-level (do ...) is several declarations spliced in place, and this \
-       is a position that takes exactly one — a macro answering several is a \
-       file's form, not an expression's"
+      "a top-level (do ...) is several declarations, and this position takes \
+       exactly one"
   | List ({ v = Sym s; _ } :: _) -> fail f "unknown top-level form (%s ...)" s
   | _ -> fail f "expected a top-level declaration, found %s" (Form.to_string f)
 
diff --git a/lib/render.ml b/lib/render.ml
index 5f92f8b..1e3d334 100644
--- a/lib/render.ml
+++ b/lib/render.ml
@@ -389,5 +389,9 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
        is not milestone 1's. *)
     | Types.Dyn ->
       [ unit_ (Tast.Prim (Tast.Rt "flan_dyn_print", [ e ])) ]
+    (* Reachable: [(println m)] on a Map. Everything else in [Types.t] has an
+       arm above, and a [Var] never reaches a backend. So this names the fix
+       rather than only the refusal. *)
     | t ->
-      fail loc "no printer for %s" (Types.to_string t)
+      fail loc "no printer for %s — print the values you want out of it"
+        (Types.to_string t)
diff --git a/lib/session.ml b/lib/session.ml
index 8847b23..77dcf35 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -283,9 +283,8 @@ let compatible ?(origin = fun _ -> None) ?(relaxed = []) ~loc
                    gname )
            in
            fail loc
-             "%s changes signature, from (Fn [%s] %s) to (Fn [%s] %s); \
-              the calls already compiled into the running program pass the old \
-              one.%s Restart to change it."
+             "%s changes signature, from (Fn [%s] %s) to (Fn [%s] %s).%s \
+              Restart to change it."
              what
              (String.concat " " (List.map Types.to_string g.Tast.params))
              (Types.to_string g.Tast.ret)
@@ -318,17 +317,15 @@ let compatible ?(origin = fun _ -> None) ?(relaxed = []) ~loc
               && Types.equal g.Tast.gty h.Tast.gty
               && not (same_const g.Tast.ginit h.Tast.ginit) ->
          fail loc
-           "%s is used at compile time — an array length or a type — so the \
-            running program has its old value in its shape, where a reload \
-            cannot reach it. Restart to change it."
+           "%s is used at compile time, in an array length or a type. \
+            Restart to change it."
            g.Tast.gname
        | Some h when not (Types.equal g.Tast.gty h.Tast.gty) ->
          (* The storage exists and has a shape. Reusing it for another one
             reads fields at the wrong offsets; allocating fresh storage would
             silently discard the state the reload exists to preserve. *)
          fail loc
-           "%s changes type, from %s to %s; the running program already laid \
-            that storage out. Restart to change it."
+           "%s changes type, from %s to %s. Restart to change it."
            g.Tast.gname (Types.to_string h.Tast.gty) (Types.to_string g.Tast.gty)
        (* Which form declared a global is not in the storage, it is in the
           code the process was *built* with: [Emit.startup_plan] wrote the
@@ -396,8 +393,7 @@ let compatible ?(origin = fun _ -> None) ?(relaxed = []) ~loc
             including ones held in globals that the reload is preserving. *)
          if not same then
            fail loc
-             "%s changes layout; the values the running program is holding have \
-              the old one. Restart to change it."
+             "%s changes layout. Restart to change it."
              s.Tast.sname
        | None -> ())
     new_.Tast.structs
@@ -420,8 +416,7 @@ let compatible_enums ~loc old_ new_ =
        match List.assoc_opt n before with
        | Some old_ms when old_ms <> ms ->
          fail loc
-           "%s changes its members; the running program folded the old values \
-            into every call site that names one. Restart to change it."
+           "%s changes its members. Restart to change it."
            n
        | _ -> ())
     (members new_)
@@ -504,7 +499,7 @@ let redefinition (t : t) ?retains ?call ?(consts = []) program ~fns =
          refusal it belongs to, and reaches [flan reload] too. *)
       fail loc
         "the x86 dev backend cannot compile this: %s. Restart the daemon with \
-         flan dev --llvm, which compiles every form this one refuses" m
+         flan dev --llvm" m
 
 (* ── Undoing an acceptance ─────────────────────────────────────────── *)
 
diff --git a/lib/shim.ml b/lib/shim.ml
index ccad00d..6b75f0e 100644
--- a/lib/shim.ml
+++ b/lib/shim.ml
@@ -195,8 +195,7 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
          "int32_t"
        else if Hashtbl.mem env.datas n then
          fail loc
-           "%s is %s, a data type, and a Flan data type has no C layout — the shim \
-            cannot be generated for it"
+           "%s is %s, a data type, which has no C layout"
            what n
        (* A union is the one refusal here that is not about the type. It has a
           C layout — it *is* a C layout, which is the whole reason it exists —
@@ -206,14 +205,12 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
           way through is the way every other aggregate crosses. *)
        else if Hashtbl.mem env.unions n then
          fail loc
-           "%s is %s, a union, and the shim generator writes structs only — a \
-            union has a C layout but nothing here emits the declaration for \
-            it yet. Pass (Ptr %s) and let the C side read it"
+           "%s is %s, a union, and the shim generator writes structs only. \
+            Pass (Ptr %s) and let the C side read it"
            what n n
        else if String.equal n "string" then
          fail loc
-           "%s is a string, and a string only crosses as a parameter — a C \
-            function that *returns* one returns something Flan has no owner for"
+           "%s is a string, and a string only crosses as a parameter"
            what
        else if String.equal n "Unit" || String.equal n "Never" then
          fail loc "%s is %s, which is not a value C can carry" what n
@@ -222,15 +219,14 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
   | Ast.Tapp ("Ptr", [ e ]) -> cty env ~needed ~loc ~what e ^ " *"
   | Ast.Tapp ("Option", _) ->
     fail loc
-      "%s is an Option, which is a Flan shape and not a C one — declare what C \
-       returns and build the Option in Flan"
+      "%s is an Option, which C has no shape for — declare what C returns and \
+       build the Option in Flan"
       what
   | Ast.Tslice _ ->
     fail loc
-      "%s is a slice, which crosses as ptr+len with an i64 length, and the \
-       count parameter the C function actually takes has a type this \
-       declaration does not say — declare (Ptr T) with an explicit count and \
-       pass (addr (at s 0)) and (len s) from Flan"
+      "%s is a slice, and nothing here says what type the C count parameter \
+       is — declare (Ptr T) with an explicit count, and pass \
+       (addr (at s 0)) and (len s) from Flan"
       what
   | Ast.Tarray _ ->
     fail loc
@@ -247,9 +243,8 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
      elements cross the way any other run of elements does. *)
   | Ast.Tapp ("Vec", _) ->
     fail loc
-      "%s is a Vec, which owns its storage — handing its header to C hands out \
-       an owner. Pass (slice v) as (Ptr T) and (len v), the same shape a \
-       slice crosses in"
+      "%s is a Vec, which owns its storage. Pass (slice v) as (Ptr T) and \
+       (len v)"
       what
   | Ast.Tfn _ ->
     fail loc "%s is a function type, and a C callback is not implemented" what
diff --git a/lib/x86.ml b/lib/x86.ml
index 97cb40b..2b0d10d 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -965,8 +965,8 @@ let store_scalar_at f ~reg ~base ~disp (t : Types.t) =
 let blockcopy f n =
   if n > 0 then begin
     note f (Printf.sprintf
-              "rep movsb: %d bytes from rsi to rdi. An aggregate is copied rather than \
-                aliased — spec-memory.md's assignment rule" n);
+              "rep movsb: %d bytes from rsi to rdi. An aggregate is copied \
+                rather than aliased." n);
     movabs f.b ~dst:rcx (Int64.of_int n);
     rep_movsb f.b
   end
@@ -2413,8 +2413,9 @@ and bounds_call f sym (loc : Loc.t) (extra : int list) =
   call_sym f.b sym;
   guard f;
   note f
-    "ud2, where emit.ml writes unreachable. Nothing answered the signal, so the runtime \
-      already died inside that call and nothing falls through to here.";
+    "ud2, where the LLVM backend writes unreachable. Nothing answered the \
+      signal, so the runtime already died inside that call and nothing falls \
+      through to here.";
   ud2 f.b
 
 (* The length an index is checked against, or [None] for the one form
@@ -3684,9 +3685,9 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
    | Some fr ->
      if ann then set_ind f.b "";
      note f
-       "The shadow stack's push — runtime/flan_dev.c. Dev builds only, and it is what \
-         lets a stopped program say where it is. The pop is the first thing in the \
-         epilogue, so a transfer out of this frame pops it too.";
+       "The shadow stack's push. Dev builds only, and it is what lets a stopped \
+         program say where it is. The pop is the first thing in the epilogue, so \
+         a transfer out of this frame pops it too.";
      (* Every entry, not only the named ones: "null means not bound" has to
         hold at every index, or a reader has to know which indices it may
         trust, and that is a second thing to keep in step. *)
@@ -3746,8 +3747,8 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
     jmp_lbl f.b f.retlbl;
     if ann then set_ind f.b "";
     note f
-      "The transfer exit — spec-conditions.md §5. A transfer that found no restart-case \
-        in this frame leaves the way a return does, which is what runs the defers.";
+      "The transfer exit. A transfer that found no restart-case in this frame \
+        leaves the way a return does, which is what runs the defers.";
     lbl f.b f.xfer_lbl;
     (* [emit.ml] leaves here with [ret zeroinitializer]. The value is
        meaningless to a caller — its guard sees the channel set and never looks
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 9a3aed9..2e79e6c 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -753,9 +753,8 @@ _Noreturn void flan_restart_unarmed(const uint8_t *loc, int64_t loclen,
                                     const uint8_t *want, int64_t wantlen) {
   rt_flush_out();
   fprintf(stderr,
-          "%.*s: restart %.*s takes %.*s, and whatever took it supplied no "
-          "arguments — a restart with parameters cannot be taken from the "
-          "break loop yet\n",
+          "%.*s: restart %.*s takes %.*s, and none was supplied — a restart "
+          "with parameters cannot be taken from the break loop yet\n",
           (int)loclen, (const char *)loc, (int)namelen, (const char *)name,
           (int)wantlen, (const char *)want);
   rt_trap((const uint8_t *)"RestartUnarmed", 14);
@@ -769,8 +768,7 @@ _Noreturn void flan_restart_unarmed(const uint8_t *loc, int64_t loclen,
 _Noreturn void flan_transfer_fail(const uint8_t *loc, int64_t loclen) {
   rt_flush_out();
   fprintf(stderr,
-          "%.*s: a defer invoked a restart, which a defer may not do — it is "
-          "the cleanup a transfer runs on its way out\n",
+          "%.*s: a defer invoked a restart, which a defer may not do\n",
           (int)loclen, (const char *)loc);
   rt_trap((const uint8_t *)"TransferFromDefer", 17);
 }
@@ -905,13 +903,9 @@ _Noreturn void flan_slice_promise_fail(const uint8_t *loc, int64_t loclen,
                                        int64_t n) {
   rt_flush_out();
   fprintf(stderr,
-          "%.*s: slice-from-ptr was promised %lld elements behind the pointer, "
-          "and a count of elements is never negative\n",
+          "%.*s: slice-from-ptr was promised %lld elements behind the "
+          "pointer, and a count is never negative\n",
           (int)loclen, (const char *)loc, (long long)n);
-  fprintf(stderr,
-          "  the caller promises the pointer addresses n elements and nothing "
-          "else can know it, so the sign of n is the whole of what this check "
-          "can see\n");
   rt_die();
 }
 
@@ -994,9 +988,8 @@ static void flan_arith_fail(const uint8_t *loc, int64_t loclen, int32_t op,
   case FLAN_ARITH_DIV_OVERFLOW:
   case FLAN_ARITH_REM_OVERFLOW:
     fprintf(stderr,
-            "%.*s: (%s %lld %lld) overflows: the quotient is one past the "
-            "largest value the type holds, and this is the only pair of "
-            "operands for which that is true\n",
+            "%.*s: (%s %lld %lld) overflows — the quotient is one past the "
+            "largest value the type holds\n",
             (int)loclen, (const char *)loc,
             op == FLAN_ARITH_DIV_OVERFLOW ? "/" : "%", (long long)lhs,
             (long long)rhs);
@@ -1491,9 +1484,8 @@ _Noreturn void flan_null_alloc_fail(const uint8_t *loc, int64_t loclen) {
 _Noreturn void flan_free_all_fail(const uint8_t *loc, int64_t loclen) {
   rt_flush_out();
   fprintf(stderr,
-          "%.*s: this allocator does not offer free-all — it has no region to "
-          "release, and releasing nothing is not the same as releasing "
-          "everything\n",
+          "%.*s: this allocator does not offer free-all — it has no region "
+          "to release\n",
           (int)loclen, (const char *)loc);
   rt_trap((const uint8_t *)"NoFreeAll", 9);
 }
@@ -1547,12 +1539,10 @@ void flan_alloc_region_only(flan_allocator *a, const uint8_t *loc,
 _Noreturn void flan_region_only_fail(const uint8_t *loc, int64_t loclen) {
   rt_flush_out();
   fprintf(stderr,
-          "%.*s: this container's elements own storage, and this allocator can "
-          "free one block — so a free here would release the slots and leak "
-          "everything inside them, and nothing type-erased can walk them. "
-          "Build it against a region allocator, whose free-all takes the "
-          "inner blocks too: (with-allocator context/temp ...) or an "
-          "(arena-new n)\n",
+          "%.*s: this container's elements own storage, and this allocator "
+          "frees one block at a time, so freeing it here would leak what the "
+          "elements hold. Build it against a region allocator: "
+          "(with-allocator context/temp ...) or an (arena-new n)\n",
           (int)loclen, (const char *)loc);
   rt_die();
 }
@@ -2885,9 +2875,8 @@ int64_t flan_file_fail_reason(void) { return flan_file_fail; }
 _Noreturn void flan_shim_nul_fail(const char *site) {
   rt_flush_out();
   fprintf(stderr,
-          "%s: a string passed to C contains a NUL byte — C reads to the "
-          "first one, so the value this function would act on is a prefix of "
-          "the one passed. Remove the NUL before the call.\n",
+          "%s: a string passed to C contains a NUL byte — C reads only up "
+          "to it. Remove the NUL before the call.\n",
           site);
   rt_die();
 }
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 7364e66..43143d0 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1052,7 +1052,7 @@ let () =
        spellings, not one form that changes type with its context. *)
     refuses_src "embed asked for a type it cannot read a file as"
       "(defn main [] i32 (len (embed \"no-such-asset.bin\" i32)))"
-      "`string` is the only one";
+      "embed's second argument is string";
 
     (* Allocators, spec-memory.md. The tier on its own, with no container
        above it, so that a failure here is not read as a Vec bug. What is
@@ -1356,7 +1356,7 @@ let () =
          one branch per container, where the allocator is still a value the
          site is holding. *)
       traps "a container of owning elements against the heap" "1"
-        "this allocator can free one block";
+        "this allocator frees one block at a time";
       (* A different mechanism, pinned separately: the epoch, and specifically
          an inner header copied *out* of its container before the release. It
          traps because an Allocator is a pointer — a copied-by-value one would
@@ -1368,7 +1368,7 @@ let () =
          first push is what adopts the context. Pinned from both sides — run 0
          above grows the same zeroed field in a region and must not trap. *)
       traps "a zeroed field of owning elements grown against the heap" "3"
-        "this allocator can free one block";
+        "this allocator frees one block at a time";
       (try Sys.remove exe with Sys_error _ -> ())
     in
     region ();
@@ -2938,7 +2938,7 @@ let () =
        and cannot change. *)
     refuses "a package generic's bound, refused at the call"
       "programs/pkg-generic-reject.flan"
-      "string does not answer ordered?";
+      "string is not ordered?";
     refuses "and the refusal quotes the clause the package wrote"
       "programs/pkg-generic-reject.flan" "{:where (ordered? $t)}";
 
@@ -2971,7 +2971,7 @@ let () =
        chain of instantiations and not a depth it gave up at. *)
     refuses "an unconstrained operator in a generic body"
       "programs/generic-reject.flan"
-      "only what it is declared to support";
+      "nothing declares t numeric?";
     refuses "an unconstrained operator names the way out"
       "programs/generic-reject.flan" "{:where (numeric? $t)}";
     refuses "a runaway instantiation" "programs/generic-runaway.flan"
@@ -2999,7 +2999,7 @@ let () =
        requirement the author wrote down. What is asserted is that it names
        the type passed and the predicate it failed, and not the body. *)
     refuses "a generic over maps, instantiated at a key that cannot be hashed"
-      "programs/generic-map-reject.flan" "does not answer hashable?";
+      "programs/generic-map-reject.flan" "f64 is not hashable?";
     refuses "and it names the type the call site asked for"
       "programs/generic-map-reject.flan" "at $t = f64";
 
@@ -3010,7 +3010,7 @@ let () =
       refuses "a package's main is not visible" "programs/pkg-hidden-main.flan"
         "sand/main is not a name";
     refuses "one directory under two aliases" "programs/pkg-two-aliases.flan"
-      "one directory is one set of names";
+      "one directory takes one alias";
     (* A ring is refused and the ring is named. The needle is the chain, not
        the word "cycle": what a person needs is which three imports, and the
        refusal that says only "there is a cycle" leaves them to find it. The
@@ -3025,7 +3025,7 @@ let () =
        is that the clash is caught at all when the two halves are a page and a
        directory apart, rather than side by side as in the case above. *)
     refuses "one directory under two aliases, through a package"
-      "programs/pkg-alias-clash.flan" "one directory is one set of names";
+      "programs/pkg-alias-clash.flan" "one directory takes one alias";
     (* A ring is refused and the ring is named. The needle is the chain, not
        the word "cycle": what a person needs is which three imports, and the
        refusal that says only "there is a cycle" leaves them to find it. The
@@ -3063,7 +3063,7 @@ let () =
        one — or anywhere to put the flan_allocator, Allocator being opaque and
        pointer-width. Two reasons, both named, neither a function value. *)
     refuses "a user-written allocator" "programs/user-allocator.flan"
-      "is no longer what is missing";
+      "a user-written allocator is not implemented yet";
     (* Move-only, spec-memory.md, since the repeal: the three fixtures that
        were refused here — a use after a pass, a double free, a move inside a
        loop — now compile, and what they do at run time is the allocator's and
@@ -3087,7 +3087,7 @@ let () =
        storage. Refused by the shim generator, where the message can say what
        to pass instead. *)
     refuses "a Vec crossing to C" "programs/vec-to-c.flan"
-      "handing its header to C hands out an owner";
+      "is a Vec, which owns its storage";
 
     (* ── wasm32 (NEXT.md, deferred item 6) ──────────────────────────────
        The second target, and the reason sand-headless imports no raylib. What
@@ -3584,14 +3584,14 @@ level "1"
 
     shim_refuses "declare-c: a slice parameter, by name and reason"
       (v2 ^ "(declare-c poly [pts [Vector2]] bool \"Poly\")")
-      "the count parameter the C function actually takes";
+      "what type the C count parameter is";
     shim_refuses "declare-c: an Option"
       (v2 ^ "(declare-c maybe [] (Option Vector2) \"Maybe\")")
-      "which is a Flan shape and not a C one";
+      "an Option, which C has no shape for";
     shim_refuses "declare-c: a data type"
       ("(defdata Shape [(Circle [r f32]) (Square [s f32])])\n\
         (declare-c area [s Shape] f32 \"Area\")")
-      "a data type, and a Flan data type has no C layout";
+      "a data type, which has no C layout";
     shim_refuses "declare-c: a fixed array"
       "(declare-c takes [xs [4 f32]] \"Takes\")"
       "which C passes as a pointer and Flan as a value";
@@ -3757,7 +3757,7 @@ level "1"
     refuses_src "a float is not a map key"
       "(defn f [m (Map f32 i32)] () 0)" "is not a map key";
     refuses_src "a Ptr is not a map key"
-      "(defn f [m (Map (Ptr i32) i32)] () 0)" "hash an address";
+      "(defn f [m (Map (Ptr i32) i32)] () 0)" "is not a map key. A key is an integer";
     (* A map value that owns storage is no longer refused at the type: that
        refusal was about teardown, and which tier the map will meet is not
        knowable where its type is written. What it became is a branch on the
@@ -4740,7 +4740,7 @@ level "1"
       "A is a case of the data type U";
     refuses_src "a data type type used as a constructor"
       "(defdata U [(A [x i32])])\n(defn main [] i32 (let [v (U {.x 1})] 0))"
-      "a data type value names the case as well as the type";
+      "so a value of it names a case";
     refuses_src "a case with fields written bare"
       "(defdata U [(A [x i32])])\n(defn main [] i32 (let [v U.A] 0))"
       "has fields, so it needs them";
@@ -4789,7 +4789,7 @@ level "1"
     refuses_src "a data type is not a map key"
       "(defdata U [A B])\n\
        (defn f [m (Map U i32) k U] () (put m k 1))"
-      "the payload past the case in hand is indeterminate";
+      "a data type is not a map key";
     (* A *constant* cannot hold a case, because writing one at link time means
        serialising the fields into the payload blob and a string field is a
        relocation a byte array has nowhere to put. Refused in the checker since
@@ -4811,7 +4811,7 @@ level "1"
        incr failures;
        Printf.printf "FAIL  %s\n        it was accepted\n" name
      | exception Loc.Error { Loc.dmsg = m; _ } ->
-       if not (contains m "needs a byte-level encoder that does not exist")
+       if not (contains m "a constant cannot be U.B")
        then begin
          incr failures;
          Printf.printf "FAIL  %s\n        said: %S\n" name m
@@ -4862,12 +4862,12 @@ level "1"
        assume cannot be reached. *)
     refuses_src "uninit on a data type global"
       "(defdata U [A B])\n(defonce g U uninit)\n(defn main [] i32 0)"
-      "its tag steers every match";
+      "Drop the uninit — a zeroed U is U.A";
     (* A data type's fields belong to a case, so .field is not a read anyone can
        do without having read the tag first. match is how one is opened. *)
     refuses_src "reading a field of a data type directly"
       "(defdata U [(A [x i32])])\n(defn f [u U] i32 (.x u))"
-      "reached by (match ...)";
+      "its fields belong to a case";
     (* And a zeroed one is fine, which is the other half of the same rule: it
        is the first declared case, all bytes zero, and needs no encoder. *)
     (let name = "a zeroed data type global" in
diff --git a/test/test_flan.ml b/test/test_flan.ml
index b2a9f4f..11a0d8f 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -524,15 +524,15 @@ let () =
   (match (parse_decl "(def counter i64 (start))").d with
    | Defvar ("counter", Some { t = Tname "i64"; _ }, Init _, Every) -> ()
    | _ -> check "a typed def with an initialiser" false);
-  (* The old name, refused with the migration in the message: what it is
-     called now, why the name, and both new spellings — each of which
-     compiles as written. *)
+  (* The old name, refused as a name that does not exist rather than as a
+     rename: the reader has this compiler and nothing else, so what they need
+     is the name that does exist, what it does, and the other one beside it.
+     Both spellings compile as written. *)
   parse_rejects "the old defvar spelling names defonce"
     "(defvar counter i64 7)"
-    ~needle:"defvar is now called defonce — the name says what it does: it \
-             initialises once and keeps its value across re-runs. Write \
-             (defonce counter i64 7), or (def counter i64 7) if the value \
-             should follow the source on every re-run";
+    ~needle:"there is no defvar. Did you mean defonce? (defonce counter i64 \
+             7) initialises once and keeps its value; (def counter i64 7) \
+             re-initialises on every re-run";
   (match read "(defvar counter i64 7)" |> Parse.program with
    | _ -> check "the old defvar spelling has a kind" false
    | exception Loc.Error { Loc.kind; _ } ->
@@ -542,8 +542,8 @@ let () =
      malformed new one as its fix. *)
   parse_rejects "the old spelling with no arguments names the shapes"
     "(defvar)"
-    ~needle:"It is (defonce name Type value?), or (def name Type value?) if \
-             the value should follow the source on every re-run";
+    ~needle:"(defonce name Type value?) initialises once and keeps its \
+             value; (def name Type value?) re-initialises on every re-run";
   (match (parse_decl "(import rl \"vendor:raylib\")").d with
    | Import ("rl", "vendor:raylib") -> () | _ -> check "import" false);
 
@@ -598,7 +598,7 @@ let () =
   parse_rejects "defmacro with a non-name param" "(defmacro m [1] x)"
     ~needle:"a macro's parameter is a name or a [ ] pattern";
   parse_rejects "defmacro in expression position" "(defn f [] () (defmacro m [] 1))"
-    ~needle:"top-level declaration";
+    ~needle:"cannot be used as an expression here";
 
   (* The tagged sum is [defdata] now. The old spelling is refused by name
      rather than aliased, because the name is reserved for a type with
@@ -606,13 +606,13 @@ let () =
      which of the two it means instead of being quietly given one of them. *)
   parse_rejects "the old defunion spelling"
     "(defunion Shape [(Circle [r f32]) (Square [s f32])])"
-    ~needle:"the tagged sum is defdata now";
+    ~needle:"This reads as a tagged sum";
   (* The shape that would otherwise parse: two bare case names read as one
      member of a type. Same refusal, and this is the one that matters — it
      would have compiled. *)
   parse_rejects "the old defunion spelling with payload-less cases"
     "(defunion U [A B])"
-    ~needle:"the tagged sum is defdata now";
+    ~needle:"This reads as a tagged sum";
   (match read "(defunion U [A B])" |> Parse.program with
    | _ -> check "the old spelling has a kind" false
    | exception Loc.Error { Loc.kind; _ } ->
@@ -730,7 +730,7 @@ let () =
     ~needle:"the member B of E is 4294967296, which does not fit i32";
   parse_rejects "the out-of-range refusal says what the range is"
     "(defenum E [A 0  B 4294967296])"
-    ~needle:"its members run from -2147483648 to 2147483647";
+    ~needle:"an enum's members run from -2147483648 to 2147483647";
   (* Nothing in the source wrote 2147483648, so the sentence has to say where
      it came from before it can say it is wrong. *)
   parse_rejects "an autoincrement off the top of i32"
@@ -1347,7 +1347,7 @@ let () =
   accepts "all-distinct over a type variable"
     "(defn three [a $t b $t c $t] bool {:where (equal? $t)} (!= a b c))";
   rejects_check "a chain still wants the right predicate"
-    ~needle:"nothing here says t is ordered?"
+    ~needle:"nothing declares t ordered?"
     "(defn between [a $t b $t c $t] bool {:where (equal? $t)} (< a b c))";
   (* One operand and none. Both would have to be [true] whatever they were
      handed, which is a typo carrying a value. *)
@@ -1564,6 +1564,15 @@ let () =
   accepts "a dyn in a condition's payload"
     "(defstruct Boom [what dyn])\n\
      (defn main [] () (signal (Boom {.what 1})))";
+  (* What a condition may still not *be*. A handler matches on the condition's
+     type, and a dyn has no type until it runs, so the dyn itself is refused
+     where the struct it holds would have been fine. This is the arm the
+     "a dyn in a condition's payload" row above used to reach by accident, by
+     way of the struct-field refusal that fired first and is now gone: a dyn
+     value has to be signalled directly to get here at all. *)
+  rejects_check "a dyn signalled as the condition itself"
+    "(defn f [d dyn] () (signal d))"
+    ~needle:"a condition is matched by its type and dyn is not one";
   (* Nested by value, which is the case the flattening is for: the inner
      struct's dyn word appears in the outer's table at the sum of the two
      offsets, and there is no second descriptor to follow at run time. *)
@@ -2117,10 +2126,10 @@ let () =
      written in, which is what the acceptance program sorts. *)
   rejects_check "slice of a returned array"
     "(defn mk [] [3 i32] [7 8 9]) (defn f [] [i32] (slice (mk)))"
-    ~needle:"a returned array is a temporary";
+    ~needle:"a temporary the slice would outlive";
   rejects_check "slice of a returned array, three arguments"
     "(defn mk [] [3 i32] [7 8 9]) (defn f [] [i32] (slice (mk) 0 3))"
-    ~needle:"a returned array is a temporary";
+    ~needle:"a temporary the slice would outlive";
   accepts "slice of an array literal"
     "(defn f [] [i32] (slice [7 8 9]))";
   (* One builtin, one answer about a bound. A slice bound is a subscript and
@@ -2166,7 +2175,7 @@ let () =
      store. *)
   rejects_check "the address of a string's byte"
     "(defn f [s string] (Ptr u8) (addr (at s 0)))"
-    ~needle:"take the address of";
+    ~needle:"(at s i) is a value and not a place";
   (* And a string is still not a [u8]: slicing one does not smuggle a byte
      slice out of it. *)
   rejects_check "a string slice is not a byte slice"
@@ -2325,11 +2334,10 @@ let () =
   accepts "a local is assignable"
     "(defn f [] i32 (let [x 1] (set x 2) x))";
   rejects_check "a parameter is not assignable"
-    "(defn f [x i32] () (set x 2))" ~needle:"a parameter is not a place you can assign to";
+    "(defn f [x i32] () (set x 2))" ~needle:"a parameter is not assignable";
   rejects_check "a constant is not assignable"
     "(defconst k 1) (defn f [] () (set k 2))"
-    ~needle:"k is a constant, and a constant is not assignable — it is \
-             written into the image and there is nothing to assign to. \
+    ~needle:"k is a constant, and a constant is not assignable. \
              Declare it with defonce if it has to change";
   accepts "addr of a local gives a pointer"
     (cursor ^ "(defn g [c (Ptr Cursor)] i32 (.pos c)) \
@@ -2651,7 +2659,7 @@ let () =
   rejects_check "a dispatch value is written out, not computed"
     "(defmulti d [x] dyn x)\n(defmethod d (f 1) [x] 1)\n\
      (defn main [] i32 0)"
-    ~needle:"is written out rather than computed";
+    ~needle:"It is written out, not computed";
   (* A method has no return slot: the generic states the type once, for all
      of them. What that means for anyone writing the defn spelling by habit
      is that the slot they would have written is read as the first form of
@@ -2695,7 +2703,7 @@ let () =
   rejects_check "Map takes two types"   "(defn f [x (Map i32)] ())"
     ~needle:"exactly two types";
   rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)"
-    ~needle:"milestone 6";
+    ~needle:"(Result T E) is not implemented";
 
   (* ── The region rule, spec-memory.md's arena rule ────────────────────
      The compile-time half of it, which is the only half a checker row can
@@ -2723,7 +2731,7 @@ let () =
   rejects_check "free on a container of owning elements"
     "(defdata V [Nil (L [xs (Vec V)])])\n\
      (defn f [v (Vec V)] () (free v))"
-    ~needle:"(free-all a) takes it";
+    ~needle:"Write (free-all a) on the region";
   (* clone is refused for a reason the region does *not* dissolve: it promises
      an independent copy and a bytewise one is an alias. *)
   rejects_check "clone on a container of owning elements"
@@ -2747,12 +2755,12 @@ let () =
     "(defonce g (Vec u8) (slurp \"game-data.edn\")) (defn f [] ())";
   rejects_check "a move-only global as a defconst"
     "(defconst g (Vec u8) (slurp \"game-data.edn\")) (defn f [] ())"
-    ~needle:"a defonce and not a defconst";
+    ~needle:"is a defonce, not a defconst";
   (* uninit is the one initialiser a container still refuses, and it is a
      different rule: a garbage block pointer is not a garbage number. *)
   rejects_check "a global Vec declared uninit"
     "(defonce g (Vec u8) uninit) (defn f [] ())"
-    ~needle:"steers every read of it";
+    ~needle:"Write (defonce g (Vec u8)) with no initialiser";
 
   (* ── What may be filled with raw bytes ─────────────────────────────
      [(filled b)] and [(dead-beef)] are [zeroed]'s siblings, and the
@@ -3161,7 +3169,7 @@ let () =
     ~needle:"with no handler-bind or restart-case around it";
   rejects_check "an invoke-restart in a global initialiser"
     "(defonce w i64 (do (invoke-restart 'retry) 1))\n(defn f [] i64 w)"
-    ~needle:"an initialiser runs at startup";
+    ~needle:"with no handler-bind or restart-case around it";
   (* And what is *inside* one runs like any other code: the frames a
      restart-case pushes it also pops, before the initialiser returns. This is
      [slurp]'s shape, which is why a global loaded from a file works at all. *)
@@ -3177,7 +3185,7 @@ let () =
      (defn f [] () (set g (vec-new u8)) (push g 1) (set (at g 0) 2) \
        (println (len (slice g))) (let [c (clone g)] (free c)))";
   rejects_check "try is milestone 6"    "(defn f [] i32 (try 1))"
-    ~needle:"milestone 6";
+    ~needle:"try (Result) is not implemented";
   (* dotimes and defer are implemented, and a defer in a [let] is now one of
      the places it may be written: a let at the top level of a function body
      has exactly the function's extent (see test/programs/defer-let.flan). What
@@ -3278,7 +3286,7 @@ let () =
   (* Where the "refuse mutual recursion by name" answer lives: there are no
      tail calls, so a function cannot recur into itself either. *)
   rejects_check "recur outside a loop"
-    "(defn f [] () (recur))" ~needle:"no tail calls";
+    "(defn f [] () (recur))" ~needle:"only allowed inside a (loop ...)";
   rejects_check "recur with the wrong number of values"
     "(defn f [] i32 (loop [i 0  j 1] (recur 1)))"
     ~needle:"binds 2 names and this recur passes 1";
@@ -3293,10 +3301,10 @@ let () =
   accepts "a while inside a loop keeps its own break"
     "(defn f [] () (loop [i 0] (while true (break))))";
   rejects_check "break may not leave a loop"
-    "(defn f [] () (loop [i 0] (break)))" ~needle:"no value to give";
+    "(defn f [] () (loop [i 0] (break)))" ~needle:"break cannot leave a (loop ...)";
   rejects_check "a labelled break may not leave a loop"
     "(defn f [] () (while :o true (loop [i 0] (break :o))))"
-    ~needle:"no value to give";
+    ~needle:"would leave a (loop ...)";
   accepts "a while condition is an ordinary expression"
     "(defn f [] () (let [v (vec-new i32)  n 0] \
        (while (and (< n 10) (> (len v) 0)) (set n (+ n 1))) (free v)))";
@@ -3578,7 +3586,7 @@ let () =
   rejects_check "a data type case nested in a constant struct"
     "(defdata U [A (B [x i32])]) (defstruct S [u U]) \
      (defconst g S (S {.u (U.B {.x 1})}))"
-    ~needle:"needs a byte-level encoder that does not exist";
+    ~needle:"a constant cannot be U.B";
   accepts "a constant written as a literal"
     "(defconst x u64 0xcbf29ce484222325)";
   accepts "a constant written as arithmetic over other constants"
@@ -3717,7 +3725,7 @@ let () =
     (boom ^ "(defn f [] i32 (let [n 1] (handler-case 0 [(Boom [c] n)])))");
   rejects_check "a handler-bind clause still cannot"
     (boom ^ "(defn f [] i32 (let [n 1] (handler-bind [(Boom [c] (set n 2))] 0)))")
-    ~needle:"a handler cannot see n: it is a local of the enclosing function";
+    ~needle:"a handler cannot see n — it is a local of the enclosing function";
   (* Nothing static refuses a condition no clause lists: it installs no frame
      that matches, so it goes past untouched and the body carries on. *)
   accepts "a condition no clause lists"
@@ -3933,10 +3941,10 @@ let () =
      be one that kills the program instead. *)
   rejects_check "an array pattern over a slice"
     "(defn f [s [i32]] i32 (let [[a b] s] (+ a b)))"
-    ~needle:"a slice's length is a runtime value";
+    ~needle:"a slice's length is not known until the program runs";
   rejects_check "an array pattern over a slice, even with & rest"
     "(defn f [s [i32]] i32 (let [[a & r] s] (+ a (len r))))"
-    ~needle:"a slice's length is a runtime value";
+    ~needle:"a slice's length is not known until the program runs";
   rejects_check "an array pattern over something with no elements at all"
     "(defn f [n i32] i32 (let [[a b] n] (+ a b)))"
     ~needle:"i32 is not a fixed array";
@@ -3966,7 +3974,7 @@ let () =
   List.iter
     (fun (what, src) ->
        rejects_check ("a pattern in " ^ what) src
-         ~needle:"a pattern binds only in let")
+         ~needle:"this position takes a plain name")
     [ "a defn parameter",    pt ^ "(defn f [{:keys [x]} Point] i32 x)";
       "a defstruct field",   "(defstruct S [[a b] i32])";
       "an fn parameter",     "(defn f [] i32 (let [g (fn [[a b]] a)] 0))";
@@ -3996,7 +4004,7 @@ let () =
   rejects_check "a pattern inside a match arm's binds"
     "(defstruct P [x i32])\n\
      (defn f [o (Option P)] i32 (match o (Some {:keys [x]}) x None 0))"
-    ~needle:"a pattern binds only in let";
+    ~needle:"this position takes a plain name";
 
   (* The desugaring's own machinery is unspellable: the reader makes [~] a
      delimiter, so the name never reaches the parser as one symbol. *)
@@ -4054,11 +4062,11 @@ let () =
   rejects_check "a data type member"
     "(defdata D [A (B [x i32])])\n\
      (defunion U [d D  n i64])\n(defn f [u U] i32 0)"
-    ~needle:"a data type's tag steers every match";
+    ~needle:"a data type, and a union may not hold one";
   rejects_check "a data type inside a struct member"
     "(defdata D [A B])\n(defstruct S [d D  n i32])\n\
      (defunion U [s S  n i64])\n(defn f [u U] i32 0)"
-    ~needle:"a data type's tag steers every match";
+    ~needle:"a data type, and a union may not hold one";
   (* An Option is not on that list, and the difference is the lowering: its
      match is a test of the tag byte and a branch, so a scribbled tag reads as
      a Some with a payload nobody stored — which is what this language says a
@@ -4081,7 +4089,7 @@ let () =
   rejects_check "a union literal giving two members"
     "(defunion U [i i32  f f32])\n\
      (defn f [] i32 (let [u (U {.i 1  .f 2.0})] (.i u)))"
-    ~needle:"only one of them can be written";
+    ~needle:"only one member can be written";
   rejects_check "a union literal giving a member it does not have"
     "(defunion U [i i32])\n(defn f [] i32 (let [u (U {.z 1})] (.i u)))"
     ~needle:"U has no member z";
@@ -4091,7 +4099,7 @@ let () =
   rejects_check "match on a union"
     "(defunion U [i i32  f f32])\n\
      (defn f [u U] i32 (match u _ 0))"
-    ~needle:"there is nothing in one to match on";
+    ~needle:"nothing in one records which member was written";
   (* A member narrower than the union leaves the rest indeterminate, so two
      values that agree about everything anybody wrote would hash apart. *)
   rejects_check "a union as a map key"
@@ -5348,9 +5356,8 @@ let () =
        (d.Loc.kind = "check/shortcircuit-operand" && d.Loc.dloc.Loc.col = 39);
      check "and states what the two answers are"
        (contains d.Loc.dmsg
-          "an and answers false when it stops early and its last operand \
-           otherwise, so the two have to be one type — this operand is (Vec \
-           i32), and false is a bool")
+          "an and answers false or its last operand, so the two have to \
+           be one type — this operand is (Vec i32), and false is a bool")
    | None -> check "a mistyped and operand is refused" false);
 
   (* The reader's own two-place error. The bracket that is open is the error
@@ -5461,7 +5468,7 @@ let () =
   accepts "numeric? admits +"
     "(defn add [a $t b $t] $t {:where (numeric? $t)} (+ a b))";
   rejects_check "equal? does not admit <"
-    ~needle:"nothing here says t is ordered?"
+    ~needle:"nothing declares t ordered?"
     "(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))";
   (* The entailments, which are the reason a signature is one predicate long
      rather than two. Every type the language orders is a number or an enum,
@@ -5489,10 +5496,10 @@ let () =
   accepts "integer? admits the shifts"
     "(defn dbl [x $t] $t {:where (integer? $t)} (<< x 1))";
   rejects_check "numeric? does not admit bit-and"
-    ~needle:"nothing here says t is integer?"
+    ~needle:"nothing declares t integer?"
     "(defn low? [x $t] bool {:where (numeric? $t)} (= (bit-and x 1) 1))";
   rejects_check "nor the shifts"
-    ~needle:"nothing here says t is integer?"
+    ~needle:"nothing declares t integer?"
     "(defn dbl [x $t] $t {:where (numeric? $t)} (<< x 1))";
   (* An integer?-bounded caller satisfies a numeric?-bounded callee: the
      entailment carries across generic calls exactly as ordered?-over-equal?
@@ -5508,13 +5515,13 @@ let () =
     "(defn bump [x $t] $t {:where (integer? $t)} (+ x 300))";
   (* A float at integer?, refused at the call that asked, naming the bound. *)
   rejects_check "a float does not instantiate an integer?-bounded variable"
-    ~needle:"f64 does not answer integer?"
+    ~needle:"f64 is not integer?"
     "(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))\n\
      (defn main [] () (println (bump 1.5)))";
   (* And dyn is refused by the bound too — the clause's own refusal, the more
      specific of the two answers, exactly as at numeric?. *)
   rejects_check "dyn does not instantiate an integer?-bounded variable"
-    ~needle:"dyn does not answer integer?"
+    ~needle:"dyn is not integer?"
     "(defn bump [x $t] $t {:where (integer? $t)} (+ x 1))\n\
      (defonce d dyn 5)\n\
      (defn main [] () (println (bump d)))";
@@ -5623,7 +5630,7 @@ let () =
     "(defn same [a $t b $t] bool {:where (equal? $t)} (= a b)) \
      (defn f [] bool (same \"a\" \"b\"))";
   rejects_check "ordered? $t instantiated at string"
-    ~needle:"does not answer ordered?"
+    ~needle:"is not ordered?"
     "(defn less [a $t b $t] bool {:where (ordered? $t)} (< a b)) \
      (defn f [] bool (less \"a\" \"b\"))";
 
@@ -5675,7 +5682,7 @@ let () =
      it and the call site, or the refusal moves into code the caller did not
      write. *)
   rejects_check "a predicate is not carried through a generic call"
-    ~needle:"has to be carried by every signature"
+    ~needle:"Add {:where (ordered? $t)} to this function's own clause"
     "(defn outer [s [$t]] () {:where (equal? $t)} (sort s))";
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
@@ -5801,7 +5808,7 @@ let () =
      nor i64 holds every value of the other, and inventing a third type
      would be picking one neither argument was written at. *)
   rejects_check "u64 and i64 meet at no type"
-    ~needle:"the two meet at no type"
+    ~needle:"neither holds every value of the other"
     "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
      (defonce u u64 3)\n(defonce i i64 3)\n\
      (defn main [] () (println (eq2? u i)))";
@@ -5882,10 +5889,10 @@ let () =
      instantiation at which it means nothing — and the refusal below is what
      stops that reaching the call site. *)
   rejects_check "an unconstrained type variable admits no literal"
-    ~needle:"may be instantiated at a type that holds no number"
+    ~needle:"nothing declares $t numeric"
     "(defn f [x $t] bool (> x 0))";
   rejects_check "and ordered? is not the bound that admits one"
-    ~needle:"Declare the bound"
+    ~needle:"Write {:where (numeric? $t)}"
     "(defn f [x $t] bool {:where (ordered? $t)} (> x 0))";
   (* The asymmetry, and it is the concrete arms' asymmetry rather than a new
      one: an untyped integer constant is usable where a float is wanted, and
diff --git a/test/test_repl.ml b/test/test_repl.ml
index e5c1510..9579130 100644
--- a/test/test_repl.ml
+++ b/test/test_repl.ml
@@ -145,9 +145,9 @@ let () =
          name defonce", which is why the reason asserted here was empty; now
          that an expression expands, a macro can produce one, and the head
          says what it is wherever it appears. *)
-      refuses "a declaration" "(defonce nope i64)" "top-level declaration";
+      refuses "a declaration" "(defonce nope i64)" "cannot be used as an expression here";
       refuses "a declaration inside an expression" "(do 1 (defn f [] i32 1))"
-        "top-level declaration";
+        "cannot be used as an expression here";
       refuses "an unknown name" "no-such-name" "unknown name";
       (* [defmacro] is in that same head list, and it is the shape that stays
          refused now that a [defmacro] typed at the editor means something: a
@@ -156,7 +156,7 @@ let () =
          about an unknown function. C-c C-c is where a declaration goes, which
          is the case below. *)
       refuses "a defmacro at C-x C-e" "(defmacro m [& args] args)"
-        "top-level declaration";
+        "cannot be used as an expression here";
 
       (* And the session is untouched by all of it: an evaluation is not a
          declaration, so nothing named eval/N accumulates in the program. *)
diff --git a/test/test_session.ml b/test/test_session.ml
index 3dd5ed8..f8f395a 100644
--- a/test/test_session.ml
+++ b/test/test_session.ml
@@ -712,12 +712,12 @@ let () =
   (match Session.eval_expr ~origin:"programs/pkg-macro.flan" tm "(defn f [] i32 1)" with
    | _ -> fail "a declaration was accepted as an expression"
    | exception Loc.Error { Loc.dmsg = m; _ } ->
-     if not (has m "top-level declaration") then
+     if not (has m "cannot be used as an expression here") then
        fail "a declaration as an expression said %S" m);
   (match Session.eval_expr ~origin:"programs/pkg-macro.flan" tm "(do 1 (defonce g i64))" with
    | _ -> fail "a nested declaration was accepted as an expression"
    | exception Loc.Error { Loc.dmsg = m; _ } ->
-     if not (has m "top-level declaration") then
+     if not (has m "cannot be used as an expression here") then
        fail "a nested declaration as an expression said %S" m);
 
   (* The two non-termination refusals. They matter more here than in a build:
diff --git a/vendor/agent/flan_agent.c b/vendor/agent/flan_agent.c
index 6f13371..b2bf2c2 100644
--- a/vendor/agent/flan_agent.c
+++ b/vendor/agent/flan_agent.c
@@ -843,8 +843,8 @@ static void break_loop_at(const uint8_t *name, int64_t namelen, void *condition,
      * describing two different programs. */
     if (!s->resumable)
       fprintf(stderr,
-              "  this trap has no transfer channel, so nothing here can be "
-              "resumed into; read the frame, then fix and reload, or abort\n");
+              "  nothing here can be resumed into; read the frame, then fix "
+              "and reload, or abort\n");
     else if (s->n == 0)
       fprintf(stderr, "  no restarts are active; abort, or fix and reload\n");
     for (int32_t i = 0; i < s->n; i++)