feat(typecheck): detect import binding-name collisions

`gather_declarations` silently skipped `import` declarations entirely, so two
imports introducing the same name were accepted without complaint. The type
checker now validates them.

Every binding an import introduces — an `as` alias, each selective
`from … import` item, or (for a bare `import a.b.c`) the last path segment
`c` — must be unique across the program. A collision makes that name
ambiguous at use sites and is now a `DuplicateImport` error:

    import agents.research as x
    import agents.review   as x     -- error: `x` bound twice

    from std.math import abs, abs   -- error: `abs` imported twice

New `TypeErrorKind::DuplicateImport { name }` + a `check_import_bindings` pass
(run in both `check_program` and `check_program_snapshot`); surfaced to agents
via `agent_api` code `IMPORT_DUPLICATE_BINDING` with `rename_import` /
`remove_duplicate` remediations. This is distinct from the existing
`import_resolver`, which only detects *circular* imports.

4 new typechecker tests (alias collision, alias-vs-item collision, duplicate
item in one `from`, and distinct-imports-are-fine mirroring
`examples/imports.007`). 894 oo7-core lib tests pass; fmt + clippy clean.
`examples/imports.007` and the other import-bearing examples are unaffected.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Layer-10 rung 3b: cross-handler residues through agent state — residue cell in agent state + evaluator runtime Holding/Spent (ResidueCell, takeForReverse:Maybe) + EchoResidueLinear bridge lemma; then continue parser gap fill (types, imports, locales, choreographies)"
-last_action: "Hardened + gated what landed: (1) gated the L10 echo-types proofs in the canonical-proof-suite MANIFEST — new 'language' domain L1 (EchoResidue.idr / reverseAfterIrreversibleIllTyped) + L2 (EchoResidueLinear.idr / reverseLinear), 37 entries total; reworded their 'zero believe_me/assert_total/sorry' disclaimer comments so the substring banned-scan doesn't false-positive; verified runner-style (banned-clean, idris2 --check exit 0, symbol sig+clause present). (2) Added examples/named_reversibility.007 exercising reversible-as/reverse-name end-to-end (oo7 parse + check + run all PASS). Decided NOT to regenerate REPORT.a2ml locally (no Rocq 9 here → would falsely downgrade rocq entries; nightly CI regenerates). bag-of-actions repo evaluated as a CI-billing workaround and ruled out (it's an Elixir/Zig continuation runtime, not a GitHub Actions runner). Prior: phase-3 rung-3a (PR #42 merged), phase-2 (PR #41), phase-1 (#34), CI gates (#38), 6a2 (#39), estate (#40)"
-updated: 2026-06-15T18:15:00Z
+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)."
+updated: 2026-06-18T12:00:00Z
 
 @blockers:
 - id: proof-debt

.machine_readable/session-log.txt

