fix(check): a pair where Data is expected names the spelling that is (#1632)

bend2/bend.ts

@@ -3779,7 +3779,9 @@ export function term_check(book: Book, lhs: LHS, tm: HTerm, qt: Quant, ty: HTerm
   if (term_compare("LE", book, x_inf.ty, ty, d)) {
     return x_inf;
   }
-  throw Err(book, ctx, ty, x_inf.ty, tm.s, lhs.def);
+  const sigma = (x: HTerm) => x.$ === "ADT" && x.k === "Sigma";
+  const nte = expr_show(book, ty) === "Data" && sigma(term_wnf(book, tm)) ? "Note: A & B is Type. A pair that is Data is +Sigma<A, _ => B>." : undefined;
+  throw Err(book, ctx, ty, x_inf.ty, tm.s, lhs.def, nte);
 }
 
 export function def_check(book: Book, k: Name, def: Def, z?: number): LTerm {

tests/check/pair_sugar_not_data.bend

@@ -0,0 +1,18 @@
+# A & B is Sigma<&1, &1, ..>, which is Type; a list element here asks
+# for Data, so the note names the spelling that is.
+import Base
+
+def f(xs: List<&2, U32 & U32>) -> List<&2, U32 & U32>:
+  xs
+
+#|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>.
+#|exit 1