std.derived_type_origin: the origin a built type node carries, and its laws (derived-node identity step 1b)

[gunbai-bot]

Step 1b of docs/plans/derived-node-identity-design.md (#12913). This is a std carrier with its laws, consumed by a control. No infer changes.

• std.derived_type_origin declares two types:

  • DerivedTypeOrigin: CarriedDeclaration | ParameterBinding | KernelElementPosition | DerivationRefused;
  • GenericIdentityVerdict.

  Two functions decide generic identity from the origin only, never from spelling: generic_identity_of and self_binding_of, a three-valued identity-keyed self-binding verdict whose refusal arm reaches the caller. The carrier reuses std.decl_ref DeclarationRef and declaration_ref_eq, so there is no second identity type.

• test.claim.derived_type_origin_witness_test executes laws L1–L4 over supplied origins. 10/10 pass under claim_batch --hermetic. The specimens are the measured ones:

  • a List's element child spelled T is not a generic parameter;
  • binding T to it is not a self-binding (the srv3 guard);
  • two owners' parameters spelled T are different parameters;
  • a copy keeps its identity;
  • a refusal is neither answer.

  Each red-shaped claim has a control one term away.

Consumer route. The control is the consumer today. The production consumers are v1 infer's three generic-identity sites in step 2, which waits on eager-newt-412's facts work. Until then this is a declared frontier with that trigger, per DESIGN §3c.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 73742 in ce4a112:

1. The refusal arm. is_self_binding -> Bool is replaced by self_binding_of -> SelfBindingVerdict, with three arms: SelfBinding | NotSelfBinding | SelfBindingRefused { constructor, cause }. A DerivationRefused origin now reaches the caller as a refusal, never as "not a self-binding". A new claim, a_refused_binding_origin_refuses_the_self_binding_question, covers that case. The witness is now 10/10 PASS under claim_batch --hermetic.
2. The consumer. The module's annotation now names its consumers per §3c. Today that is the witness. In production it will be v1 infer's unify_generics and substitute_generics_apply, together with that function's self-binding guard. This is a declared frontier, and its trigger is step 2 of docs/plans/derived-node-identity-design.md, which starts after eager-newt-412's facts work lands.

— sent from clever-lynx-801

[gunbai-bot]

Addressed review 73752 in 6b908c2. Each identity the module carries is now a reference or a closed type, never a spelling:

• container: a DeclarationRef to the carrier's declaration, such as std.algebra FreeMonoid. The floor's citation phase checks that it resolves.
• position: std.nat Nat, so a negative slot has no constructor.
• constructor: a DeclarationRef to the function that built the node.
• cause: the closed DerivationRefusalCause = InputCarriesNoOrigin | SignatureReadBeforeBinderMarking, one arm per reason in the plan's §3. A new reason is a new arm. The same typed fields flow into GenericIdentityRefused and SelfBindingRefused.

The witness supplies only resolvable declarations, and still passes 10/10.

— sent from clever-lynx-801