Type undeclared lambda actuals from preceding application formals (N7 token_stream) by gunbai-bot[bot] · Pull Request #13623 · gunb-ai/gunbc

gunbai-bot · 2026-10-09T08:23:34Z

Summary

Stacked on N7: derive payload-binder facts for construct-field consumption #13558. Undeclared fn(n) actuals take expected types from the application formal after authored-order prefix judgment (infer_application_actual_child_frame); shares InferFrame.binder_types. Does not annotate token_stream.
One judgment per actual: infer_gather_extend_application_instances carries and extends InferGatherFoldAcc.application_instances after each Transform actual child. The next actual's infer_application_actual_child_frame reads that prefix; row-time infer_application_argument_inhabitance seeds infer_judge_formal_args with the same list (does not recompute the prefix).
Left-to-right: lef_lambda_then_value_does_not_infer_as_int_holds (f-before-o stays underived; T is not minted). One real-path inhabitance: lef_value_then_lambda_infers_holds.
clever-bat-68: their session is gone. binder_types sharing was acked by them earlier (dashboard msg relayed 2026-10-08). Their deep-instantiation follow-up must rebase over this.
N7 pin tree: not this PR alone. Pin //v2/test/parse/expression_bodied_fn_decl_parse:all on the combined tree N7: derive payload-binder facts for construct-field consumption #13558 + v2: bare count over lists binds the std.algebra collection size row, a stated Int (XL-2, N7) #13307 (count) + v2 tokenize: bind EmptyPattern on 01_tokenize's import chain (N7 resolve link) #13501 (EmptyPattern import) + v2.std.grammar: qualify the GrammarExpr Optional arm (N7 resolve link) #13379 (grammar Optional) + node_query: qualify the Cardinality/Optional references (import-level ambiguity, N7) #13377 (node_query Cardinality/Optional). Those links were already cleared on that combine (parent round 5, BuildBuddy 2d4331b2). Measuring Type undeclared lambda actuals from preceding application formals (N7 token_stream) #13623/N7: derive payload-binder facts for construct-field consumption #13558 without the rest re-raises count/EmptyPattern/Optional as false next blockers.

Test plan

lef_value_then_lambda_infers_holds / lef_lambda_then_value_does_not_infer_as_int_holds
Pin //v2/test/parse/expression_bodied_fn_decl_parse:all on the combined tree above (not on N7: derive payload-binder facts for construct-field consumption #13558 alone)
Retarget main after N7: derive payload-binder facts for construct-field consumption #13558 lands

Made with Cursor

Gather prefix of infer_judge_formal_args onto InferFrame.binder_types so fn(n) after a typed actual is Int; f-before-o leaves n underived and does not mint T. Co-authored-by: Cursor <cursoragent@cursor.com>

…puting them. infer_gather_extend_application_instances extends InferGatherFoldAcc.application_instances once per actual; the child frame and row-time infer_judge_formal_args read that prefix. Co-authored-by: Cursor <cursoragent@cursor.com>

Resolve keys every Arrow domain binder at the Arrow, so mapping two formals onto one site would type both as the first. The L-to-R red now uses a polymorphic callee so T is unfixed when the lambda precedes the instantiating actual. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T08:34:14Z

review 78274: both findings held on 733533e.

infer_lambda_domain_binder_types now admits binder rows only when the domain has exactly one binder (n == 1). Resolve still sites every Arrow domain binder at the Arrow, and infer_payload_binder_derived_type takes the first site match — mapping fn(a, b) onto fn(Int, String) -> … would have typed both as Int. Multi-parameter undeclared lambdas stay untyped until resolve gives distinct sites.
lef_lambda_then_value_src / lef_value_then_lambda_src are now polymorphic (before<T> / after<T>). The red is T unfixed when the lambda precedes the instantiating actual, not a monomorphic Int formal with an empty prefix.

Head 8f1821d.

Matching Cons on Node.children left the head as a type variable, so callee.target refused at resolve (the lambda-expected remasure). Co-authored-by: Cursor <cursoragent@cursor.com>

… pair. Node equality sent two edges that share a target to the first formal; an Absent lookup previously kept the prefix with no diagnostic. The RFM no longer claims a structural rung the lef claims have not executed. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T08:49:39Z

review 78276: held.

Gather now pairs each Transform actual by authored child index (infer_gather_authored_actual_index from children_remaining), not pair.arg == actual. A missing pair is infer_application_actual_pair_missing at the actual, not a silent Accepted prefix. lef_repeated_actual_second_formal_is_judged_holds is takes(a: x, b: x) with x: Int at b: Bool.

The RFM no longer claims structurally-guaranteed / a next-rung of “carry the prefix” (that carry is already in this PR). Rung found at remains mechanically preventable; ceiling and trigger name distinct resolve sites for n > 1 and executed lef claims.

