Clash when compiling a datatype containing a static const Default

[mschlaipfer]

Dafny version

4.0.0.50303

Code to produce this issue

module m {
  datatype D = A
             | B
             | C {
    static const Default: D := A
  }
}

Command to run and resulting output

$ dafny build -t java bug.dfy

Dafny program verifier finished with 0 verified, 0 errors
<snip>/bug-java/m_Compile/D.java:37: error: method Default() is already defined in class D
  public static D Default()
                  ^
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

Dafny seems to codegen a Default method for datatypes, but does not check if there is a user-defined one. When defining Default ourselves there's a clash.

$ cat <snip>/bug-java/m_Compile/D.java

// Class D
// Dafny class D compiled into Java
package m_Compile;


@SuppressWarnings({"unchecked", "deprecation"})
public abstract class D {
  public D() { }

  private static final D theDefault = m_Compile.D.create_A();
  public static D Default() {
    return theDefault;
  }

// ...

  public static D Default()
  {
    return m_Compile.D.create_A();
  }
}

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

Mac