# 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?