proof(idris2): tighten Ephapax.Parse.Parser to %default covering (#99)

## Summary

Eighth file in the `%default partial` → totality-tightening chain.
Companions: SExpr (#89), Stream (#90), Util (#91), Lexer (#93), AST
(#94), Decode (#96), Typecheck (#97).

**Distinct outcome for this file**: lands as `%default covering` rather
than `%default total`.

## Why covering, not total

`Parser.idr` is a hand-written recursive-descent parser with ~30
mutually-recursive `Parser X = Stream → Either ParseError (X, Stream)`
combinators. Every parser function consumes ≥1 token from the input
stream on success, but the recursion is on a `Stream` record
(Int-indexed token buffer), not on a structural recursor. Idris2 0.8.0
SCT cannot trace termination through Int-indexed records.

The errors form one large mutual cycle:
```
parseModule → parseDecls → parseDecl → parseFnDecl → parseFnAfterParams →
  parseType → parseSumType → sepBy1 (Util) → sepTail → ... → parseExpr →
  parseLambda → parseType (back to top)
```

Fuel-converting every combinator (the pattern used in SExpr / Stream /
Util / Lexer) would require:

- adding a `Nat` fuel parameter to ~30 function signatures
- updating ~150 call sites
- threading fuel through `where`-bound mutual blocks
(`parsePostfix.{parseCall, parseFst, parseSnd, parsePostfixTail}`,
`parseBlock.{parseBlockExpr, parseBlockTail}`, `parseExpr.{parseLetKw,
...}`, etc.)
- introducing a top-level fuel computed from `bufLen` at every
`parseModuleTokens` entry

Substantially larger than the other 7 files combined. Chose the
pragmatic intermediate annotation.

`covering` is **strictly stronger** than the previous `partial`: it
asserts exhaustive pattern matching has been verified (it has); only
termination is deferred. No `assert_total` / `believe_me`. This is the
truthful annotation for an LL(k) recursive-descent parser whose
recursive structure is the *input grammar*, not the *input data*.

## Verification

```
$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Parser.idr
6/6: Building Ephapax.Parse.Parser (Ephapax/Parse/Parser.idr)
```

## Cross-PR dependency note

Downstream `Main.idr` does not yet compile on `origin/main` due to a
**pre-existing** baseline-rot parse error in
`Ephapax.Affine.Typecheck.idr` (lines 184–186, 3-line `if-then-else`
layout Idris2 0.8.0 rejects). That bug is fixed independently in PR #97.
**Unrelated to this PR's scope** — `Parser.idr` itself builds clean in
isolation; the merge ordering issue clears once #97 lands.

## Refs

- `#124` (proof-debt audit epic)
- `#134` (ephapax totality sub-issue)
- Companions: PR `#89` (SExpr), `#90` (Stream), `#91` (Util), `#93`
(Lexer), `#94` (AST), `#96` (Decode), `#97` (Typecheck)

## Test plan

- [x] `idris2 --check Ephapax/Parse/Parser.idr` builds green under
`%default covering`
- [ ] CI green
- [x] No `assert_*` / `believe_me`; `covering` annotation is justified
above

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

idris2/src/Ephapax/Parse/Parser.idr

@@ -7,7 +7,7 @@ import Ephapax.Parse.Util
 import Ephapax.Parse.ZigBuffer
 import Ephapax.IR.AST
 
-%default partial
+%default covering
 
 parseDecl : Parser Decl
 parseFnDecl : Parser Decl