What is the scenario when we get a s-ordinary B on the right, and weakly positive + negative reflexive case appears both on the left?
i.e., What happen if we get into?
A = mu a. Top -> mu b. (Int -> b)
& mu a. Int -> mu b. (a -> Int) --- the Int cannot be Top
<:
mu a. Int -> mu b. (Int -> b)
& mu a. Int -> mu b. (a -> Int)
B = mu a. Int -> (mu b. (Int -> b) & (a -> Int))
Meanwhile, this also holds:
A = mu a. Top -> mu b. (Int -> b) & (b -> (Int -> Int ))
& mu a. Int -> mu b. (b -> Int)
--- note that neg b + pos b is strict subtyping
--- note that here Int can be changed to Top
<:
mu a. Int -> (mu b. (Int -> b)) -- wp, RHS
& mu a. Int -> (mu b. (b -> Int)) -- neg, LHS
B = mu a. Int -> (mu b. (Int -> b) & (b -> (Int -> Int) ) & (b -> Int))
i.e., What happen if we get into?
This is a failing subtyping <<---- TODO; check why
A = mu a. Top -> mu b. (Int -> b)
& mu a. Int -> ((mu b. a -> Int) & (mu b. b -> Int))
<:
mu a. Int -> mu b. (Int -> b)
& mu a. Int -> ((mu b. a -> Int) & (mu b. b -> Int))
& mu a. Int -> (mu b. b -> Int)
B = mu a. Int -> (mu b. (Int -> b) & (a -> Int) & (b -> Int))