Type Refinement via Assignment

[DavePearce]

At the moment, type refinement via assignment is permitted. This is a useful feature which, for example, allows the following to compile:

int|null x = 1
int y = x + 1

However, there is currently an unfortunately mistake in the refinement process. Specifically, the type of the assigned expression is used as the refinement. Whilst this seems quite logical, it is flawed. For example:

import string from js::core
string s = "hello"
assert s[0] == 'h'

The problem here is that the type of s in the access expression is int[] not string. Since these types are not equivalent on the implementation side, this does not work. Another interesting example is this:

function f(bool[] ps) -> int:
   return |ps|

function f(int[] xs) -> int:
  return |xs|

method main():
   int[] xs = []
   assume f(xs) == 0

This complains with the following error:

./src/main.whiley:9: unable to resolve name (is ambiguous)
        found function main::f(bool[])->(int)
        found function main::f(int[])->(int)
   assume f(xs) == 0

See also related problem that arose which was pretty confusing: https://github.com/Whiley/WhileyCompiler/issues/970

Proposal

The solution is actually pretty straightforward. Instead of using the type of the assigned expression directly, we instead use the type of the assigned expression to refine the declared variable type. This gives the benefits of refinement without the apparent disconnect between a variables declared type and its assumed type.