Limitations of Type Inference

[DavePearce]

Despite the considerable progress made on improving type inference in Whiley using a bidirectional algorithm, there remain some problematic cases. Consider this:

function select<T>(T x, T y, bool f) -> (T z)
ensures f ==> (z == x)
ensures !f ==> (z == y):
    ...

(The implementation of this doesn't matter). Using the above, we can construct a problematic case like so:

nat a = select(1,2,true)

This fails with the following error:

test.whiley:15: expected nat, found int
    nat a = select(1,2,true)
                   ^

The reason is fairly straightforward. The constraints generated are {nat :> ?0; ?0 :> int} which are not solvable. At this stage, it's not clear what the best approach is. The workaround is to explicitly specify the template parameter as e.g. select<nat>(1,2,true).