Double-Vision Recursive Modules
A recursive module module rec X1 : S1 = … and X2 : S2 = … exhibits double vision when each component must be typed against two views of its siblings: its own strengthened internal view (what it knows about itself / the cyclic group) and only the external view of the others. The typing rule E-Typ-Rec-Double-Rec accepts such modules subject to a set of premises.
The two key obligations
Of the rule’s premises, two carry the abstraction content (the source-to-source encoding reduces correctness to exactly these):
- Premise (5) — typing of the generated functor bodies
F1 / F2under the strengthened internal view. - Premise (6) — the final ascription / subtyping check when exporting
I.X1 / I.X2back to the external signaturesS1 / S2.
Where sealing happens (and doesn’t)
The intermediate recursive package I : Str is intentionally transparent — Str exposes all witnesses, so I = rec I : Str { X1 = F1(I); X2 = F2(I) } checks by single vision. The abstraction boundary is restored only at the final export module rec X1 : S1 = I.X1 and X2 : S2 = I.X2. The argument coercion I : Str → functor-argument signature is a null/refinement check, not the external abstraction proof.
Caveat: applicative vs generative
Two mode-specific encodings may be needed; the generative variant may require inserting a () barrier to prevent path equality from leaking. See Applicative vs generative encoding barrier.
Related
Source-to-Source Encoding Correctness · Locator-Anchored Signatures · Partial Recursive Signatures · project notes Recursive Modules Paper Writing Log, RMC vs Momegarec double vision in second submodule, POPL 2026 (MOC)