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

The Parser is a hand-written recursive-descent parser with ~30
mutually-recursive Parser combinators threaded through a Stream
record (Int-indexed token buffer). Every parser function decreases
the stream-index on success but the recursion is on a record, not a
structural recursor, so Idris2 0.8.0 SCT cannot detect termination.

Fuel-converting every Parser combinator would require threading a Nat
fuel through ~30 function signatures and ~150 call sites -- a much
larger refactor than the rest of the campaign. Chose the pragmatic
intermediate: `%default covering` instead of `%default total`.

`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*.

The file itself builds clean under `%default covering`. Downstream
Main.idr blocks on a baseline-rot parse error in Affine/Typecheck.idr
that is fixed independently in PR #97 -- unrelated to this PR's scope.

Refs #124 (proof-debt epic), #134 (ephapax totality)
Part of ephapax %default partial -> total campaign: 8/9 files done
(SExpr PR #89; Stream PR #90; Util PR #91; Lexer PR #93; AST PR #94;
Decode PR #96; Typecheck PR #97; Parser here -- the only file
landing as `%default covering` rather than `%default total`).

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