Skip to content

Resolve a callable type's parameter and return types: a lambda parameter's receiver had no method surface - #9411

Merged
briansrls merged 1 commit into
mainfrom
session/quick-bat-372
Aug 27, 2026
Merged

briansrls merged 1 commit into
mainfrom
session/quick-bat-372

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

resolve_node_bounded dispatches on connective. A callable type node is Arrow — parse_callable_type_expr puts its parameter types in params and its return type in inferred, leaving children empty. Every arm of that dispatch copied params: n.params through verbatim, and Arrow fell into the coproduct arm, which walks children. The arm was a no-op: a callable's parameter and return types were never resolved at all.

A parameter type that is a plain leaf survived that anyway, because a leaf grounds through its own name downstream — which is why the hole stayed invisible. A type application did not: resolve_scrutinee_type_node has an arm for children-present-with-inferred and an arm for no-children, and none for children-present-inferred-absent, so it returns such a node untouched. The receiver reached method lookup with no surface, and the existence wall could decide nothing about it — MethodExistenceUndecided, blocking, against a receiver rendered Node(..).

The arm that separated cause from symptom

Five fixture arms, built from source. The same receiver type reached through an annotated fn parameter compiled with 0 blocking, while the callable-field spelling refused. So the defect is the callable-parameter position, not the lambda binding the diagnostic names — a compiler suggestion locates where a failure was detected, never where it was caused. A non-generic callable field also compiled clean, which is what identifies the failing shape as the type application rather than the callable field as such.

The fix

An Arrow arm in that same dispatch, resolving parameter types and the return type through the one traversal authority the rest of the file uses, at depth + 1 and inheriting masked per resolve_node_bounded_masked_boundary. The rendered-use-site rule resolve_param already applied to a parameterized head — keep the authored head and args, attach the resolved target as inferred — is extracted as rendered_use_site_type so both consume one authority rather than two copies (DESIGN §3).

Measured

Pre-fix binary vs regenerated-mirror post-fix binary:

arm before after
armD — callable field, AlgebraL<Payload3> 1 blocking, Node(AlgebraL) 0 blocking
armE — annotated param, same receiver type 0 0 (control unmoved)
armC — declared type is the type variable 1 1 (untouched, see below)
src/v2/compiler/01_tokenize.dag 7 advisory 7 advisory
whole-closure advisory totals 536 / 198 536 / 198

The advisory totals holding is what establishes the fix did not buy its green by widening anything.

What is not repaired — and it is not the same defect

01_tokenize's seven sites are a lambda parameter whose own declared type is the type variable (LexPatternFold's algebra fields, fn(R, R) -> R). Nothing binds R: call_subst accumulates across arguments after each is inferred, and unify_record_lit_generics recovers R from the already-typed record literal — too late for the lambda fields inside it. That renders Primitive() rather than Node(..); this change cannot touch it, and measurement confirms it did not.

Dispatched separately as node://adhoc-b99a2a7b-866. The v2.compiler.tokenize frontier row therefore stays, measured unchanged at seven.

The work item this PR answers asserted one root. That premise was refuted by measurement before any code was written, and repairing the second half would mean a corpus-wide reordering of record-literal field inference in a load-bearing stage — not something the brief authorises. Reported and split rather than improvised.

A wrong mechanism in a live carrier, corrected here

method_existence_wall_note and the unresolved_method_frontier row both blamed "the LexMatchThunk { apply: fn(s) } idiom" for those seven. That is the wrong idiom, and it routes the next reader into repairing the wrong thing: apply: fn(s) declares its parameter String, a leaf, and a non-generic record field holding a callable measures 0 blocking. The seven receivers are left_r/right_r/elem_r/open_r — LexPatternFold's algebra parameters, not s. Upstream defect (2) in the wall note is now recorded as split, with this half fixed and the type-variable half explicitly still open.

Evidence

dag/test/claim/lambda_receiver_type_witness_test.dag, two arms, both PASS on the post-fix binary and both RED on the pre-fix one. Both assert a success that requires resolution to have happened, rather than the absence of a refusal from a wall — a weakened wall cannot make alg.unit produce a conforming type.

Two absent-member arms were designed and rejected by reading the producer, and the note records why:

  • MethodNotFound is unreachable — the wall's decidability predicate is kernel_profile_lookup, so a resolved user product still answers MethodExistenceUndecided.
  • FieldNotFound is produced only for record-literal unknown fields and pattern bindings, never for field access, which raises an InternalError naming the receiver's authored name — the same string either way.

Both would have been permanently green in the wrong direction, which is worse than absent because they would have been cited as coverage.

Mirror

Regenerated via claim_executor --required-regen, not hand-edited. v1_compiler_infer_resolve.rs shows 1931 changed lines for a ~35-line .dag addition; git diff -w reduces that to 331, and the residue is rustfmt reflow from nesting the existing body one level deeper, plus the Arrow import, the match arm, the new fn and its three call sites. v1_compiler_infer.rs is string data only (the two prose corrections).

🤖 Generated with Claude Code

…ter's receiver had no method surface

resolve_node_bounded dispatches on connective. A callable type node is Arrow --
parse_callable_type_expr puts its parameter types in `params` and its return type
in `inferred`, leaving `children` empty. Every arm of that dispatch copied
`params: n.params` through verbatim, and Arrow fell into the coproduct arm, which
walks `children`. So the arm was a no-op: a callable's parameter and return types
were never resolved at all.

