[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, 3f22cc5b, rebased on main; the repo gate is green.
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.