@@ -35,3 +35,5 @@
 [2026-06-15 18:13:25] Session continued (in-site, billing still blocked): HARDEN + GATE on branch claude/gate-l10-proofs off main (post-#42-merge). User asked whether the CI billing block could be solved via the hyperpolymath/bag-of-actions repo; investigated (search_repositories + WebFetch of its public README): bag-of-actions is an early-stage Elixir/Zig/WASM distributed-continuation runtime ("mobile continuations / Batons"), NOT a GitHub Actions runner — no Actions integration, no webhook/job scheduling, no arbitrary-task CLI. Cannot run 007's CI; also can't add it to MCP scope (no add_repo this session). Reported; user directed "continue in site." Chose (via AskUserQuestion) "Harden + gate what landed". Delivered: (1) Gated the L10 proofs in audits/canonical-proof-suite/MANIFEST.a2ml — new 'language' domain, L1=EchoResidue.idr (headline reverseAfterIrreversibleIllTyped), L2=EchoResidueLinear.idr (headline reverseLinear); 37 entries total, paren-balanced (490/490), runner awk parses both with correct prover/path/symbol. CRITICAL fix: scan_banned uses grep -qF (substring, whole file) so the two files' own "ZERO believe_me / assert_total / sorry" disclaimer comments would have false-flagged them as stub — reworded all 4 comment lines to "no escape hatches" phrasing (meaning preserved, banned tokens gone). Verified runner-style (the runner cd's into dirname + checks basename, so module EchoResidue matches EchoResidue.idr — my first repo-root test wrongly failed on module-name-vs-path): both exit 0, banned-scan 0 hits, verify_idris2_symbol sig+clause PASS for both headlines. Did NOT regenerate REPORT.a2ml locally (coqc 8.18 can't parse From Stdlib → would falsely downgrade the ~30 rocq entries that need Rocq 9; nightly CI regenerates with full toolchain). (2) New e2e example examples/named_reversibility.007 (agent NamedReversal, on receive, reversible as undo { } + reverse undo in one handler) — built oo7 and ran all three e2e sections: parse PASS, check PASS ("type check passed"), run PASS. CHANGELOG + 6a2 STATE updated; A2ML 6a2 validate clean. Pushing to claude/gate-l10-proofs → draft PR. CI remains billing-blocked (maintainer admin-merges, as with #40/#41/#42); everything verified locally.
 
 [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.

CHANGELOG.md

@@ -11,6 +11,7 @@ All notable changes to this project will be documented in this file.
 - **Layer 10 phase 3 (rung 3a) — named residues within a body.** New surface syntax `reversible as <name> { … }` binds the echo residue to a name; `reverse <name>` replays it (anonymous `reversible {…}`/`reverse {…}` unchanged). The named residue is tracked per body as a `Holding(Linear<Echo<T>>)` cell that `reverse` transitions to `Spent` — the static mirror of `ResidueCell` (Holding/Spent) in `EchoResidueLinear.idr`. Same affine/linear discipline: double `reverse <name>` is rejected (cell already `Spent`); a never-replayed binding is **not** an error; named residues are scoped per body (no cross-body leak). Additive AST variants `ReversibleAs`/`ReverseNamed` (existing variants untouched); grammar (`grammar.pest` + `spec/grammar.ebnf`), parser, typechecker (`named_residues` map + per-function/handler isolation), and the eval/codegen/formatter/dual-ast/metainterpreter/CFG/oracle pipeline all threaded. 2 parser + 5 typechecker tests (890 `oo7-core` lib tests passing; fmt clean, clippy `-D warnings` exit 0). Remaining rung 3b: cross-handler residues through agent state (irreducibly partly runtime — `takeForReverse : Maybe`). Spec: TYPE-SYSTEM-SPEC §11b.5; docs `docs/echo-residue-integration.adoc`.
 - **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.
 - **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

@@ -655,6 +655,29 @@ fn type_error_to_agent_error(te: &typechecker::TypeError) -> AgentError {
                 },
             ],
         },
+        TypeErrorKind::DuplicateImport { name } => AgentError {
+            code: "IMPORT_DUPLICATE_BINDING".to_string(),
+            level: 1,
+            message: te.message.clone(),
+            location: None,
+            context: serde_json::json!({ "binding": name }),
+            remediations: vec![
+                Remediation {
+                    strategy: "rename_import".to_string(),
+                    description: format!(
+                        "Give one import a distinct name with `as` (e.g. `import … as {name}2`)"
+                    ),
+                    confidence: 0.8,
+                    patch: None,
+                },
+                Remediation {
+                    strategy: "remove_duplicate".to_string(),
+                    description: format!("Remove the redundant import that re-introduces `{name}`"),
+                    confidence: 0.7,
+                    patch: None,
+                },
+            ],
+        },
     }
 }
 

crates/oo7-core/src/typechecker.rs

@@ -354,6 +354,13 @@ pub enum TypeErrorKind {
         /// Human/agent-readable explanation of which residue is missing.
         detail: String,
     },
