Skip to content

A lambda parameter whose declared type is a type variable now binds it: two independent defects, one of them a fabricated empty type - #9416

Merged
briansrls merged 2 commits into
mainfrom
session/warm-gull-528
Aug 27, 2026
Merged

briansrls merged 2 commits into
mainfrom
session/warm-gull-528

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 27, 2026

Copy link
Copy Markdown
Contributor

Root 2 of the receiver-type-never-propagated lane (node://adhoc-b99a2a7b-866).

A lambda argument contributes nothing to a call's generic substitution — the argument fold skips it — yet reads its own parameter types out of that substitution. Two defects sat under that asymmetry. Neither subsumes the other, and each was measured necessary by fixing the other alone first.

1. Order

call_subst accumulates only from arguments already inferred, so a lambda saw only what the arguments to its left had bound. The fold is extracted to one function (infer_call_arguments_generic_pass) and run a second round seeded with the substitution the first ended with — gated on generic_names nonempty, a nonempty substitution, and an argument containing a lambda.

Sound rather than merely convenient: lambda arguments are skipped for unification, so deferring what they would have contributed cannot change the result, and a slot already bound substitutes to a concrete node that unify_generics no longer binds. Bounded at two rounds, and the annotation states the narrowing — a binding derivable only from a substituted expected type is still out of reach.

2. A fabricated empty type — the one the first fix did not reach

record_lit_instantiated_fields built its slot substitution with resolved_type, which answers the empty error_type for any node carrying no inferred type — which is every authored type argument. So instantiating a generic record's fields substituted its type parameter to nothing.

Harmless on a scalar field, fatal on a callable one: the parameter node was replaced wholesale, param_node_type_expr found nothing, type_node_is_established answered false, and the lambda bound to that field fell to type_variable_node("callable_param"). Measured with the type argument already concrete — instantiating Sink<List<Int>> produced a parameter node with empty name, no children and no params — so inference is not part of the question. child_type_node is the total read of the same fact.

This is why the fabricated value was worse than a refusal (§5): error_type is a plausible-looking Node, so it substituted silently and surfaced stages later as an unresolvable method on a receiver nobody could point back to a declaration.

Measured

Same probe both ways, v2 pipeline closure (--entry src/v2/compiler/00_compile.dag, 175 files emitted):

blocking advisory
baseline (HEAD) 0 1983
this branch 0 1892

The 91 partition exactly: 7 ReceiverTypeUnestablished + 13 undecidable-at-call in tokenize + 71 undecidable-at-list-element. No advisory class rose. The other four unresolved_method_frontier rows' modules were compiled as entries; none moved.

Regen fixed point reached — required-regen: first_generation_equal=true.

The tokenize frontier row is deleted, not lowered

Its seven apply sites measure zero observed. The budget is an equality in both directions, so leaving the row would leave headroom a reintroduction could slip into — the same deletion the object_store rows got.

Its cause: field also named the wrong idiom: LexMatchThunk { apply: fn(s) } declares its parameter String, a leaf, and a non-generic record field holding a callable compiles 0 blocking. The real receivers were the generic algebra parameters declared fn(R, R) -> R. Three carrier clauses that repeated the wrong attribution or the stale seven-sites count are corrected with it. The misattribution was found by quick-bat-372; their annotated-parameter measurement is recorded as theirs rather than restated as mine.

Evidence, enrolled rather than retired (§4b(4))

dag/test/claim/generic_lambda_parameter_binding_witness_test.dag carries the three sources that refused — record-field lambda, lambda argument before its binder, and the field-access form that reported no field 'px' on type 'R' — plus a control whose method is genuinely absent from the bound type. The control asserts MethodNotFound fires and MethodExistenceUndecided does not: a pair reachable only when the parameter is bound, so a regression that unbinds it fails both halves rather than going quietly green.

All four measured FAIL on a claim_batch built from HEAD and PASS on this tree.

v1 seed admission

src/v1/04_infer.dag is frozen-with-active-maintenance. The admission test is purpose (operator ruling 2026-08-20): this is a compiler inference repair in direct support of the v2 self-host program — the seven sites are in v2.compiler.tokenize — and it adds no growth surface to the seed.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 2 commits August 27, 2026 07:58
…t: two independent defects, one of them a fabricated empty type

A lambda argument contributes NOTHING to a call's generic substitution -- the
argument fold skips it -- yet reads its own parameter types OUT of that
substitution. Two defects sat under that asymmetry and neither subsumes the
other; each was measured to be necessary by fixing the other alone first.

1. ORDER. call_subst accumulates only from arguments already inferred, so a
   lambda saw only what arguments to its LEFT had bound. The fold is extracted
   to one function and run a SECOND round seeded with the substitution the
   first ended with, gated on generic_names + a nonempty substitution + an
   argument containing a lambda. Sound rather than merely convenient: lambda
   arguments are skipped for unification, so deferring what they contribute
   cannot change the result, and an already-bound slot substitutes to a
   concrete node unify_generics no longer binds. Bounded at two rounds and the
   annotation says so.

2. A FABRICATED EMPTY TYPE, and this is the one the first fix did not reach.
   record_lit_instantiated_fields built its slot substitution with
   resolved_type, which answers the empty error_type for any node carrying no
   inferred type -- which is EVERY authored type argument. So instantiating a
   generic record's fields substituted its type parameter to nothing. Harmless
   on a scalar field, fatal on a callable one: the parameter node was replaced
   wholesale, param_node_type_expr found nothing, type_node_is_established
   answered false, and the lambda fell to callable_param. Measured with the
   type argument ALREADY CONCRETE -- instantiating Sink<List<Int>> produced a
   parameter with empty name, no children and no params -- so inference is not
   part of the question. child_type_node is the total read of the same fact.

MEASURED, same probe both ways, v2 pipeline closure (entry
src/v2/compiler/00_compile.dag, 175 files emitted):

  baseline  0 blocking, 1983 advisory
  final     0 blocking, 1892 advisory

The 91 are 7 ReceiverTypeUnestablished + 13 undecidable-at-call in tokenize +
71 undecidable-at-list-element. No advisory class rose. The four other
unresolved_method_frontier rows were compiled as entries and none moved.

THE TOKENIZE FRONTIER ROW IS DELETED, not lowered. Its seven `apply` sites
measure zero observed, and the budget is an equality in both directions, so
leaving the row would leave headroom a reintroduction could slip into -- the
same deletion the object_store rows got. Its cause: field ALSO named the wrong
idiom: LexMatchThunk { apply: fn(s) } declares its parameter String, a leaf,
and a non-generic record field holding a callable compiles 0 blocking. The
real receivers were the generic algebra parameters declared fn(R, R) -> R.
Three carrier clauses that repeated the wrong attribution or the stale count
are corrected with it (found by quick-bat-372, whose annotated-parameter
measurement is recorded as theirs).

EVIDENCE, enrolled rather than retired (DESIGN 4b(4)):
test.claim.generic_lambda_parameter_binding_witness carries the three sources
that refused plus a control whose method is genuinely absent from the bound
type, asserting MethodNotFound fires AND MethodExistenceUndecided does not --
a pair reachable only when the parameter IS bound, so a regression that unbinds
it fails both halves. All four measured RED on a claim_batch built from HEAD
and GREEN on this tree.

Regen fixed point reached: first_generation_equal=true.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…eric-binding fix, and close the half its carrier declared still open

#9411 repaired one half of upstream defect (2) -- the callable-parameter
RESOLUTION hole, where a type APPLICATION in a callable's params was never
resolved -- and its carrier text explicitly declares the other half open,
naming this session's node as the owner. That half is what this branch closes,
so the conflict is entirely in the two clauses that say "still open".

RESOLUTION, per agreement with quick-bat-372 (they land first, the session that
measured the post-fix state writes the post-fix text):

- method_existence_wall_note -- MAIN'S text is the base, not this branch's. It
  is richer: the SPLIT of defect (2), the Arrow mechanism, and the
  cause-vs-symptom arm are all theirs and are kept verbatim. Only the two
  clauses this branch falsifies are rewritten: "(2) SPLIT ... AND HALF FIXED"
  becomes "NOW FIXED IN BOTH HALVES", and "The half STILL OPEN is the generic
  one" becomes the account of what closed it -- itself two defects, the fold
  ordering and record_lit_instantiated_fields substituting to the empty
  error_type, with the note that neither alone sufficed.
- the v2.compiler.tokenize frontier row -- DELETED. Main rewrote its cause:
  field with the correct LexPatternFold attribution; that field now measures
  zero observed, and the budget is an equality in both directions, so the row
  goes rather than dropping to a lower count.
- the two seven-sites sentences on frontier_occurrence_budget_note and
  unresolved_method_frontier_note -- this branch's corrected versions, which
  main did not touch.
- src/v1/stage0/src/v1_compiler_infer.rs -- not hand-merged. Taken from main,
  then regenerated wholesale from the merged .dag.

MEASURED ON THE MERGED TREE, not carried forward from either side:

  entry src/v2/compiler/00_compile.dag   0 blocking, 1893 advisory, 175 files
  required-regen                          first_generation_equal=true
  this branch's four witnesses            PASS
  #9411's two witnesses                   PASS

The advisory figure is 1893 rather than the 1892 this branch measured alone
because main's own baseline moved under it; the claim that matters is 0
blocking on the composed tree, which is the tree that ships.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@briansrls
briansrls merged commit b5af75f into main Aug 27, 2026
3 checks passed
@briansrls
briansrls deleted the session/warm-gull-528 branch August 27, 2026 16:19
@briansrls
briansrls restored the session/warm-gull-528 branch August 27, 2026 16:21
gunbai-bot Bot pushed a commit that referenced this pull request Aug 27, 2026
…same two rows

#9405 rewrote the CI and emit-stage rows in gunbc.design_document while this
branch was rehoming orphaned prose into those same rows, so git could not
merge them. Both sides carry real content and neither side was taken whole.

The decisive measurement: main's DESIGN.md no longer contains the orphaned
passages either. #9418 landed its emit-census result into the GENERATED file
only, never into the authority; #9405 then edited the authority and
regenerated, and the orphan was deleted as a side effect. That is the same
mechanism this branch exists to repair, caught a second time on the same file
while repairing the first.

Resolution, per row:

  row 0 (CI)  main's newer text is the base -- it adds the emitted-closure
              cargo phase and the partition-crate boundary. The lost
              repo_ruleset clause is re-inserted between two anchors that
              exist verbatim on both sides, so the splice is positional
              only, not editorial.

  row 4 (emit) main's newer text is the base -- it adds the "A REQUIRED PHASE
              NOW COMPILES AN EMITTED CLOSURE ... NARROWED RATHER THAN
              RETIRED" narrowing. Its "POPULATION: UNCOUNTED AND UNBOUNDED"
              clause is REPLACED, because it is stale rather than merely
              older: gunbc.emit_stage_blocking_population_census exists on
              main and carries census_run_invocation, and #9418 landed before
              #9405. A census was taken; the authority still said it had not
              been. Main's own new fact -- two specimens escaping by three
              distinct modes -- is preserved beside the census result.

DESIGN.md is REGENERATED from the merged authority, never hand-merged. The
generator was rebuilt from the composed tree first, because #9416 changed
lambda type-variable binding in the compiler and regenerating with the old
binary would not have been the generator that will execute here.

Evidence: zero tokens lost against this branch's pre-merge DESIGN.md. Three
lost against main -- `UNBOUNDED.`, `bound.` and `recording.` -- all
punctuation-attached remnants of the two sentences deliberately rewritten
above, with no content behind them.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 5, 2026
…cords the specimens, not a commit (review 76610)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant