Repository navigation
v2 resolve/infer: the dotted-path decision keeps its binding kind, and projection inference stops calling an unretrievable declaration a fieldless receiver - #12506
Conversation
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…nt and one Bool value type An application of a derived Arrow now takes the type the Arrow declares it returns (read from the return atom as written), and a bodied Arrow is admitted only when its body's type equals that return, else arrow_body_does_not_inhabit_declared_return. Before this, no application derived, Int included, and eval refused both Int and Bool applications. dag_binding_denotation is the one binding->value-type join, and its rows point at v2.std.integer integer_int_type_node and v2.std.logic bool_node. The literal rules consume it, a type-name atom derives its kind (TypeDenotationKind), and the evaluator's own Int and Bool type nodes are replaced by the same authorities. Model and ruling are in docs/plans/arrow-elimination-model.md; the composed-evidence defect is filed as function_type_evidence_carries_its_body. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… kind, not the retired inhabitant denotation The parameter conj's composed evidence carries each Int type atom's derived grounding. After the arrow-elimination ruling that grounding is the atom's kind (TypeDenotationKind); the control still asserted the roster's Int inhabitant record, the denotation this PR retired. Found by the srv1 base-vs-head run over the v2 infer/eval/compile test modules (the one true->false). The partial-evidence control's use of the inhabitant node as a roster member is unrelated and unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…_discharge to holds/violated; one runtime encoding of true - infer_arrow_elimination eval control: after the merge of main (#12375) infer returns ObligatedInferredTree, so the control reaches eval through discharge_refinement_obligations, the only route to an InferredTree. - refinement_discharge's frontier row flips as it said it would: a true predicate admits, a false one refuses refinement_predicate_violated. The undischargeable arm is kept over a genuinely unevaluable application (an undenoted return). - The flip exposed two runtime encodings of true: v2_eval_bool_true_primitive was a one-bit byte while every evaluated Bool is built by v2_eval_bool_runtime_value (eight bits), so discharge read an evaluated true as violated. The primitive is now that constructor's value. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…; cut every consumer root-first Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…heck clean) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…over-reached) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…parameter_order, reference_closure) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… conflict with #12361) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
THE GAP. v2.compiler.infer's infer_node_facts routes a declaration reference --
Conj-shaped, so infer_atom_binding_sym answers Absent -- straight to
inferred_facts_not_derived. An entry IS admitted for the node and its grounding is
GroundingNotDerived, so inference ACCEPTS the tree and eval refuses later at
whatever consumes it. Nothing typed a reference to a function.
THE REPAIR, IN ONE ARM. Resolution answers WHICH declaration a reference denotes
and carries it as a declaring path; this arm answers WHAT TYPE that declaration
establishes for the use. Two questions, two stages: nothing here re-resolves a
name and resolution mints no types.
declaration_reference_path_optional(n) the declaring path, never the leaf
symbol_index_lookup(resolved.symbol_index, path) the GUARDED read: a path with
more than one bound declaring
answers Absent, so a contested
binding cannot yield a type
arrow_domain_binder_labels(declared.children) evidence check
inferred_facts_from_derived_type(n, declared) evidence attached to the USE
A LOOKUP HIT IS NOT TYPE EVIDENCE. The index is built from validated normalized
roots, which does not establish that every indexed declaration carries usable type
evidence, so this arm does not ground on presence. A callable's evidence is its
Arrow and the check is that its domain reads; an unsupported or unresolved
signature stays explicitly ungrounded. Non-callable declarations are left to their
own derivation rather than stamped.
THE EVIDENCE ATTACHES TO THE USE. derived_type is the DECLARATION's node while the
entry is keyed by the REFERENCE node, so the use keeps its own occurrence and
locus and canonical_grounding_from_derived_type's self-evidence refusal still
holds.
THE CARRIER IS #12432's, CONSUMED NOT REBUILT. ResolvedTree { root, symbol_index }
already reaches fn infer(tree: ResolvedTree); it was never threaded past there --
symbol_index appeared exactly once in 04_infer.dag, in a comment. The thread is
`resolved: ResolvedTree` under a NEW name at every site, not a second
`index: SymbolIndex` parameter: passing root and index side by side lets them come
from different trees and disagree, and nothing would stop it, while the paired
carrier makes the mismatch unwritable (DESIGN section 5, construction over
validation). Functions that want the root read resolved.root.
ELEVEN FUNCTIONS, NOT THE SIX ESTIMATED. The compiler found the other five --
infer_gather_transform_row_on_entries, infer_gather_application_row_on_entries,
infer_gather_bind_annotation_row_on_entries, infer_gather_fold_step_merged,
infer_gather_settled_row -- which is the argument for renaming at every site
rather than adding a parallel parameter. Non-path callees keep `tree: Node` and
receive resolved.root, so their contracts are untouched. The thread landed first
as a 41/41 behaviour-neutral change, verified by the regression guards passing
with the control still red, so any guard breakage would be attributable to the
derivation rather than the rename.
PARAMETER TYPING IS NOT REPLACED. infer_parameter_scope_search /
infer_parameter_type_in_scope stay. Their comment names "the SymbolIndex /
ResolvedTree.bindings lookup" as their dissolution trigger, and it is tempting to
read this change as that trigger; it is not. A local use resolves to a canonical
Atom at its own occurrence and never acquires a declaring path, so the index
answers a different question. What was established here is only that
symbol_index_fill puts Arrow DOMAINS in the index -- a fact about fill, not about
what a parameter use resolves to. Deleting the walk on that basis would have
reintroduced the defect its comment records: `fn positive(x: Int)` beside
`fn f(x: Pos)` grounding every `x` in `f` as Int.
EVIDENCE.
dre_a_reference_grounds_to_its_declarations_contract_holds FAIL -> PASS
bcn_cast_into_a_refinement_refuses_at_infer PASS unchanged
bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS unchanged
bcn_identity_cast_into_a_refinement_admits PASS unchanged
The control asserts the CONTRACT, not the grounding tag: it selects every node
whose decoded declaring path ends in the wanted leaf, requires EXACTLY ONE, and
requires the derived type's Arrow domain to bind exactly the name the fixture
text specifies. A DerivedGrounding carrying the wrong type fails it.
NOT QUALIFIED, STATED AS SUCH. dre_a_same_leaf_reference_gets_its_own_declarations
_contract_holds passes but is NOT yet an identity-collapse detector. The forced-
collapse mutation turned BOTH controls red rather than only the same-leaf one,
because the mutation's path does not exist in the first fixture either -- it broke
everything instead of specifically collapsing identity. Within a single-module
fixture the discriminating case cannot be built: a reference that reaches this arm
denotes a module-level callable whose declaring path IS [module, leaf], so path
and leaf coincide. Qualifying it needs a two-module fixture where each module
declares the same leaf. Until that runs, this control is specified, not qualified.
NOT DONE HERE. The application connection (#12379's rule wants a callee Arrow, and
a reference now grounds to one) and the s3 end-to-end assertion are the next step,
and the outer equality may still lack a typing rule of its own.
Based on #12432 (ResolvedTree carrier) and #12379 (application-result typing);
rebases onto #12379, which lands first.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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. |
|
Draft until the stack lands. Two things a reviewer needs before this is rebaseable. This PR is third in a stack and cannot target main yet. It depends on #12432 (the A second parameter is being threaded through the same chain. Main now carries That is worth a decision rather than a merge resolution. The reasoning that chose a single paired carrier here — root and index passed side by side could come from different trees and disagree, with nothing to stop it, so pairing makes the mismatch unwritable — applies with equal force to a third parameter. If No evidence in this PR changes: the control went FAIL → PASS and the three refinement guards are unchanged, all measured on the pinned base |
![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: 3c43400b1a
ℹ️ 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".
| fn infer_transform_application_optional(node: Node, entries: List<InferredFactsEntry>) -> Optional<Outcome<InferredFacts>> { | ||
| match infer_application_callee_arrow(node: node) { | ||
| Absent => optional_absent() |
There was a problem hiding this comment.
For ordinary resolved source such as callee(only_arg: y), the operator is a declaration-reference Conj, not the declaration's raw Arrow. Consequently infer_application_callee_arrow returns Absent; argument checking reports FormalsUnresolved, arguments_decided becomes false, and this new elimination path is never reached. Thus applications of named corpus functions remain GroundingNotDerived even though the callee's inferred facts now carry the Arrow; only the inline-Arrow test fixture exercises this branch. Read the callee's derived evidence from entries and use that Arrow for both formal checking and elimination.
Useful? React with 👍 / 👎.
MY COMMENT CLAIMED MORE THAN MY GUARD CHECKED. The arm grounded a reference when arrow_domain_binder_labels could read the declaration's parameter names, and the comment beside it said an unsupported or unresolved signature stayed ungrounded. That was false of the guard. That reader takes only `children`, so it never establishes the declaration IS an Arrow, and it inspects no parameter type, no return type, no scope and no body. "I can read the parameter names" is a different property from "this declaration establishes this callable type", and the comment asserted the second while the code checked the first -- rung inflation in the annotation, caught in review rather than by a control, because no control distinguished the two. THE GUARD IS NOW THE APPLICATION PATH'S OWN REQUIREMENTS, reused rather than restated: infer_operator_arrow (the node IS an Arrow), infer_formals_from_domain (every formal is named), and arrow_declared_parameter_order, where both Absent and Malformed refuse -- the domain is sorted by label for identity, so its stored sequence is not the declared order and an Arrow without the order edge is one a binder already refuses. Grounding a reference whose declaration cannot satisfy those would mint evidence no consumer can use. WHAT IT STILL DOES NOT ESTABLISH, stated rather than implied: the type references inside that signature are not resolved in the declaration's scope here, and no body or return obligation is discharged. Those stay with the existing inference contract; a reference consuming a declared signature does not recheck a body at every use. The claim is the structural callable contract and nothing wider. Controls unchanged in outcome and now discriminating for the right reason: dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
FIVE ATTEMPTS, NO DISCRIMINATING CONTROL. A single-module fixture cannot produce one: a reference reaching this arm denotes a module-level callable whose declaring path IS [module, leaf], so path and leaf coincide and a leaf-keyed lookup is accidentally right. A two-module fixture reaches the right shape -- two modules each declaring `shared(alpha: ...)` with different types, the consumer importing one -- but the assertion needs the parameter's declared TYPE read out of the derived Arrow's domain, and neither a walk-order atom search nor find_named_child on the domain produced it. The control stayed GREEN under a mutation that forced the wrong declaration, and then went RED on correct code once the reader changed: both arms wrong, so it distinguished nothing. A green control that does not discriminate is worse than no control, because it would be cited as coverage. A red one blocks the PR while asserting nothing. So neither ships; the gap is recorded where the control would have been. WHAT IS THEREFORE NOT CLAIMED: that this arm resists declaration-identity collapse. The declaring path is what it looks up and symbol_index_lookup is the guarded read, but no executed control here demonstrates that a leaf-keyed answer would be caught. Qualifying it needs a reliable reader for a parameter's declared type inside a derived Arrow domain; that reader is the missing piece. Retained and passing: the two controls that do discriminate their own properties, and the three refinement guards. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Two follow-ups landed, and one asked-for control is reported as a gap rather than shipped. 1. The guard now checks what my comment claimed ( Worth noting the detection path: this was caught in review, not by a control. Both of my controls passed under the weak guard and the strong one, so nothing I had written distinguished readable labels from established callable type. 2. The same-leaf discriminator is NOT qualified ( A single-module fixture cannot discriminate: a reference reaching this arm denotes a module-level callable whose declaring path is A green control that does not discriminate is worse than none, since it would be cited as coverage; a red one blocks the PR while asserting nothing. So neither ships, and the gap is recorded in the file where the control would have been. What this PR therefore does not claim: that the arm resists declaration-identity collapse. The declaring path is what it looks up and Also corrected from my earlier comment: |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Exact-head re-review: 707cc49 — HOLD.
Reviewed the two-commit successor delta from 3c43400, the complete reference-evidence witness, and the relevant inference/application/grounding consumers at this exact head. This is a source review, not an execution receipt or a re-review of all prerequisite PRs. No tests, mutations, native builds, or seven-test runs were executed here. This COMMENT is not a formal GitHub REQUEST_CHANGES review.
The explicit Arrow check and absent/malformed parameter-order handling are real improvements. Keeping local-parameter typing unchanged is also correct. Recording the unsuccessful identity-control attempts rather than claiming coverage is appropriate. Three items remain before merge qualification:
- [P1] infer_declaration_callable_evidence still proves callable syntax, not the resolved type asserted by DerivedGrounding.
infer_operator_arrow checks node.kind. infer_formals_from_domain checks Conj/Named structure and copies each e.target into InhabitanceFormal.declared without validating its type. arrow_declared_parameter_order checks order metadata. None resolves parameter/return type references in the declaration's scope or even reads the return type in this new guard. Nevertheless infer_declaration_reference_facts calls inferred_facts_from_derived_type with the entire indexed declaration as derived_type. canonical_grounding_from_derived_type only rejects evidence equal to the use node; it does not discharge those missing derivations.
Consequently a readable, correctly ordered Arrow whose signature has unavailable/unresolved type evidence can be stamped DerivedGrounding at this interface. This is a source-derived counterexample obligation, not an executed exploit or a claim that a complete invalid program passed. The new comment narrowing the claim to 'structural callable contract' cannot narrow the established meaning of InferredFacts.grounding for downstream readers.
Required: consume or derive the actual callable signature evidence through existing declaration/type authorities. Keep unresolved type evidence explicitly underived/refused; retain body/refinement obligations through their existing contract rather than silently discharging them, and do not recheck/copy an entire body at every reference. Add the previously requested readable-signature-with-unresolved-types negative against this actual producer, with a supported positive beside it. Also discriminate the newly fixed non-Arrow and missing/malformed-order guards cheaply. This does not require completing all inference.
- [P1] The intended application consumer is still structurally disconnected, not merely unmeasured.
infer_application_callee_arrow reads the application's first positional child and calls infer_operator_arrow on that NODE. A resolved declaration reference is still a Conj, even when its facts now contain an Arrow. The helper has no facts input. It therefore returns Absent before consulting the new evidence. infer_application_formals consequently returns FormalsUnresolved, and infer_transform_application_optional uses the same helper. Adding an Arrow to facts cannot change either branch.
Required: have the existing application path obtain the callable contract from the actual callee use and its established evidence, then use that same contract for formals, type parameters, argument checking and result typing. Preserve the reference occurrence and canonical declaration identity; do not inline declaration bodies or introduce a second named-call rule. Facts lookup must remain anchored to the relevant subject rather than treating a type-evidence node as an interchangeable source-node key. Add one named-call control proving the application itself grounds and executes, plus an invalid-argument negative; the reference-only PASS cannot substitute. Then rerun s3. Equality may remain a separate frontier and must not be used to misreport whether this application connection works.
- [P2] The same-leaf identity obligation remains unqualified, and the positive witness still observes labels rather than types.
dre_uses_of selects by last segment, and dre_grounded_domain_labels checks only the domain labels via a children-only reader. A wrong contract with identical binder names can satisfy it. The existing two tests do not demonstrate preservation of declaring identity or parameter/return types. A source comment accurately records the gap, but does not discharge the boundary's acceptance condition.
A reader already exists at this exact head: after obtaining the established callable Arrow and its domain, infer_formals_from_domain returns InhabitanceFormal { parameter_identity, declared: e.target }. Select the intended formal by identity and inspect .declared; do not search for an arbitrary descendant atom. Compare against independently specified expected type evidence (or a complete expected callable contract using the existing structural equality authority), not a second lookup through the implementation under test.
Use two qualified declarations with the same leaf AND the same parameter label but distinct types. Select each reference by full expected path. Force the wrong EXISTING declaration so lookup still succeeds and the contract assertion must fail; forcing an absent path tests a different property. If this currently yields raw unresolved type nodes, that is finding 1, not a reason to weaken the expected types. Keep one supplied-input discriminator and one real source/resolve/infer connection, without rebuilding the whole compiler for every unit assertion.
Landing scope remains unchanged: no parameter-scope deletion, no new context unification, no new scanner or general typechecker. Management owns reconciling #12432/#12379/current main once; this lane owns the safe declaration-evidence derivation and its actual named-application consumer. The current PR is not ready merely by documenting the two missing controls, and no progress on s3 or the seven is established by the reference-only claim.
…still is not enough THE CONNECTION WAS ABSENT IN CODE, not merely unmeasured. infer_application_callee_arrow read the callee EXPRESSION's own kind through infer_operator_arrow, and a resolved declaration reference stays a Conj however well typed it is -- so the helper answered Absent for it and every consumer (formals, type parameters, argument inhabitance, result typing) fell through to the undecidable-accepted arm. Giving the reference callable facts did not make any of them read those facts. Adding evidence and consuming evidence are two changes and only the first had landed. infer_application_callee_arrow_with_facts falls back to the callee's own facts entry when the node is not itself an Arrow, taking ONLY the type from DerivedGrounding's structural evidence. The use keeps its node and occurrence; the declaration's body and identity are not substituted. Wired at the three sites that asked the old helper, with entries threaded into infer_application_formals and infer_application_type_params -- the other two callers already carried entries. NECESSARY, NOT SUFFICIENT, AND THE CONTROL SAYS SO. A named call still does not ground. dre_a_named_call_is_grounded_expected_red is enrolled as an executed expected-red rather than a passing claim or a deleted one: the boundary is real, its cause is not yet identified, and naming it is the next step rather than widening the reader until something goes green. What is missing between a grounded callee and a grounded application is unestablished -- I did not determine whether the call's facts entry is absent or present-and-ungrounded, and that distinction picks the repair. Guards unchanged, including the two application-typing rows: bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS dre_a_reference_grounds_to_its_declarations_contract_holds PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Coordination request from session eager-ibex-722 (node adhoc-c5971a11-e8a, ruled by neat-boar-16). After #12432 lands, v2 resolve will emit named-fn parameter references as declaration-reference spines keyed in SymbolIndex (paths like A reference to a parameter would then reach your "reference to a corpus declaration is typed by that declaration" arm and be typed by its declared type, which is the intended grounding. Questions for this PR's owner:
|
…e type
THE REMAINING FAILURE WAS ONE MISKEYED LOOKUP. After the application path could SEE
a reference's callable evidence, the call still did not ground, and the cause was
in infer_transform_application_optional:
match infer_application_callee_arrow_with_facts(...) {
Present { value: arrow } =>
match lookup_inferred_facts_in_entries(entries: entries, key: arrow) {
That key is right only while an arrow can be the callee node itself. Once the arrow
may be a DECLARATION's Arrow reached through the use's facts, it is a node of the
declaring module with no entry in this tree, so the lookup answered Absent and the
application dropped to the frontier however well the callee was typed. The grounding
question is about the CALLEE USE; the arrow supplies only the TYPE. They are two
things and only the first has facts here. infer_application_callee_use names the
first; the second stays what it was.
dre_a_named_call_is_grounded_holds goes from an enrolled expected-red to a passing
claim on that one change.
A BOOL-RETURNING CALL STILL DOES NOT GROUND, AND IT IS A DIFFERENT BOUNDARY.
Measured three ways on this base: an Int-returning call grounds; a Bool-returning
call with a literal body does not; a Bool-returning call whose body is its own
parameter does not either. The variable is the RETURN TYPE, not the body, and the
reference itself grounds in every one of the three -- so this sits downstream of the
reference repair, in the application's return derivation,
infer_arrow_declared_return_type -> dag_binding_denotation. Enrolled as an executed
expected-red rather than deleted or chased: which binding symbol a Bool return
actually carries is the next question and answering it is a separate change.
THE EXECUTION CONTROL IS DELIBERATELY BOOL-RETURNING, which is why the boundary
surfaced here rather than later: an Int-returning call compared with `==` would have
coupled the first execution proof to equality, which has its own unproven typing.
Guards unchanged, including both application-typing rows:
bcn_cast_into_a_refinement_refuses_at_infer PASS
bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS
bcn_identity_cast_into_a_refinement_admits PASS
bcn_infer_admits_int_to_int PASS
bcn_infer_refuses_int_to_bool PASS
dre_a_reference_grounds_to_its_declarations_contract_holds PASS
dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
INT MASKED THE READER'S ASSUMPTION AND BOOL EXPOSED IT. infer_arrow_declared_return_type sent every return Atom's identity to dag_binding_denotation, which is a BINDING-to-type operation. Int survives that because its canonical type constructor retains the historical spelling ^dag_binding_type_int, so its binding and type identities coincide and a second denotation is a no-op. Bool arrives as the DENOTED node -- v2.std.logic bool_node, ^bool_node_symbol -- so the binding lookup answered Absent and BOTH consumers of this shared reader lost the return: application result typing dropped to the frontier, and the body-versus-declared-return check skipped its comparison. MEASURED BEFORE REPAIRING. An Int-returning call grounds; a Bool-returning call with a literal body does not; a Bool-returning call whose body is its own parameter does not either. The reference itself grounds in all three, so the variable is the RETURN TYPE and not the body. The return atom was then read directly: Int carries ^dag_binding_type_int, Bool carries ^bool_node_symbol. THE REPAIR RECOGNISES BY AUTHORITY, NOT BY SPELLING. The established case is compared against v2.std.logic's own bool_node() through the existing structural equality, rather than teaching a second meaning for ^bool_node_symbol here or widening dag_binding_denotation to accept a denoted symbol -- that lookup stays strictly binding-to-type, so a specimen fix does not become a muddied contract. Ordered denotation-first, so the Int path is byte-identical and only a return the binding lookup cannot denote reaches the established-type question. ONE reader, so introduction and elimination cannot disagree about the same signature. dre_a_named_call_to_a_bool_fn_is_grounded_holds: expected-red -> PASS. THE MISMATCH NEGATIVES ARE RED, AND THAT IS PRE-EXISTING, NOT INTRODUCED. infer ACCEPTS a Bool-declared function with an Int body and the converse. The cause is upstream of this reader: infer_arrow_body_inhabits_declared_return is only reached when the Arrow carries evidence edges; without them the arm answers inferred_facts_not_derived, and a frontier is not a refusal, so the comparison never runs. Verified by reverting ONLY the return reader and re-running -- both rows fail identically. Enrolled as executed expected-reds rather than deleted: they are exactly the controls that would catch a return recognition which admitted nodes without activating the check, they cannot discharge that duty while the check is unreachable, and when the evidence-edge condition is repaired they become its guard without anyone rediscovering the shape. The eight input-inspection diagnostics that located this are removed; their results are recorded above rather than left as permanent obligations. Guards unchanged: bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS dre_a_named_call_is_grounded_holds PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… again THE PREREQUISITE WAS THE RETURN ATOM'S OWN GROUNDING, not the check. infer_arrow_body_inhabits_declared_return runs only when infer_product_child_evidence_edges answers Present, and that collector requires EVERY Arrow child to carry a resolved type. A Bool return atom carried none, so the whole Arrow dropped to inferred_facts_not_derived -- the frontier -- and the comparison never ran. A frontier is not a refusal, which is why a Bool-declared function with an Int body was ACCEPTED rather than reported. So the same defect had two faces: the reader could not denote an already-denoted return (fixed in 53022c2), and infer_node_facts could not ground one either. Both are the same assumption -- that a type-position Atom is a binding awaiting denotation -- and Int masked both because its binding and type identities coincide. THE SECOND HALF, BY THE SAME AUTHORITY. The denotation arm of infer_node_facts now consults infer_established_return_type_optional, which compares against v2.std.logic's own bool_node() through the existing structural equality. One recognition, reused; no second meaning for ^bool_node_symbol, and dag_binding_denotation still stays strictly binding-to-type. Ordered after the binding lookup, so every previously-denoted path is byte-identical. UNAVAILABLE EVIDENCE DID NOT BECOME A PASSED CHECK. The repair makes the return atom GROUND, which makes the check RUN, which makes the mismatch REFUSE. Nothing was forced to ground to get there and no refusal was weakened: the two controls went from ACCEPTED (wrongly) to REFUSED (correctly), which is the opposite direction from admitting more nodes. dre_a_bool_declared_int_body_still_refuses_holds expected-red -> PASS dre_an_int_declared_bool_body_still_refuses_holds expected-red -> PASS Reference typing, application typing and the return derivation stay connected: dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS dre_a_named_call_is_grounded_holds PASS dre_a_named_call_to_a_bool_fn_is_grounded_holds PASS bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…efused FOUR CONTROLS, BATCHED ON THE PINNED BASE. dre_an_unresolved_signature_does_not_ground_holds PASS dre_an_invalid_argument_call_does_not_ground_holds PASS dre_an_imported_reference_grounds_the_same_way_holds PASS (with the two mismatch negatives promoted in 5359640) UNAVAILABLE EVIDENCE DOES NOT BECOME A PASSED CHECK. A signature whose parameter type names nothing reads structurally and means nothing: the shape is readable, the evidence is not, and the reference stays underived. That is the control a permissive fallback would have turned green, and it is the one that keeps infer_declaration_callable_evidence honest about what "callable evidence" claims. AN INVALID ARGUMENT DOES NOT GROUND THE CALL. A Bool passed where the declared parameter is Int leaves the application ungrounded, so the contract is not satisfied merely because the callee's type was found. THE IDENTITY DISCRIMINATOR IS NOW QUALIFIED, and by the mutation that the earlier five attempts could not construct. Those attempts failed because a single-module fixture cannot separate path from leaf -- a module-level callable's declaring path IS [module, leaf]. Across two modules it separates: repointing the imported reference's lookup at a DIFFERENT EXISTING declaration (m.app rather than m.lib.helper, so the lookup still SUCCEEDS) turns that row red while the same-module call stays green. That is wrong-declaration selection being detected, which an absent-path mutation could never establish -- it tests missing evidence instead. So the claim this PR would not make three commits ago is now made on executed evidence: the arm resists declaration-identity collapse. Full set on the pinned base 80e9a04: dre_a_reference_grounds_to_its_declarations_contract_holds PASS dre_a_same_leaf_reference_gets_its_own_declarations_contract_holds PASS dre_a_named_call_is_grounded_holds PASS dre_a_named_call_to_a_bool_fn_is_grounded_holds PASS dre_a_bool_declared_int_body_still_refuses_holds PASS dre_an_int_declared_bool_body_still_refuses_holds PASS dre_an_unresolved_signature_does_not_ground_holds PASS dre_an_invalid_argument_call_does_not_ground_holds PASS dre_an_imported_reference_grounds_the_same_way_holds PASS bcn_cast_into_a_refinement_refuses_at_infer PASS bcn_cast_out_of_a_refinement_refuses_until_carrier_widening PASS bcn_identity_cast_into_a_refinement_admits PASS bcn_infer_admits_int_to_int PASS bcn_infer_refuses_int_to_bool PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
THE TYPING IS DONE; THE EXECUTION IS NOT, AND THE BOUNDARY IS ELSEWHERE.
A named Bool-returning call now grounds under infer -- reference typing, application
typing and the return derivation all reached -- and the same call through the REAL
native route refuses at EVAL with eval_rejected_grounding_not_derived at a SYNTHETIC
node carrying no authored locus.
So this lane's subject is complete in the sense it was scoped: a reference obtains a
justified callable contract, the application consumes it, valid and invalid cases
separate, and the body/return check is reachable again. What it does not deliver is
an executed assertion, because eval's facts gate is asked about a node this lane
never touches.
THE FALSE CONTROL EARNED ITS PLACE BY NOT DISCRIMINATING. Both rows refused
identically, so neither body ran and a refusal is indistinguishable from a false
answer at this point. Had only the positive row existed, the same outcome would have
read as "the call returned false" rather than "nothing executed".
THE SIGNATURE IS NOT NEW, which is the useful part: a plain-binder match over a
coproduct, and a trivial `fn f(b: Box) -> Int { 7 }` whose assertion never touches a
field, both refuse at eval on this same cause at a synthetic node. Three unrelated
subjects, one wall. That says the next boundary is eval's grounding consumer and not
anything about calls, and it is where the next lane should start rather than
rediscovering it.
Enrolled executed as expected-reds rather than deleted, so the measurement survives
in the corpus with its subject attached.
nc_a_named_bool_call_executes_expected_red eval refusal
nc_the_false_returning_call_is_the_deliberate_false_control_expected_red eval refusal
universe=2 population=2 file_refusals=8
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ng path
The native qualification refused with eval_rejected_grounding_not_derived on a
node the renderer prints only as "<synthetic node occurrence>", which is a
PROVENANCE CATEGORY and not an identity -- so that log alone could not say which
node, and could not distinguish this from an unrelated universal eval defect.
This control supplies the same call shape at the eval boundary and reads the
refusal anchor directly. It is the one comparison that decides it, and it says:
the anchor is a node strictly inside the callee reference's encoded declaring
path.
So eval is demanding value-grounding for the internal representation of a
declaration identity rather than consuming that identity as a reference. The
route is established by source and now confirmed by measurement:
eval_node_is_callee_reference admits an Arrow and a bare Atom only
-> a resolved reference is a MARKED CONJ (resolve resolved_reference_node)
-> the callee edge is not recognized, eval_fold_child_for_edge takes its
ordinary recursive arm
-> the walk descends into the encoded declaring path, whose spine
declaration_reference_node builds at OccurrenceSynthetic
-> infer visited those spine nodes too, so each holds an entry with
grounding UNDERIVED rather than no entry, which is why the gate reports
grounding_not_derived and not a facts lookup miss.
The fixture's own positive control is enrolled beside it, so a later red is a
statement about eval and not about an assembly that stopped producing a call.
Both claims PASS on this base.
This corrects the earlier grouping. Three subjects sharing a reason string is
not evidence of one defect; a synthetic occurrence is a provenance category, and
two of those subjects contain applications of their own. They are grouped only
once their failing nodes and consumer paths agree, and this file establishes the
failing node for THIS subject alone.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…unbc into HEAD # Conflicts: # src/v2/workflow/floor_pure_producer_share.dag
…ough nullary reason producers a_receiver_with_no_such_child_never_accepts and a_local_receiver_method_call_never_accepts asserted !infers, so any refusal satisfied them; they now assert infer_reason_projection_receiver_declares_no_fields, read from one nullary producer per fixture (xl0r_field_access_infer_reason, xl0r_method_call_infer_reason) over the already-warm resolve. The method-call row measured 76.6k steps against the 72.3k new-witness budget on run 37083779039. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… xl0r infer-reason producers WARM Roster-only, separable. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…dence-consumer Two conflicts. non_fold_residue: this lane's eval-projection reason/dissolution pair beside main's change at the same anchor (kept). design-rung-drops.md is generated and its driver refused: composed main's version (which retires the self-host emission board row) with this lane's match_arm_binder_typing section at the same anchor; the generated-artifact phase adjudicates it against the roster. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…artifact drift after the main merge) Regenerated with the recipe the generated-artifact phase names (docs_projection_gate regen); the drifted row is an existing one whose text changed on main, not this lane's. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ted to main) #12506 was squash-merged, while this branch carried its unsquashed history, so its files conflicted. Per file: on the 13 conflicted files outside this PR's own four, this branch's side was byte-identical to #12506 at f09191e, an ancestor of #12506's final head, which main contains through the squash. They contribute nothing main lacks, so they resolve to main. src/v2/test/claim/projection_dispatch/fold_step_receiver_test.dag is removed: #12506 deleted it in 82187ba and main never had it, so keeping it would have resurrected a deleted probe. Per region: in fold_lowering.dag the conflicting hunk is the loop-edge construction this PR never touched (main's core_edge_label spelling is kept; the fv_* reader change merged cleanly). floor_pure_producer_share.dag keeps both independent rows (#13029's iap_verdicts and this PR's alb_verdicts). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Conflict in v2.workflow.floor_pure_producer_share: main added 53 hand warm rows (#12506's 44 and #13050's) to the roster this PR deletes. Resolved to this PR's side; each row is dispositioned from this head's floor run (derived, or a single-declared-claim fill reported to its owning lane, calm-boar-904, for the s3 supply-the-inputs restructure). Two comments in main's new test modules that cited the deleted roster are rewritten. docs/design-rung-drops.md regenerated against the merged tree. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…keep the derived rung-drop roster (main's new drop is a member by its file), union imports Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…#12506 types callees kvr_a_named_calls_bool_formal_is_counted_not_judged_holds pinned the counted-not-judged state and went red on main once #12506 typed a call's callee by its declaration, as its comment said it would. Its successor asserts the refusal infer now gives, measured on this head: application_argument_does_not_inhabit. The old identity is rostered WitnessDeleted with its successor named. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…vr named-call Bool formal now refuses since #12506 types references by declaration -- control rewritten to assert the refusal, as its own note required Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The 24 #12506 witnesses are restructured per the DESIGN section 3 witness rule, so their single-claim fill debt retires by typed disposition: RestructuredPerWitnessRule for cref (6), fps (10) and dre (4); BecameSharedByDemand for mbt underived_arm_body and sevens_call; ClaimDeleted for fps_a_root_bound_data_value_is_not_yet_projectable_holds (replaced on main by the projects positive control after #13216). mbt hiding and dre imported stay ActiveFillDebt. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
1 participant
What this is
The lane's original subject — a reference to a corpus declaration is typed by that declaration — plus the chain of roots that reading it uncovered. Each commit stands on its own receipts; none of them claims movement on the native seven/eight.
Landed here
Qualified-name resolution retains the binding kind (
82b5f154185).qualified_head_bound_on_chaincollapsedBoundInFrameandBoundAtRootinto oneBool, and that Bool was the sole discriminator between reading a dotted path as a field projection and reading it as a qualified declaration name. Those are different questions. The decision now carriesScopeBinding, decides both readings in one place, and refuses rather than substituting a projection when the declaration reading fails — an earlier revision fell back, which is §5's absorbing fallback. 15/15 oncross_module_reference_resolutionmeasured on that commit alone.Field-projection inference distinguishes an unretrievable declaration from a fieldless receiver (
a509caabc92).ReceiverNotARecordcarried both "the type is established and is not a declaration reference" and "the type names a declaration this context cannot retrieve", and both said declares no fields. The second convicts a correct program. The cause was structural:resolved_declarations_offills from one module root, so an imported provider's records were absent by construction.resolved_tree_ofnow takes the closure's resolved roots, andclosure_resolved_rootscuts the recursion by giving per-root resolves no closure — N + 1 resolves, not N².The diagnosed root, filed (
54725fe66b3).gunbc.recurring_failure_modeinfer_child_context_cannot_depend_on_a_sibling_result. Diagnosis only, no repair.The canonical-symbol derivation, reverted (
14a8710905b). See below.Two merges of main, plus the integration repairs they required.
Evidence
field_projection_stagesdeclaration_reference_evidencecross_module_reference_resolutionprojection_dispatch.receiver_dispositionfold_lowering00_compileThe strongest single piece is not mine.
declaration_reference_evidencecarried an expecting-red probe whose header declared this repair's trigger before it was built — "a resolved-declaration index over every resolved module root, minted by resolve beside the per-module carrier". That is what landed, so it greened. Under §4b(4) it did not retire: renameddre_an_imported_reference_grounds_through_the_closure_index, same subject and fixture, assertion inverted, enrolled as the permanent control.Things a reviewer should check me on
A commit was reverted because main fixed the defect it faithfully reproduced.
6b3490b2621rewrote the route to the DAG canonical symbol set and proved exact set equality with the old derivation. main has since narrowed that set, because carrying the grammar's atoms let an unboundnodein a body resolve silently to a grammar atom. So the equality proof certifies the commit as a faithful reproduction of a silent-wrongness class. Reverted rather than rebased: against main's narrower set there is nothing left to minimize.Three causal accounts of the native refusal were wrong before the right one. I attributed it to wall 3d being unrepaired, then to my own
BoundAtRootgate, then to my absorbing fallback. Each was falsified by measurement. The actual cause anchorse.target— a fold step binder — and resolve is not implicated at all. The misreads came from reading a diagnostic chain head as its cause; in one measured diagnostic the head reason appeared 209 times and the actual cause once.A lane capability regressed and is recorded at its refusal, not repaired. Match-arm binder typing (#12641, lane-only, never on main) no longer infers: main froze
infer_parameter_scope_searchto lambda parameters, and a match-arm binder is neither that nor a path-keyed reference. Attributed by probe — the binder gate, the closure index and the arm walk were each bypassed and the rows failed identically. Two rows now assert the refusal with the restoration trigger stated; a §4b(3) rung-drop row on #12641's subject may be owed and is flagged rather than filed, since that capability is not this lane's.Scope
This is a large PR. It is one lane's chain of roots rather than one change, and it edits resolve, infer and body lowering — where main is active, which cost two merges with real conflicts against the same files.
🤖 Generated with Claude Code
Main merges and their declared consequences (owner handover, swift-ram-269)
Merged main twice with merge commits (ea11297, 2b45150). Each conflict was resolved on its merits; the commit messages list them. The second merge took main's #12799 EdgeLabel cut into every lane-added label read and construction.
Declared rung drop:
gunbc.rung_drop match_arm_binder_typing_lost_to_lexical_carrier.match_binder_typingrows (mbt_binder_is_not_yet_typed_and_its_arm_body_is_reported,mbt_match_is_not_yet_typed_at_the_binder_arm,mbt_an_underived_arm_body_is_a_counted_frontier); and the twofield_projection_stagesmatch-binder rows (fps_a_match_binder_receiver_is_not_yet_typed,fps_a_match_binder_projection_is_in_the_resolved_tree).match_binder_typingrows were two reader defects, not the loss. Both are fixed:infer_match_variant_payloadandinfer_field_pattern_binds.Not a rung drop: where-predicate calls. They walk unjudged under the existing
RefinementDeclaration.where_clausefrontier, with oneinhabitance_undecidable_where_predicate_subject_unmodelledadvisory per call, so they are counted by execution. This is no lower than main, which judged no named call at all. Every other named call stays judged;pr_ordinary_named_call_deficit_still_refusesholds that. The row is PARKED by operator ruling: no infer judgment is coming, because refinements are being deleted in favour of checked constructors returning Optional. Its trigger names that removal.Removed: the lane-only
projection_dispatch.fold_step_receiverprobe. It was debugging scaffolding, mutually exclusive reason guesses that never passed. Its fixtures are handed to N7-1.Review 74212: the closure is resolved once per context (
closure_declarations_demand), not once per subject. Details are in the PR comment.