[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.

book_valid knows from last which names get a body later in the order. It now marks those cleared copies (w), and infer-ref picks the message by that mark:

• a def, or a law, filled below its use: "a def written above its use (defs are checked in file order)";
• 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)
  |   ^

The review's case, a law declared below a and filled below it, now 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. It names neither the caller nor @unsafe. In that test the caller is the instance app~0. And a template below is refused even in an @unsafe caller.

The rule itself does not change. Only the message changes. The infer-ref and Valid comments now name the def-below-its-use case.

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, 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.

  forward_reference's comment no longer calls a def below a bodiless claim, and forward_reference_scope's says the refusal names the file order.

• 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 rebased onto main at 10256a7 (it merges cleanly):

• gates/test.ts, run locally: PASS 1690 / 1692. 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,857 tokens (cap 48,000).
• tsc -p bend2/pack/tsconfig.json (TypeScript 5.9.3): the same 11 errors as main, 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.