A literal trusts a user-defined Nat/String constructor name, forges its field type, and admits Empty

[jasisz]

What you did

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

What happened

All terms check.

The file has a closed boom() -> Empty and derives False{} == True{} from it. It does not import Base and uses no @unsafe, FFI, law, hole, template, native definition, or runtime backend.

This is a regression in 2.0.24. The same file is rejected on the 2.0.23 release commit (4de77734) at extract(1n):

Error:
- expected : a declared constructor (Empty declares )
- observed : 0n
Location: boom

The file

type Empty is Data:

type Nat is Data:
  Succ{e: Empty}

type Bit is Data:
  False{}
  True{}

def extract(n: Nat) -> Empty:
  match n:
    case Succ{e}:
      e

def boom() -> Empty:
  extract(1n)

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

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

Why it happens

The new check-lit fast path recognizes a literal-compatible datatype by the unqualified datatype name (Nat or String) and the presence of its head constructor (Succ/Zero or SCon/SNil):

if (t_wnf.$ === "ADT" && t_wnf.k === T
  && ctrs_find(book_adt(book, t_wnf, ctx, lhs.def).c, c) !== null) {
  return Check(tm, ty, uses_nil());
}

It does not verify that the constructor has the representation assumed by the literal. Bend intentionally permits a file without Base to declare its own Nat. Here 1n is accepted as that Nat because it has a constructor named Succ, but the literal unfolds as Succ{0n} while this Succ declares its field as Empty. Matching the value therefore exposes 0n at type Empty.

The same issue exists for String. Replacing the custom datatype and extraction with the following also makes a closed Empty pass in 2.0.24 and fail in 2.0.23:

type String is Data:
  SCon{e: Empty, tail: Empty}

def extract(s: String) -> Empty:
  match s:
    case SCon{e, tail}:
      e

def boom() -> Empty:
  extract("x")

Additional variants checked

The empty heads are affected too: 0n checks against a custom Nat whose only constructor is Zero{e: Empty}, and "" checks against a custom String whose only constructor is SNil{e: Empty}. Matching either literal extracts the nonexistent field as a closed Empty. Both files pass on 2.0.24 and are rejected on 2.0.23 with Zero with 1 field or SNil with 1 field.

A shape check must reject extra fields as well as wrong ones. 1n checks against Succ{pred: Nat, e: Empty}, and "x" checks against SCon{head: Char, tail: String, e: Empty}; matching the extra field again produces a closed Empty. Thus checking only the canonical prefix (pred: Nat, or head: Char, tail: String) would leave the hole open. Version 2.0.23 rejects these with Succ with 2 fields and SCon with 3 fields.

The other literal sugars tested do not share this path: malformed user-defined Char, U32, F32, List and Bool constructors are checked structurally and rejected. The source fast path is limited to the new Lit node for Nat and String.

A custom Nat in an imported module is also rejected when the root imports Base: the resolved ADT key is qualified (custom.Nat), so it does not compare equal to the hard-coded Nat. The exploit applies when the root book itself binds the unqualified key Nat or String, as a file without Base is allowed to do.

The previous checker expanded the literal and checked the actual constructor fields, so it rejected both variants. The fast path needs to be restricted to the canonical literal representation (or otherwise validate that representation) rather than trusting source-level datatype and constructor names alone.

bend --version

bend 2.0.24
commit 99f9c6cd

uname -sm

Darwin arm64

clang --version (the first line)

Apple clang version 21.0.0 (clang-2100.0.123.102)

[VictorTaelin]

Fixed in 2.0.25. The check-lit fast path now fires only when the datatype is Base's own (book_load marks Base's TLDs); any other Nat or String checks the literal's first step structurally, as 2.0.23 did. Your file, the String variant, the empty heads and the extra-field variants are all refused again (expected : a declared constructor (Empty declares ) / observed : 0n). Pinned as tests/check/nat_literal_own_succ.bend and string_literal_own_scon.bend. Thank you for the precise report and the variant list.

Note: this reply was written by an AI after it reported the issue to me and I made the decision. If anything here is wrong, reply and I will review it myself.