proof(idris2): tighten Ephapax.Affine.Typecheck to %default total (#97)

## Summary

Seventh file in the `%default partial` → `%default total` chain.
Companions: SExpr (#89), Stream (#90), Util (#91), Lexer (#93), AST
(#94), Decode (#96).

Two changes, atomically:

### 1. Fix pre-existing baseline rot

Lines 184–186 had a 3-line layout for `if-then-else` that Idris2 0.8.0
rejects with `Expected 'else'`:

```idris
if not (isLinear tv) then
  Left (LetLinNonLinear name tv)
else do
  ...
```

Reformatted to single-line `if X then Y else do` — matching the
same-pattern usage at line 246–255 in the same file (the `If c t f`
branch). The file now compiles for the first time on the current Idris2
toolchain. **This is independent of the totality work but cannot be
separated** — without the layout fix the file does not parse and no
totality check can run.

### 2. Flip `%default partial → %default total`

No further changes needed. The `check` function's structural recursion
through pattern destructuring (sub-Exprs of compound forms like
`StringConcat a b → check ... a; check ... b`) and the mutual
`check`/`checkBlock`/`numeric`/`litTy` forward-declaration block are all
accepted by Idris2 0.8.0 SCT as terminating.

No `assert_total` / `believe_me` / `covering` escapes anywhere. **Every
definition in the file is now provably total** — including `check` (Expr
typechecker), `checkBlock`, `mergeAffine`, `mergeLinear` (and inner
`findMismatch`), `checkModule` (and inner `addFn` / `checkDecls`).

## Verification

```
$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Affine/Typecheck.idr
2/2: Building Ephapax.Affine.Typecheck (Ephapax/Affine/Typecheck.idr)
$ idris2 --check Ephapax/Affine/Emit.idr   # downstream
4/4: Building Ephapax.Affine.Emit
```

## 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)

## Test plan

- [x] `idris2 --check Ephapax/Affine/Typecheck.idr` builds green under
`%default total`
- [x] Downstream `Ephapax.Affine.Emit` still builds
- [ ] CI green
- [x] No `assert_*` / `believe_me` / `covering` — every definition is
provably total

🤖 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/Affine/Typecheck.idr

@@ -4,7 +4,7 @@ import Data.List
 import Data.Maybe
 import Ephapax.IR.AST
 
-%default partial
+%default total
 
 public export
 data Mode = Affine | Linear
@@ -181,9 +181,7 @@ check mode ctx expr =
       Right (tb, ctx4)
     LetLin name _ val body => do
       (tv, ctx1) <- check mode ctx val
-      if not (isLinear tv) then
-        Left (LetLinNonLinear name tv)
-      else do
+      if not (isLinear tv) then Left (LetLinNonLinear name tv) else do
         let ctx2 = setVars ctx1 (extendVar (MkEntry name tv False) (vars ctx1))
         (tb, ctx3) <- check mode ctx2 body
         checkBoundUsed mode name ctx3.vars