Avoiding Cycles with Unification and Subtyping

Question

Context

I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail there is not a single most general solution, and where annotations can be added to aid inference.

Suppose that we have a type system where, during typechecking, some types need to be inferred using unification, and may be type variables $\alpha, \beta$ etc.

If, at some point, the constraint $\alpha <: T_1 \to T_2$, where $\to$ is the usual function type constructor, then we can decompose this into $\alpha = \alpha_1 \to \alpha_2$, with $T_1 <: \alpha_1$ and $\alpha_2 <: T_2$.

The Problem

The problem arises if you have constraints $\alpha_2 <: \beta_1 \to \beta_2$, $\beta_2 <: \alpha_1 \to \alpha_2$.

In such a case, we get: $\alpha_2 = \alpha_{21} \to \alpha_{22}, \beta_1 <: \alpha_{21}, \alpha_{22} <: \beta_2 $ from the first constraint, and $\beta_2 = \beta_{21} \to \beta_{22}, \alpha_2 <: \beta_{21}, \beta_{22} <: \alpha_2$ from our second problem.

If we substitute from our equalities, we then get (among other constraints), $\alpha_{22} <: \beta_{21} \to \beta_{22}$ and $\beta_{22} <: \alpha_{21} \to \alpha_{22}$, which is identical to the form of our original problem. Clearly if we continue solving this way, we will never terminate.

When going to write a proof of termination, the problem is that substitution decreases the number of unsolved variables but increases the structural-size of the problems, and solving subtyping decreases the structural size of the problems, but increases the number of unsolved variables, so they don't work in a well-founded ordering.

My Solution Attempt

With my definition of subtyping, if $\alpha_2 <: \beta_1 \to \beta_2$, $\beta_2 <: \alpha_1 \to \alpha_2$ has no solution. The problem seems to be the "cycle", so if we do a sort of occurs check and fail when cycles are detected (or turn them into equality cycles, which will fail except for $\alpha <: \beta \wedge \beta <: \alpha$).

I'm not exactly certain how to formalize a cycle like this, and how such a check would give me something that I can use in a proof of termination.

My Question

My work is about the specifics of a particular subtyping system, but the problem here seems very general, so I'm wondering if this is a known problem, if there are known solutions to it, and if there is research that either formalizes or disproves my intuition about cycles.

What kind of cycles in subtyping constraints do I need to eliminate to avoid this infinite looping? Or is this a deeper problem with no solution?

Answer 1

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.