Missing where clause on handle types and incorrect subtyping checks on maps containing arrows

[MikaelMayer]

method test(p: (int --> int) --> nat) {
  var m: map<string, (int --> int) --> nat> := map[
    "p" := p];
}

The code should clearly work, however, Dafny reports an error:

value does not satisfy the subset constraints of '(int ~> int) ~> int'

[MikaelMayer]

I found a workaround for now

method test(p: (int --> int) --> nat) {
  var m: map<string, (int --> int) --> nat> := map[];
  var m2 := m["p" := p];
}

[cpitclaudel]

There are two bugs in one here:

First, the resolver doesn't correctly compute the subtyping relation between arrows, and hence it issues a verification condition. This happens for maps but not for sequences:

method test(p: (int --> int) --> nat) {
  var s: seq<(int --> int) --> nat> := [p]; // OK
  var m: map<string, (int --> int) --> nat> := map["p" := p]; // NOK
}

Second, the translator does not produce any assumptions about the type of p. The Boogie code looks like this:

implementation {:verboseName "test (correctness)"} Impl$$_module.__default.test(p#0: HandleType) returns ($_reverifyPost: bool)
{
…
    assert $Is(p#0, Tclass._System.___hFunc1(Tclass._System.___hFunc1(TInt, TInt), TInt));

… that assert should be preceded by an assume saying the exact same thing (or most likely a where clause).

For example, when we write this:

method testNat(n: nat) {
  assert n >= 0;
}

… we get this, with a where clause:

procedure {:verboseName "testNat (well-formedness)"} CheckWellFormed$$_module.__default.testNat(n#0: int where LitInt(0) <= n#0);