Compatibility via Conversion (Coercive Subtyping)
Implicit type conversion functions, also known as coercions, provide an alternative approach to implement subtyping. Instead of interpreting subtyping as set inclusion (where the values of one type are contained within another), a coercive subtype system regards two types as compatible if there exists a conversion function between them. In this view, subtyping expresses compatibility via conversion. During type checking, the compiler automatically inserts coercion functions wherever they are needed to resolve a mismatch. After this coercion-insertion phase, the program contains no implicit subtype steps: all conversions are explicit in the internal representation. The subsequent type checker can therefore proceed as if no subtyping existed at all. This separation simplifies the reasoning process and provides a clear semantics.
For example, if Int is declared to be a subtype of Real via a coercion function, the
compiler can insert the conversion:
Real r = 2 + 3.0;
becomes
Real r = coerce_int_to_real(2) + 3.0;
After this step, the type checker only sees Real-typed values and can verify the addition without reasoning about subtyping directly.