From 49704abee375aa67a80c692a236dc2ab974b4a43 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Mon, 2 Nov 2026 15:10:09 +0100 Subject: [PATCH] fix(check): a pair where Data is expected names the spelling that is (#1632) Co-Authored-By: Claude Opus 5.5 --- bend2/bend.ts | 4 +++- tests/check/pair_sugar_not_data.bend | 18 ++++++++++++++++++ 2 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 tests/check/pair_sugar_not_data.bend diff --git a/bend2/bend.ts b/bend2/bend.ts index 077d0401f..22b1cbac5 100644 --- a/bend2/bend.ts +++ b/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 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 { diff --git a/tests/check/pair_sugar_not_data.bend b/tests/check/pair_sugar_not_data.bend new file mode 100644 index 000000000..7614001a3 --- /dev/null +++ b/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 B>. +#|exit 1