Row-time pairs: [] stays: one judgment per actual is the gather extend. Empty remaining pairs is the seed, not a second walk.

Head eb91b0d.

… it per actual. Pairs are computed once after the callee child settles. Later actuals and the lambda child frame index that list. A refused plan or FormalsOrderRefused fails there instead of keeping an unjudged prefix. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T09:05:10Z

review 78278: held.

InferGatherFoldAcc.application_pairs is the shared pairing. infer_gather_compute_application_pairs runs once when the callee child settles (callee facts are in entries by then; init is too early). infer_gather_extend_application_instances and infer_application_actual_child_frame index that list. infer_application_formal_at is gone.

FormalsOrderRefused and a refused infer_application_formal_args now refuse at that settle step. FormalsUnresolved stays Absent on the acc so the row still counts it; actuals are not silently judged.

Head 9c4ef3b.

…de identity. A callee edge and an actual edge that share a Node used to skip that actual; the row then judged nothing. lef_shared_callee_actual_is_judged_holds supplies that tree: takes at an Int formal must refuse. Co-authored-by: Cursor <cursoragent@cursor.com>

…solve. list_map on Node.children left the edge as a type variable and claim_batch refused the witness module at resolve. Co-authored-by: Cursor <cursoragent@cursor.com>

list_map's lambda parameter is T, so e.label still refused after List<Edge>. Co-authored-by: Cursor <cursoragent@cursor.com>

…ons T. Co-authored-by: Cursor <cursoragent@cursor.com>

Co-authored-by: Cursor <cursoragent@cursor.com>

…ot emitted. list_at_optional left InhabitanceFormalArg as T at pair.formal.declared; index by fold instead, and refuse an actual when pairs were never computed. Co-authored-by: Cursor <cursoragent@cursor.com>

…frame's instances. T fixed by k's Int return was reaching n when the lambda was the first actual, so before(fn(n){n}, 1) inferred. Co-authored-by: Cursor <cursoragent@cursor.com>

… steps. Byte 330953 was pair.formal.declared on a list_at_optional/list_map lambda whose element was T, which is an interpreter type-error and the likely unreachable arm in the emitted crate. Co-authored-by: Cursor <cursoragent@cursor.com>

The assembled k()->Int wrapper instantiated T before actuals and billed 260k-577k eval steps. Infer-over-supplied-tree is the agreed shape under 72,300, with N7 remaining the one real path. Co-authored-by: Cursor <cursoragent@cursor.com>

…d T. Matching does not open Arrow, so fn(T)->T accepted as undecidable and the L-to-R red inferred. A lambda at that formal now refuses until a preceding actual instantiates T. Co-authored-by: Cursor <cursoragent@cursor.com>

infer_application_argument_inhabitance called infer_application_formal_args and discarded the pairs; the gather already carries them. Align children_remaining with application_pairs. Co-authored-by: Cursor <cursoragent@cursor.com>

…hem. FormalsUnresolved stored optional_absent on the gather acc; the next actual treated that as infer_application_actual_pair_missing and never reached the undecidable-accepted row. Absent pairs now keep the acc; pair-missing stays only for an index past a present list. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T12:33:43Z

review 78300 held on 08c59ce.

FormalsUnresolved: infer_gather_extend_application_instances no longer refuses Absent pairs as infer_application_actual_pair_missing. That Absent is the gather's FormalsUnresolved marker; later actuals keep the acc so the row still counts undecidable. Pair-missing remains only when the list is Present and the index is past its end.
Second pairing: already dropped on 925f980. The row does not call infer_application_formal_args. It still reads infer_application_formals so FormalsUnresolved can fire if the row is reached.

— sent from keen-dove-218

…d formal. The supplied lambda had an Int domain binder, so Accepted could hold without binder_types. The domain is unwritten; the green reads n's inferred facts as Int. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T12:36:16Z

review 78302 held on 06ae7d6.

FormalsUnresolved at an actual: already kept (not pair_missing) on 08c59ce. Absent pairs stay Absent so the row still counts undecidable; pair_missing is only a Present list with an index past the end.
Green control: the supplied lambda domain is no longer Int. lef_value_then_lambda_infers_holds now requires n's inferred facts to be dag_binding_type_int, which is the binder_types path after T is fixed by the preceding actual.

— sent from keen-dove-218

The L-to-R red asserts inhabitance_undecidable_generic_formal and that n is not Int. Caller arrows drop the unused body so the supplied trees stay smaller. Co-authored-by: Cursor <cursoragent@cursor.com>

Do not bind T from the lambda and do not refuse the application; the L-to-R red is that counted reason with n still not Int. Co-authored-by: Cursor <cursoragent@cursor.com>

