[adeerkhan]

This is a prototype for proposal 2 of #1632 (a value used twice), in reply to the request to prototype 1–7. It is opened against bendlang/bend for review: bend2/bend.ts is human-written per AGENTS.md, so it is not a merge request as it stands. The branch is proto/1632-2-uses-point-at-uses on the fork, 2db198d8, one commit on main (9d514f3).

The error is reported where the second use is found, while the uses are summed. There is no new pass, no new field, and no span is stored on Quant; the span comes from the term being checked. The whole change is one check in uses_add (bend.ts +14/−7):

// a + b; at s, a Lone binder used by both a and b is consumed a second time
export function uses_add(a: Uses, b: Uses, book?: Book, ctx?: Ctx, s?: Span, def?: Name): Uses {
  for (const [i, q] of book && s ? pmap_to_array(b) : []) {
    const ann = pmap_get(ctx!, i);
    if (ann?.q.$ === "Lone" && q.$ !== "None" && (pmap_get(a, i) ?? None()).$ !== "None") {
      throw Err(book!, ctx!, ann.k, ann.k + " (consumed more than once)", s, def);
    }
  }
  return pmap_union(a, b, quant_add);
}

The other lines are the seven callers (App, Min, tele_check, Let ×2, Rwt), which now pass the span of the argument / operand / value / body they add. uses_close is unchanged and still catches the cases the sum doesn't see (a Lone value used under a + position keeps main's message, with the caret on the binder). Match arms still join, so one use in each arm is still one use.

Your repro:

SOME PROOFS FAIL
Error:
- expected : f
- observed : f (consumed more than once)
Context:
- f : @_:U32 -> U32
Location: both
3 | def both(f: U32 -> U32) -> (U32 -> U32) & (U32 -> U32):
4>|   (f, f)
  |       ^
5 | 

A pattern field used twice points at the second use too. No extra note is needed, because the field can already take the + itself: case 1n+(+p): checks on main.

SOME PROOFS FAIL
Error:
- expected : p
- observed : p (consumed more than once)
Context:
- p : Nat
Location: twice
10 |     case 1n+p:
11>|       Nat.add(p, p)
   |                  ^
12 |

Trade-offs:

• The error is thrown in the context of the second use, so its Context: block now lists the binder itself (and anything bound after it). Expected outputs gain those lines.
• The caret covers the whole term that adds the second use. Usually that is the variable, but it can be larger: in tests/io/reuse_across_effect.bend it underlines the whole c <- … statement that uses the value again.

Tests: 19 existing expected outputs were regenerated (caret moved and/or Context: lines added). tests/check/pattern_use_twice.bend pins the pattern case. tests/check/equation_endpoints_dead.bend pins that a mention in a type position (an equation's endpoints) is not counted as a use. Results: repo 54/54, test 1785/1785, tsc errors the same as main, gates/test.ts wall time ~16.5 s.

[nicolas-abril]

Closing this one: pointing at the second use costs too much code for what it gives.

The checker only learns that a value was used twice where two use maps are added together, and at that point it no longer knows where either use was. To point at the second use you have to do one of these:

• keep a span inside every quantity (wrong place: quantities shouldn't carry spans),
• walk the body again when the error happens (a new recursive pass), or
• pass the span of the term into uses_add from each of its 6 callers (the smallest version, +14/-7 in bend.ts, is still more than this message is worth).

None of these is small enough, so the error keeps pointing at the binder, as it does on main.