Drawbacks of adding type equality to 1ML

Question

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?