Unsoundness with testing of function types

This code

(fun ((Int -> Int) -> `true; (Any \ (Int -> Int)) -> `false)
| ((Int -> Int) \ (Bool -> Bool)) -> `true
| (Int -> Int) & (Bool -> Bool) -> `true
| _ -> `false)
  (fun (x: Int): Int = x + 1)

breaks type preservation (in the cduce-next branch), producing

- : `true = false

The first function is well-typed; in particular, when the argument has type Int -> Int, the result must be true since either of the first two branches must apply (together, they cover Int -> Int entirely). The application is well-typed as well, but it reduces to the third branch (which is statically predicted to be unused) because the second function can be assigned neither type (Int -> Int) \ (Bool -> Bool) nor type (Int -> Int) & (Bool -> Bool).

This behaviour actually seems consistent with that described in the formalization (POPL '14 and '15), but it's unsound. When type tests are performed at runtime functions should probably be given negations of arrow types to ensure soundness. I'm not sure how this interacts with polymorphism though.