Java Build Name Clash

[DavePearce]

Dafny version

4.2.0

Code to produce this issue

module Stack {
  type StackContent = s:seq<nat> | |s| < 65536

  datatype Stack = Stack(contents: StackContent)

  function Create() : Stack {
    Stack([])
  }
}

module Main {
  import Stack

  datatype VM = OK(pc: nat, stack: Stack.Stack) {
    function next() : VM {
      var st ≔ Stack.Create();
      OK(0,st)
    }
  }
}

Command to run and resulting output

dafny build --target java src/main.dfy

Dafny program verifier finished with 3 verified, 0 errors
/home/djp/projects/DafnyBug/src/main-java/Main/VM.java:67: error: cannot find symbol
    dafny.DafnySequence<? extends java.math.BigInteger> _0_st = Stack.__default.Create();
                                                                     ^
  symbol:   variable __default
  location: class Stack
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

The problem is that, at the top of the generated Java file we have:

import Stack.*;

This results in the call Stack.__default.Create() applying not to the package, but to the generated class Stack.

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

Linux

[olivier-aws]

Duplicate of #6014, fixed by #6016.