Docs as executable spec: reconcile documented-vs-implemented contradictions

[zharinov]

Problem

At least five documented rules contradict the implementation. For a project whose docs are treated as a constitution, each contradiction is either a code bug or a doc bug — currently it's unresolved which:

1. Array unification: docs/type-system.md describes unification failures that the code can't produce — unify.rs's IncompatibleStructs / IncompatibleArrayElements variants are never constructed.
2. Missing-array defaults: * and + behave differently for missing arrays ([] vs null), contradicting both each other and the docs. Also tracked as part of Single source of truth for capture value semantics (inference vs emission) #420 item 7 — coordinate.
3. Row capture on node patterns: documented legality differs from what the checker accepts.
4. Ref encapsulation: documented scoping of definition captures differs from runtime bubbling. See Single source of truth for capture value semantics (inference vs emission) #420 item 4 — coordinate.
5. Mutual recursion: A = (foo (B)) B = (bar (A)) is documented as OK (each step descends) but the checker rejects it. The checker is arguably right — likely fix the docs.

Also: the project's own CLAUDE.md example run -q '(identifier) @id' matches nothing, because execution is root-anchored. Either fix the example or decide that bare patterns should search the tree — a language-level decision worth recording either way.

The docs/lang-reference.md Supertypes section documents #subtype as accepted but not yet enforced (the pattern collapses to its supertype). This is an intentional deferred-semantics gap — tracked by #417 (interim reject) and #423 (implementation), not accidental drift. The corpus should encode it as such (parses and check-passes unlinked; rejected when linked once #417 lands) rather than flagging it as a contradiction.

Approach

• Turn every example in docs/type-system.md and docs/lang-reference.md into a snapshot test in the conformance corpus (Conformance test layer for the compiler→VM seam #418). Examples that can't run are themselves findings.
• For each of the five contradictions: decide deliberately (change code or change docs) and record the decision in the doc.
• Dead UnifyError variants: either wire them up or delete them — dead error variants hide exactly this class of drift.