Avoiding Cycles with Unification and Subtyping
From what I understand, it is likely that your subtyping constraints will always be of the form $\alpha \subseteq A$ or $A \subseteq \alpha$, where $\alpha$ is a unification variable. If that is the case, then one idea would be to follow a kind of occurs-check discipline. One thing that you can do to eliminate cycles is to maintain the invariant that there is a solution to your system. The solution that is the easiest to built (but the least general in some sense) is to set $\alpha := A$ for all constraints of the form $\alpha \subseteq A$, and to set $\alpha := \top$ for all constraints of the form $A \subseteq \alpha$ (and there is probably some work to do if $\alpha$ appears to the left/right of several constraints). For this solution to be valid, the simultaneous instantiation of all the unification variables should not induce a cycle in their definition. To do that, you can construct a form of dependency graph on unification variables, in which $\alpha$ depends on the unification variables of $A$ for each constraint $\alpha \subseteq A$. You then need to ensure that the obtained graph does not contain cycles.