Draft:Atomic subtyping

Atomic subtyping is a restricted form of subtyping where type statements can only depend on coercions between atomic types (including type variables), rather than between arbitrary types. For example, $int\subseteq real$ is an atomic coercion, and $(r\to s)\subseteq t$ is a non-atomic coercion. When atomic subtyping is used, one type can be a subtype of another only if they have the same pattern of type constructors. This allows for more efficient type inference algorithms.Template:Sfn

References

• Template:Cite journal