How the original rule fails

Note the example in the original rule:

js1 = inputTyp "(mu a. Int -> (mu b. a -> Int)) & \
              \ (mu a. Int -> (mu b. Top -> (Int -> Int)))"
 
js2 = inputTyp "mu a. Int -> (mu b. (a -> Int) & (a -> (Int -> Int)))"
 
ghci> (jsub (-1) js1 js2, tsubdp2 js1 js2)
(False,True)

The rule fails since we never split js2 due to the negative occurrences of a, but this example requires the subtyping then merge strategy. We are supposed to try to split js2 into mu a. Int -> (mu b. a -> Int) and mu a. Int -> (mu b. a -> (Int -> Int)) first, and then compare them with parts of js1.

Fix: enumerate all possible splits, including the negative ones