Function values requires exact domain type

[RustanLeino]

The current encoding of function values in the verifier only expands a function value to its definition if the static types involved in its application are exactly as in the original function definition. This means that, if Y is a subset type of X, then a function of type X -> int cannot be used in a context that expects a Y -> int.

The following repro illustrates:

function Apply<T>(x: T, f: T -> int): int {
  f(x)
}
function F(x: int): int {
  x
}
lemma Test() {
  assert Apply<int>(4, F) == 4;  // this is verified
  assert Apply<nat>(4, F) == 4;  // this reports an error
}

Internally, the axiom about the function value F (which is called F#Handle in the Boogie encoding) has the form (where Apply1 is a function introduced by Dafny in the Boogie encoding to apply arity-1 function handles):

axiom (forall heap: Heap, bx: Box ::
  Apply1(TInt, TInt, heap, F#Handle(), bx)
     == $Box(F($Unbox(bx): int)));

Note the parameters TInt, which make this axiom useless when these types are applied as something else. A better encoding would leave flexibility in these parameters or, ideally, leave those type parameters out altogether among the arguments to Apply.