Skip to content

Derived-node identity in v1 infer: model and class row (step 1a) - #12913

Merged
gunbai-bot[bot] merged 3 commits into
mainfrom
session/clever-lynx-801-derived-node-identity
Oct 1, 2026
Merged

gunbai-bot[bot] merged 3 commits into
mainfrom
session/clever-lynx-801-derived-node-identity

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 1, 2026

Copy link
Copy Markdown
Contributor

Model-first, as ruled by quiet-gull-780 (2026-10-01) and scheduled by neat-boar-16. No infer code changes.

What this adds

  • docs/plans/derived-node-identity-design.md: what identity a type node carries when v1 infer builds it after resolution, with each constructor naming its cause and no cause inferred from shape (bold-fox-455's constraint). "Builds" covers:

    • substitution,
    • instantiation of generic record fields and alias chains,
    • call-plan formals,
    • kernel container minting.

    The note also:

    • argues the model is the std.decl_ref identity carried further, not a new §3b keying relation and not an extension of std.occurrence_identity;
    • reconciles it with A′ and the facts site key in keying-relation-design.md §3e (this is A′'s type-level interior, one model item);
    • states its scope, its laws L1–L4, and the three hypotheses step 2 must settle first, labelled as bets.
  • gunbc.recurring_failure_mode generic_identity_decided_by_spelling: the class row.

What the row records

  • The three sites that decide generic identity by spelling: unify_generics, substitute_generics_apply, and that function's self-binding guard.
  • Where the spelling collides: the kernel container type names its element child after its own template parameter T.
  • Two measured shapes:
    • valid code refused: test.claim.srv3_websocat_sequence_witness, red on main since 2026-09-04 and counted on this row as its specimen;
    • wrong code accepted: head_of(xs: [1], d: 2) into a String parameter.
  • The bisect: first bad is Carry declaration-bound direct-call formal authority #10146, and its parent is good. The wrong-code shape predates Carry declaration-bound direct-call formal authority #10146.
  • Why each attempted repair did not land:
  • The inventory of unmarked inputs: about 250k of about 505k events, broken down by constructor.

The next-rung trigger is step 2's landing: identity carried through every node-copying constructor in infer.

Not in this PR

  • The std carrier for DerivedTypeOrigin and its laws, with its consuming control. Next PR.
  • Step 2, the infer implementation. It waits for eager-newt-412's facts work to land, because both rewrite infer's copying paths.

Note on counting srv3

#12860's amendment list covers only the v2.test.* family under required_gate_bankruptcy. test.claim.srv3_websocat_sequence_witness is outside that population, so it is counted on this row instead of being added to a list it doesn't belong to.

🤖 Generated with Claude Code

docs/plans/derived-node-identity-design.md models the identity a type node carries when v1
infer builds it after resolution (substitution, instantiation, call-plan formals, kernel
container minting), each constructor naming its cause; reconciles it with A' and the facts
site key in keying-relation-design.md 3e. No infer changes.

gunbc.recurring_failure_mode generic_identity_decided_by_spelling records the class: generic
identity decided by spelling at unify_generics / substitute_generics_apply / its self-binding
guard, the srv3 specimen with its bisect (#10146), the older wrong-code admission, why each
attempted repair did not land, and the measured inventory of unmarked inputs by constructor.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…scribed counts, name the instrument (review 73739)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title Derived-node identity in v1 infer: model (step 1) and the class row Derived-node identity in v1 infer: model and class row (step 1a) Oct 1, 2026
@gunbai-bot

gunbai-bot Bot commented Oct 1, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 73739 in 867b529:

  1. Carrier. Step 1 is now split explicitly in the plan's §6. 1a is this PR (the note and the class row). 1b is std.derived_type_origin: the origin a built type node carries, and its laws (derived-node identity step 1b) #12914: std.derived_type_origin plus test.claim.derived_type_origin_witness_test, which executes L1–L4, 9/9 PASS. Until step 2 lands, that control is the carrier's only consumer, a declared frontier per §3c. This PR is retitled to step 1a.
  2. Transcribed counts. Removed from the row and the note. The row keeps only the identity-grain facts: which constructors produce unmarked nodes, and that the binder mark does not reach them. Per DESIGN §6, the magnitudes are left to the instrument. §7 now describes that instrument and makes it step 2's first task, a gunbc test label over the whole-corpus compile. It also says that the single measurement taken so far was a one-off local probe and is not quoted.

— sent from clever-lynx-801

…al residue to step 2

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 1, 2026
Merged via the queue into main with commit 224cdc4 Oct 1, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/clever-lynx-801-derived-node-identity branch October 1, 2026 18:15
gunbai-bot Bot pushed a commit that referenced this pull request Oct 1, 2026
#12892 #12920 #12741 #12613 #12913)

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.

0 participants