Skip to content

Bind #9359's insertion dissolution to OccurrenceProjected - #9376

Closed
briansrls wants to merge 1 commit into
mainfrom
repair/9359-bind-insertion-dissolution
Closed

briansrls wants to merge 1 commit into
mainfrom
repair/9359-bind-insertion-dissolution

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Restoration after #9359

#9359 merged before its late hold reached the operator. Its new OccurrenceProjected arm made one existing machine-consumed fact false on main:

data legacy_binding_projection_insertion_dissolution: DissolutionCondition = UnboundDissolution { ... }

std.dissolution.dissolution_status consumes that carrier. After #9359, the debt must no longer report unbound while the binding declaration exists in the same tree.

Change

  • replace the unbound dissolution with:
bound_dissolution(
  ref: decl_ref(
    module_path: "std.occurrence_identity",
    decl_name: "OccurrenceProjected"
  )
)
  • correct the module annotations that still asserted the cause arm did not exist;
  • rename the witness whose name still asserted that no carrier could express the cause.

The refusal itself remains. ProjectionInsertionUnrepresentable still names the current capability boundary: the shared carrier can express projector provenance, but this projector has not yet been wired to allocate and emit through the new arm.

Why now

This is the first revision where the binding citation can be authored honestly. On the prior base, the citation wall would have refused OccurrenceProjected because it did not exist. Deferring now would leave a false machine-consumed dissolution on main.

Provenance and scope

This PR is a clean two-file transplant of corrective commit caae856826c9a584c2b65a31d0688c4ec6de7cfe, rebased onto current main after #9359's squash. No #9359 implementation code is changed.

The originating lane reported: 4097 files parse-clean; projection witness 8/8 PASS; citation population 1516 → 1517 with debt unchanged at 42, establishing that the new DeclarationRef resolves rather than joining debt.

Do not merge until review and required CI are terminal on this exact head.

#9359 landed OccurrenceProjected, making legacy_binding_projection_insertion_dissolution's UnboundDissolution false on main. Bind the machine-consumed dissolution to std.occurrence_identity.OccurrenceProjected at the first revision where the citation resolves, and correct the three prose/name claims the new arm falsified.

The ProjectionInsertionUnrepresentable refusal remains: the carrier can now express the cause, but this projector is not yet wired to emit through that arm.

Source correction: caae856, authored immediately after #9359 merged.

Copy link
Copy Markdown
Contributor Author

Superseded by #9377. Both PRs are based on 96e8b623dd1ae5338b628233d626a8481d7fd979 and produce the exact same resulting tree, 6dbccfff232e5735a685ecba2c3c5ccfcb0234d9. #9377 is the originating lane's fresh PR and already has an exact-head Claude review running on 3b9997ed113256956a933bc80ed5565c4ef4f162; preserving that subject is cheaper than carrying this duplicate. Closing unmerged.

@briansrls briansrls closed this Aug 27, 2026
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