Algebraic subtyping

[tiansivive]

Incorporate Algebraic Subtyping to infer and typecheck singleton types, type unions and liquids

[tiansivive]

Requirements:

• Discharge Subtype relationships
• Polar types for identifying the variance of the subtyping relationships.
• Biunification
• Bisubstitution

[tiansivive]

Follow up:

No need for discharging subtype relationship.
Instead, emit polarity for each inferred type, which will allow deciding between sub or super types in function parameter and return types

Unification:
The current unification is already emitting "bisubstitutions", in that it emits proofs of subtypes for each type variable. This is currently essential for liquid refinements. We can extend the system to typecheck and infer correct sub/super relationship in arrow fn types and type unions.

[tiansivive]

Polarity might not be needed if all we're doing is subtyping of singletons, type unions and liquids.

While liquids can be considered subtypes, there should be no need for a formal subtyping relationship. Simple constraint work well.
Singletons can be modelled with a row polymorphism analogue.
Type unions can also be considered a subtyping relationship but they require specific machinery too.

This all means we probably DO NOT need a formal subtyping system.

That said, polarity might still be useful, and the "bisubstitution" mechanism can be extended for other features!