`main` does not type-check: `SafeJson.Proofs.appendLengthInc` has swapped `lengthSnoc` args, and the Idris build is not gating merges

[hyperpolymath]

Two linked problems

1. main currently fails idris2 --build proven.ipkg

src/Proven/SafeJson/Proofs.idr (appendLengthInc, introduced by #127) calls:

appendLengthInc v arr =
  cong Just (trans (lengthSnoc arr v) (plusCommutative 1 (length arr)))

Data.List.Equalities.lengthSnoc is element-first — lengthSnoc : (x : a) -> (xs : List a) -> length (xs ++ [x]) = S (length xs). So the correct call is lengthSnoc v arr; lengthSnoc arr v does not type-check:

Error: While processing right hand side of appendLengthInc. When unifying:
    JsonValue
and:
    List ?a
Mismatch between: JsonValue and List ?a.

Proven.SafeJson.Proofs:208:36--208:37

Because the module fails to elaborate, every proof in SafeJson.Proofs is currently unchecked on main.

Reproduced on a clean Idris2 v0.8.0 + contrib install (the exact toolchain .github/workflows/idris2-ci.yml provisions: chezscheme + make bootstrap, branch v0.8.0):

1/5: Building Proven.Core
2/5: Building Proven.SafeJson.Parser
3/5: Building Proven.SafeJson.Access      (warning: unreachable deletePath clause — pre-existing)
4/5: Building Proven.SafeJson
5/5: Building Proven.SafeJson.Proofs       ← Error: Mismatch JsonValue vs List ?a

The fix (lengthSnoc v arr) is in #144 (and on #138's branch). With it, all five SafeJson modules build with 0 errors.

Note: #127's PR description quotes the proof as lengthSnoc arr v and calls it "(contrib)" — the argument order was simply never checked against the actual contrib signature.

2. The Idris build is not gating merges (root cause)

This is the more important problem: a non-compiling change reached main because the Idris build check did not block the merge.

Evidence from #127:

• created 2026-05-30T18:50:58Z, merged 2026-05-30T18:53:32Z — ~2.5 minutes later
• a cold-cache build (0.8.0) / verify-idris-build takes ~20 min (bootstrap + typecheck, per the workflow's own comments)
• proof(SafeJson): DISCHARGE appendLengthInc via lengthSnoc + plusCommutative (proven#90 #107 #119) #127's build (0.8.0) and verify-idris-build check runs are still recorded as queued — i.e. they had not completed (let alone passed) at merge time
• the only check that had reported was SonarCloud Code Analysis (success)

So a green SonarCloud + a fast manual merge let broken Idris through. The same pattern is visible across recent proof PRs: the Idris jobs sit queued for a long time while merges proceed.

Suggested remediation

1. Land the fix (proof(SafeJson): fix appendLengthInc so the module compiles (completes #138) #144) so main compiles again.
2. Make the Idris build a required status check on main (branch protection): at minimum build (0.8.0); ideally also verify-idris-build. Until it's required, "merged green" does not imply "type-checks."
3. Reduce Idris CI latency / queue saturation so requiring it is practical — e.g. cache the Idris2 build (the workflow already has an actions/cache step keyed on version+OS; confirm it's hitting), or split the per-module --check matrix so the gating job is fast. The estate-wide 40-job concurrency ceiling noted in idris2-ci.yml is part of why these jobs sit queued.
4. Consider a fast pre-merge idris2 --check src/Proven/SafeJson/Proofs.idr-style smoke (cone check) as a required gate that runs in well under a minute, with the full matrix kept as non-blocking/post-merge.

Acceptance

• idris2 --build proven.ipkg is green on main
• The Idris build is a required status check on main
• A PR that breaks idris2 --build cannot be merged green

Refs #127 (origin of the swapped args), #138 / #144 (the fix).