One algorithm on the source type to try

Sub(A, mu a. B)
for Ti in spl(B):
    1. check if there are (negative) labels in Ti
    2. If so, let Bmi = Inv(T)
    3. Otherwise, find the (source) ordinary type in A and set Bmi = Ai
return Sub(mu a. (Bm1 & Bm2 & ... & Bmn), mu a. B)
which can be further checked by nominal unfolding

we can argue termination by setting the maximal depth of mu binders as the primary size.

Idea:

• only when all variables are positive in B can we do free rewriting, and transform T back to a source type
• the negative variable gives some information, though not essentially equivalence (as we had expected), but we hope that calling the subtyping check on the merge with the original type Ai can preserve that information

Gap in reasoning (expected):

• we still hope to obtain B <: Ai <: Tj for negative cases. However, we are not sure if it follows from the current case condition
  • the weakly positive restriction needs to be strengthened