feat(typecheck): detect duplicate locale / choreography declarations

Companion to the import binding-collision check. `locale` and `choreography`
declarations were also silently skipped by `gather_declarations` (the
`_ => {}` arm), so two declarations sharing a name were accepted with the
later one silently winning.

Two `locale x = …` (or two `choreography y(…) { … }`) now raise a
`DuplicateDefinition { kind, name }` error — the name is otherwise ambiguous.
New `check_duplicate_definitions` pass (run in both `check_program` and
`check_program_snapshot`); surfaced to agents via `agent_api` code
`DUPLICATE_DEFINITION`. The variant is kind-generic so it can extend to other
name-bearing declarations later.

3 new typechecker tests (duplicate locale, duplicate choreography, and
distinct-names-are-fine mirroring the examples). 897 oo7-core lib tests pass;
fmt + clippy clean. `examples/locales.007` and `examples/choreography.007`
are unaffected.

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: "Continue parser/typecheck gap-fill: locales + choreographies are still skipped by the gather pass (only TypeDecl/Function/DataBinding/Agent/Protocol handled); apply the same duplicate-name discipline (or richer validation) to them. Then Layer-10 rung 3b (cross-handler residues via agent state — partly runtime, ResidueCell/takeForReverse:Maybe)."
-last_action: "Parser/typecheck gap-fill #1 — IMPORT binding-collision detection. gather_declarations silently skipped imports; added check_import_bindings pass (in check_program + _snapshot) flagging when two imports introduce the same name (alias / from-import item / bare last-segment) as new TypeErrorKind::DuplicateImport, surfaced via agent_api code IMPORT_DUPLICATE_BINDING (+rename/remove remediations). Distinct from existing import_resolver (circular-import only). 4 new typechecker tests; 894 oo7-core lib pass; fmt+clippy clean; imports.007 unaffected (full_language.007's check-fail is pre-existing undefined-symbols). Per user 'do it right not looks-fine': installed local toolchain — A2ML validator symlinked onto PATH, panic-attack (assail) cargo-installed — so `just gate` runs those stages instead of skipping. Prior: just gate (#45), L10 proofs gated (#43), rung-3a (#42), phase-2 (#41), phase-1 (#34)."
+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: "Parser/typecheck gap-fill (PR #46, branch claude/import-binding-collisions): (1) IMPORT binding-collision detection — check_import_bindings flags two imports introducing the same name (alias/item/bare last-segment) as TypeErrorKind::DuplicateImport (agent_api IMPORT_DUPLICATE_BINDING). (2) LOCALE/CHOREOGRAPHY duplicate detection — check_duplicate_definitions flags two same-named locale/choreography decls as TypeErrorKind::DuplicateDefinition (agent_api DUPLICATE_DEFINITION). Both were silently skipped by gather_declarations' _=>{} arm; distinct from import_resolver (circular only). 7 new typechecker tests total; 897 oo7-core lib pass; fmt+clippy clean; locales/choreography/imports.007 unaffected. TOOLCHAIN (per user 'do it right'): A2ML validator symlinked to PATH + panic-attack cargo-installed (just gate now runs a2ml+assail). NOTE assail pollutes session-log — restore from HEAD before commit. ROCQ-9 install: opam.ocaml.org/coq.inria.fr/gitlab.inria.fr all 403 (network is github-only); working attempt uses git+github.com/ocaml/opam-repository as the opam default repo (OPAMROOT=/root/.opam3, switch rocq9) — building OCaml+coq.9.0.0+mathcomp-ssreflect from github source; Coquelicot unavailable (gitlab.inria.fr blocked → its 2 proofs stay CI-only). Prior: just gate (#45), L10 proofs gated (#43), rung-3a (#42)."
 updated: 2026-06-18T12:00:00Z
 
 @blockers:

.machine_readable/session-log.txt

