Proposal
Add an (idiomatic-pattern) for Validation chain over tuple match. case (a, b, c, d, e, f, g) of (Ok, Ok, Ok, ...) => ... blows ambiguity-resolution budgets at N≥5. The Validation applicative chain is the right shape.
Source observation
ProvenBridge's extractLevelData had a 7-tuple case match ((devicesR, zonesR, guardsR, ztR, hasPbxR, pbxIpR, pbxWxR)). Idris2's default %ambiguity_depth of 3 couldn't resolve it; even at 12 the cascade into surrounding code was fragile. Splitting into 4-tuple + 3-tuple matches fixed it. The Validation applicative gives this as one-liner MkRecord <$> a <*> b <*> c <*> ... <*> g.
Suggested patch (LESSONS.md L5)
(pattern
(name "validation-chain-over-tuple-match")
(composition "Validation applicative + <*>")
(purpose "Accumulate errors across N independent extractions without N-tuple matches.")
(anti-pattern "case (a, b, c, d, e, f, g) of (Ok, Ok, Ok, ...) — N>=5 tuple matches blow type inference.")
(sketch "MkRecord <$> a <*> b <*> c <*> d <*> e <*> f <*> g"))
Filed from idaptik Wave 3 pilot. See LESSONS.md and PILOT.md. Idaptik commit hyperpolymath/idaptik@aef38db.
Proposal
Add an
(idiomatic-pattern)for Validation chain over tuple match.case (a, b, c, d, e, f, g) of (Ok, Ok, Ok, ...) => ...blows ambiguity-resolution budgets at N≥5. The Validation applicative chain is the right shape.Source observation
ProvenBridge's
extractLevelDatahad a 7-tuplecasematch ((devicesR, zonesR, guardsR, ztR, hasPbxR, pbxIpR, pbxWxR)). Idris2's default%ambiguity_depthof 3 couldn't resolve it; even at 12 the cascade into surrounding code was fragile. Splitting into 4-tuple + 3-tuple matches fixed it. The Validation applicative gives this as one-linerMkRecord <$> a <*> b <*> c <*> ... <*> g.Suggested patch (LESSONS.md L5)
Filed from idaptik Wave 3 pilot. See LESSONS.md and PILOT.md. Idaptik commit hyperpolymath/idaptik@aef38db.