Opaque functions passed as arguments causes type checking errors

[EkanshdeepGupta]

Dafny version

4.1.0

Code to produce this issue

opaque function F(x: int): char
{ 'D' }

method InitArray<D>(f: int -> D) returns (a: D)
{
  return f(44);
}

method Main() {
  reveal F();
  var c := InitArray(F);
}

Command to run and resulting output

$ dafny verify ../../Test/test.dfy
/Users/ekanshdg/Test/test.dfy(44,16): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)
/Users/ekanshdg/Test/test.dfy(44,16): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)
/Users/ekanshdg/Test/test.dfy(44,16): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)
/Users/ekanshdg/Test/test.dfy(44,16): Error: wrong number of arguments to function: _module.__default.F (2 instead of 3)
/Users/ekanshdg/Test/test.dfy(44,16): Error: wrong number of arguments to function: _module.__default.F (2 instead of 3)
/Users/ekanshdg/Test/test.dfy(44,16): Error: wrong number of arguments to function: _module.__default.F (2 instead of 3)
/Users/ekanshdg/Test/test.dfy(54,21): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)
7 type checking errors detected in /var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl(4580,4): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl(4581,2): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl(4582,8): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl(4589,13): Error: wrong number of arguments to function: _module.__default.F (2 instead of 3)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl(4602,4): Error: wrong number of arguments to function: _module.__default.F (2 instead of 3)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl(4603,2): Error: wrong number of arguments to function: _module.__default.F (2 instead of 3)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/test__module.bpl(4641,12): Error: wrong number of arguments to function: _module.__default.F#Handle (2 instead of 1)

What happened?

Because opaque functions generate an extra argument, that is causing type-checking to fail when an opaque function is passed as an argument.

What type of operating system are you experiencing the problem on?

Mac

[stefan-aws]

See also #3504