Repository navigation
v2: typed cast node (Transform[coerce, e] + <cast-target>) — retire the as-cast refusal - #12368
gunbai-bot[bot] wants to merge 28 commits into
Conversation
…ted, instead of being dropped Step (0) of neat-boar-16's ordering for adhoc-bf64ffff-6d6. Measured on 748535d with a locally built gunbc: `fn f(x: Int) -> Int { let y: Q = x; y }` was ACCEPTED with Q declared nowhere -- Bind[binder, value, body] has no position for the annotation, so lowering dropped it before resolve. - body_lower_let_annotation_optional reads the annotation positionally (`let NAME : type_expr`); the statement-spine lowering refuses body_lowering_reason_type_annotation_not_carried at it. - New row gunbc.recurring_failure_mode body_type_annotation_dropped_before_resolve_in_v2. It also records the worse fn-literal route: `let g = fn(y) -> Q { y }` lowers to Bind[g, Atom(kw_fn), ..], the whole literal dropped by body_lower_bound_value's operand arm. That route is left to gunbc#12210, which rewrites exactly that lowering, and is named as its trigger. - Controls v2.test.claim.body_type_annotation_refusal: btar_let_annotation_refuses (red before), btar_unannotated_let_accepts (twin), specimens enrolled in floor_pure_producer_share. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…fused population and its restoration trigger (review 71023) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…atom operand fallback no longer answers a keyword token Side-chat REQUEST_CHANGES on 7d0262d (overrides the deferral to #12210: a deferred silent accept is what section 5 forbids). - body_lower_bound_value refuses a fn literal's return annotation (body_lowering_reason_type_annotation_not_carried) at the authored type expression before the operand arm sees the literal. Census: the grammar admits no other annotation on a function literal (fn-literal and arrow-lambda parameters are bare identifiers). - The eraser: body_lower_try_operand_or_reject's first-atom fallback returned Atom(dag_token_kw_fn) for a literal wherever it ran (let value, if arm). body_lower_atom_is_keyword_token declines a lexer keyword token there (true/false are read earlier as literals). Probed positions (let value, if arm, fn tail, match arm, record field, data initializer) all refuse loudly now. - Controls: btar_fn_literal_return_annotation_refuses (exact reason + locus is the authored Q), btar_unannotated_fn_literal_is_not_erased (disposition changes on purpose: it was Accepted only by erasure), btar_if_arm_fn_literal_is_not_erased; btar_let_annotation_refuses now asserts the locus, and anchoring it at the surrounding let reds it (mutation run locally). All 5 green locally. - RFM: fn-literal climb recorded; rung revision explicitly pending the floor run. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…revised to rung 1 after the required floor passed on d2d840a Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rget> label rule (handoff to the let-annotation lane; unbuilt) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…annotation_not_carried reason Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ot_carried, located at T) instead of being dropped Census branch for neat-boar-16 (measure before choosing the carrier). Unrun locally. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ms reach the fold's refusal; if/match-arm controls Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…_carried; RFM row rung + typed-cast-node trigger; enroll producers Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e-applied as OperandRefRefused at Q on the new arm reader Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…left behind Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…pair Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e' into session/loyal-crab-333
…adable chain carrying a cast refuses
… on the rung with its capability trigger
…nts; Bind stays PositionalEdges until the let carrier lands its producer (review 71396)
…o refusal (review 71406)
… a Loop's own named edges pass the resolver gate (neat-boar-16)
…havior Named edges are validated at resolve (rung 3); trigger is a closed label coproduct in v2.std.node (review 71525 ruling)
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3759fdc9c1
ℹ️ 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".
| Named { name: _ } => | ||
| if edge_is_cast_target(e: e) { | ||
| resolve_type_role_target(ctx: ctx, target: e.target) |
There was a problem hiding this comment.
When a valid cast node places <cast-target> before its positional children, child_walk_step advances acc.ordinal for the named edge, so the first positional coerce child bypasses resolve_transform_operator_child and is resolved as an ordinary value. The new node discipline permits the named edge in either position—and content hashing explicitly canonicalizes both orders to the same identity—so equivalent cast nodes can have different resolve outcomes. Track the positional ordinal rather than the total edge ordinal.
Useful? React with 👍 / 👎.
| bind_outcome( | ||
| o: target_transform_positional_operand_binding(node: body, index: 1), | ||
| f: fn(operand_binding) { | ||
| bind_outcome( | ||
| o: target_value_expr_arrow_body_scope_binding(arrow: arrow, body: body, binding: operand_binding, target: target), |
There was a problem hiding this comment.
For a cast whose operand is computed or literal, such as (x + x) as Int or 1 as Int, this binding-only helper rejects the operand: target_transform_positional_operand_binding accepts only an atom and the following scope check requires that atom to denote an arrow parameter. Lowering and inference added here explicitly accept computed cast operands, but emission therefore fails with a transform-shape or scope-binding diagnostic instead of emitting the representation-preserving operand. Project the operand through the existing body-subexpression path rather than treating every cast operand as a parameter reference.
Useful? React with 👍 / 👎.
|
Closing. This PR was auto-opened by the dashboard bot from session/loyal-crab-333 AFTER that branch's content landed as #12315 (squash 696a77d, approved at 7a25102). The diff against main is the pre-squash branch, plus scratch debug probes under src/v2/test/scratch/ that review 71610 correctly flags as unconsumed (§3c/§6). Nothing here is pending work. The typed cast node is on main; the refinement-predicate follow-up is tracked separately. — sent from neat-boar-16 |
Auto-opened by session-dashboard for session
loyal-crab-333.Pushing to
session/loyal-crab-333advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan