A linear chain of quantity definitions makes kind checking exponential

[jasisz]

A linear chain of quantity definitions makes kind checking exponential

What I did

I defined each quantity as the meet of two references to the previous quantity, then used the final quantity as a datatype's declared kind. This is the complete 991-byte reproducer.

import Base

def q0() -> Quant:
  &1

def q1() -> Quant:
  q0 <&> q0

def q2() -> Quant:
  q1 <&> q1

def q3() -> Quant:
  q2 <&> q2

def q4() -> Quant:
  q3 <&> q3

def q5() -> Quant:
  q4 <&> q4

def q6() -> Quant:
  q5 <&> q5

def q7() -> Quant:
  q6 <&> q6

def q8() -> Quant:
  q7 <&> q7

def q9() -> Quant:
  q8 <&> q8

def q10() -> Quant:
  q9 <&> q9

def q11() -> Quant:
  q10 <&> q10

def q12() -> Quant:
  q11 <&> q11

def q13() -> Quant:
  q12 <&> q12

def q14() -> Quant:
  q13 <&> q13

def q15() -> Quant:
  q14 <&> q14

def q16() -> Quant:
  q15 <&> q15

def q17() -> Quant:
  q16 <&> q16

def q18() -> Quant:
  q17 <&> q17

def q19() -> Quant:
  q18 <&> q18

def q20() -> Quant:
  q19 <&> q19

def q21() -> Quant:
  q20 <&> q20

def q22() -> Quant:
  q21 <&> q21

def q23() -> Quant:
  q22 <&> q22

def q24() -> Quant:
  q23 <&> q23

def q25() -> Quant:
  q24 <&> q24

def q26() -> Quant:
  q25 <&> q25

type D is Kind(q26):
  C{f: Unit -> Unit}

def main() -> Unit:
  Unit{}

I generated otherwise identical files ending at different depths and ran each with bun bend2/main.ts FILE --check-only.

What happened

All files check successfully, but the time grows exponentially while the source grows linearly.

Final definition	Wall time
q18	0.15 s
q20	0.22 s
q22	0.48 s
q24	1.61 s
q26	6.36 s
q28	25.95 s

Adding two definitions multiplies the expensive part by approximately four. Extrapolating the measured curve, only a few more short definitions are enough to hold the checker for tens of seconds or minutes.

Why it happens

The definitions themselves are cheap to validate because each qN body only needs both references to infer as Quant. The exponential work begins when constructor validation checks the function field's kind against the declared Kind(q26).

Kind comparison weak-head normalizes the declared quantity. Each qN unfolds to qN-1 <&> qN-1, and the meet normalizer evaluates both occurrences independently. Global references are not shared or memoized, so normalizing qN performs twice the work of normalizing qN-1. bend.ts:2920-3057

The comparison is forced by the Typ branch of term_compare, which normalizes both kind quantities before applying their order. bend.ts:3215-3244

This is distinct from #983: that issue recomputes overlapping literal suffixes in the descent check, while this reproducer contains no recursive definition or literal and expands a DAG of quantity aliases during kind comparison.

Expected behavior

Checking time should not expand a shared acyclic chain of quantity definitions into an exponential tree. Memoizing normalization of closed references, or preserving sharing between the two occurrences of the same closed definition, would keep this case linear in the number of definitions.

Version

bend 2.0.25
main commit a4952426
Bun 1.4.2
Darwin arm64