Get rid of most subtyping constraints

[kyouko-taiga]

Although I like to claim Hylo doesn't have subtyping, the type checker actually understands and uses the concept in a few places. As of this writing, subtyping is involved in the following cases:

1. A cast expression like x as T checks that the type of x is subtype of T.
2. A binding initialization sink let x: T = y is valid if the type of y is subtype of T.
3. Passing an argument of type U to a parameter of type T type checks if U is subtype of T.

Type checking a subtyping relationship T <: U succeeds iff the compiler knows how to convert a value of type T to a value of type U. Because Hylo aims at making the cost of changing a value's representation explicit, however, these conversions won't always be inserted. That means your program may pass type checking but fail during code generation, when the compiler realizes that the conversion is not "free".

As of this writing, conversions are inserted automatically only for binding initialization and cast expressions. The rationale in the former case is that there's a cost to move/construct a value into storage anyway.

I don't think we can remove subtyping from the picture entirely. If anything, we need a way to type check an upcast. But I also think it should be possible to pass a lambda [](T) let -> U to a parameter of type [](T) inout -> U. Nonetheless, I think we can iron out the design and have the type checker be much stricter about subtyping.

[kyouko-taiga]

For information, simplifying parameter constraints as equality rather than subtyping constraints only fails the following tests:

• EndToEnd/RemotePart.hylo
• TypeChecking/RemoteExpr.hylo
• TypeChecking/Overloading.hylo
• TypeChecking/LambdaCoercion.hylo
• TypeChecking/For.hylo
• TypeChecking/AbstractType.hylo

[dabrahams]

If Hylo has no subtypes, then all those checks fail as described. So clearly Hylo has subtypes. I thought we eliminated all of them. What are examples of the subtypes that remain?

[kyouko-taiga]

Yes, Hylo does have a subtyping relationship, as I acknowledged.

Arrow types are in the relationship. For example [](Int) let -> Int <: []() inout -> Int. Removing this relationship would make it very hard to work with higher-order functions in generic code because maximally generic signatures take mutating lambdas while most arguments are non-mutating:

extension Array {
  fun map<E, R>(_ transform: inout [E](Element) inout -> R) -> Element[] { ... }
}
public fun main() {
  Array([1, 2, 3]).map(fun(_ e) { e + 1 }) // type of lambda is [](let Int) let -> Int
}

Note that the other usual rules about subtyping between functions do not apply because they would involve a change of representation at call boundary. For example [](Int) -> Int is not subtype of [](Int) -> any Regular and [](any Regular) -> Int is not subtype of [](Int) -> Int.

Existentials are in the relationship. For example any Regular <: any Copyable since clearly having a conformance to Regular implies having a conformance to Copyable and there is no change of representation.

Also:

• T <: remote let T
• T <: let T, where let T is a parameter type
• T <: @autoclosure [E]() -> T

The following relationships are understood by the type checker but they involve changes of representation, which must be written explicitly in source with the as operator:

• T <: Union<T, U>
• Union<T, U> <: Union<T, U, V>
• T <: any P, where T: P holds

And of course we have the standard additional rules that make the subtyping relationship a transitive reflexive closure.