Equality checking revisits a shared constructor DAG exponentially

[jasisz]

What I did

bun bend2/main.ts shared_tree_equality.bend --check-only

type N is Data:
  Z{}
  S{p: N}

type T is Data:
  L{}
  B{l: T, r: T}

def d(n: N) -> T:
  match n:
    case Z{}:
      L{}
    case S{p}:
      +x = d(p)
      B{x, x}

def n() -> N:
  S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{S{Z{}}}}}}}}}}}}}}}}}}}}}}}}}

def boom() -> {d(n()) == d(n()) : T}:
  {==}

What happened

The file is accepted, but equality checking takes about 1.9 seconds. Increasing only the number of S constructors makes the time grow exponentially even though d returns a linearly sized DAG: each B shares the same x in both fields.

I generated otherwise identical files and measured parse_book plus book_valid in one Bun process:

Depth	Check time
18	28 ms
20	103 ms
22	417 ms
24	1.85 s
25	4.37 s
26	8.84 s
27	16.50 s

The depth-27 source is 314 bytes without formatting whitespace. As a control, changing only B{x, x} to B{x, L{}} at depth 24 reduces the same check from 1.72 seconds to 8.2 milliseconds.

Why it happens

Weak-head normalization preserves the let sharing. A demanded value becomes a share cell, and constructor fields are themselves placed in cells when that value is filled (bend.ts:2892-2901, bend.ts:3018-3032). Each side of the equation therefore normalizes to a DAG with one node per level.

term_compare only short-circuits when the left and right objects are identical. The two independently written calls d(n()) produce distinct left and right cells, so that shortcut does not apply (bend.ts:3194-3201). The constructor case then compares both fields independently (bend.ts:3277-3279). Both fields contain the same already compared pair of share cells, but the comparison has no visited-pair cache, so it walks that sub-DAG twice. The recurrence is approximately C(n) = 2 C(n - 1).

This is distinct from #984: that issue expands duplicated global quantity references while normalizing a definition DAG. Here normalization preserves the local sharing, but structural equality repeatedly traverses the same pair of normalized nodes. It is also separate from #983, which is in term_descend and uses literal-pattern suffixes.

Expected behavior

Equality checking should preserve the linear sharing already present in the normalized terms. Memoizing compared node pairs for one term_compare call would make this reproducer linear in the depth of d(n()).

Version

bend 2.0.25
commit a49524265bdfa5753a4bf38e25f0574a705dd868
Bun 1.4.2
Darwin arm64
Apple clang version 21.0.0 (clang-2100.0.123.102)