# Drawbacks of adding type equality to 1ML

In the 1ML – Core and Modules United (F-ing First-Class Modules) paper, the author gives the following example for why module types do not form a lattice under subtyping:

 f1 : {type t a; x : t int} → int
f2 : {type t a; x : int} → int
g = if condition then f1 else f2


There are at least two possible types for g:

 g : {type t a = int; x : int} → int
g : {type t a = a; x : int} → int


Neither is more specific than the other, so no least upper bound exists. Consequently, annotations are necessary to regain principal types for constructs like conditionals, in order to restore any hope for compositional type checking, let alone inference.

At first glance, it seems like the problem can be remedied by adding in type equalities:

g : (t int ~ int) ⇒ {type t a; x : int} → int


However, this "solution" isn't discussed in the paper. So it feels like I'm overlooking some obvious drawback of this idea, apart from the one that it might not be possible to encode type equality in System Fω (which is the raison d'être for the paper). Does adding type equalities make type checking/inference even more problematic in other situations?

Your proposal is an instance of a general design pattern for type systems that some would call a design smell: whenever you are stuck on an inference constraint that you cannot solve, or cannot solve in a principal way, include it in the resulting type. "It's not a problem, it's in the solution."

This solution can be made to work, but in general it may run into several practical issues:

• Constraint explosion. If those tricky problems occur more often than you would think, you can end up with many constraints (in particular if you sometimes need to introduce disjunctions of constraints; this is the end). This is problematic for user readability, and type-checking time.

• Loss of abstraction. The collected constraints reveal which unifications were done in the implementation, and sometimes they reveal too much details about the implementation compared to what the user had in mind. (On the other hand, they are usually principal, so what the user has in mind is not more general.)

• Delayed error. If you don't check that those delayed constraints are solvable, then you may delay error: all attempts to use the value will be an error, but there is no error as definition-site. (This gives the same usability issues as C++ templates.)

Not all instances of this "putting constraints in the solution" pattern have all these problems. In your example for example, it may be possible that the specific shape of equality constraints occurring (1) have no need for disjunction of equalities and (2) let you check solvability of constraints when they are introduced. You would have to think carefully about that.