Finally, we describe the subtyping rule. The rules for subtyping types
and environments are shown in fig:subtyping. For integer types,
the rules require the refinement of a supertype is a logical consequence of
the subtype's refinement conjoined with the lifting of \(\Gamma \) .
The subtype rule for references is covariant in the type
of reference contents. It is widely known that in a language with unrestricted aliasing
and mutable references such a rule is unsound: after a write into the coerced
pointer, reads from an alias may yield a value disallowed by the alias' type
[1]}. However, as in
the assign case, ownership types prevent unsoundness; a write to the
coerced pointer requires the pointer to have ownership 1, which guarantees
any aliased pointers have the maximal type and provide no information about their contents
beyond simple types.
<FIGURE>