[HamedShams]

Closes #1787.

parse_term_do_stmt reads a statement's first term before it knows what the statement is, and only a : after a variable makes it a bind or a let. So a bind or a let written without its type was read as something else: x <- m as the exec form A <- m with x as the type, which reports "a defined name" for a new x and "expected Type, observed U32" when x is a parameter; x = v as the block's result, after which the = has nowhere to go. None of the three errors mentioned the annotation.

Now, right after typed is decided, a bare name that cannot be a type and is followed by <-, or any bare name followed by =, fails with:

- expected : a typed bind (x : A <- m) or let (x : A = v)
- observed : 'x <- IO.pure(U32, 1)'

with the caret under the whole statement. The name's scope is what tells a lost annotation from the exec form. A declared name, or a local binder that may be a type (a parameter typed Type, or one whose type the parser does not know), stays the exec form: Unit <- IO.print("a"), U32 <- IO.pure(U32, 1), a <- IO.pure(a, x) with a: Type a parameter, and foo <- m with a declared type foo all keep working. A value binder of the def, or an unbound lowercase name, is the lost annotation. For that, parse_def records the def's value binders, from its telescope or from the filled law's leading domains. A single = after a bare name is never exec syntax, so it fails regardless. An unbound uppercase name on the left of <- keeps "a defined name". The first commit decided this by the case of the name instead and refused the two exec forms above; @YidaWeng caught it in review and proposed the scope rule, which the second commit takes.

Tests, in tests/parse/: the three files from the issue, a bind of a new name, a let, and a bind of an existing name, each pinning the new message; on main they print the three old errors. Plus the two exec forms a lowercase type can take, do_exec_type_var (a type variable) and do_exec_lower_type (a declared lowercase type), which print ok on main and here, and fail on the first commit alone.

tests/parse/do_bind_continuation.bend is a census test for a trailing bind with nothing after it, and it wrote that bind without a type, so it met this message first. Its bind takes : U32 now; it still fails on the missing continuation, and its expected output is unchanged (main prints the same for the edited file).

What I ran: every file under tests/ through bend <file> on main (e7c3de9) and on the first commit: 1,696 shared outputs identical, the one above explained, the three new tests the only additions; then the first commit against the second: 1,700 shared outputs identical, the two exec tests the only additions. The five tests through the --checkup aggregator the test gate uses, same lines; the two exec tests also built and run as JS and as C, ok in both. bun gates/repo.ts 54/54, with bend.ts at 44,054 tokens of 48,000 (43,767 on main). Not run: the cluster gates.

[YidaWeng]

I checked the three cases from #1787 and the new output; this is the right diagnostic, and the do_bind_continuation edit keeps that test's intent.

One regression to settle before merge: /^[a-z]/ rejects valid exec statements whose type name starts lowercase. On main, both of these check and run (print ok):

import Base

def f(-a: Type, x: a) -> IO(Unit):
  do IO<Unit>:
    a <- IO.pure(a, x)
    IO.print("ok")

def main() -> IO(Unit):
  f(U32, 1)

import Base

type foo is Type:
  Mkfoo{}

def main() -> IO(Unit):
  do IO<Unit>:
    foo <- IO.pure(foo, Mkfoo{})
    IO.print("ok")

Both fail here with expected : a typed bind ...; (a) <- ... fails too. for -a: Type appears in the tree (tests/parse/rewrite_motive_annotation_000.bend) and type foo is legal, so this is not only a style question. Also, a : Type <- m is not a workaround: it binds a Type result, while a <- m is the exec form with a as the result type.

A refinement that keeps the message without reading intent from case:

• x = v: fire unconditionally — a single = after a bare variable is never exec syntax.
• x <- m: fire only when x is known not to be a type. A declared name (book.tlds / book.ctrs) or a local binder whose annotation is Typ stays an exec; a known value binder (n: U32) or an unbound name fires; a binder of unknown type keeps the old behavior.
• Track the known value binders in parse_def: from the def telescope, or from the filled law's leading All domains for a law-backed def.

The core check is:

if (!typed && t.$ === "Var") {
  const q = parse_reso(p, t.k);
  const loc = p.stk.some(([, i]) => i === t.i);
  const ty = q in p.book.tlds || q in p.book.ctrs || (loc && !p.vals.has(t.i));
  if ((parse_at(p, "=") && !parse_at(p, "==")) || (parse_at(p, "<-") && !ty)) {
    const eol = p.str.indexOf("\n", p.pos);
    parse_fail(p, "a typed bind (x : A <- m) or let (x : A = v)", beg, eol === -1 ? p.str.length : eol);
  }
}