A parameter type that is a plain LEAF survived that anyway, because a leaf grounds
through its own name downstream -- which is why the hole stayed invisible. A type
APPLICATION did not: resolve_scrutinee_type_node has an arm for
children-present-with-inferred and an arm for no-children, and none for
children-present-inferred-absent, so it returns such a node untouched. The receiver
then reached method lookup with no surface and the existence wall could decide
nothing about it, reporting MethodExistenceUndecided (blocking) against a receiver
it rendered as Node(..).

THE ARM THAT SEPARATED CAUSE FROM SYMPTOM. Five fixture arms, built from source:
the SAME receiver type reached through an ANNOTATED fn parameter compiled with 0
blocking, while the callable-field spelling refused. So the defect is the
callable-parameter POSITION, not the lambda binding the diagnostic names -- a
compiler suggestion locates where a failure was DETECTED, never where it was CAUSED.
A non-generic callable field also compiled clean, which is what identifies the
failing shape as the type application rather than the callable field as such.

THE FIX is an Arrow arm in that same dispatch, resolving parameter types and the
return type through the one traversal authority the rest of the file uses, at
depth + 1 and inheriting `masked` per resolve_node_bounded_masked_boundary. The
rendered-use-site rule resolve_param already applied to a parameterized head --
keep the authored head and args, attach the resolved target as `inferred` -- is
extracted as rendered_use_site_type so both consume one authority rather than two
copies (DESIGN §3).

MEASURED, pre-fix binary vs regenerated-mirror post-fix binary:

  armD (callable field, AlgebraL<Payload3>)   1 blocking Node(AlgebraL) -> 0
  armE (annotated param, same receiver type)  0 -> 0        control unmoved
  armC (declared type IS the type variable)   1 -> 1        untouched, see below
  src/v2/compiler/01_tokenize.dag             7 advisory -> 7 advisory
  whole-closure advisory totals               536 / 198 -> 536 / 198 unchanged

The advisory totals holding is what establishes the fix did not buy its green by
widening anything.

WHAT IS NOT REPAIRED, and it is not the same defect. 01_tokenize's seven sites are
a lambda parameter whose OWN DECLARED TYPE IS the type variable (LexPatternFold's
algebra fields, fn(R, R) -> R). Nothing binds R: call_subst accumulates across
arguments AFTER each is inferred, and unify_record_lit_generics recovers R from the
already-typed record literal, too late for the lambda fields inside it. That renders
Primitive() rather than Node(..), this change cannot touch it, and measurement
confirms it did not. It is dispatched as node://adhoc-b99a2a7b-866. The
v2.compiler.tokenize frontier row therefore stays, measured unchanged at seven.

A WRONG MECHANISM IN A LIVE CARRIER, corrected here. method_existence_wall_note and
the unresolved_method_frontier row both blamed "the LexMatchThunk { apply: fn(s) }
idiom" for those seven. That is the wrong idiom and it routes the next reader into
repairing the wrong thing: `apply: fn(s)` declares its parameter String, a LEAF, and
a non-generic record field holding a callable measures 0 blocking. The seven
receivers are left_r/right_r/elem_r/open_r, which are LexPatternFold's algebra
parameters, not `s`. Upstream defect (2) in the wall note is now recorded as split,
with this half fixed and the type-variable half explicitly still open.

EVIDENCE: dag/test/claim/lambda_receiver_type_witness_test.dag, two arms, both PASS
on the post-fix binary and both RED on the pre-fix one. Both assert a SUCCESS that
requires resolution to have happened, rather than the absence of a refusal from a
wall -- a weakened wall cannot make alg.unit produce a conforming type. Two
absent-member arms were designed and rejected by reading the producer, and the note
records why: MethodNotFound is unreachable because the wall's decidability predicate
is kernel_profile_lookup, so a resolved USER product still answers
MethodExistenceUndecided; and FieldNotFound is produced only for record-literal
unknown fields and pattern bindings, never for field access, which raises an
InternalError naming the receiver's authored name -- the same string either way.
Both would have been permanently green in the wrong direction.

The stage0 mirrors are regenerated, not hand-edited. v1_compiler_infer_resolve.rs
shows 1931 changed lines for a ~35-line .dag addition: `git diff -w` reduces that to
331, and the residue is rustfmt reflow from nesting the existing body one level
deeper, plus the Arrow import, the match arm, the new fn and its three call sites.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit 5a3b3db into main Aug 27, 2026
5 of 9 checks passed
@briansrls
briansrls deleted the session/quick-bat-372 branch August 27, 2026 12:55
gunbai-bot Bot pushed a commit that referenced this pull request Aug 27, 2026
…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>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 27, 2026
…the seed closure

main's #9411 extracted rendered_use_site_type in v1.compiler.infer_resolve.
The export-surface manifest records each seed-closure module's declarations,
so that module's decl row gained a member and the committed artifact -- which
was generated against the previous emitter -- no longer matched.

One line, one added symbol, verified against a regenerated candidate rather
than hand-edited: regen reports planned=137 executed=137 with main.rs as the
one pre-existing declared divergence, and the candidate differs from the
committed tree in this file alone.

Worth recording why this was not obvious. My diff between the passing SHA and
the failing one was thirty comment lines in a v2 module that carries no row in
this artifact, so it could not be the cause; the artifact also does not exist
on main, so it could not be main's staleness either. Both readings were wrong.
A generated artifact on a branch is that branch's responsibility even when
every line of it was authored elsewhere and every line of the author's own
diff is inert -- the diff bounds what was authored, not what can break.

Co-Authored-By: Claude Opus 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