[viridale]

Fixes #1782.

What changes

book_valid clears every def's body and restores the bodies in file order. So while a def is checked, a def or law filled below it has v === null, as an unfilled law does, and infer-ref refused both with the law message. A reader with no law in sight went looking for a missing proof.

The parser now records in w the module a def's body is written in. infer-ref picks the message by comparing w with the module of the use (the file its span is in):

• a def, or a law, filled below its use in the same file: "a def written above its use (defs are checked in file order)";
• a law filled by an importing file, used in the file that declares it: the law message, as no order in that file helps (the LAWS / PROOF flow);
• a law that is never filled, and any other bodiless entry (such as an instance while def_inst checks it): the law message, unchanged.

The issue's fwd.bend now prints:

SOME PROOFS FAIL
Error:
- expected : a def written above its use (defs are checked in file order)
- observed : b
Context:
- x : Nat
Location: a
3 | def a(x: Nat) -> Nat:
4>|   b(x)
  |   ^

A law declared below a and filled below it prints the same message, and so does a law declared above its caller and filled below it. The message says "its use", not "its caller", so it also reads right when the def below is passed as a ~ argument, as in tests/comptime/later_def.bend, where the caller is the instance app~0. That is why the use's module comes from its span, not from the def being checked. The message names neither the caller nor @unsafe, since a template below is refused even in an @unsafe caller.

The rule itself does not change. Only the message changes. book_valid is as on main. The infer-ref comment names the def-below-its-use case and the importer's fill.

Tests

• tests/check/unsafe_forward_safe.bend already pins the issue's case: a safe h calls a plain g written below it. It now expects the new message, and its comment says so.

• tests/comptime/later_def.bend (a def below passed as a ~ argument) now expects the new message.

• Three tests call a law before its fill in the same file, and now expect the file-order message:

  • forward_reference: the law is declared below its caller;
  • forward_reference_scope and assert_fill_scope: it is declared above its caller.

  Their header comments now say the refusal names the file order.

• Two new tests cover a law filled in another file, with helpers in tests/import/law-fill/:

  • import/law_fill_importer: the helper declares foo and uses it live, and the test fills it. It expects the law message at the use, in the helper.
  • import/law_fill_below_use: the test uses an imported law above its own fill of it, and expects the file-order message.

• The five axiom tests (axiom_use, axiom_whitelist, axiom_import_warn, axiom_runtime_capture, compile/axiom_runtime) use a law that is never filled, and keep the law message.

Checks

On the branch merged onto main at b8664b0 (it merges cleanly):

• gates/test.ts, run locally: PASS 1707 / 1709. The two failures, gfx_clicks and gfx_window, expect "no display" and fail the same way on main here, because this Mac has a desktop session.
• bun gates/repo.ts: 54 / 54. bend.ts goes from 43,767 to 43,884 tokens (cap 48,000).
• tsc -p bend2/pack/tsconfig.json (TypeScript 5.9.3): 11 errors, none on the changed lines.

[Lorenzobattistela]

Thanks, the message is much clearer for a plain def written below its use. One case still gets the old message.

1. A law filled below its caller still says "an unfilled law is a dead claim", even though it has a body:

   import Base
   
   def a(x: Nat) -> Nat:
     b(x)
   
   law b:
     for x: Nat
     Nat
   
   def b(x):
     1n+x
   
   def main() -> Nat:
     a(1n)

   On this branch, --check-only prints "expected : a filled definition (an unfilled law is a dead claim: live code cannot use it) / observed : b". But b is filled, and moving it above a makes the file check. That's the confusion #1782 is about. tld.l says that a law declared the name, not whether a body is coming later in the file. A law declared above its caller and filled below it gets the same message (as in forward_reference_scope / assert_fill_scope).

   Suggestion: book_valid already knows from last which names get a body later in the order, but drops that when it writes { ...t, v: null }. If you mark those cleared copies, infer-ref can pick the message from that mark instead of from tld.l. Then a def or law filled below its use gets the file-order message, and the law message stays for laws that are never filled. This also keeps the file-order message away from other entries that have no body and no l, such as an instance while it is checked in def_inst, which has no position in the file.

2. tests/check/forward_reference.bend expects the law message for later, which is filled below its use, and its comment ("a def below is a bodiless claim ... as an unfilled law") now contradicts this PR. Once 1 is fixed, it should expect the file-order message. A test for a law declared above its caller and filled below it would cover the other case.

3. The comment on the infer-ref rule (bend.ts, just above the check) still explains a missing body only as an unfilled law. Please add the def-below-its-use case.

All gates are green on this branch merged onto main ed186a4 (repo 54/54, test 1682/1682, perf 124/124, ping 63/63, safe 0 false rejects).

[viridale]

Thanks, all three are done in 3292e72:

