Proposals for bend.ts: clearer messages for seven common mistakes

AGENTS.md keeps bend2/bend.ts human-written, so these are proposals for the team to review and implement, not a PR. Each comes with a minimal reproduction, the current output on main (e5527d5), and where the change would go. Happy to help with any of them in the form you prefer. A companion issue, #1633, covers checking speed (content-keyed template instance names).

The checker already supports a Note: line (Err's nte), and the +-parameter error uses it well:

- expected : Data
- observed : Type
Note: +f can be used many times, so its type must be Data.

Each case below would gain the same kind of explanation, and most of the information is already computed at the throw site.

1. A misspelt name: suggest the closest names

import Base

def double(n: Nat) -> Nat:
  Nat.ad(n, n)

- expected : a defined name
- observed : Nat.ad

Proposed: keep the message, and add Note: did you mean Nat.add?, listing names in book.tlds within an edit distance of 2, same namespace first. Where: infer-ref, bend.ts:3315. The search runs only on the error path, so it costs nothing on success.

2. A value used twice: point at the uses, and say what to do

import Base

def both(f: U32 -> U32) -> (U32 -> U32) & (U32 -> U32):
  (f, f)

- expected : f
- observed : f (consumed more than once)
Location: both
3>| def both(f: U32 -> U32) -> (U32 -> U32) & (U32 -> U32):
  |          ^

The caret points at the binder, and "expected f, observed f" reads as a contradiction. Proposed (prototyped, output below):

- message  : f is used 2 times (at 4:4, 4:7), but a plain binding is used at most once
Location: both
3 | def both(f: U32 -> U32) -> (U32 -> U32) & (U32 -> U32):
4>|   (f, f)
  |       ^
5 | 
Note: a +f binding may be used many times if its type is Data; otherwise use it once (a function or another Type value cannot be copied).

Where: uses_close, bend.ts:3478. Uses keeps quantities, not positions, so on this error path the prototype re-walks the checked body for the variable's Var nodes, skipping an Ann's type as uses does. Its two callers (the Lam case and the Let loop) pass f_chk.tm as one extra argument. It runs only on failure.

What the prototype showed, on a scratch copy of main:

f(f(f(x))) reports 3 uses, with the caret on the second.
A use in each of two match arms is not flagged (uses joins arms), and neither is a mention in a type annotation.
A let-bound value used twice is flagged the same way.
All 19 tests whose expected output contains "consumed more than once" get the new message (none fall back to the old one), so their expected output would need regenerating with the change.

One refinement it needs: when the variable is bound by a pattern, the + goes on the matched parameter, not the pattern variable. In match k: case 1n+p:, using p twice is fixed by writing +k: Nat, so the Note should say that in that case.

3. A missing match case: drop the internal term, name the missing pattern

import Base

def pred(n: Nat) -> Nat:
  match n:
    case 1n+p:
      p

- expected : cases for Zero
- observed : \{}

\{} is an internal term. Proposed:

- message  : this match doesn't cover Zero
Note: add `case 0n:` (or `case _:`).

using the surface spelling where one exists (0n for Zero, [] for Nil). Where: bend.ts:3628.

4. A recursive call that doesn't shrink: name the argument

import Base

def loop(a: Nat, b: Nat) -> Nat:
  match a:
    case 0n:
      b
    case 1n+p:
      loop(1n+p, b)

- expected : a decreasing self-call (arguments are read left to right: each passed unchanged until one shrinks)
- observed : loop

Proposed:

- message  : loop's 1st argument, 1n+p, is not smaller than a
Note: pass p, a part of a, or mark the def @unsafe to skip the termination check.

Where: bend.ts:3336. The loop just above already computes ord per argument (term_descend(lhs.qs[j], sp[j], cols[j])), so the first j where it isn't EQ and the reason (GT or not comparable) are already known.

5. A false `{==}`: say which side is which

import Base

def add3(n: U32) -> U32:
  U32.add(n, 3)

def bad() -> {add3(4) == 8 : U32}:
  {==}

- expected : 7
- observed : 8

Proposed:

- message  : {==} needs both sides to compute to the same value
- left     : add3(4)  ⟶  7
- right    : 8        ⟶  8

Where: check-rfl, bend.ts:3665 (throw Err(book, ctx, t_wnf.a, t_wnf.b, …)). Showing t_wnf.a/t_wnf.b as written next to their normal forms makes large equations readable.

6. A missing argument: say how many

import Base

def add2(a: U32, b: U32) -> U32:
  U32.add(a, b)

def main() -> U32:
  add2(1)

- expected : U32
- observed : @b:U32 -> U32

Proposed: keep it, and add Note: add2 takes 2 arguments, 1 given (missing b : U32). when the observed type is a ∀ and the expected type isn't. Where: check-infer's final comparison (throw Err(book, ctx, ty, x_inf.ty, …), just before def_check).

7. A pair where Data is expected: say why `A & B` is Type

import Base

def f(xs: List<&2, U32 & U32>) -> List<&2, U32 & U32>:
  xs

- expected : Data
- observed : Type
  |                    ^^^^^^^^^

Why it's Type. A & B is short for Sigma<&1, &1, A, _ => B> (GUIDE.md, short forms), and Sigma<a, b, ..> is Kind(a <&> b). So the shorthand pair is Kind(&1), which is Type, whatever A and B are. A pair of two Data types is Data only when spelled with &2: Sigma<&2, &2, U32, _ => U32> and +Sigma<U32, _ => U32> both check. The natural spelling +(U32 & U32) is rejected by the parser:

- expected : a quantified datatype after + (+D<..> sets D's leading quantities to &2)
- observed : '>'

I tried each of U32 & U32, Bool & Nat, U32 & (Bool & Nat) and (U32 & Bool) & Nat as a list element: all fail the same way, with no hint of the fix.

Proposed:

(a) A Note, when the observed Type is a Sigma at &1: Note: A & B is Sigma<&1, &1, ..>, which is Type. Write +Sigma<A, _ => B> for a pair that is Data. Where: the kind comparison that throws expected Data. The check is on the error path only.
(b) Optionally, accept +(A & B) in the parser as Sigma<&2, &2, A, _ => B>, matching what +D<..> does for named datatypes. This changes the language, so it's your call. (a) alone already removes the dead end.

8. A file declaring a name Base has: let the file's declaration win

Base's type and constructor names are global, so adding a name to Base breaks every package that declares the same name. Two cases I hit:

A Base Poll with constructor Ready broke a hub package that had its own Ready.
A U8/U16 section for Base, with byte helpers that pass Base, all three lanes, and --verdict, can't land as it is: 11 hub files declare their own type U8 and 3 declare type U16, among them both published versions of an integer kit and several UTF-8 packages.

Proposed: let a file's own declaration shadow a Base name inside that file and its importers, as an import alias does, rather than conflict with it. Base could then grow without breaking published packages. This is a language decision, and I'd understand if you'd rather keep names global and coordinate additions instead. A Note on the conflict naming the Base declaration would help in either case.

Found and measured with Claude Code, running Claude Opus 5.5, during an audit of --verdict.

A correction to proposal 8 (letting a file's declaration shadow a Base name): I'm withdrawing it. I've since found that refusing a redeclared Base name is deliberate (#1042, 2.0.28, after the name-collision soundness bugs #994 and #1002), and tests/import/shadow_base.bend pins it. A prototype of proposal 8 on a scratch copy fails that test, so it reopens what #1042 closed, and it still wouldn't help a file checked on its own, since that file shares Base's namespace. Sorry for the noise. The other seven proposals are unaffected.

For the case that motivated it, the byte types are now a draft PR using names that collide with nothing on the hub: #1660.

Companion to #1633 (checking speed), not a duplicate — the two are independent
changes to bend.ts. I prototyped #1633's content-keyed instance naming to see
how it touches the messages here:

Proposal for bend.ts: content-keyed template instance names, for parallel and cached checking #1633's change makes the template-instance names (keep~0 → keep~<content hash>)
a pure function of the ~ arguments instead of first-use order. That's what
makes any diagnostic that quotes an instance name reproducible across runs and
workers — a prerequisite for the clearer messages proposed here to be stable,
and for per-instance caching keyed by name.
The message wording proposals (1–7) are untouched by that and stand on their
own; proposal 8 was withdrawn per your correction above.

So: #1633 is the naming/stability enabler, this issue is the wording. Doing
either doesn't do the other. Prototype + measurements for #1633 are in that
issue (branch on my fork, no PR, since bend.ts is human-written per AGENTS.md).
Happy to prototype any of 1–7 here the same way if useful.

Thank you, and yes please, I'd welcome prototypes of 1–7 in the same way, as branches on your fork, since bend.ts stays human-written. Proposal 2 is the only one I prototyped, and it still needs the refinement described under it (a variable bound by a pattern takes its + on the matched parameter). None of the others has a prototype yet.

proto(check): pin the pattern-field fix for a double use (bendlang#1632)

proto(check): pin the partial-call arity note (bendlang#1632)

proto(check): pin the surface spelling of a missing Nat case (bendlan…

Prototype for proposal 1, as PR bendlang/bend#1731 (branch proto/1632-1-name-suggestions on the fork, 30a87a7d, rebased on main).

The note is added at the unknown-name throw in infer-ref (bend.ts:3359), so nothing runs on success. Candidates are book.tlds keys within edit distance 2 of the full displayed key, same namespace first — and when any same-namespace name matches, only those are listed, which keeps Nat.ad down to Nat.add. I skip internal keys (~N, leading ., leading _), require the name parts to share their first character unless the difference is a single edit (that suppressed noise like Chan/Map/Nat for a bare nan and IO/Or for _^), and only offer a name the file can see (the root, its own namespace, or an imported one), so the suggestion is one the user can actually write.

On your repro:

SOME PROOFS FAIL
Error:
- expected : a defined name
- observed : Nat.ad
Context:
- n : Nat
Location: double
3 | def double(n: Nat) -> Nat:
4>|   Nat.ad(n, n)
  |   ^^^^^^
5 | 
Note: did you mean Nat.add?

Every check-failing test that expects a defined name was run (32). Two change: tests/io/tls_connect_close.bend (TLS.connect → TCP.connect) and tests/flatten/ctor_call_syntax.bend (Aw4 → Nw4, or Rw4). The other 30 typo to names with no near neighbour and keep the old message.

Prototype for proposal 2, as PR bendlang/bend#1732 (branch proto/1632-2-uses-point-at-uses on the fork, 3f22cc5b, rebased on main).

uses_close (bend.ts:3568) gets the checked body from its two callers and re-walks it for Var nodes of the binder, as the measure counts them: a type position (an annotation's type, an equation's endpoints, a rewrite's motive, a type application) is dead, and so is an erased field, so neither is counted. It runs only on the failure path. Line:column comes from parse_col, the caret moves to the second use, and if fewer than two uses are found it falls back to the old wording. Min counts both operands (meet_charges_its_operands needed that), and a use in each match arm is still not flagged (arms join).

Your repro:

SOME PROOFS FAIL
Error:
- message  : f appears 2 times (at 4:4, 4:7), but a plain binding is used at most once
Location: both
3 | def both(f: U32 -> U32) -> (U32 -> U32) & (U32 -> U32):
4>|   (f, f)
  |       ^
5 | 
Note: a +f binding may be used many times if its type is Data; otherwise use it once (a function or another Type value cannot be copied).

The count is the mentions in the body, so the message says appears: a match's arms join, so one use in each arm is one use, and the number can be larger than what the measure saw.

The refinement: a field-pattern lambda carries the parameter it matched (set in match_flatten, carried by body_flatten/term_higher/term_lower as a non-enumerable property, so it never enters the JSON term keys comp.ts and safe.ts derive from terms), so the second Note names that parameter, not the field:

SOME PROOFS FAIL
Error:
- message  : p appears 2 times (at 8:15, 8:18), but a plain binding is used at most once
Location: twice
7 |     case 1n+p:
8>|       Nat.add(p, p)
  |                  ^
9 | 
Note: a +p binding may be used many times if its type is Data; otherwise use it once (a function or another Type value cannot be copied).
Note: p is bound by a pattern: put the + on the matched parameter, +n.

All 19 existing tests whose output contains "consumed more than once" take the new message (none fall back), and tests/check/pattern_use_twice.bend pins the pattern case, tests/check/equation_endpoints_dead.bend pins that a mention in a type position is not a use.

Prototype for proposal 3, as PR bendlang/bend#1733 (branch proto/1632-3-missing-match-case on the fork, 0d606f7b, rebased on main).

Changed the empty-match throw (bend.ts:3625). The message keeps the constructor's printed name; the Note names the constructor and the pattern to write: a nullary one by the way the surface spells it (0n for Zero, [] for Nil, True{} for True), a fielded one by its constructor alone — its fields may be dependent, so a case with them may not check — and a catch-all case for the rest. It names the pattern, not a whole case ...: line, because a match on several scrutinees takes one pattern each and the count is not known there.

On your repro:

SOME PROOFS FAIL
Error:
- message  : this match doesn't cover Zero
Location: pred
3 | def pred(n: Nat) -> Nat:
4>|   match n:
  |   ^^^^^^^^
5 |     case 1n+p:
Note: add a case for `Zero` (pattern `0n`), or a catch-all case.

15 existing tests with cases for … regenerate; tests/check/missing_nat_case.bend pins the Nat/0n spelling.

Prototype for proposal 4, as PR bendlang/bend#1734 (branch proto/1632-4-decreasing-argument on the fork, 4e0b46d7, rebased on main).

Changed the self-call descent in infer-ref (bend.ts:3340). The existing loop still decides pass/fail; on failure I compare the arguments against the def's declared parameter names (tele_unbind(def.T)), skip arguments that are literally the unchanged parameter, and report the first that isn't — so the common multi-argument case names the right one. A bare self-reference with no arguments keeps the old message. The argument is quoted as written (the check does not evaluate it) and cut at 60 characters.

Your repro:

SOME PROOFS FAIL
Error:
- message  : loop's 1st argument, 1n+p, is not smaller than a
Context:
- p : Nat
- b : Nat
Location: loop
7 |     case 1n+p:
8>|       loop(1n+p, b)
  |       ^^^^
9 | 
Note: pass a part of a, or mark the def @unsafe to skip the termination check.

The other order reports the second argument:

SOME PROOFS FAIL
Error:
- message  : loop's 2nd argument, 1n+p, is not smaller than b
Context:
- a : Nat
- p : Nat
Location: loop
7 |     case 1n+p:
8>|       loop(a, 1n+p)
  |       ^^^^
9 | 
Note: pass a part of b, or mark the def @unsafe to skip the termination check.

25 existing tests with the old message regenerate (the 6 that stay on it are bare self-references, which fall back).

Prototype for proposal 5, as PR bendlang/bend#1735 (branch proto/1632-5-rfl-sides on the fork, cdaf1bf5, rebased on main).

Changed check-rfl (bend.ts:3668). The two sides are printed as written, then their normal forms. The normal form is the weak head normal form when that is short (it is one step) and the strong one otherwise, so a big side does not print thousands of constructors: build(3000n) reads build(3000n) => LC{build(2999n)}. Both columns print the way the rest of the error prints, markers included. I used ASCII => where your sketch had ⟶; happy to switch.

Your repro:

SOME PROOFS FAIL
Error:
- message  : {==} needs both sides to compute to the same value
Location: bad
6 | def bad() -> {add3(4) == 8 : U32}:
7>|   {==}
  |   ^^^^
8 | 
- left     : add3(4)  =>  7
- right    : 8  =>  8

21 existing tests with a false {==} regenerate.

Prototype for proposal 6, as PR bendlang/bend#1736 (branch proto/1632-6-missing-argument on the fork, 4f702999, rebased on main).

Added at check-any's final comparison (bend.ts:3715), the place you named. It fires only when the observed type is a ∀ and the expected type isn't, and the head is a Ref to a Def. "Arguments" counts the def's non-erased domains. A foreign def (an effect operation) is skipped: its continuation is passed by the do block, not written (do_header_typed keeps its old output), and a template is skipped, its ~ arguments being erased in the type but written at the call.

Your repro:

SOME PROOFS FAIL
Error:
- expected : U32
- observed : @b:U32 -> U32
Location: main
6 | def main() -> U32:
7>|   add2(1)
  |   ^^^^^^^
8 | 
Note: add2 takes 2 arguments, 1 given (missing b : U32).

A bare add2 gets all of them:

SOME PROOFS FAIL
Error:
- expected : U32
- observed : @a:U32 -> @b:U32 -> U32
Location: main
6 | def main() -> U32:
7>|   add2
  |   ^^^^
8 | 
Note: add2 takes 2 arguments, 0 given (missing a : U32, b : U32).

tests/parse/glued_bracket.bend (an erased type parameter, id2) gains Note: id2 takes 1 argument, 0 given (missing x : A).; tests/check/partial_call_arity.bend and tests/check/higher_order_arity.bend pin the two cases.

Prototype for proposal 7, as PR bendlang/bend#1737 (branch proto/1632-7-pair-data on the fork, a51b45c2, rebased on main).

At the kind comparison that throws expected Data: when the observed type is Type and the term's weak head normal form is a Sigma at &1, add the Note.

Your repro:

SOME PROOFS FAIL
Error:
- expected : Data
- observed : Type
Location: f
2 | 
3>| def f(xs: List<&2, U32 & U32>) -> List<&2, U32 & U32>:
  |                    ^^^^^^^^^
4 |   xs
Note: A & B is Sigma<&1, &1, ..>, which is Type. Write +Sigma<A, _ => B> (or Sigma<&2, &2, A, _ => B>) for a pair that is Data.

(a) removes the dead end, so I left (b) — accepting +(A & B) in the parser — alone, since it changes the language. Say the word and I'll put it on a branch too. No existing test output changes; tests/check/pair_sugar_not_data.bend pins this one.

proto(check): hide the pattern marker from term identity (bendlang#1632)