N7-1: lambda-binder projection base as lexical reference; dependent-child infer driver types the fold member - #13028
Merged
Merged
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>
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>
…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>
…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>
… descending into
WHAT NOW EXECUTES. A call whose callee is a resolved corpus-declaration reference
dispatches through the declaration it names and returns that declaration's value.
Both executing controls assert the VALUE and not merely acceptance -- any
Int-returning path would satisfy "Accepted" while proving nothing about which
declaration ran, and 7 is written only in the callee's body.
THE CHAIN, one authority per link.
resolved declaration reference
-> canonical declaration identity (symbol_index_lookup, the GUARDED reader)
-> recorded on the reference's facts (InferredFacts denotation)
-> read by eval, which re-resolves nothing
-> the existing arrow dispatch: find_arrow_body_child, eval_bind_arrow_params
-> the callee's own body in the callee's own frame
Infer records the denotation because infer is the stage HOLDING the symbol index.
eval holds none, so the two routes otherwise open to it were both defects: a
second resolution path over the tree would be a WEAKER authority that accepts
references the ambiguity guard refuses (DESIGN section 3), and reading the body
out of the callable TYPE evidence would conflate two facts. The denotation is a
field separate from the grounding for exactly that reason -- a consumer wanting
the body reads the denotation, one wanting the type reads the grounding -- and
only a GROUNDED reference carries one, so a refused contract reaches no body.
WHY THE WALK WAS THE DEFECT BEFORE THE DISPATCH WAS. eval's callee classifier
admitted an Arrow and a bare Atom; a resolved reference is a marked Conj, so the
callee edge was not recognized, eval_fold_child_for_edge took its ordinary
recursive arm, and the walk descended INTO the reference's encoded declaring
path. The classifier now asks declaration_reference_path_optional -- the same
reader infer and translate ask -- rather than admitting Conj, which would admit
every record shape with it.
A REFERENCE REACHING NO EXECUTABLE DECLARATION REFUSES as an unbound runtime
binding and does not fall through to the primitive table, where it would be
looked up under a name it does not have and reported as a missing primitive
rather than as the declaration it names. The discriminating negative is enrolled:
a callee naming no declaration must not execute.
WHAT IS NOT DONE, enrolled executed and expected-red rather than described.
- PARAMETER BINDING IS NOT DEMONSTRATED. Both executing controls have CONSTANT
bodies, so a callee ignoring its argument entirely would pass both. The
parameter-bodied fixture -- whose value depends on the argument -- still
refuses. That claim is the one that would demonstrate binding and it is red.
- A BOOL-RETURNING CALL still refuses, and it is a DIFFERENT boundary: its body
is a constant, so it differs from the executing control only in return type.
TWO CORRECTIONS TO THE PRECEDING COMMIT'S READING.
The anchor measured there is an EMPTY Conj. An empty Conj is structurally equal
to any empty product, and node equality here is structural, so "inside the
declaring path" is weaker evidence than that commit's wording implies -- it is
consistent with the spine's nil terminator and does not exclude an unrelated
empty product. The classifier/walker mismatch stands on its own, established by
source and confirmed by the repair executing; the anchor comparison corroborates
it rather than proving it.
Four claims in v2.test.long.add_arrow_eval_by_execution fail on the pinned base
BEFORE this change (measured by stashing it), so they are pre-existing and not
caused here. I had no baseline for that set when I first read them as a
regression.
A CHANGE TRIED AND DROPPED. eval_fold_is_callee_reference_edge identifies the
callee edge by a processed-count, which is only correct while the callee is the
first child processed. That looked like the reason a one-argument call refused
where a zero-argument call executed, so it was rewritten to key on
eval_transform_callee_edge. Measured, it changed no verdict in either direction:
all seven controls pass without it. It is dropped rather than kept as an
unneeded second formulation, and the count-based identification is left as a
standing observation about that predicate, not a repair this change needs.
The carrier widening is five construction sites, not the forty-four a first grep
suggested: most matches were `-> InferredFacts {` signatures, and the fixtures
construct through helpers.
Regression: all 9 reference-evidence claims still pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…call WHAT THE REMAINING NAMED-CALL REFUSAL ACTUALLY IS. InferredTree keys its facts by Node; Node equality is structural over kind, children and occurrence identity; and std.occurrence_identity spells "no authored occurrence" as the NULLARY constructor OccurrenceSynthetic, so it is one VALUE and not one value per synthetic node. Two synthetic nodes with the same kind and children are therefore THE SAME KEY, whoever built them and whenever. Measured: the evaluator builds an empty synthetic Conj at runtime (v2.std.runtime runtime_value_conj_node, for a value's type), asks the facts map about it, and the map ANSWERS -- with the facts of an unrelated node that merely shares the shape. Those facts carry GroundingNotDerived, so eval refuses with eval_rejected_grounding_not_derived located at a node that exists in no source position. Three claims enroll it: the refusing node is equal to the runtime-built empty Conj; the map answers for that node; and a structurally equal node occurs in the program, which is what makes it a collision rather than a stray key. THE COLLISION IS SILENT IN BOTH DIRECTIONS, and only one direction is observed here. A lookup that should MISS instead hits, converting a fail-closed infer_facts_lookup_miss into a grounding judgment no producer intended. Had the colliding entry been DERIVED rather than underived, the same collision would hand the runtime a grounding nothing established -- a fabricated plausible output rather than a refusal (DESIGN section 5). Nothing currently makes that direction unreachable; this corpus just happens to collide with an underived entry. A CORRECTION I OWE, and it retracts my own evidence rather than someone else's. Commit b65297c attributed this refusal to the callee's encoded declaring path because the anchor was a member of that path's node set. That evidence does not discriminate: an empty synthetic Conj is a member of almost any node set it is tested against, including the spine's terminator, which is why the same probe also answered yes for the call subtree and for the declaration. The anchor comparison establishes nothing about location and should not have been read as attribution. What the classifier/walker repair rests on instead is unaffected: it is established by source -- the classifier admitted Arrow and Atom only while a resolved reference is a marked Conj -- and by named calls now EXECUTING to their callee's value, asserted by value and not by acceptance. That evidence does not pass through the anchor. WHY THIS STOPS HERE. The repair is to decide the KEYING RELATION for the facts map -- occurrence identity rather than structural identity -- which is a semantic rule about node identity, sits in the conformance-identity domain (DESIGN section 3b), and changes every facts lookup in the corpus rather than anything in this lane. Escalating rather than reaching for a local guard at the symptom link, which is the shape DESIGN section 6b names. The parameter-bodied and Bool-returning controls beside this file stay enrolled executed and expected-red; this finding explains the node they refuse at without yet discharging either. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The Bool-returning control's callee body is a constant, so it differs from an EXECUTING control only in its return type, and it refuses at the same runtime-built empty synthetic Conj as the parameter-bodied one. So this lane's two remaining reds have ONE cause rather than two. Scoped deliberately to these two subjects. A matching reason string is not evidence of a shared defect -- that was the error in an earlier grouping of three unrelated subjects -- so this claim compares the failing NODES and says nothing about any other refusal reporting the same reason. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…eration
I WAS TOLD MY EVIDENCE REPEATED THE ERROR IT CORRECTED, AND IT DID. The previous
commit replaced "the anchor lies inside the declaring path" with "the anchor is
what the runtime value constructor builds". Both were inferred from Node == Node,
and equality is the relation under suspicion, so it cannot be the instrument that
establishes provenance. An empty synthetic Conj compares equal to many unrelated
nodes; membership in a node set and equality with a constructor's result are both
uninformative about origin. Both readings are withdrawn.
WHAT ENUMERATION ESTABLISHES INSTEAD, which needs no provenance claim. Walking
infer's own entry list for one small program: MORE THAN ONE ENTRY carries the
empty synthetic Conj as its key, and those entries DISAGREE on whether grounding
was derived. So one key names at least two subjects whose facts differ, and a
consumer asking under that key receives whichever the first-match scan reaches
first. The same conflict stands in a second fixture, so it is a property of the
keying relation over ordinary programs rather than an artifact of one source text.
This is stronger than the earlier claims and differently shaped: it is not that a
freshly built equal value gets an answer, but that the relation ADMITS CONFLICTING
FACTS FOR ONE KEY. facts_map_from_entries checks each entry's own subject
correspondence and establishes no uniqueness or conflict condition across entries
that compare equal.
AND THE FAIL-OPEN DIRECTION IS REACHABLE, not hypothetical. A DERIVED entry exists
under the same key as an underived one, so a subject whose grounding was never
established can receive one that was -- a fabricated plausible output rather than a
refusal (DESIGN section 5) -- and which of the two a consumer gets is decided by
entry order. I had flagged this direction as a credible risk; the enumeration is
what makes it an observed reachability rather than a hypothetical, and it is still
short of an observed successful misexecution.
THE TRAVERSAL PATH, measured with a temporary diagnostic that gave each grounding
demand site in the evaluator its own reason symbol. The instrument is removed and
its result is recorded here rather than asserted, since asserting it would mean
keeping instrumentation in the evaluator:
- the demanding caller is eval_fold_init, through eval_fold_child_for_edge's
ORDINARY RECURSIVE ARM -- the node entered the walk as a child, not as a fold
root, so this is a traversal that descended into it rather than a consumer
asking about a supplied subject;
- the node sits under a NAMED edge and is NOT under the declaration-reference
marker, so it is not the reference spine the previous repair addressed;
- no node in the call subtree carries it as a POSITIONAL child, which is how the
named-edge conclusion was reached.
That locates the demand without asserting where the node came from, which is the
distinction the previous commits lost.
ALSO CORRECTED, and this one was a live defect rather than a wrong reading. The
annotation above eval_fold_is_callee_reference_edge described the callee-edge
identity repair as landed while the function still contained `p == 0 &&
is_positional(edge)`: I reverted the change after measuring that it moved no
verdict, and left the comment claiming it. A comment asserting a repair the
function does not contain is worse than no comment, since no Accepted program can
read one to check it (DESIGN section 4c). It now records the count-based
identification as a standing observation, states that rewriting it changed no
verdict in either direction, and says what would justify revisiting it: a call
shape where the two formulations DISAGREE, which is the discriminating case this
lane never found.
Verified after removing the instrumentation: all 7 declaration-reference eval
controls pass, including both executing calls; the 4 key-conflict claims pass. The
two executing controls return Accepted with diagnostics None, checked explicitly --
so they are executions and not acceptances carrying a suppressed refusal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ool pair THE NEXT RESULT IS NOW WRITTEN AND EXECUTED, not described. Three claims specify what "argument-dependent execution" means and run the comparison that decides it: identity(only_arg: 3) -> 3 identity(only_arg: 8) -> 8 TWO arguments, because one would not discriminate -- a callee returning a constant that happened to equal the argument would satisfy a single case. The callee's body IS its parameter, so its result cannot be produced without consuming the supplied argument, which is the gap the two constant-bodied executing controls leave open: a callee ignoring its argument entirely passes both of those. They are enrolled as the REFUSAL they are today, with the value path supplied and compared, so what remains when the boundary is repaired is inverting the assertion rather than authoring the behaviour it checks. Writing it the other way round would land a red and specify the same thing. ONE OF THEM IS VACUOUS TODAY AND SAYS SO. The claim that the identity callee must not answer the OTHER argument's value holds for the wrong reason while nothing executes -- both conjuncts are satisfied by refusal. It is enrolled anyway because it is the check that stops the repair being credited by a callee that consumes its argument and returns the wrong one, and it becomes discriminating the moment the claim above inverts. The annotation states the vacuity so no reader counts it as present coverage; an expecting-green claim that cannot currently fail is specification without execution unless its state is declared. THE BOOL PAIR GETS THE SAME TREATMENT one type further on: a true-returning and a false-returning callee must produce DIFFERENT answers, because a repair making both execute to the same value would satisfy "executes" while destroying the distinction the pair exists for. Every one of these refuses at the shared facts key rather than at anything about calls, arguments or return types -- the conflict is established by enumeration in v2.test.claim.callexec.synthetic_facts_key_collision, where more than one entry carries one key and those entries disagree on grounding. So this lane's acceptance result is blocked behind that one contract question and is fully specified while it waits, rather than waiting to be specified. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…k that closes it
THE FRONTIER WAS DECLARED AND IT IS NOW PERFORMED. Two headers named this exact
gap. v2.compiler.body_lowering_fold PostfixAccum keeps `a.b.c` as ONE qualified
name and says why -- "deciding here would be a second resolver with no scope to
consult" -- naming try_resolve_qualified_name_node as the decider. That function's
own header then said: "Head bound and no absolute hit: the projection this arm
cannot yet perform, refused Unbound rather than fabricated." So the spine arriving
at resolve was never a producer defect; answering Unbound for it was resolve
accepting the job and not doing it, and the two causes -- a bound head needing
projection, and a genuinely unbound name -- were reported identically.
MEASURED FIRST, so a later green is a change in behaviour and not in the question.
On the pinned base, `fn f(b: Box) -> Int { b.tree }` refused at RESOLVE with
resolve_reason_unbound_symbol anchored on a QUALIFIED-NAME SPINE, while the same
receiver with the projection removed resolved and inferred. So the representation
was not reaching resolve as a projection at all.
THE THREE STAGES.
resolve a bound head with no absolute candidate becomes a field projection: the
head resolves to its binder through canonical_atom, and each remaining
segment folds on left to right, `b.x.y` as `(b.x).y`. It reads segment
NODES, not the name's symbols, so every field keeps the occurrence of its
own token and a diagnostic about one field lands on that field rather
than on the whole chain. The reader for that lives in
v2.std.qualified_name beside the spine's other reader and its inverse,
because that module owns the label set.
infer a projection is typed by the field the receiver's type declares. It sits
at the HEAD of the product row because a projection is an ELIMINATION,
not a record: without it the projection Conj is typed as the product of
its own children, a type combining the receiver with the field-name atom,
which is the type of nothing the program computes. The receiver's type
comes from its own facts through the row's entries; the type's fields come
through the same GUARDED index reader the callee path uses. This is the
first production consumer of v2.std.node_query declared_field_named.
eval a projection selects the field from the receiver's value. The receiver
arrives as the one runtime argument through the existing seam, so the base
is evaluated ONCE by the ordinary walk rather than re-entered per
projection. The field edge is deliberately not an argument: it carries a
name, not a value.
THE ABSENT-FIELD CONTROL EARNED ITS PLACE TWICE. With resolve's arm landed and
infer's absent, `b.absent_field` inferred CLEAN -- resolve admits the shape and
nothing checked the field, so a misspelled field became an accepted program. That is
the fail-open the control exists to catch and it caught it.
AND IT CAUGHT A SECOND ONE, IN MY OWN REPAIR. My first infer arm collapsed two
unavailabilities into one Absent: "I could not establish the receiver's type" and
"the receiver's type is established and declares no fields". That is the absorbing
fallback DESIGN section 5 forbids -- it converts a decided negative into "no
evidence" -- and it broke the standing negative control
v2.test.claim.namespace_xl0.cross_module_reference_resolution
a_receiver_with_no_such_child_never_accepts: `Bool.v` passed at the frontier. The
two are now separate arms. ReceiverTypeUnderived waits at the frontier, because
convicting a program whose receiver is typed by a route not yet reaching here would
be wrong in the other direction. ReceiverNotARecord REFUSES.
TWO CONTROLS IN ANOTHER LANE MOVED STAGE, AND THE PROPERTY IS STRICTLY HARDER NOW.
Both asserted refusal AT RESOLVE with resolve_reason_unbound_symbol for a `Bool`
receiver. Resolve no longer refuses those -- it commits the shape -- and infer
refuses them instead. So they now assert through infer: acceptance is still
forbidden, and the claim is harder than before, because a program that resolved and
then inferred clean would fail it where previously only the resolve reason was
checked. The old reason was the collapse rather than the property, which
v2.compiler.resolve's own header already recorded as a defect. One was renamed:
"refuses_unbound_today" pinned a stage and a reason it never meant to pin, and what
the row is FOR is that a method call on a local receiver is not silently admitted.
WHAT EVAL'S EVIDENCE IS AND WHY. Its receiver value is SUPPLIED, which is DESIGN
section 3's witness rule: the subject is one interface -- what eval returns for a
projection over a given aggregate -- and computing the aggregate would re-run
production the claim is not about. The pairing obligation is discharged by a claim
in the same file rather than by assertion: fps_the_resolved_tree_carries_a_field_-
projection asserts the real producer emits this shape over the production route.
A FINDING BEHIND THAT CHOICE, measured while looking for a fixture that would
deliver a projection to eval through surface syntax. Two forms that should, do not:
`Box { .. }.tree` and `make().tree` both resolve and infer with NO field-projection
node in the tree, while the parameter form `b.tree` now produces one. So the
value-receiver path body_lowering describes (PostfixAccumValue, the accumulator
after a call suffix) is not reached from these forms, and the only projection this
corpus's surface syntax currently produces has an unbound receiver at eval -- whose
binding is blocked behind the frozen facts-key question. That is why eval's executed
evidence is at its own boundary and not through a whole-program run.
A TYPE ERROR WORTH RECORDING, because it cost two iterations and will recur.
list_at_optional answers Optional<T>, and a value destructured straight out of it
does not carry its type through a FIELD ACCESS: reading `aggregate.fields` inline
produced a runtime type error while the sibling arm, which reads no field, passed.
Naming a typed parameter restores it. The same shape appears twice more in this
change, in the runtime field walk and in the spine segment reader.
Green: 13 field-projection controls (resolve, infer and eval, valid and absent
field, and two refusal arms) and 15/15 in the namespace lane.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…form
WHAT THE SEVEN'S REAL SITE ACTUALLY IS. In v2.test.parse.expression_bodied_fn_decl_-
parse the projection is `artifact.tree`, where `artifact` is bound by the arm
`Accepted { value: artifact, diagnostics: d }`. That is a MATCH-ARM BINDER, not the
function parameter the controls beside it use, so whether the projection repair
reaches it is its own fact and gets its own controls.
MEASURED: resolve reaches it, infer does not, AND THE ISOLATING CONTROL SAYS WHY.
The match form resolves -- resolve's projection arm handles a match binder's head
exactly as it handles a parameter's -- and then fails to infer. The same match form
with the projection REPLACED BY A LITERAL fails to infer identically. So the blocker
is the match construct, not the field access: it is the pre-existing match-arm
boundary already recorded as the seven's first refusal
(body_lowering_reason_match_arm_navigation_refused), owned elsewhere.
Both conjuncts of that claim are load-bearing. The projection form refusing alone
would be consistent with a projection defect; it is the literal-bodied form refusing
too that assigns the refusal to the match construct. When match arms do infer, the
claim goes red and the projection claim beside it becomes the live question, which is
the transition worth being told about.
A VACUOUS CLAIM OF MINE, CAUGHT AND REPLACED. I first asserted that an absent field
off a match binder is not admitted, and it PASSED -- vacuously, because the VALID
projection off a match binder does not infer either. Both arms refuse, so the
assertion distinguished nothing and would have gone on reading as coverage for the
absent-field wall on that shape. The isolating pair replaces it. This is the second
time in this lane that a claim passed while establishing nothing, and both times the
cause was the same: asserting a refusal without first checking that the positive case
reaches the boundary being tested.
AND THE SEVEN THEMSELVES ARE NOT THE EVIDENCE, DELIBERATELY. All seven pass under the
development runner -- both before and after this change -- because that runner
resolves them with the SEED compiler, while their blocker is v2's OWN front end on the
native route. Reporting that green as progress would be citing a signal that was never
about the property claimed, so the shape is reproduced as a small fixture instead and
the seven are left to the route that actually exercises v2.
Green: 15 field-projection controls.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
84 commits of main, and the conflict is the one this lane has been carrying: main threaded `kinds: List<RosterKindIndex>, tree: Node` through the same infer functions where #12432's carrier threads `resolved: ResolvedTree`. 33 conflicts in 04_infer.dag, 2 in 05_eval.dag, 1 in a type-param test. RESOLVED AS THE UNION, NOT A CHOICE. Every signature and call site keeps main's `kinds` thread AND the `resolved` carrier, with main's bare `tree: Node` dropped in favour of `resolved.root` -- which is what #12432 established the carrier for. Taking either side alone would have deleted a landed thread or reverted the carrier. Two conflicts were semantic rather than threading, and both take the union: - main added eval_callee_body_refusal_reason, a per-body-form refusal so a callee whose body is a function value refuses under its own reason instead of the generic unsupported-callee. Kept, and pointed at `callee_target` -- this lane's dispatch subject, the DENOTED declaration -- so the better reason is reported about the node the call actually dispatches through. - infer_established_return_type_optional is this lane's addition and main has no counterpart; kept with both its consultation sites. A MECHANICAL PASS THAT OVERREACHED, CAUGHT BY THE COMPILER. Rewriting `tree:` to `resolved:` across conflict hunks also hit two sites where `tree` is a genuine Node argument and not the carrier -- infer_transform_derived_optional's tree parameter and partial_bounded_lattice_instances_in_tree. Both now pass `resolved.root`. The fail-closed front end named all four errors by parameter, which is why a blind pass was survivable here; it is not a technique to repeat. NOTE FOR THE NEXT RUN: the seed's Rust moved substantially under these 84 commits (v1_interpreter.rs alone is +967 lines), so every claim_batch verdict taken with the pre-merge binary is stale and none is carried forward. The binary is rebuilt before any verdict in this lane is reported again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ion_edge_field_optional Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 3, 2026
…t import where std.types List was added (10 modules double-bound it), and import it in std.compilers.sugar Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…nimported (data_initializer_identity refused its own native resolve) 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>
…39-n7 # Conflicts: # dag/gunbc/recurring_failure_mode/infer_child_context_cannot_depend_on_a_sibling_result.dag # src/v2/compiler/00_compile.dag # src/v2/compiler/03_name_resolve.dag # src/v2/compiler/03_resolve.dag # src/v2/compiler/04_infer.dag # src/v2/compiler/05_eval.dag # src/v2/compiler/body_lowering_fold.dag # src/v2/compiler/fold_lowering.dag # src/v2/compiler/self_host/closure_emission.dag # src/v2/test/claim/binder_admission/callable_binder_slice_test.dag # src/v2/test/claim/callexec/declaration_reference_eval_test.dag # src/v2/test/claim/callexec/synthetic_facts_key_collision_test.dag # src/v2/test/claim/field_projection/field_projection_stages_test.dag # src/v2/test/claim/match_binder/match_binder_typing_test.dag # src/v2/test/claim/namespace_xl0/cross_module_reference_resolution_test.dag # src/v2/test/claim/parameter_reference_test.dag # src/v2/test/claim/parse/expression_bodied_continuation_test.dag # src/v2/test/claim/reference_evidence/declaration_reference_evidence_test.dag
… (no wildcard over a closed coproduct) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… claims read the decided value Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…roducers Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…sion/silent-crab-339-n7
…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>
…39-n7 # Conflicts: # src/v2/compiler/03_resolve.dag # src/v2/workflow/floor_pure_producer_share.dag
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Fixed at 4541078 (review 74767): — sent from silent-crab-339 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
N7-1 (
node://adhoc-95789e9f-137), lane silent-crab-339 under calm-boar-904. Rebased onto main after #12506 and #13010 merged.What this PR does (the native-seven slice, re-derived per DESIGN §6b)
v2.compiler.resolve,resolve_projection_basenow mints every frame-bound head throughresolve_frame_bound_reference, and the projection route carriesResolvedAtom.lexical. Before,eine.targetwas a bare atom that nothing typed.v2.std.nodegainsfold_node_dependent, a partition-scheduled fold whosechild_contextsees the parent accumulator.v2.compiler.inferwalks the tree with it, using anInferFrameofTypeVariableInstance.init.declared_type_inhabitance.fold_realized_member_role,fold_collection_member_type,fold_step_member_formal,fold_step_carrier_formal,fold_step_body_node, …) sit besidefold_lowering's role authority.infer_loop_iteration_fold_child_targetsmakes that switch. A fold Bind row judges the body (and any declared return) against the carrier.infer_branch_operand_resolved_type_in_treeno longer reads a lexical binding's declared type directly, which bypassed the frame. It reads the reference's facts.closure_declarations_demandrecords each closure root whose own resolve refused (ClosureProviderRefusal, onResolvedTree.unavailable_providers). Every closure-index miss over it carries that refusal: chained ahead of a receiver miss, and advisory on a declaration-reference miss.List/Optional/Present/Absentimports, also split out as v2 std: import std.types List where it was used unimported (native resolve refusals) #13048.Ledger rows: the climb receipts on
infer_child_context_cannot_depend_on_a_sibling_result;bind_and_match_binders_not_typed_from_their_dependency_sibling;lambda_value_has_no_derived_type_in_v2_infer; a nested-payload re-box shape onnested_pattern_accepted_by_the_interpreter_and_broken_in_emitted_rust; a keyword-as-value shape onseed_admits_a_keyword_as_a_pattern_binder.Evidence
v2.test.claim.compiler.infer_fold_member_instancehas 6 controls, all green on the seed at this head:e.targetraises no projection refusal.found + e.targetis accepted.Red on base for the r / driver / (a) controls. Mutations: dropping the frame join reds (1), forcing the canonical atom reds (r), dropping the carrier frame reds the accept control.
Costs:
loopLoops.eval_stepsonfield_projection_stagesis +0.70%.Native: the controls are gated on the step-body
||derivation, which lands in #13054/#13060. The native-seven target's wall moved: fromroot.children(x), thend.reason(fixed), tov2.std.node's own resolve atmap.mapis realized in #13069 (stacked on this PR).Stack
||) are independent of this PR.🤖 Generated with Claude Code