The next-error claim was inferred, and it is weaker than it read

compile.el puts note in the same capture group as info — group 7, level 0 —
while warning is group 6, level 1, and compilation-skip-threshold defaults to
1. So next-error walks the errors with no configuration, which is the claim
M-x compile rests on and it holds; it steps over the notes until the
threshold is 0. They are still parsed, coloured and clickable.

Labelling notes warning: would make them navigable at the default and is
refused. A note is not a warning, and a compile whose only complaint is an
error would start reporting warnings that are not warnings.

The macro expansion field gets the test it was missing, through a real
expansion rather than a unit test on either half: the tag is put on by Macro
and defaulted into the diagnostic by Loc, and either half alone would pass
with the other broken. clamp misused expands into a call to a name that does
not exist, so the checker refuses something the author never wrote, which is
the case the field is for.

BUILT.md

@@ -3974,7 +3974,16 @@ prog.flan:1:1: info: Cursor is declared here, with row, col
 ```
 
 A note gets an **entry of its own** rather than being folded into the error's block. That is gcc's shape and it is the
-point of notes having locations at all: the second place becomes somewhere `next-error` can take you.
+point of notes having locations at all: the second place becomes a place the compilation buffer knows about.
+
+**Stated at its true strength, because it was checked rather than assumed** (`compile.el`, Emacs 30.2). The `gnu`
+entry in `compilation-error-regexp-alist-alist` puts `Note`/`note` in the *same capture group* as `Info`/`info` —
+group 7, level 0 — while `warning` is group 6, level 1. `compilation-skip-threshold` defaults to **1**, "skip
+anything less than warning". So: **errors** are navigable with `next-error` out of the box, which is the claim that
+matters and the one `M-x compile` rests on. **Notes** are parsed, coloured and clickable, and `next-error` steps over
+them until `compilation-skip-threshold` is 0. Renaming the label from `info:` to `note:` does not change that — same
+group. Labelling notes `warning:` *would* make them navigable at the default, and is refused: a note is not a
+warning, and a compile whose only complaint is an error would start reporting warnings that are not warnings.
 
 Every part of it degrades to the bare first line. A location the checker invented has line 0 and a file called
 `<unknown>`, the prelude and the REPL have names that are not paths, and a file can change under us between being

NEXT.md

@@ -885,6 +885,15 @@ run one lane at a time; item 4 is disjoint and runs alongside any of them.
      declaration.
    - **There are not a hundred kinds.** The reader's fourteen have them and the checker's have them where a test
      asserts on one; `check.ml` alone has 163 refusal sites and minting an id for each is a sweep nothing reads.
+   - **`Load` and `Shim` do not collect.** They sit between the two collecting phases and still stop at the first
+     refusal, for pass one's reason: an import that could not be resolved leaves a hole the checker would report
+     once per use.
+
+   **One claim checked rather than assumed,** and it is weaker than it first reads: `compile.el` groups `note` with
+   `info` at level 0, and `compilation-skip-threshold` defaults to 1, so `next-error` walks the **errors** with no
+   configuration — that part holds — but steps over the notes unless the threshold is set to 0. The notes are still
+   parsed, coloured and clickable. Labelling them `warning:` would make them navigable and is refused: a note is not
+   a warning.
 
    **What the daemon sees, which the brief asked to be worked out and stated:** the single-diagnostic exception is
    still the single-diagnostic exception. `Session.eval` and the daemon check one form, keep catching `Loc.Error`,

test/test_acceptance.ml

@@ -1909,6 +1909,41 @@ ERR@7 unexpected token: not the kind the caller was reading
     outputs ~opt:"-O0" "unless, now a prelude macro, -O0"
       "programs/macro-unless.flan" unless_out;
 
+    (* An error on code a macro produced says which macro, and it has to be
+       asserted through a real expansion: the tag is put on by [Macro] and
+       defaulted into the diagnostic by [Loc], and a unit test on either half
+       alone would pass with the other one broken.
+
+       [clamp] with the wrong number of arguments expands into a call to a name
+       that does not exist, on purpose -- that is how a prelude macro reports a
+       misuse. So the checker refuses a name the author never wrote, which is
+       exactly the case the field exists for. *)
+    (let src = "(defn f [] i32 (clamp 1 2))\n(defn main [] i32 0)\n" in
+     match
+       Check.program (Parse.program (Reader.read_all ~file:"<expansion>" src))
+     with
+     | _ ->
+       incr failures;
+       print_endline "FAIL  an error in an expansion is refused"
+     | exception Loc.Error d ->
+       (match d.Loc.expansion with
+        | Some (name, _) when name = "clamp" -> ()
+        | Some (name, _) ->
+          incr failures;
+          Printf.printf "FAIL  an error in an expansion names the wrong macro: %s\n"
+            name
+        | None ->
+          incr failures;
+          Printf.printf
+            "FAIL  an error in an expansion names no macro\n        error: %s\n"
+            d.Loc.dmsg);
+       (* And it reaches the printed report, which is the only part a reader
+          ever sees. *)
+       if not (contains (Loc.report d) "expanded from the macro clamp") then begin
+         incr failures;
+         print_endline "FAIL  the report does not say which macro"
+       end);
+
     (* The two ways expansion does not terminate, and they are different
        failures. A ring is a compile-order problem -- each body calls the other
        while the other is being compiled -- and there is no order, so it is