Drawbacks of adding type equality to 1ML
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.