Dafny version

4.9.2

Code to produce this issue

Issue has existed since at least v4.9.2

First, clone this branch of MPL.

include "[path to MPL]/libraries/src/MutableMap/MutableMap.dfy"
import opened DafnyLibraries

//import opened Std.Concurrent // NB: compiles successfully with --standard-libraries

method Main() {
  var m: MutableMap<nat, nat> := new MutableMap((_, _) => true, true);
}

Command to run and resulting output

For example, run dafny translate go [file below].dfy

This will generate the following code snippet:

func (_static *CompanionStruct_Default___) Main(__noArgsParameter _dafny.Sequence) {
  var _0_m *m_DafnyLibraries.MutableMap
  _ = _0_m
  var _nw0 *m_DafnyLibraries.MutableMap = m_DafnyLibraries.New_MutableMap_(true)
  _ = _nw0
  _0_m = _nw0
}

What happened?

This breaks the convention that allocation and initialization are performed by two different functions in target code. In particular, the externs (e.g., in Go and Java) for MutableMap have a parameter-less (excepting type descriptors) constructor (in Go, called New_MutableMap_) that allocates the object with default field values and a separate "constructor" function (c/C)tor__ with the expected parameters that does the expected initialization. So the output code should look like this:

...
  var _nw0 *m_DafnyLibraries.MutableMap = m_DafnyLibraries.New_MutableMap_()
  _ = _nw0
  _nw0.Ctor__(true)
...

The culprit is in SinglePassCodeGenerator.TrRhs():

...
        // Proceed with initialization
        if (allocateClass.InitCall != null) {
          if (constructor != null && IsExternallyImported(constructor)) {
            // initialization was done at the time of allocation
          } else {
            var wrBefore = wStmts.Fork();
            var wrCall = wStmts.Fork();
            var wrAfter = wStmts;
            TrCallStmt(allocateClass.InitCall, nw, wrCall, wrBefore, wrAfter);
          }
        }
...

IMO the comment about externs is inconsistent with what we say in the docs.

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

Mac