1. book_valid now marks the copies it clears for a name whose body comes later in the order (w), and infer-ref picks the message from that mark instead of tld.l. Your example prints "a def written above its use (defs are checked in file order)", and so does a law declared above its caller and filled below it. A law that is never filled keeps the law message, as do the instance copies in def_inst, which are never marked.
2. forward_reference now expects the file-order message, and its comment no longer calls a def below a bodiless claim. forward_reference_scope and assert_fill_scope are the law-declared-above case, and they expect it too. The five axiom tests (laws never filled) keep the law message.
3. The infer-ref comment now names a def or law filled below its use, and the Valid comment says what w marks.

Rebased onto main at 10256a7 locally, it merges cleanly. There, gates/test.ts passes 1690 / 1692, and the two failures are the gfx tests that need a display-less session. Repo passes 54 / 54, with bend.ts at 43,857 tokens, and tsc shows the same 11 errors as main.

[Lorenzobattistela]

Thanks, the w mark fixes my repro, and the copies never carry it outside book_valid, so nothing downstream sees it. Gates are green on this branch merged onto main 66ced68 (repo 54/54, test 1698/1698, ping 73/73, safe 0 false rejects; perf fails the same cells on main). 1 and 4 below must be fixed before approving; 2, 3 and 5 are optional.

1. (must fix) A law filled by an importing file now gets the file-order message inside the imported file, where no reordering can fix it:

   # LAWS.bend
   import Base
   
   law foo:
     U32
   
   law bar:
     U32
   
   def bar():
     foo

   # PROOF.bend
   import Base
   import ./LAWS.bend as L
   
   def L.foo():
     0

   bend PROOF.bend --check-only prints "expected : a def written above its use (defs are checked in file order) / observed : foo" at bar, in LAWS.bend. But bend LAWS.bend prints the law message at the same spot. LAWS.bend is checked in full before PROOF.bend, so the prover can't move the fill above the use, and in this case the law message was the right one. w asks whether a body exists anywhere later in the book; it should ask whether it comes later in the same file (for example, by comparing the module of the fill with the module of the use). This is the LAWS/PROOF flow, so it's the case that matters most.

2. (optional) Mutual recursion now says to reorder: with f calling g and g calling f, either order gives "a def written above its use". The law message on main was also wrong there, so this isn't a regression, but if there's a cheap way to tell (the caller is itself marked w, say), "mutual recursion is not allowed" would be better.

3. (optional) For a law declared above its use and filled below it (forward_reference_scope), "a def written above its use" reads as already true, since the law foo: line is above. It's the fill that has to move. Something like "a def or law fill written above its use" would point at the right line. Wording only, your call.

4. (must fix) The header comments of tests/comptime/later_def.bend ("a def below is a bodiless claim") and tests/check/assert_fill_scope.bend ("an assert declares a DEAD claim") still argue for the law message, but both tests now expect the file-order one.

5. (optional) A test for 1 (two files, law filled by the importer, expecting the law message) would pin the fix.

[viridale]

Thanks. 1, 4 and 5 are done in 2acfb57. I left 2 and 3 as they were, with reasons below.

1. w now records the module a def's body is written in. The parser sets it where it reads the body. infer-ref names the file order only when that module is the use's module, taken from the file its span is in. Your LAWS / PROOF example now prints the law message at bar from both bend PROOF.bend and bend LAWS.bend. A use in PROOF.bend above its own fill of L.foo still gets the file-order message, since moving the fill up does fix that one. I took the use's module from its span, not from the def being checked, because in later_def the caller is the instance app~0, which has no module of its own. The span of ~later is in main's file. book_valid is back as on main.

   One thing changes from the last round: w now stays on every def that has a body, not just on book_valid's copies. Only infer-ref reads it, and only when v is null, which means a body is still to come.

2. Not done. While a def checks, its own copy stays bodiless until its event ends, so "the caller is itself marked" holds for every caller and would call every forward reference mutual recursion. Telling the two apart needs a walk of the callee's unchecked body for a path back to the caller, and infer-ref only sees the cleared copies. So f calling g and g calling f still reads "a def written above its use". Main gave the law message there.

3. Kept the wording. A law's fill is itself a def line, so "a def written above its use" points at def foo(x):, which is the line that has to move. "or law fill" would also lengthen the plain-def message, which is Calling a def written below its caller reports "an unfilled law is a dead claim", not the ordering rule #1782's case. Happy to change it if you'd rather have it.

4. The headers of later_def and assert_fill_scope now say the refusal names the file order. Each header keeps its line count, so the expected locations don't move.

5. import/law_fill_importer is your example: the helper tests/import/law-fill/used.bend declares foo and uses it, and the test fills it. It expects the law message at bar, and it fails on 3292e72. import/law_fill_below_use covers the other side: an importer uses L.foo above its own fill, and expects the file-order message.

Merged onto main at b8664b0, gates/test.ts passes 1707 / 1709 locally. The two failures are the gfx tests, which need a session with no display. Repo passes 54 / 54, with bend.ts at 43,884 tokens. tsc shows 11 errors, none on the changed lines.