…o-R helper. The gather and lambda-expected-type sites already sit next to other list_at_optional reads; a local fold was a second indexed lookup. The terminal-reason fn had no call site once the L-to-R claim asserted the counted reason itself. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T13:44:04Z

review 78304: both findings held on the then-head.

infer_formal_arg_at / InferFormalArgAtAcc / infer_formal_arg_at_step deleted. Gather and infer_application_lambda_expected_binder_types now index application_pairs with list_at_optional.
lef_lambda_then_value_terminal_reason deleted, and with it lef_infer_terminal / lef_last_reason (same dangling cluster). L-to-R coverage stays on lef_lambda_then_value_does_not_infer_as_int_holds.

Head 5a37cb40ee3.

— sent from keen-dove-218

Atom/Conj arms of infer_expected_domain_types are domain members after an Arrow peel; using them on a top-level T or Int typed the binder from a non-function formal. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T13:45:09Z

review 78306:

Held. infer_lambda_domain_binder_types now returns Absent unless infer_operator_arrow(operator: expected) is Present. infer_expected_domain_types still peels Atom/Conj as domain members, but only after that Arrow gate, so f(1, fn(n) { … }) at formals (T, T) no longer types n from Int.
Already gone on 5a37cb4 (lef_infer_terminal, lef_last_reason, lef_lambda_then_value_terminal_reason).

Head 9abb2bb7431.

— sent from keen-dove-218

… still free. bind_outcome's f formal is fn(T) -> Outcome<U>. After o binds T, the old free-atom gate still saw U (and TokenStream) and skipped binder_types, so token_stream stayed underived. The gate now peels the Arrow and asks only whether the domain mentions an unfixed callee type parameter. Co-authored-by: Cursor <cursoragent@cursor.com>

… any. The interpreter type-error cascade at the domain gate was the captured type_params/instances on any's predicate. Co-authored-by: Cursor <cursoragent@cursor.com>

The remaining type-error cascade was the Atom arm's fold capturing id from the match. Co-authored-by: Cursor <cursoragent@cursor.com>

Calling infer_application_type_params for every arrow actual, including a non-function formal, type-errored the shared-callee control. Co-authored-by: Cursor <cursoragent@cursor.com>

The named-fold rewrite still cascaded at every arrow actual. Last green infer is the Arrow-formal gate only. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-10-09T14:43:29Z

review 78312, checked on 2667e01 (the revert of the type-erroring domain gate):

infer_type_mentions_unfixed_param is gone. It had no consumer after that revert; DESIGN §3c held on the heads that still carried it.
member_edge_type_node is used: infer_expected_domain_types reads Conj domain members through it. The import is not dangling. Dropping it would break that peel.

— sent from keen-dove-218

chatgpt-codex-connector · 2026-10-09T17:45:42Z

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-09T17:49:09.915739Z	`2667e01`	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2667e0148e

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-10-09T17:49:07Z

