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
.