Module name "Module" cannot be used with Java

[RustanLeino]

Dafny version

2023-06-03 (post 4.1.0)

Code to produce this issue

method Main() {
  Module.Hello();
}

module Module {
  method Hello() {
    print "hello Module\n";
  }
}

Command to run and resulting output

% dafny run --target:java test.dfy

Dafny program verifier finished with 1 verified, 0 errors
./test-java/_System/__default.java:13: error: cannot find symbol
    Module.__default.Hello();
          ^
  symbol:   variable __default
  location: class Module
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

For some reason, the name Module cannot be used as a module in Java. Everything works by renaming the module to, say, ModuleM or MODULE, in the Dafny source.

Another repro that shows the same problem is to rename Module to String in the example above.

It seems that Java is resolving these names to java.lang.Module or java.lang.String.

Notes:

• The Dafny compilers all have a mechanism for mangling Dafny identifiers that would otherwise clash with target-language keywords. However, there's currently no mechanism to mangle names that may be picked up from some standard always-included library. One simple solution would be to include these names (Module, String, ...) among the reserved keywords. A more precise solution would be to build a similar mechanism that's applied only to module names.
• A similar problem for the module name enum in Python, which seems to always resolve to the standard-library enum in Python. If this bug gets fixed, Python should be updated accordingly. See also Test/dafny4/Bug116.dfy.

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

Mac