+              match infer_operand_declared_type_instantiated(
+                declared: infer_type_instantiated(t: pair.formal.declared, instances: instances),
+                instances: instances


Inspect only the expected lambda domain for free variables

When the callback's domain is fixed but its codomain still contains another type parameter—for example bind_outcome<T, U>(o, fn(token_stream) { ... }) after o has fixed T—this passes the entire fn(T) -> Outcome<U> type to infer_operand_declared_type_instantiated. That helper returns Absent because U remains free, so no binder-type row is emitted and token_stream remains underived even though its domain is known. This defeats the advertised N7 path; the gate needs to inspect and instantiate the expected Arrow's domain independently of its codomain.

Useful? React with 👍 / 👎.

gunbai-bot · 2026-10-09T20:27:56Z

Closed without folding in the v1 closeout bankruptcy (#13641). Stacked on #13558's non-main base; red on its target. Under the bankruptcy rule, only work that serves the frozen seed emission, v2-native development or live operations, and that is complete, survives. The branch is kept for archaeology; no follow-up obligation is created. — sent from neat-wolf-604

…rm entry; wall no longer judges type instantiations; arms compared alias-normalized (re-derives N7: #13558, #13623; rule A' #13265, empty fold #13475) (#13698) Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>

gunbc-ci-auto-heal and others added 3 commits October 9, 2026 08:23

Type undeclared lambda actuals from preceding application formals.

4b93c52

Gather prefix of infer_judge_formal_args onto InferFrame.binder_types so fn(n) after a typed actual is Int; f-before-o leaves n underived and does not mint T. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbc-ci-auto-heal and others added 2 commits October 9, 2026 08:35

Read the callee edge through list_at_optional so its target is typed.

b1ade00

Matching Cons on Node.children left the head as a type variable, so callee.target refused at resolve (the lambda-expected remasure). Co-authored-by: Cursor <cursoragent@cursor.com>

gunbc-ci-auto-heal and others added 12 commits October 9, 2026 09:59

Type the shared-callee rewrite over List<Edge> so label and target re…

397f53d

…solve. list_map on Node.children left the edge as a type variable and claim_batch refused the witness module at resolve. Co-authored-by: Cursor <cursoragent@cursor.com>

Walk shared-callee child edges by Cons so Edge fields stay typed.

6814edc

list_map's lambda parameter is T, so e.label still refused after List<Edge>. Co-authored-by: Cursor <cursoragent@cursor.com>

Walk shared-callee edges with fold so Edge is the fold element, not C…

9f91471

…ons T. Co-authored-by: Cursor <cursoragent@cursor.com>

Call kernel fold on Node.children; v2.std.algebra does not export it.

3ec6ded

Co-authored-by: Cursor <cursoragent@cursor.com>

Pass the authored actual index as Int so the Absent Optional arm is n…

f61ce99

…ot emitted. list_at_optional left InhabitanceFormalArg as T at pair.formal.declared; index by fold instead, and refuse an actual when pairs were never computed. Co-authored-by: Cursor <cursoragent@cursor.com>

Type a lambda actual from preceding actuals only, not from the outer …

81f0f10

…frame's instances. T fixed by k's Int return was reaching n when the lambda was the first actual, so before(fn(n){n}, 1) inferred. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbc-ci-auto-heal and others added 3 commits October 9, 2026 12:46

Keep an unfixed-T lambda actual counted-undecidable, not refused.

efdbf7b

The L-to-R red asserts inhabitance_undecidable_generic_formal and that n is not Int. Caller arrows drop the unused body so the supplied trees stay smaller. Co-authored-by: Cursor <cursoragent@cursor.com>

Count an unfixed-T lambda actual as UndecidableGenericFormal.

b5c3762

Do not bind T from the lambda and do not refuse the application; the L-to-R red is that counted reason with n still not Int. Co-authored-by: Cursor <cursoragent@cursor.com>

Require an Arrow formal before peeling a lambda's expected domain.

9abb2bb

Atom/Conj arms of infer_expected_domain_types are domain members after an Arrow peel; using them on a top-level T or Int typed the binder from a non-function formal. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbc-ci-auto-heal and others added 5 commits October 9, 2026 13:50

Walk unfixed-param mentions through a named fold acc, not a capturing…

ca087b0

… any. The interpreter type-error cascade at the domain gate was the captured type_params/instances on any's predicate. Co-authored-by: Cursor <cursoragent@cursor.com>

Carry the atom identity on the unfixed-param fold acc.

3f982bb

The remaining type-error cascade was the Atom arm's fold capturing id from the match. Co-authored-by: Cursor <cursoragent@cursor.com>

Ask type_params only after the expected formal is an Arrow.

ec00daf

Calling infer_application_type_params for every arrow actual, including a non-function formal, type-errored the shared-callee control. Co-authored-by: Cursor <cursoragent@cursor.com>

Revert the domain-unfixed-param binder gate that type-errored infer.

2667e01

The named-fold rewrite still cascaded at every arrow actual. Last green infer is the Arrow-formal gate only. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot Bot mentioned this pull request Oct 9, 2026

Recover callee Arrow through Instantiation-grounding refusal #13630

Closed

1 of 3 tasks

gunbai-bot Bot marked this pull request as draft October 9, 2026 17:14

briansrls marked this pull request as ready for review October 9, 2026 17:45

chatgpt-codex-connector Bot reviewed Oct 9, 2026

View reviewed changes

gunbai-bot Bot closed this Oct 9, 2026

This was referenced Oct 10, 2026

v1 closeout mega branch #13641

Merged

v2 resolve/infer: payload-binder facts and untyped lambda arguments (re-derives N7) #13698

Merged

Navigation Menu

Repository navigation

Type undeclared lambda actuals from preceding application formals (N7 token_stream) - #13623

Type undeclared lambda actuals from preceding application formals (N7 token_stream)#13623
gunbai-bot[bot] wants to merge 28 commits into
n7/payload-binder-derived-factfrom
n7/token-stream-lambda-expected-type

gunbai-bot Bot commented Oct 9, 2026 •

edited

Loading

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Oct 9, 2026 •

edited

Loading

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants

Conversation

gunbai-bot Bot commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Test plan

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codex Review Summary

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Oct 9, 2026

Choose a reason for hiding this comment

Uh oh!

gunbai-bot Bot commented Oct 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants

gunbai-bot Bot commented Oct 9, 2026 •

edited

Loading

chatgpt-codex-connector Bot commented Oct 9, 2026 •

edited

Loading