Unsoundness with testing of function types
(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.