I prototyped the full patch on this branch: the three #1787 tests still print the new message; the two programs above check and run; existing tests/parse outputs are unchanged (after the same do_bind_continuation edit); bend.ts is 44,042 / 48,000 ttok.

Refined diff against this branch

--- a/bend2/bend.ts
+++ b/bend2/bend.ts
@@ -334,7 +334,7 @@
 
 // Parser
 export type File  = { str: string; ns: string; al: Record<Name, Name>; };
-export type Parse = File & { book: Book; dir: string; pos: number; stk: Array<[Name, number]>; frs: number; };
+export type Parse = File & { book: Book; dir: string; pos: number; stk: Array<[Name, number]>; frs: number; vals: Set<number>; };
 export type Span  = { file: File; beg: number; end: number; };
 
 // Machine
@@ -2255,17 +2255,19 @@
   const t = parse_term(p);
   parse_skip(p);
   const typed = t.$ === "Var" && parse_take(p, ":");
+  if (!typed && t.$ === "Var") {
+    const q = parse_reso(p, t.k);
+    const loc = p.stk.some(([, i]) => i === t.i);
+    const ty = q in p.book.tlds || q in p.book.ctrs || (loc && !p.vals.has(t.i));
+    if ((parse_at(p, "=") && !parse_at(p, "==")) || (parse_at(p, "<-") && !ty)) {
+      const eol = p.str.indexOf("\n", p.pos);
+      parse_fail(p, "a typed bind (x : A <- m) or let (x : A = v)", beg, eol === -1 ? p.str.length : eol);
+    }
+  }
   const step  = !typed && parse_more(p, col);
   const A     = typed ? parse_term(p, 1) : step ? parse_var(p, "Unit", t.s) : t;
   parse_skip(p);
   const asg = typed && !parse_at(p, "==") && parse_take(p, "=");
-  // A lowercase name followed by `<-` or `=` is a bind or a let that lost its
-  // type: read as the exec form, the name would be the type, and the error
-  // would be about that instead.
-  if (!typed && t.$ === "Var" && /^[a-z]/.test(t.k) && (parse_at(p, "<-") || (parse_at(p, "=") && !parse_at(p, "==")))) {
-    const eol = p.str.indexOf("\n", p.pos);
-    parse_fail(p, "a typed bind (x : A <- m) or let (x : A = v)", beg, eol === -1 ? p.str.length : eol);
-  }
   if (typed && !asg) {
     parse_eat(p, "<-");
   } else if (!typed && !step && !parse_take(p, "<-")) {
@@ -2468,6 +2470,17 @@
     def = book.tlds[k] = { $: "Def", n: tele.length, x: tk.length, T: term_higher(tele_bind(tele, parse_term(p))), v: null, m: p.ns };
   }
   def.u ||= un;
+  if (law) {
+    let T = law.T;
+    for (let i = 0; T.$ === "All"; i++) {
+      if (T.A.$ !== "Typ") p.vals.add(i);
+      T = T.B(Var(T.k, i));
+    }
+  } else {
+    for (const cell of tele) {
+      if (cell[3].$ !== "Typ") p.vals.add(cell[2]);
+    }
+  }
   parse_eat(p, ":");
   if (parse_at_word(p, "import")) {
     if (def.x > 0) {
@@ -2494,7 +2507,7 @@
 }
 
 export function parse_book(book: Book, dir: string, src: string, ns: string, al: Record<Name, Name>): void {
-  const p: Parse = { book, dir, str: src, pos: 0, stk: [], frs: 0, ns, al };
+  const p: Parse = { book, dir, str: src, pos: 0, stk: [], frs: 0, ns, al, vals: new Set() };
   while (true) {
     parse_skip(p);
     if (p.pos >= p.str.length) {
@@ -2502,6 +2515,7 @@
     }
     p.frs = 0;
     parse_close(p, 0);
+    p.vals.clear();
     if (parse_take(p, "@")) {
       if (!parse_word(p, "unsafe")) {
         parse_fail(p, "'unsafe' (the one decorator)");

Happy to push a branch or add the positive tests (do_exec_lower_typevar.bend, do_exec_lower_alias.bend) if that is easier.

[HamedShams]

@YidaWeng Good catch, thank you. Both programs run on main and my check refused them: I read the case of the name as intent, and a type variable or a lowercase type is a type all the same.

Took your refinement: = fires after any bare name, <- only after a name that cannot be a type (a value binder of the def, or an unbound one), with the def's value binders tracked as in your diff. One thing I kept from the old rule: an unbound uppercase name, Foo <- m with no Foo anywhere, still gets a defined name. Both readings are errors there, and that one names the actual problem.

Your two programs are in as tests/parse/do_exec_type_var and do_exec_lower_type, the three #1787 tests keep the new message, bend.ts is 44,054. Pushed as a second commit.