Decision needed: should Word[n] == Word[m] widen, like compose already does? (blocks stdlib + 4 examples) #92

A cross-engine language-design decision, in the same shape as #50. It cannot be made in OCaml alone: Lean's tEqWord is normative and TG-3's 496 kernel-checked obligations tie OCaml's infer_expr to it, so changing one engine silently breaks the differential.

The rule today

| tEqWord (Γ : Ctx) (e₁ e₂ : Expr) (n : Nat) :   -- [T-Eq-Word]
    HasType Γ e₁ (.word n) →
    HasType Γ e₂ (.word n) →                      -- SAME n, both sides
    HasType Γ (.eq e₁ e₂) .bool

Both engines agree with each other. The problem is that the language disagrees with itself, in four separate ways.

Evidence 1 — compose already widens; equality does not

Same file, same type language:

| tComposeWord … : HasType Γ e₁ (.word n) → HasType Γ e₂ (.word m) →
                   HasType Γ (.compose e₁ e₂) (.word (max n m))   -- WIDENS
| tEqWord      … : HasType Γ e₁ (.word n) → HasType Γ e₂ (.word n) →
                   HasType Γ (.eq e₁ e₂) .bool                     -- same width only

So braid[s1] . braid[s2] is fine (Word[2] . Word[3] → Word[3]), but braid[s1] == braid[s2] is a type error. You can build a thing you are not allowed to test. Auto-widening is documented as a language feature at the top of typecheck.ml; equality is the exception.

Evidence 2 — ~ already accepts differing widths, and since TG-7 calls the same function

In adjacent match cases of infer_binop:

| Eq -> …
  | TWord n, TWord m when n = m -> TBool
  | TWord n, TWord m -> type_error "Cannot compare words of differing width: …"

| Isotopy -> …
  | TWord _, TWord _ -> TBool            (* no width check at all *)

Since #87 both operators evaluate through Braid_equiv.equiv — the identical decision procedure. Demonstrated on main:

==  : In definition 'a': Cannot compare words of differing width: Word[2] == Word[3]
~   : typechecks fine, evaluates

Identical operands, identical runtime function, identical answer — one is rejected by the typechecker and the other is not. That is not a design choice anyone made; it is drift.

Evidence 3 — two Lean step rules are all but unreachable

| eqIdBraid : Step (.eq .identity (.braidLit gs)) (.boolLit (isTrivialBraid gs))
| eqBraidId : Step (.eq (.braidLit gs) .identity) (.boolLit (isTrivialBraid gs))

identity : word 0 (tIdentity), so under tEqWord these only ever type when generatorWidth gs = 0 — i.e. when gs = []. The semantics has dedicated rules for "is this braid trivial?", and the typing rule forbids asking. The rules were clearly written expecting cross-width comparison.

Evidence 4 — the decision procedure never cared

braid_equiv.equiv takes two generator lists and reduces u · v⁻¹. It has no width parameter and no width check. Only the typing rule forbids what the implementation already computes correctly.

What it blocks

Four of the five remaining #88 failures are this one rule. (The fifth, recursive scalar functions, is fixed in #91.)

The mathematics

Braid groups embed: Bₙ ↪ Bₙ₊₁ by adding a strand that does nothing. A word on 2 strands is a word on 3 strands that never touches the third. So "are these equal?" across widths is not ill-formed — it is asked in the larger group, which is exactly what equiv already does.

identity == braid[s1, s1^-1] is the most natural phrasing of "is this trivial?", and it is currently a type error.

Options

(a) Widen — Word[n] == Word[m] is well-typed, decided in B_max(n,m).
Matches tComposeWord, matches ~, matches the implementation, un-blocks the stdlib and four examples, and makes eqIdBraid/eqBraidId reachable. Cost: change tEqWord in Lean and Eq in OCaml, re-check Progress/Preservation/Determinism (likely cheap — as with TG-7 the theorems need the rule's shape, not its side condition), and regenerate TG3Differential.lean via tg3_emit.

(b) Keep the restriction; fix the corpus.
Rewrite the stdlib and four examples to avoid cross-width comparison. Cheap and local, but it leaves == stricter than ~ for the same computation, leaves two step rules unreachable, and makes "is this braid trivial?" unsayable via ==. It also means the language's own stdlib is shaped around a rule the implementation doesn't need.

(c) Narrow ~ to match ==.
Consistent, but the wrong direction: it would break examples/isotopy.tangle, which is currently the only example demonstrating the central claim, and it contradicts TG-7 — where the whole point was that equivalence is not syntactic.

Recommendation

(a), with the match-arm width join decided at the same time (the turing_complete case) so the two don't drift apart the way == and ~ just did.

I would take it in one change across both engines, exactly as #87 did — OCaml, Lean, regenerate the TG-3 differential, and tests that distinguish the semantics. Not before a ruling, though: this changes what type-checks, and #50 established that is an owner call.