Type Aliases
Type aliases give names to existing types, making code more readable and self-documenting. They are transparent: an alias does not create a new nominal type, it names a structural shape.
Subtyping Rules
Subtyping determines when one type can be used where another is expected. In verification mode, ordinary type compatibility is further constrained by ownership, heap identity, and contract preservation.
Type Operators
Type operators manipulate and combine types at the type level, enabling flexible type definitions without runtime overhead. They are most useful for deriving public interfaces from richer internal record or module shapes.
Generic Type Definitions
Generic types are parameterized type definitions. Instead of writing separate aliases for Box, Box, and Box, you define one shape Box and instantiate it with concrete types. The same monomorphization model used for generic functions applies to generic type definitions during verification.
Function Type Contracts
Function types can carry contracts using a contract { ... } block after the return type. This lets you describe behavior and effects for function values, callbacks, iterators, and higher-order APIs, not just for named function bodies.
Verified Subtyping
Verification mode applies additional type rules to keep