Pure subtype system type safety

Can a checking guarantee for one expression survive when it is put into a larger program? An identity function returns its argument, so applying it to another identity function leaves that argument. In a pure subtype system, the same expressions can act as programs and as types. The proposed checking rules still need a general guarantee for replacing expressions in specified positions, with both completed expressions passing the rules.[1] [2]

Can a well-formed expression retain its checking guarantees as it is placed inside a function and evaluated? Let $I=\lambda x\leq\mathrm{Top}.x$ be the identity function. The application $I\,I$ reduces to $I$: replacing its parameter by its argument leaves the argument itself. This small instance illustrates substitution, not the missing general theorem.

For the Section 4 machine-based pure subtype system, progress says a well-formed term is in normal form or can take an evaluation step. Preservation says that if $t$ is a transitive well-subtype of $u$ and $t$ evaluates to $t^{\prime}$, then $t^{\prime}$ retains that relation to $u$. The substitution argument depends on Conjecture 8, which transfers well-subtyping through the specified covariant contexts when both plugged terms are well-formed.[1] [2]

A 2026 paper proves an important interaction between two forms of reduction. But its proposed checked language still needs a separate conjecture about replacing expressions inside a larger program. The complete safety argument depends on that remaining step.[1] [2]

Conjecture 8 states: if Γ⊢u≤*wf t and both Co[u] and Co[t] are well-formed in Γ, then Γ⊢Co[u]≤*wf Co[t]. The allowed contexts are the hole, a hole inside a function body, and the function position of an application, recursively. Both well-formedness premises matter; the target is not closure under every arbitrary program context.[1] [2]

Allowing expressions to act as types gives one language for describing values and constraints on those values. The mathematical challenge is compositional: guarantees for small checked expressions must remain meaningful when functions use them inside larger expressions and execution substitutes arguments. This connects the proposed expressiveness to reasoning about whole programs, without claiming a finished compiler or guarantees for every language with subtyping.[1] [2]

When an evaluated function replaces a parameter by its argument, the checker needs to carry a relation established for that argument into the function body. That lets the safety argument use local checking facts inside an assembled expression as evaluation changes it. In this proposed calculus, Conjecture 8 supplies the missing compositional bridge for the specified covariant contexts, only when both plugged expressions are well-formed. It would connect local well-subtyping facts to the conditional progress and preservation argument. It would not establish termination, theorem-prover consistency or equivalence with Hutchins’ original rules.[1] [2]