Agda red on main since #327: unsolved metas in EchoHaplotypeCollapsing.agda:153,159; #328 merged on a startup_failure run

[hyperpolymath]

Measured (2026-09-30)

• Agda on main is red since 1f67753 (PR feat(applications): haplotype collapsing as Echo fiber #327, 2026-09-27). Latest run 36357916037 on 39a7a99: both jobs (cold-check, check) fail with exit 42:

proofs/agda/All.agda:101,1-36
Unsolved metas at the following locations:
  proofs/agda/EchoHaplotypeCollapsing.agda:153,17-33
  proofs/agda/EchoHaplotypeCollapsing.agda:159,33-49
when scope checking the declaration
  open import EchoHaplotypeCollapsing

Both locations are aggregate-values countAggregator … (line 153 example-count, line 159 count-clones-per-haplotype): an implicit argument Agda cannot infer.

• PR feat(applications): haplotype collapsing as Echo fiber #327's own Agda run (36286997524) was already failure; the rule suite recorded the merge as pass, so nothing in the rulesets gates this workflow.
• PR fix(agda): restore main typecheck — carry the fiber invariant in FiberBundle #328 ("restore main typecheck — carry the fiber invariant in FiberBundle", arena bot, merged 39a7a99) did not cure it: main is still red at 39a7a99, and fix(agda): restore main typecheck — carry the fiber invariant in FiberBundle #328's own run 36357715429 was startup_failure, so the change was never typechecked before merge.
• Last green main run: 5f8f65c (2026-09-20).

Acceptance criteria

1. agda.yml green on main at the curing commit, both jobs, with EchoHaplotypeCollapsing still imported from All.agda. The two metas are resolved by supplying the argument (or an instance), not by removing the module from the suite.
2. The curing PR's own Agda run is green before merge (neither feat(applications): haplotype collapsing as Echo fiber #327 nor fix(agda): restore main typecheck — carry the fiber invariant in FiberBundle #328 had one).
3. The startup_failure on fix(agda): restore main typecheck — carry the fiber invariant in FiberBundle #328's head is explained and fixed (lock or allow-list mismatch is the usual cause), or documented as a caller defect with its own issue.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57

[hyperpolymath]

Cured on main. #331 (the fix) landed via the stacked #332, merge commit ab48b286.

The on-main Agda run at that commit is green with real jobs, not a vacuous suite: https://github.com/hyperpolymath/echo-types/actions/runs/36737525917

• check: success, about 2.5 minutes.
• cold-check: success, about 7 minutes.

The other five suites on ab48b286 are green too: CodeQL, Hypatia, Governance, Mirror and Secret Scanner.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57