[nicolas-abril]

Proposal 7 of #1632, in a smaller form than #1737.

A & B is Sigma<&1, &1, ..>, so it is Type whatever A and B are, and nothing in the error says how to write a pair that is Data:

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

• bend2/bend.ts: 3 lines at check-any's final throw, +81 ttok. prototype #1632.7: say why A & B is not Data #1737 adds about 287.
• The note fires when Data is expected and the term is a Sigma. The quantity checks in prototype #1632.7: say why A & B is not Data #1737 aren't needed, since the mismatch already says it's Type. A wider version, on any Data/Type mismatch, fired on 11 unrelated tests, so it stays narrow.
• +Sigma<U32, _ => U32> was checked as a List<&2, ..> element.
• No existing test output changes. tests/check/pair_sugar_not_data.bend pins the note.
• This doesn't make +(A & B) parse, which would change the language.

Touches the same throw as #2008, which merges second and combines the two notes.

Gates on the three PRs combined, on origin/main 3ca3df32: repo 54/54, test 1819/1819, perf 124/124. Ping fails 80/81 on the BendHub LICENSE check, the same as unchanged main on this machine.

🤖 Generated with Claude Code