feat(typecheck): detect duplicate function / type / agent declarations

Roadmap item 1 (parser/typecheck gap-fill). Extends the `DuplicateDefinition`
check from locale/choreography to the remaining name-bearing top-level decls.

`fn`, `type`, and `agent` declarations were *gathered* but silently *last-win*
on redefinition — two `fn f`, two `type T`, or two `agent A` were accepted with
the second quietly shadowing the first. They now error.

Detection is per parsed top-level declaration and within-kind, so an
`agent Name(args)` reference inside a `supervisor children:` list (the
agent-creates-agent pattern used by several examples) is NOT a declaration and
is correctly not flagged. Verified against every example — zero false
positives.

4 new typechecker tests (duplicate fn / type / agent, and the
agent-reference-in-supervisor regression). 901 oo7-core lib tests pass; fmt +
clippy clean.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -6,8 +6,8 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Layer-10 rung 3b (cross-handler residues via agent state — partly runtime, ResidueCell/takeForReverse:Maybe). Also: extend duplicate-definition detection to the other name-bearing decls (functions/types/agents currently last-wins on redefinition). Rocq-9 proof-stack install in progress (see below) to run the rocq canonical-proof-suite locally."
-last_action: "Governance + handover artifacts (branch claude/affirmation-and-handover): added AFFIRMATION.adoc (root, RSR-convention timestamped attestation of current standing — musts met, intends in_progress, blocked/open declared honestly), docs/status/must-intend-wish-2026-06-19.adoc (the full Echidna + 007 must/intend/wish tables), and docs/handover/NEXT-CLAUDE-PROMPT.md (paste-ready handoff with env gotchas). Followed confirmed RSR conventions (SPDX+AsciiDoc+a2ml attestation+contractile vocab); standards-repo AFFIRMATION template not retrievable (standards public but out of session MCP scope; web search 0 results). Banned-token-clean (reworded the believe_me/sorry/etc. examples). PRIOR completed this session: runner awk POSIX-portability fix \\s->[[:space:]] (PR #47 merged) — suite now runs locally; ROCQ 9.0 installed locally (OPAMROOT=/root/.opam3 switch rocq9, via github opam-repository mirror) → 35/37 canonical .v compile; last 3 (mathcomp chain + Coquelicot) walled by github-only network (menhir@gitlab.inria.fr, cmdliner@erratique.ch, coq-released@coq.inria.fr all 403) — CI-only. Echidna = unspecified ecosystem placeholder (no spec). Prior PRs: #46 (import+locale+choreography dup-detection), #45 (just gate), #43 (L10 proofs gated), #42 (rung-3a)."
+next_action: "User roadmap (in order): (1) parser/typecheck gap-fill [DONE: function/type/agent dup-detection this branch] — remaining gap-fill candidates: the `trace { }` standalone-statement parse gap (semantic_analysis_example.007:71 fails), and extend dup-detection to protocols/behaviours/supervisors if wanted. (2) L10 RUNG 3b — cross-handler residues via agent state (partly runtime: residue cell in agent state + evaluator Holding/Spent, ResidueCell/takeForReverse:Maybe). (3) FULL PROOF SUITE GREEN — write M5-yoneda.agda (only agda entry, not-started/stub); the 3 rocq holdouts (M2 mathcomp, E1_ndim+S3_ndim Coquelicot) are CI-only by network policy. (4) CONSOLIDATE."
+last_action: "Roadmap item 1 — extended DuplicateDefinition to FUNCTION/TYPE/AGENT (branch claude/dup-detection-fn-type-agent). These were gathered but silently last-win on redefinition; check_duplicate_definitions now flags two top-level fn/type/agent of the same name (within-kind, per parsed decl, so an `agent Name(args)` ref in a supervisor children: list is NOT a duplicate — verified no false positives across all examples). 4 new tests; 901 oo7-core lib pass; fmt+clippy clean. Also re-verified machine-checking with the local toolchain: ROCQ 35/38 .v compile (3 network-walled), AGDA 0/1 (M5-yoneda not-started), IDRIS2 16/16 incl L10 (EchoResidue+EchoResidueLinear). Prior this session: governance/handover docs (#48), runner awk fix (#47), Rocq 9 local (35/37), #46 import+locale+choreography dup-detection, #45 just gate. Echidna still unspecified placeholder."
 updated: 2026-06-19T21:45:00Z
 
 @blockers:

