ch:oo-self-types: ch:oo-self-types

Problem, result, and invariant. Implement the selected positive-Self, matching, and package-opening checks. The result is the seven-case report in appendix E. Package introduction and opening maintain one hidden witness: the payload and result positions must refer to that same witness throughout.

Representation. Represent polar type expressions, record protocols, matching obligations, payloads, packages, and opening results as nominal data. Carry polarity as an explicit parameter. Keep matching evidence separate from any value-subtyping result so that protocol width cannot silently authorize subsumption.

First complete version. Reverse polarity in arrow domains and preserve it in codomains. Accept positive clone/update families and reject the negative equality method. Make references invariant: $\mathsf{Ref}\mathsf{Nat}$ is admissible, while a reference containing Self is rejected.

Remaining cases. Compare finite protocols by width and reproduce $\mathsf{NamedOrdered}\mathrm{\#}\mathsf{Ordered}$. Package introduction checks positivity and matching before sealing a payload with a hidden witness. Opening recovers that witness locally and compares it with the payload and result tags; mismatched public protocol, payload, or result cases are rejected.

A failing version. Omit the result-witness comparison when opening. The implementation remains type-correct but accepts a result tagged by a different hidden type, so the package case fails. Preserving arrow-domain polarity and treating every reference field as positive give two independent variance controls.

Acceptance test. Run the four gates in appendix E. Require seven exact PASS lines, the frozen summary, and [] from audit. Replay the arrow-polarity, reference-invariance, and result-witness mutations; each must fail the stdout oracle before the accepted source is restored.

Mathematical boundary. The artifact executes finite polarity, matching, package-introduction, and package-opening checks. It proves neither positive-Self subtyping, matching soundness, preservation, progress, nor the step-indexed fundamental theorem.