@@ -37,3 +37,5 @@
 [2026-06-18 01:42:28] Added `just gate` — one-command billing-independent local green-check (branch claude/just-gate-local-ci off main). Context: 007 is a PRIVATE repo (confirmed via GitHub API: visibility=private, "Private while dual-use safety/proof/release boundaries mature"), so its GitHub-hosted Actions runs on the owner's GitHub Pro INCLUDED minutes (3,000/mo) — that IS the right mechanism; the instant-reject-404 block is a billing-settings state (exhausted included minutes and/or $0 spending limit / payment), fixable owner-side in Settings → Billing (raise spending limit to allow paid overage, or wait for monthly reset). Self-hosted runners are the free fallback (exempt from the hosted-minute spending cap) but need an always-on host the user controls — overkill if the included minutes are simply topped up. bag-of-actions re-investigated from the actual repo (raw README + file tree, not the earlier small-model summary): it's a Zig/Elixir continuation runtime whose only entrypoints are `bag_of_actions init`/`run` of its own demo; its ci-checks.exs are the checks it runs on ITSELF; no runner/executor/task-submission interface for other repos — confirmed it cannot run 007's CI. Deliverable: new Justfile `gate` recipe (named `gate` to avoid the existing `ci`=build/test/lint/verify and `check`=fmt/lint/test). Runs rustfmt + clippy + cargo test + grammar-check + verify-harvard + e2e + idris2 --check(all 12 proofs); self-skips a2ml (validate-a2ml.sh not on PATH locally) and assail (panic-attack absent); per-stage PASS/FAIL/SKIP summary + nonzero exit on FAIL. Ran end-to-end: GREEN (7 PASS, 2 SKIP, 0 FAIL; e2e internal 49 pass/0 fail/17 intentional-skip). CHANGELOG updated. CI still billing-blocked (maintainer admin-merges #34/#41/#42/#43); local gate is the authoritative substitute. Pushing → draft PR.
 
 [2026-06-18 12:54:48] Parser/typecheck gap-fill #1: IMPORT binding-collision detection (branch claude/import-binding-collisions off main). User chose "Language/parser gap-fill". gather_declarations silently skipped Import/Locale/Choreography (the _ => {} arm); no duplicate-detection existed anywhere; import_resolver catches CIRCULAR imports only. Added TypeErrorKind::DuplicateImport{name} + check_import_bindings pass (wired into check_program AND check_program_snapshot) flagging two imports that introduce the same name (as-alias / from-import item / bare-module last segment), incl. repeated item in one from-import; agent_api code IMPORT_DUPLICATE_BINDING (level 1, rename_import/remove_duplicate). 4 typechecker tests; 894 oo7-core lib pass (was 890); fmt+clippy clean. imports.007 unaffected; full_language.007 check-fail is PRE-EXISTING undefined-symbols. Per user "install them locally, do the job right not looks-fine": symlinked validate-a2ml.sh onto PATH + cargo-installed panic-attack; FULL just gate now runs all 9 stages (rustfmt/clippy/test/grammar-check/verify-harvard/e2e/idris2-proofs/a2ml/assail) = GREEN exit 0. NOTE: panic-attack assail writes cargo-test output into .machine_readable/session-log.txt (had to restore the log from HEAD before committing) - the assail stage pollutes the log, flag/guard before re-running just gate. Only rocq canonical-proof-suite (needs Rocq 9 + mathcomp/Coquelicot/infotheo) remains un-run locally; irrelevant to this Rust change.
+
+[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).

CHANGELOG.md

