# 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.