.machine_readable/session-log.txt

@@ -41,3 +41,5 @@
 [2026-06-18 13:20:34] Gap-fill (a): LOCALE + CHOREOGRAPHY duplicate-name detection on the same branch (extends PR #46 to "duplicate detection for the silently-skipped decls"). Added TypeErrorKind::DuplicateDefinition{kind,name} + check_duplicate_definitions pass (Pass 1c in check_program + _snapshot) flagging two same-named locale or choreography decls; agent_api DUPLICATE_DEFINITION (rename_or_remove). 3 tests (dup-locale, dup-choreography, distinct-locales-OK); 897 oo7-core lib pass; fmt+clippy clean; locales.007/choreography.007/imports.007 all still check OK. Ran cargo test directly (NOT just gate) to avoid assail polluting session-log. ROCQ-9 install attempt 3 progressing in background (/tmp/rocq3.log, OPAMROOT=/root/.opam3): github-mirror opam init succeeded, rocq9 switch building OCaml 4.14.2 then coq.9.0.0+mathcomp from github source; Coquelicot blocked (gitlab.inria.fr 403).
 
 [2026-06-19 21:47:43] Governance + handover artifacts (branch claude/affirmation-and-handover, off latest main 2c52cf6). User asked to (1) store the must/intend/wish status tables in-repo, (2) write a paste-ready prompt for the next 007 Claude, (3) make an AFFIRMATION.adoc per standards-repo guidance, timestamped. Delivered: AFFIRMATION.adoc (root) — RSR-convention attestation (SPDX+AsciiDoc+a2ml attestation ethos+contractile must/intend/wish vocab), timestamp 2026-06-19T21:43:26Z, commit 2c52cf6; affirms musts met (Harvard, L1-L10, honest proofs, RSR hygiene), labels intends in_progress (rung 3b, gap-fill, full suite) and the two owner-side blocks (Actions billing, github-only network) honestly. docs/status/must-intend-wish-2026-06-19.adoc — the full Echidna (thin: placeholder, no spec) + 007 tables. docs/handover/NEXT-CLAUDE-PROMPT.md — paste-ready handoff incl. env gotchas (billing-blocked CI+admin-merge, github-only network, OPAMROOT=/root/.opam3 rocq9 switch, assail-pollutes-session-log, branch/gate discipline). standards-repo AFFIRMATION template NOT retrievable (public but out of session MCP scope; web search 0 results; tree listings errored) so followed confirmed conventions + said so in the doc. Reworded believe_me/sorry/etc. examples out of the docs to stay banned-token-clean. Doc-only; A2ML 6a2 clean. Pushing -> draft PR.
+
+[2026-06-19 23:08:35] Roadmap item 1 (parser/typecheck gap-fill) — extend DuplicateDefinition to FUNCTION/TYPE/AGENT (branch claude/dup-detection-fn-type-agent off main). These three are gathered (gather_function/type/agent_decl) but silently last-win on redefinition; added Function/TypeDecl/Agent arms to check_duplicate_definitions (within-kind, keyed on (kind,name), per parsed top-level decl). SAFETY: text-grep flagged apparent dup agent names in 5 examples, but inspection showed the 2nd occurrence is always `agent Name(args)` in a supervisor children: list (a REFERENCE, not a top-level decl) — so the per-decl check ignores them; confirmed empirically (oo7 check on every example → zero false positives). 4 tests (dup fn/type/agent + agent-reference-in-supervisor-not-a-dup); fixed the regression snippet after learning `agent Name(args)` is only valid in supervisor children:, not as a control_stmt. 901 oo7-core lib pass (was 897); fmt+clippy clean. Also (answering user q on "done intra-body"): re-verified machine-checking with local provers — ROCQ 35/38 .v (3 walled: M2 mathcomp, E1_ndim+S3_ndim Coquelicot), AGDA 0/1 (M5-yoneda not-started), IDRIS2 16/16 incl L10. User roadmap remaining: (2) L10 rung 3b, (3) full proof suite green (write M5 agda; rocq holdouts CI-only), (4) consolidate. Pushing -> draft PR.

CHANGELOG.md

@@ -13,6 +13,7 @@ All notable changes to this project will be documented in this file.
 - **`just gate` — one-command, billing-independent local green-check.** Runs every locally-faithful CI stage in sequence (rustfmt, clippy, `cargo test`, grammar-check, verify-harvard, e2e, `idris2 --check` of all 12 Idris proofs), continues past failures, and prints a per-stage PASS/FAIL/SKIP summary with a non-zero exit on any FAIL. Stages needing an absent toolchain (idris2) or an external GitHub action (A2ML/K9 validators, security scans) self-skip with a notice rather than failing, so it runs anywhere; the rocq canonical-proof-suite (needs Rocq 9) and external manifest/security scans stay CI/nightly-only. Verified GREEN on `main`. Distinct from `just ci` (build/test/lint/verify simulation) and `just check` (fast fmt/lint/test pre-commit).
 - **Import binding-collision detection.** The type checker now validates `import` declarations: every binding an import introduces — an `as` alias, each selective `from … import` item, or a bare `import a.b.c`'s last segment (`c`) — must be unique across the program. A collision (e.g. `import a as x` + `import b as x`, or `from m import abs, abs`) is now a `DuplicateImport` error instead of being silently accepted (imports were previously skipped by the gather pass entirely). Surfaced to agents via `agent_api` code `IMPORT_DUPLICATE_BINDING` (+`rename_import`/`remove_duplicate` remediations). Complements the existing `import_resolver` (which only detects *circular* imports). 4 new typechecker tests (894 `oo7-core` lib tests passing); `examples/imports.007` and the other import-bearing examples are unaffected.
 - **Duplicate locale / choreography detection.** `locale` and `choreography` declarations were likewise silently skipped by the gather pass, so two declarations sharing a name were accepted. Two `locale x = …` (or two `choreography y(…) { … }`) now raise a `DuplicateDefinition` error (agent_api code `DUPLICATE_DEFINITION`). 3 new typechecker tests (897 `oo7-core` lib tests passing); `examples/locales.007` and `examples/choreography.007` are unaffected.
+- **Duplicate function / type / agent detection.** Extends `DuplicateDefinition` to the name-bearing decls that were *gathered but silently last-win* on redefinition: two top-level `fn f`, two `type T`, or two `agent A` now error. Detection is per parsed top-level declaration and within-kind, so an `agent Name(args)` reference in a `supervisor children:` list (the agent-creates-agent pattern) is correctly *not* a duplicate. Verified against every example (no false positives). 4 new typechecker tests (901 `oo7-core` lib tests passing; fmt + clippy clean).
 - **752 tests** (up from 207 at 0.5.0). CRG-C achieved 2026-04-04 for `oo7-core`.
 - **31 multi-language backends** via `mk2_bridge::create_backend_registry()`. Real dispatch to `elixir`, `idris2`, `gleam`, `rescript`, `nickel`, `guile`, `psql`, etc. Tier-5 coprocessor backends (CUDA/Vulkan/Metal/OpenCL/FPGA/TPU/DSP) do phase-1 device discovery with documented "kernel launch is future work" status.
 - **Metainterpreter** (`metainterpreter.rs`, ~3,075 LOC): reify/reflect/step/replay, four modes, 40 inline tests, 18 benches.

crates/oo7-core/src/typechecker.rs

@@ -4674,15 +4674,23 @@ fn check_import_bindings(program: &Program, env: &mut TypeEnv) {
 }
 
 /// Validate that no two top-level declarations of the same kind share a name.
-/// Covers `locale` and `choreography` declarations — previously skipped by the
-/// gather pass, so duplicates were silently accepted. A collision makes the
-/// name ambiguous and is reported as a `DuplicateDefinition` error.
+/// Covers `locale`, `choreography`, `function`, `type`, and `agent`
+/// declarations. The locale/choreography kinds were skipped by the gather pass
+/// entirely; the function/type/agent kinds were gathered but last-win on
+/// redefinition (silently). A within-kind collision makes the name ambiguous
+/// and is reported as a `DuplicateDefinition` error. Detection is per parsed
+/// top-level declaration, so an `agent Name(args)` spawn/instantiation inside a
+/// body is not a declaration and never collides with the `agent Name { … }`
+/// that declares it.
 fn check_duplicate_definitions(program: &Program, env: &mut TypeEnv) {
     let mut seen: HashSet<(&'static str, String)> = HashSet::new();
     for decl in &program.declarations {
         let (kind, name) = match decl {
             TopLevelDecl::Locale(ld) => ("locale", ld.name.clone()),
             TopLevelDecl::Choreography(cd) => ("choreography", cd.name.clone()),
+            TopLevelDecl::Function(fd) => ("function", fd.name.clone()),
+            TopLevelDecl::TypeDecl(td) => ("type", td.name.clone()),
+            TopLevelDecl::Agent(ad) => ("agent", ad.name.clone()),
             _ => continue,
         };
         if !seen.insert((kind, name.clone())) {

crates/oo7-core/src/typechecker_tests.rs

@@ -2096,3 +2096,59 @@ fn distinct_locales_are_not_an_error() {
         );
     }
 }
+
+// ── Duplicate function / type / agent detection ──────────────────────
+//
+// These were gathered but silently last-win on redefinition. Two top-level
+// declarations of the same kind sharing a name now raise DuplicateDefinition.
+// An `agent Name(args)` spawn inside a body is NOT a declaration and must not
+// collide with the `agent Name { … }` that declares it.
+
+#[test]
+fn duplicate_function_is_error() {
+    let src = "@impure fn f() { let x = 1 }\n@impure fn f() { let y = 2 }";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-function error");
+    assert!(
+        has_duplicate_definition(&errs),
+        "two `fn f` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn duplicate_type_is_error() {
+    let src = "type Url = String\ntype Url = Int";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-type error");
+    assert!(
+        has_duplicate_definition(&errs),
+        "two `type Url` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn duplicate_agent_is_error() {
+    let src = "agent A { control { on receive(x: Int) { let y = x } } }\nagent A { control { on receive(x: Int) { let z = x } } }";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-agent error");
+    assert!(
+        has_duplicate_definition(&errs),
+        "two `agent A` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn agent_reference_in_supervisor_is_not_a_duplicate() {
+    // `agent Name(args)` in a supervisor `children:` list references the agent;
+    // it is not a second top-level declaration and must not collide with the
+    // `agent Name { … }` that declares it. (This is the real shape that the
+    // examples use — agent_creates_agent.007, full_language.007, etc.)
+    let src = "agent Worker(caps: Cap[reason]) { control { on receive(x: Int) { let y = x } } }\nsupervisor Sup {\n  strategy: one_for_all\n  max_restarts: 3 per 60 s\n  children: [\n    agent Worker(caps: [reason]),\n  ]\n}";
+    if let Err(errs) = parse_and_check(src) {
+        assert!(
+            !has_duplicate_definition(&errs),
+            "an agent reference in a supervisor must NOT raise DuplicateDefinition, got: {:?}",
+            errs
+        );
+    }
+}