+    /// Two import declarations introduce the same binding name — an `as` alias,
+    /// a selective `from … import` item, or a bare module's last path segment.
+    /// The name is then ambiguous at use sites, so this is a compile-time error.
+    DuplicateImport {
+        /// The colliding binding name.
+        name: String,
+    },
 }
 
 impl fmt::Display for TypeError {
@@ -4617,12 +4624,55 @@ fn collect_warnings_for_type(
 /// effect types (L8), and path types (L9). These features are parsed
 /// and stored in the type IR but their constraints are not verified.
 /// Using them without awareness of this creates false confidence.
+/// Validate import declarations: every binding name an import introduces must
+/// be unique across all imports in the program. The name an import introduces
+/// is its `as` alias, or each selective `from … import` item, or — for a bare
+/// `import a.b.c` — the last path segment (`c`). A collision makes that name
+/// ambiguous at use sites, so it is reported as a `DuplicateImport` error
+/// (this also catches a repeated item within one `from … import a, a`).
+fn check_import_bindings(program: &Program, env: &mut TypeEnv) {
+    // binding name -> the module path that first introduced it (for the message)
+    let mut seen: HashMap<String, String> = HashMap::new();
+    for decl in &program.declarations {
+        let TopLevelDecl::Import(imp) = decl else {
+            continue;
+        };
+        let path = imp.path.join(".");
+        let names: Vec<String> = if !imp.items.is_empty() {
+            imp.items.clone()
+        } else if let Some(alias) = &imp.alias {
+            vec![alias.clone()]
+        } else if let Some(last) = imp.path.last() {
+            vec![last.clone()]
+        } else {
+            Vec::new()
+        };
+        for name in names {
+            if let Some(first) = seen.get(&name) {
+                env.error(
+                    TypeErrorKind::DuplicateImport { name: name.clone() },
+                    format!(
+                        "import binding `{name}` is introduced more than once \
+                         (already bound by `{first}`, re-bound by `{path}`); \
+                         rename one with `as`, or drop the duplicate"
+                    ),
+                );
+            } else {
+                seen.insert(name, path.clone());
+            }
+        }
+    }
+}
+
 pub fn check_program(program: &Program) -> Result<(), Vec<TypeError>> {
     let mut env = TypeEnv::new();
 
     // Pass 1: gather all declarations.
     gather_declarations(program, &mut env);
 
+    // Pass 1b: validate import declarations (binding-name collisions).
+    check_import_bindings(program, &mut env);
+
     // Pass 2: type-check all declaration bodies.
     check_declarations(program, &mut env);
 
@@ -4718,6 +4768,9 @@ pub fn check_program_snapshot(program: &Program) -> TypeEnvSnapshot {
     // Pass 1: gather all declarations.
     gather_declarations(program, &mut env);
 
+    // Pass 1b: validate import declarations (binding-name collisions).
+    check_import_bindings(program, &mut env);
+
     // Pass 2: type-check all declaration bodies.
     check_declarations(program, &mut env);
 

crates/oo7-core/src/typechecker_tests.rs

@@ -1983,3 +1983,66 @@ fn l10_phase3_named_residue_does_not_leak_across_functions() {
         errs
     );
 }
+
+// ── Import binding-collision detection ───────────────────────────────
+//
+// Two import declarations that introduce the same binding name — an `as`
+// alias, a selective `from … import` item, or a bare module's last path
+// segment — make that name ambiguous, raising DuplicateImport. Distinct
+// imports (as in examples/imports.007) are unaffected.
+
+fn has_duplicate_import(errs: &[crate::typechecker::TypeError]) -> bool {
+    errs.iter().any(|e| {
+        matches!(
+            e.kind,
+            crate::typechecker::TypeErrorKind::DuplicateImport { .. }
+        )
+    })
+}
+
+#[test]
+fn import_alias_collision_is_error() {
+    let src = "import agents.research as x\nimport agents.review as x";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-import error");
+    assert!(
+        has_duplicate_import(&errs),
+        "two imports aliased `x` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn import_item_vs_alias_collision_is_error() {
+    // An `as` alias and a selective item that share a name still collide.
+    let src = "import std.math as helper\nfrom std.ops import helper";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-import error");
+    assert!(
+        has_duplicate_import(&errs),
+        "alias `helper` vs imported item `helper` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn duplicate_item_in_one_from_import_is_error() {
+    let src = "from std.math import abs, abs";
+    let errs = parse_and_check(src).expect_err("expected a duplicate-import error");
+    assert!(
+        has_duplicate_import(&errs),
+        "`abs` imported twice in one `from` must collide, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn distinct_imports_are_not_an_error() {
+    // Mirrors examples/imports.007 — distinct bindings, no collision.
+    let src = "import std.collections\nimport agents.research_team as team\nfrom std.math import sqrt, abs";
+    if let Err(errs) = parse_and_check(src) {
+        assert!(
+            !has_duplicate_import(&errs),
+            "distinct imports must NOT raise DuplicateImport, got: {:?}",
+            errs
+        );
+    }
+}