proof(idris2): tighten Ephapax.IR.AST to %default total (#94)

## Summary

Fifth file in the `%default partial` → `%default total` chain.

Single-line change: `%default partial` → `%default total`. The 6
`covering` markers already in the file (Eq Expr, Show Expr, Eq Decl,
Show Decl, Eq Module, Show Module) cover the interface-dispatch totality
blind spot Idris2 0.8.0 has around the `showPrec` / `(/=)` defaults
across nested data instances — those markers stay, nothing new is added.

I verified empirically: removing the existing `covering` markers, even
one at a time, makes the build fail with `showPrec -> show -> showPrec
-> show` (Show side) and `(/=) -> (==) -> (/=) -> (==)` (Eq side) loops.
These are *not* unsoundness; the recursion is genuinely structural.
Idris2 just can't trace the decrease through the interface defaults.
`covering` is the project's existing escape and stays.

## What gets stricter

About ten previously-implicitly-partial definitions are now provably
total under the file default: `Eq Linearity`, `Eq BaseTy`, `Eq Ty`, `Eq
Literal`, `Eq BinOp`, `Eq UnaryOp`, the matching `Show` instances, and
`isLinear`. The data-only declarations are unaffected.

No `assert_total` / `believe_me` escapes.

## Verification

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

## Refs

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

## Test plan

- [x] `idris2 --check Ephapax/IR/AST.idr` builds green under `%default
total`
- [x] Downstream `Ephapax.Parse.Parser` still builds
- [ ] CI green
- [x] No new `covering` markers; no `assert_*` / `believe_me`

🤖 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/IR/AST.idr

@@ -1,6 +1,6 @@
 module Ephapax.IR.AST
 
-%default partial
+%default total
 
 public export
 data Linearity = Linear | Unrestricted