feat(#92): widths need not agree for ==, and match arms join on width

[hyperpolymath]

Implements the #92 ruling across both engines — plus two bugs found while verifying it.

The rule

T-Eq-Word required both operands at the same width. Four ways that was inconsistent with the language itself (evidence in #92):

• tComposeWord already widens to max n m — you could compose two braids you were then forbidden to compare.
• ~ accepted differing widths and, since TG-7, evaluates through the same Braid_equiv.equiv. Identical operands, identical answer, one rejected by the typechecker.
• eqIdBraid/eqBraidId decide "is this braid trivial?" against identity : word 0, so under the old rule they could only fire when the braid was empty. The step relation had rules for a question the typing rule forbade asking.
• braid_equiv.equiv has no width parameter at all.

Lean's tEqWord now takes (n m); infer's .eq case drops the if n = m; OCaml Eq mirrors it. Match arms join on width for words and still require exact agreement otherwise.

The metatheory needed no patching

Progress, Preservation, Determinism, TypeSafety, infer_sound, infer_complete all still hold — lean Tangle.lean reports 0 errors, sorry/axiom gate passes.

infer_sound's proof got simpler: with no if n = m there's no inner split to case on. A restriction whose removal shortens the proof was carrying no weight.

TG-3 regenerated and kernel-checked: 496 obligations, 0 errors. 46 flipped from = none to = some .bool — exactly the identity == braid shape that was unreachable before.

Two bugs found while verifying

1. Statement order. parse_file_recovering did stmts := prog @ !stmts then List.rev on the flattened result. That reversal is correct for an accumulator built by prepending single items (as diagnostics is) — but whole segments were prepended, so every program came out backwards:

def x = 5     parses to    def z = 7
def y = 6      ------->    def y = 6
def z = 7                  def x = 5

Any program whose statements depend on order died with "Unbound variable". The test suites never caught it because they call Tangle.Parser.program directly — only the CLI goes through the recovering path.

2. A false assertion in examples/trefoil.tangle:

assert reversed == braid[s1, s1, s1]     # reversed = reverse(trefoil)

reverse reverses the word and negates exponents, yielding the inverse braid. Verified by invariant: writhe(trefoil) = 3, writhe(reversed) = -3, and writhe is invariant under the braid relations — so they cannot be equal. The assertion had been wrong since it was written; nothing ran the examples until #89. Corrected to braid[s1^-1, s1^-1, s1^-1], which passes.

Result

	before	after
examples evaluating	2/7	7/7
lib/stdlib.tangle	did not typecheck	typechecks
conformance	18/19	18/19 (v11 is the Harvard sub-language, #94)

All seven examples are now in the corpus gate's must-run set, so none can regress.

⚠ Trusted base — registered as A-TG-92.1

The embedding Bₙ ↪ Bₙ₊₁ that justifies cross-width comparison is standard mathematics, but it is asserted in prose, not mechanised — no Lean lemma states it.

What is machine-checked: that the metatheory holds under the widened rule, and that OCaml infer_expr still agrees with Lean infer on the corpus. That distinction is recorded in ASSUMPTIONS.md rather than left implicit.

Tests

6 new typecheck cases, including two negatives — mismatched kinds still rejected, match arms of different kinds still rejected — so widening cannot quietly become "anything compares to anything". Three test_check cases repointed at an error that is still an error (and an assertion helper left unused by the change was put back to work rather than deleted).

🤖 Generated with Claude Code

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved

Removes strict width agreement requirements for equality comparisons and adds match arm width joining across both engines, enabling all 7 example programs to evaluate successfully. No issues found.

Auto-approved and auto-merge armed: No blocking issues found.
Please see Auto-approve Docs for details on setting custom approval criteria. — merges when pipeline and required approvals pass.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}

[gitar-bot]

⚠️ Gitar auto-approved this PR but could not enable auto-merge: auto-merge is disabled for this repository — enable "Allow auto-merge" in the repository settings.

[gitar-bot]

Gitar has auto-approved this PR and enabled auto-merge (configure)