A constructor name reused by a later definition bypasses #905 and admits Empty

[jasisz]

What I did

Put these three files in one directory and check main.bend.

law.bend:

law k:
  for ~B.x: Data
  Data

law.k~B.bend:

import ./law.bend as L

type Empty is Data:

type Bit is Data:
  False{}
  True{}

type Marker is Data:
  x{}

def L.k(B.x):
  x

type Bad is Type:
  MkBad{apply: @+b: L.k(~Empty) -> Empty}

def x() -> Type:
  Bad

def Bad.apply(b: Bad) -> (@+x: L.k(~Empty) -> Empty):
  match b:
    case MkBad{f}:
      f

def step(+b: L.k(~Empty)) -> Empty:
  Bad.apply(b)(MkBad{Bad.apply(b)})

def boom() -> Empty:
  step(MkBad{step})

def absurd(-A: Type, e: Empty) -> A:
  match e:

def false_theorem() -> {False{} == True{} : Bit}:
  absurd({False{} == True{} : Bit}, boom())

main.bend:

import ./law.k~B.bend as E

def boom() -> E.Empty:
  E.boom()

Then run:

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

What happened

All terms check.

The accepted safe book has no holes, open laws, @unsafe definitions, FFI, or Base import. It contains the closed boom() -> Empty and derives False{} == True{}.

Why it happens

The imported module's namespace is law.k~B. Its constructor x{} therefore owns the constructor key law.k~B.x. The fill body x resolves through that constructor-table entry to Ref("law.k~B.x"). Definitions and constructors use separate freshness checks, so the later def x() -> Type is also admitted under the TLD key law.k~B.x. parse_reso parse_fresh

book_valid hides later TLDs and reveals declarations in order. When it checks the earlier fill of law.k, the constructor is visible but the later TLD law.k~B.x is not. def_check constructs exactly that name for the opaque ~B.x parameter and tests freshness only in the currently visible TLD table. The test therefore passes, the opaque temporarily shadows the constructor key, and the body checks as Data. def_check book_valid

Validation then reaches the later def x() -> Type and installs it under the same key. From that point, reducing the already checked body of L.k resolves its Ref("law.k~B.x") to this definition and yields Bad, which is Type-kinded. The declared result of L.k is still Data, so L.k(~Empty) licenses the + binder over the negative Bad type. The ordinary Curry term in step then inhabits Empty.

This is a bypass of the opaque-name freshness guard added for #905. Moving the later def x before the law fill makes that guard reject the opaque name as expected; leaving it later keeps it outside the visible TLD table during generic checking.

Expected behavior

An opaque template parameter should have an identity that cannot be captured by constructor or definition names, including declarations revealed later. At minimum, constructor and TLD keys should not be reusable in this order-sensitive way, and opaque-name freshness should cover the complete namespace rather than only the currently visible TLD table.

Version

bend 2.0.25
commit a49524265bdfa5753a4bf38e25f0574a705dd868
Bun 1.4.2
Darwin arm64

[jasisz]

I confirmed that the capture is not specific to a later def. A later datatype declaration can occupy the same TLD key and gives a slightly smaller route to Empty because the captured type can itself carry the Curry payload.

Using the same law.bend and main.bend, replace law.k~B.bend with:

import ./law.bend as L

type Empty is Data:

type Marker is Data:
  x{}

def L.k(B.x):
  x

type x is Type:
  MkBad{apply: @+b: L.k(~Empty) -> Empty}

def x.apply(b: x) -> (@+z: L.k(~Empty) -> Empty):
  match b:
    case MkBad{f}:
      f

def step(+b: L.k(~Empty)) -> Empty:
  x.apply(b)(MkBad{x.apply(b)})

def boom() -> Empty:
  step(MkBad{step})

This also prints All terms check. on a49524265bdfa5753a4bf38e25f0574a705dd868. Here the earlier constructor and the later datatype both have the global key law.k~B.x. During generic checking that key temporarily denotes the opaque Data parameter; after replay it denotes the Type-kinded ADT x. Thus the fix needs to cover constructor collisions with every TLD kind, including ADTs, rather than only later ordinary definitions. Same-named constructors belonging to their own datatype (for example type U32 ...: U32{...}) still need their intentional exception.