Locator-Anchored Signatures
The mechanism (thm:locator-anchor) that recovers a strengthened source signature for the double-vision encoding — and the reason source-level with type sugar is not enough.
The claim
thm:locator-anchor: each anchor_L(τ_k) over canonical signatures elaborates to the same canonical substitution as the lookup equations in premises (3)–(4) of E-Typ-Rec-Double-Rec. This is what makes premise (5) equal to the typing of the generated functor bodies.
Why with type sugar is insufficient
When strengthened variables occur under applicative functor bodies (e.g. P.F(X).r), with type cannot express the needed strengthening. The DoubleVisionCase example shows this concretely: the proof must rely on anchor_L(·) over canonical signatures, not on source-level sugar / simple refinement.
Related
Double-Vision Recursive Modules · Source-to-Source Encoding Correctness · Partial Recursive Signatures