@@ -12,6 +12,7 @@ All notable changes to this project will be documented in this file.
 - **Layer 10 proofs gated in the canonical proof suite.** The L10 echo-types proofs are now first-class suite entries (`audits/canonical-proof-suite/MANIFEST.a2ml`), gated nightly like the M/S/E classics: new `language` domain `L1` (`proofs/idris2/EchoResidue.idr`, headline `reverseAfterIrreversibleIllTyped`) and `L2` (`proofs/idris2/EchoResidueLinear.idr`, headline `reverseLinear`) — 37 entries total. Each gets the runner's banned-construct scan + `idris2 --check` + symbol-defined check; both verified locally (exit 0, zero banned constructs). The two files' "zero believe_me/assert_total/sorry" disclaimer comments were reworded so the substring banned-scan doesn't false-positive on the very tokens they disclaim. New end-to-end example `examples/named_reversibility.007` exercises `reversible as`/`reverse <name>` through the full pipeline (parse + typecheck + run all pass).
 - **`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.
 - **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/agent_api.rs

@@ -678,6 +678,21 @@ fn type_error_to_agent_error(te: &typechecker::TypeError) -> AgentError {
                 },
             ],
         },
+        TypeErrorKind::DuplicateDefinition { kind, name } => AgentError {
+            code: "DUPLICATE_DEFINITION".to_string(),
+            level: 1,
+            message: te.message.clone(),
+            location: None,
+            context: serde_json::json!({ "kind": kind, "name": name }),
+            remediations: vec![Remediation {
+                strategy: "rename_or_remove".to_string(),
+                description: format!(
+                    "Rename or remove one of the two `{kind} {name}` declarations"
+                ),
+                confidence: 0.8,
+                patch: None,
+            }],
+        },
     }
 }
 

crates/oo7-core/src/typechecker.rs

@@ -361,6 +361,15 @@ pub enum TypeErrorKind {
         /// The colliding binding name.
         name: String,
     },
+    /// Two top-level declarations of the same kind share a name (e.g. two
+    /// `locale x = …` or two `choreography y(…) { … }`). The name is then
+    /// ambiguous, so this is a compile-time error.
+    DuplicateDefinition {
+        /// The declaration kind, e.g. "locale" or "choreography".
+        kind: String,
+        /// The duplicated name.
+        name: String,
+    },
 }
 
 impl fmt::Display for TypeError {
@@ -4664,6 +4673,33 @@ 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.
+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()),
+            _ => continue,
+        };
+        if !seen.insert((kind, name.clone())) {
+            env.error(
+                TypeErrorKind::DuplicateDefinition {
+                    kind: kind.to_string(),
+                    name: name.clone(),
+                },
+                format!(
+                    "duplicate {kind} `{name}`: a {kind} of this name is already \
+                     declared — rename or remove one"
+                ),
+            );
+        }
+    }
+}
+
 pub fn check_program(program: &Program) -> Result<(), Vec<TypeError>> {
     let mut env = TypeEnv::new();
 
@@ -4673,6 +4709,9 @@ pub fn check_program(program: &Program) -> Result<(), Vec<TypeError>> {
     // Pass 1b: validate import declarations (binding-name collisions).
     check_import_bindings(program, &mut env);
 
+    // Pass 1c: reject duplicate locale / choreography declarations.
+    check_duplicate_definitions(program, &mut env);
+
     // Pass 2: type-check all declaration bodies.
     check_declarations(program, &mut env);
 
@@ -4771,6 +4810,9 @@ pub fn check_program_snapshot(program: &Program) -> TypeEnvSnapshot {
     // Pass 1b: validate import declarations (binding-name collisions).
     check_import_bindings(program, &mut env);
 
+    // Pass 1c: reject duplicate locale / choreography declarations.
+    check_duplicate_definitions(program, &mut env);
+
     // Pass 2: type-check all declaration bodies.
     check_declarations(program, &mut env);
 

crates/oo7-core/src/typechecker_tests.rs

@@ -2046,3 +2046,53 @@ fn distinct_imports_are_not_an_error() {
         );
     }
 }
+
+// ── Duplicate locale / choreography detection ────────────────────────
+//
+// Locale and choreography declarations were skipped by the gather pass, so
+// two declarations sharing a name were silently accepted. They now raise
+// DuplicateDefinition. Distinct names (as in the examples) are unaffected.
+
+fn has_duplicate_definition(errs: &[crate::typechecker::TypeError]) -> bool {
+    errs.iter().any(|e| {
+        matches!(
+            e.kind,
+            crate::typechecker::TypeErrorKind::DuplicateDefinition { .. }
+        )
+    })
+}
+
+#[test]
+fn duplicate_locale_is_error() {
+    let src = "locale edge = Edge(region: \"eu\")\nlocale edge = GPU(device: 0)";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-locale error");
+    assert!(
+        has_duplicate_definition(&errs),
+        "two `locale edge` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn duplicate_choreography_is_error() {
+    let src = "choreography deal(a: Agent<Auctioneer>, b: Agent<Bidder>) {\n    a -> b : announce\n}\nchoreography deal(a: Agent<Auctioneer>, b: Agent<Bidder>) {\n    a -> b : announce\n}";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-choreography error");
+    assert!(
+        has_duplicate_definition(&errs),
+        "two `choreography deal` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn distinct_locales_are_not_an_error() {
+    // Mirrors examples/locales.007 — distinct names, no collision.
+    let src = "locale gpu0 = GPU(device: 0)\nlocale cloud = Remote(url: \"https://x.example\")";
+    if let Err(errs) = parse_and_check(src) {
+        assert!(
+            !has_duplicate_definition(&errs),
+            "distinct locales must NOT raise DuplicateDefinition, got: {:?}",
+            errs
+        );
+    }
+}