Proof-drift: src/types.rs Language enum disagrees with src/abi/PatternCompleteness.idr (Chapel vs C) #41

Discovered while running the docs staleness audit (PR #40).

Both `src/types.rs::Language` and `src/abi/PatternCompleteness.idr::Lang` enumerate 49 named variants + Unknown — but they disagree on which 49.

This means the Idris proof `completeScanForAll` covers a `Lang` constructor (`C`) that doesn't exist in the Rust enum, and fails to cover a Rust `Language` variant (`Chapel`) that the analyzer must handle.

Impact

• The completeness theorem is technically vacuous for `C` (no analyzer dispatch to verify)
• `Chapel` analyzer dispatch is unverified by the proof

Reproduction

```bash
awk '/pub enum Language \{/,/^}/' src/types.rs | grep -E "^\s+[A-Z][a-zA-Z]+(,|$)" | sort > /tmp/rust-langs
grep -E "Rust|Cpp|Chapel|^\s+\|" src/abi/PatternCompleteness.idr # see Lang enum
```

Fix options

1. Add `Chapel` to Idris `Lang`, drop `C` (matches Rust source — preferred if C is not a target).
2. Add `C` to Rust `Language`, drop `Chapel` (matches Idris proof — only if Chapel is being deprecated).
3. Add both to both (enumerate 50 named languages — only if both are real targets).

Option 1 looks correct from the project description ("49 languages" everywhere; CLAUDE.md lists `Chapel` under planned/shipped features; `C` is not mentioned in the README's family breakdown).

Acceptance

• `cargo build --release` still clean
• `idris2 --check src/abi/PatternCompleteness.idr` still total
• The two enumerations are bijective.

cc: filed by audit; no immediate action required, but flagging so `completeScanForAll` is not silently lying.