--check-only hangs on a four-line self-application during eager beta reduction

[jasisz]

What you did

Run bun bend2/main.ts omega.bend --check-only on the file below.

What happened

The command consumes a CPU core indefinitely and produces no output. I confirmed that it was still running after 20 seconds and had to interrupt it. The same command on ordinary invalid files returns immediately with a diagnostic.

The term is invalid and should be rejected quickly: the lambda parameter is self-applied and used twice. This is therefore a frontend/checker denial of service from a four-line source file, rather than accepted nontermination.

The file

type Empty is Data:

def boom() -> Empty:
  (x => x(x))(x => x(x))

Cause

term_higher eagerly beta-reduces an App whenever its elaborated function is a Lam: bend.ts:781-787. For Ω, substituting the right lambda into x(x) reconstructs the same application, so term_higher recurses forever before term_check can reject the non-inferrable or affine-invalid lambda.

I have not derived a checked nonterminating term or an inhabitant of Empty; the observed issue is nontermination while processing invalid input.

Version / system

Bend 2.0.25 (a49524265bdf), Bun 1.4.2, Darwin arm64 27.0.

[jasisz]

I found that the four-line definition is not specific to function bodies or to the checker. The same nontermination has a one-line parser/elaborator reproducer:

law omega: (x => x(x))(x => x(x))

bun bend2/main.ts law.bend --check-only consumes a core without producing output. I also confirmed the timeout with a harness that calls only parse_book and never calls book_valid; a law is installed by applying term_higher directly to its type.

The same Ω also hangs in every term-bearing declaration position I tested: the domain and codomain of an All, a datatype kind, a constructor field type, a definition parameter type, a definition return type, and the type side of an annotation.

I also tested the elaborator wrappers separately. A variable match, which lowers through Sub, still hangs; a valid local Unit let followed by Ω still hangs; and an annotated erased lambda whose body contains Ω hangs only when checking the annotation forces the lambda body. In contrast, placing an annotation directly around the lambda at the head or argument of the self-application prevents eager beta reduction and produces a finite ordinary type error.

The distinction matches the implementation. Sub immediately calls term_higher again on its body, Let stores a closure and term_lower later forces that closure during the term_higher(term_lower(term_higher(...))) canonicalization in parse_def, and Ann recursively converts both children without itself reducing. All observed infinite cases ultimately reach the same eager App/Lam branch; I did not find an independent cycle in Sub, Let, or Ann alone.

An expanding variant, (x => x(x)(x))(x => x(x)(x)), terminates with Bend's generic caught stack-overflow diagnostic instead of hanging. The exact Ω is worse because it reconstructs an equal redex indefinitely without reaching the host stack overflow that the CLI catches.

Relevant paths are parse_def, term_higher for Sub, Let, App, and Ann, and term_lower forcing a Let closure.

[VictorTaelin]

This follows from a design choice. The checker reduces a written redex as it reads it, and WONTFIX.txt makes a dropped argument dead code: "The checker skips dead code (#820, #878)". Checking every redex argument would make (x => x)(3) fail with "cannot infer". So (x => x(x))(x => x(x)) never ends; the next release names this case in that WONTFIX entry.

Note: an AI wrote this reply after I made the decision. If anything here is wrong, reply and I will review it myself.