Type inference could be more flexible

[nickbattle]

Consider the following:

	f[@T]: @T * @T -> nat
	f(a, b) == a + b
	pre is_real(a) and is_real(b);

This is type clean, and allows a pair of any type of number to be added (since a "nat" number is a real too). Without the precondition, the type checker cannot know that the parameters are numeric, and you get errors:

Error 3139: Left hand of + is not numeric in 'DEFAULT' (test.vdm) at line 3:18
Actual: @T
Error 3140: Right hand of + is not numeric in 'DEFAULT' (test.vdm) at line 3:18
Actual: @T

This is fine. But if the function is more complex, perhaps passing a map @T to @T, it would be nice to be able to say that part of this type is numeric, so that the function can add those parts. But if you say is_(rng m, real) the type inference cannot work out that the @T parameter is a map of ? to real:

	f[@T]: map @T to @T -> nat
	f(m) == m(1) + m(2)
	pre is_real(dom m) and is_real(rng m);

Error 3139: Left hand of + is not numeric in 'DEFAULT' (test.vdm) at line 3:18
Actual: @T
Error 3140: Right hand of + is not numeric in 'DEFAULT' (test.vdm) at line 3:18
Actual: @T