What you did
Run bun bend2/main.ts repro-descent-literal-exponential.bend --check-only on the file below.
What happened
The checker does not return. This self-call increases its argument from 32n to 33n, so I expected the ordinary expected: a decreasing self-call diagnostic.
The slowdown begins with small literals and approximately doubles for every added Succ on my machine: 16n -> 17n takes 0.23 s, 20n -> 21n 0.55 s, 21n -> 22n 0.83 s, 22n -> 23n 1.47 s, 23n -> 24n 2.69 s, 24n -> 25n 5.25 s, and 25n -> 26n 10.50 s. The 32n -> 33n file did not finish within 30 seconds.
The file
import Base
def down(n: Nat) -> Nat:
match n:
case 32n:
down(33n)
case _:
n
Cause
A numeric pattern is expanded into its full Succ chain by lit_full (bend.ts:1807). When the recursive argument is larger than that chain, term_descend first compares corresponding fields recursively (bend.ts:912); after that comparison returns GT, it recursively searches the same argument against each field of the pattern (bend.ts:920). On unary Succ chains this recomputes overlapping suffix comparisons and gives the observed exponential growth.
This is a checker denial of service on a small source file. I have not derived an accepted non-decreasing definition or an inhabitant of Empty from it.
Version / system
bend 2.0.25 (a49524265bdf), Bun 1.4.2, Darwin arm64 27.0.0, Apple clang 21.0.0.
What you did
Run
bun bend2/main.ts repro-descent-literal-exponential.bend --check-onlyon the file below.What happened
The checker does not return. This self-call increases its argument from
32nto33n, so I expected the ordinaryexpected: a decreasing self-calldiagnostic.The slowdown begins with small literals and approximately doubles for every added
Succon my machine:16n -> 17ntakes 0.23 s,20n -> 21n0.55 s,21n -> 22n0.83 s,22n -> 23n1.47 s,23n -> 24n2.69 s,24n -> 25n5.25 s, and25n -> 26n10.50 s. The32n -> 33nfile did not finish within 30 seconds.The file
Cause
A numeric pattern is expanded into its full
Succchain bylit_full(bend.ts:1807). When the recursive argument is larger than that chain,term_descendfirst compares corresponding fields recursively (bend.ts:912); after that comparison returnsGT, it recursively searches the same argument against each field of the pattern (bend.ts:920). On unarySuccchains this recomputes overlapping suffix comparisons and gives the observed exponential growth.This is a checker denial of service on a small source file. I have not derived an accepted non-decreasing definition or an inhabitant of
Emptyfrom it.Version / system
bend 2.0.25(a49524265bdf), Bun 1.4.2, Darwin arm64 27.0.0, Apple clang 21.0.0.