📝 Rename test-loop "blue" phase to "type"; cite TDD

The type-first spec step was labelled "Blue", which collides with the
Red-Green-Blue convention where blue means the refactor phase (and our
loop already has an explicit Refactor step). Rename phase 1 to Type and
describe the loop as type -> red -> green -> refactor.

Tie the discipline to its established name: Type-Driven Development
(Edwin Brady), quoting the Idris framing -- treat the type as the plan,
let the compiler/type-checker drive you to a program that satisfies it.
Section heading becomes "Testing discipline (type-driven)"; update the
AGENTS.md pointer + anchor. Add "idris" to the cspell dictionary.

De-duplicate: CONTRIBUTING.md no longer re-lists the banned directives
(@ts-ignore, as casts, ...); it links to AGENTS.md "Never do", the
single home for that rule, so the lists can't drift.

AGENTS.md

@@ -35,7 +35,7 @@ Never start a long-lived / blocking process such as `npm run watch`. It runs unt
 ## Read these
 
 - [CONTRIBUTING.md § Rules the tools don't enforce](./CONTRIBUTING.md#rules-the-tools-dont-enforce) — the constraints the linters don't catch; CI/review bounce these. **The most important section.**
-- [CONTRIBUTING.md § Testing discipline (type-first)](./CONTRIBUTING.md#testing-discipline-type-first) — write the `expectTypeOf` (blue) before the `assert` (red); the types are the feature.
+- [CONTRIBUTING.md § Testing discipline (type-driven)](./CONTRIBUTING.md#testing-discipline-type-driven) — write the `expectTypeOf` (type) before the `assert` (red); the types are the feature.
 - [CONTRIBUTING.md § Script prefix convention](./CONTRIBUTING.md#script-prefix-convention) — adding an `npm run` script? reuse an existing prefix or it doesn't belong.
 - [CONTRIBUTING.md § Commit messages](./CONTRIBUTING.md#commit-messages) — gitmoji + imperative + 50/72.
 - [CONTRIBUTING.md § Feedback tiers](./CONTRIBUTING.md#feedback-tiers) — what runs when and at what cost (`watch` / pre-commit / pre-push / `check` / `verify` / `fix` / `maintain` / CI).

CONTRIBUTING.md

@@ -60,16 +60,16 @@ The tools are organized into a feedback ladder. Each tier catches different thin
 
 Run `npm run verify` — the one-shot correctness gate in the table above. Run `npm run maintain` only on a maintenance / update-deps branch.
 
-## Testing discipline (type-first)
+## Testing discipline (type-driven)
 
-For this library the types _are_ the feature — narrowing, `exhaustive()` returns, the `Matcher<T>` contract — so a runtime-only test loop would verify the wrong thing. New behavior is written **type-first**, in a red/green/blue loop:
+For this library the types _are_ the feature — narrowing, `exhaustive()` returns, the `Matcher<T>` contract — so a runtime-only test loop would verify the wrong thing. New behavior follows **type-driven development** (in Edwin Brady's sense): _treat the type as the plan for a program, and use the compiler and type checker as your assistant, guiding you to a complete program that satisfies the type_ ([idris-lang.org](https://www.idris-lang.org/)). Here that plan is the `expectTypeOf` assertion, written first. The loop is **type → red → green → refactor**:
 
-1. **Blue** — write the compile-time expectation first (`expectTypeOf(...).toEqualTypeOf<…>()`) and let `npm run check:tsc` fail on the _type_. The type error is the spec you want to hit before the runtime logic exists.
+1. **Type** — write the compile-time expectation first (`expectTypeOf(...).toEqualTypeOf<…>()`) and let `npm run check:tsc` fail on the _type_. The type error is the spec you want to hit before the runtime logic exists.
 2. **Red** — add the matching runtime assertion (`assert.*`) so `npm run test:unit` now fails on behavior.
 3. **Green** — implement in `src/*.ts` until both the type check and the test pass.
 4. **Refactor** — with the type system and the tests as the safety net, then `npm run verify` as the definition-of-done gate.
 
-This is why every test in the suite pairs an `expectTypeOf(...)` with an `assert.*` — keep them together. Blue-first is also enforced structurally: `npm test` runs `check:tsc` before the test runner, so a wrong type can never be papered over by a passing assertion. Per [AGENTS.md § Never do](./AGENTS.md#never-do), never reach green by suppressing the type system (`@ts-ignore`, `as` casts, `expectTypeOf` removed) — fix the types so both blue and red go green honestly.
+This is why every test in the suite pairs an `expectTypeOf(...)` with an `assert.*` — keep them together. Type-first is also enforced structurally: `npm test` runs `check:tsc` before the test runner, so a wrong type can never be papered over by a passing assertion. Per [AGENTS.md § Never do](./AGENTS.md#never-do), reach green honestly — fix the types so both the type check and the runtime assertion pass, never suppress the ones you can't make pass.
 
 ## Publishing workflow
 

cspell.json

@@ -28,7 +28,8 @@
         "Zilla",
         "kacl",
         "bestikk",
-        "silverwind"
+        "silverwind",
+        "idris"
     ],
     "ignorePaths": ["dist", "node_modules", "coverage", "*.svg", ".gitignore"]
 }