From 56b818908a274124667368d09bd5c266dfc641cd Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 30 Sep 2026 11:59:01 +0100 Subject: [PATCH] fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `countAggregator`'s group-by key `K` is phantom in `GroupAggregator` (never mentioned by `agg`), so Agda's unifier cannot solve it from `V`, `M`, or the result type at either `aggregate-values countAggregator …` call site (line 153 `example-count`, line 159 `count-clones-per-haplotype`). Supply it explicitly as `Haplotype`, the key this module actually groups clones by (the GROUP BY analogue the surrounding comment names) — semantically honest, not just a syntactically convenient placeholder. Reproduced the unsolved metas verbatim against agda 2.6.4.3 with stdlib v2.3 + absolute-zero@3ff5cee (the pins agda.yml uses), fixed both sites, and confirmed a clean typecheck of All.agda, Smoke.agda, characteristic/All.agda, examples/All.agda, and EchoImageFactorizationPropCubical.agda (the full `check` job recipe). A mutant reverting only the `example-count` site reproduced the unsolved meta at exactly that line while `count-clones-per-haplotype` stayed solved, confirming the fix is what clears each site. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57 --- proofs/agda/EchoHaplotypeCollapsing.agda | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/proofs/agda/EchoHaplotypeCollapsing.agda b/proofs/agda/EchoHaplotypeCollapsing.agda index fb5d05e..225cd1a 100644 --- a/proofs/agda/EchoHaplotypeCollapsing.agda +++ b/proofs/agda/EchoHaplotypeCollapsing.agda @@ -150,13 +150,21 @@ clone-count-aggregation G = aggregation-as-fold G example-clones : List Clone example-clones = clone₁ ∷ clone₂ ∷ [] -example-count : aggregate-values countAggregator example-clones ≡ 2 +example-count : aggregate-values {K = Haplotype} countAggregator example-clones ≡ 2 example-count = refl -- Count clones per haplotype via monoid fold (the GROUP BY analogue). -- In production: groupByKey + fold, not filter + length, to stay O(n). +-- +-- `K` (the group-by key) is genuinely phantom in `GroupAggregator`/ +-- `countAggregator` (issue #175's `agg` field never mentions it), so +-- nothing here forces Agda's unifier to solve it from `V`, `M`, or the +-- result type — it must be supplied. `Haplotype` is the key this +-- aggregator is used to group by in this module (the GROUP BY +-- analogue the comment above names), so it is also the semantically +-- honest choice, not just a syntactically convenient one. count-clones-per-haplotype : List Clone → ℕ -count-clones-per-haplotype cs = aggregate-values countAggregator cs +count-clones-per-haplotype cs = aggregate-values {K = Haplotype} countAggregator cs ------------------------------------------------------------------------ -- 5. Choreographic framing: Raw ⊑ Collapsed