Replace the Idris2 ABI module-wide partiality waiver

[hyperpolymath]

Estate-policy gap

idris2/src/Main.idr uses module-wide %default partial. That is a real totality waiver across the affine front-end executable, not a comment or scanner false positive. The affected boundary includes argument parsing, file I/O orchestration, parser invocation, type checking, and IR emission.

Because Idris2 is the estate ABI language, a global waiver is too broad to serve as the final trust boundary.

Required outcome

• Audit every definition in idris2/src/Main.idr under %default total.
• Make pure parsing, option transformation, and orchestration helpers total where their signatures permit it.
• Represent recoverable failures in result types rather than relying on partial evaluation.
• If an I/O primitive is inherently partial in the available Idris2 library, attach partial only to the smallest boundary and document the exact precondition/failure semantics.
• Publish which functions are total, which boundary remains partial, and why.
• Add a CI totality check.

Acceptance controls

1. The module builds total-by-default.
2. Every remaining local partial is individually documented and gate-visible.
3. A deliberately non-total pure fixture is rejected, proving that the CI gate detects the failure class.
4. Existing affine-front-end behaviour and Rust bridge integration tests continue to pass.

Adding a local annotation or a workflow scaffold is not proof of totality. Keep configured, checked, and proved distinct.