Corpus debt: 5 examples don't typecheck, 5 conformance valid/ programs don't parse

[hyperpolymath]

Found by wiring examples/ and conformance/ into CI for the first time (scripts/check-corpus.sh). Both directories existed but were executed by nothing — not CI, not the Justfile.

The cost of that was concrete: examples/isotopy.tangle — the file whose whole purpose is to demonstrate the language's central claim — was failing its own assertions, and had been for as long as ~ used free reduction. It only started passing when TG-7 (#87) made ~ decide real braid-group equivalence. Verified by building the pre-TG-7 commit and running it: Runtime error: Assertion failed.

The gate is a ratchet: current state is locked in, nothing may regress, nothing may join the known-bad lists, and anything that starts working must be removed from them (a stale entry fails the build). This issue tracks emptying those lists.

---

A. Examples that parse but do not typecheck (5 of 7)

File	Cause
trefoil.tangle, braids_as_data.tangle	Recursive function returning Num. def length(w) = match w with | identity => 0 | s1 . rest => 1 + length(rest) ... — the recursive call infers as Word[0], so 1 + length(rest) is rejected: "Cannot add Num and Word[0]". The typechecker has no recursive-binding rule, so a function's own return type isn't available while checking its body.
compositional_pd.tangle, tensor_product.tangle	identity == braid[...] is a width mismatch. identity : Word[0] vs Word[n], and T-Eq-Word requires equal widths: "Cannot compare words of differing width: Word[0] == Word[3]". Note the Lean model has dedicated eqIdBraid / eqBraidId step rules for exactly this shape, so the semantics anticipates a comparison the typechecker forbids — worth reconciling deliberately rather than by accident.
turing_complete.tangle	Match arms disagree in width — Word[2] vs Word[0]. Arms must agree, and there is no width subsumption/widening at the match join.

These are genuine language gaps, not broken files. Each is a decision:

1. Recursive typing — add a recursive binding rule (bind the function's declared/inferred type in its own body). Biggest of the three, and the one that unlocks the most idiomatic Tangle.
2. Identity/word comparison — either widen T-Eq-Word so Word[0] (identity) is comparable with any Word[n], or make identity polymorphic in width. The Lean side already models it; this is mostly a decision about which.
3. Match-arm width join — decide whether arms may differ in width and what the join is.

B. conformance/valid/ programs the parser rejects (5 of 19)

File	Unimplemented surface
v02_weave, v08_crossing, v09_twist, v12_weave_expr	weave strands a:Q, b:Q into (...) yield strands b:Q, a:Q — typed strands with a yield strands clause. The parser accepts a simpler weave form; these use the fuller spec syntax.
v11_add_block	add{ 1 + 2 + 3 } — the add{} block (JTV data injection). Not in parser.mly at all.

These are spec-vs-implementation divergences: the conformance corpus encodes surface syntax the parser does not implement. Either the parser catches up, or the spec/corpus is corrected to match the intended language — but the divergence should not sit silent.

C. Incidental: the conformance runner never worked

conformance/run_conformance.sh invoked dune exec -- tangle --parse-only. Both halves were wrong: the executable is main (see compiler/bin/dune), not tangle, and there has never been a --parse-only flag. So every invocation failed, and the suite reported 3/19 — where all three "passes" were invalid/ cases, which "pass" precisely when the command fails. It failed for the wrong reason and scored points for it. Fixed in the same PR; the real number is 14/19.

---

Suggested order: B is mechanical (parser work, well-bounded). A2 and A3 are small typing decisions. A1 (recursive typing) is the substantial one and the most valuable — it is what makes length-style programs expressible, which is most of what the examples are trying to show.

[hyperpolymath]

Status after #91

Half of section A is done. #91 fixed recursive functions returning a scalar — the length shape. Cause was a hard-coded TWord 0 "placeholder" return type used while checking a function's own body, with nothing ever checking the inferred type back against it. Now solved as a fixpoint. (The logic also existed in two places and only one was reached, which is why it survived so long.)

The rest of A, and the stdlib, are one decision — raised as #92.

With recursion fixed, four of the five example failures collapse to a single rule: T-Eq-Word requires both operands at the same width. Same for turing_complete's match-arm variant.

It also blocks something not in this issue's original scope: lib/stdlib.tangle does not typecheck — Cannot compare words of differing width: Word[2] == Word[0]. The language's own standard library is unusable for the same reason.

Evidence gathered in #92, briefly:

• tComposeWord widens to max n m; tEqWord does not — you can compose braids you are not allowed to compare.
• ~ already accepts differing widths and, since feat(tg-7): == on braids decides braid-group equivalence (#50 ruling) #87, calls the same function as ==. Identical operands, identical answer, one rejected.
• Lean's eqIdBraid / eqBraidId step rules are unreachable except when the braid is empty.
• braid_equiv.equiv has no width parameter at all.

That needs a ruling before it can be implemented, since it changes what type-checks across both engines and requires regenerating the TG-3 differential.

Remaining in this issue

• A1 — recursive functions returning Num (fix(typecheck): infer recursive functions' return type by fixpoint (#88) #91)
• A2/A3 — == and match-arm widths → blocked on Decision needed: should Word[n] == Word[m] widen, like compose already does? (blocks stdlib + 4 examples) #92
• B — conformance/valid/ parse failures: typed weave … yield strands (v02/v08/v09/v12) and add{} blocks (v11). Untouched; independent of Decision needed: should Word[n] == Word[m] widen, like compose already does? (blocks stdlib + 4 examples) #92 and of each other.

[hyperpolymath]

Both sections are done.

Section A — examples that did not typecheck

• A1 recursive scalar functions — fix(typecheck): infer recursive functions' return type by fixpoint (#88) #91. The return type was seeded with a hard-coded TWord 0 "placeholder" and never checked back against the inferred body type; now solved as a fixpoint. (The logic also existed in two places with only one reachable, which is how it survived.)
• A2/A3 widths on == and match arms — feat(#92): widths need not agree for ==, and match arms join on width #95, under the Decision needed: should Word[n] == Word[m] widen, like compose already does? (blocks stdlib + 4 examples) #92 ruling. Widened in both engines; metatheory re-verified with no proof edits needed, TG-3 regenerated and kernel-checked at 496 obligations.

Section B — conformance programs that did not parse

• v02, v08, v09, v12 — feat(parser): weave is an expression, not only a statement (#88 B) #93. They use weave as a definition body; it was a statement only, and as a statement it is inert (eval is a no-op, the computed Tangle[A,B] is discarded). Now accepted in definition-body position — deliberately not as a general expression, which introduced a grammar ambiguity.
• v11 add{} — split out as Implement the Harvard data sub-language: add{ ... } blocks #94. Not a parse gap: it is the Harvard data sub-language, 288 lines of spec across 12 sections with its own type system, environments, typing judgement and Embed/Unembed.

Two bugs found by actually running things

• The CLI reversed every program's statement order. parse_file_recovering prepended whole segments then List.rev'd the flattened list. Test suites missed it entirely — they call Tangle.Parser.program directly and never touch the recovering path.
• examples/trefoil.tangle asserted something false — reverse(trefoil) == trefoil, when reverse yields the inverse braid. Proven false by invariant: writhe +3 vs −3.

Result

	at filing	now
examples evaluating	2/7	7/7
conformance	14/19 (a fake 3/19 before #89)	18/19
lib/stdlib.tangle	did not typecheck	typechecks

All seven examples are in the corpus gate's must-run set, so none can silently regress. The single remaining known gap is v11_add_block, tracked in #94.