Java backend: Unboxed bool return type in trait implementations

[eivindfjeldstad]

Dafny version

4.9.1

Code to produce this issue

test.dfy:

module Test {
  trait Something<T> {
    function hey(): T
  }

  datatype Broken extends Something<bool> = create(value: bool) {
    function hey(): bool {
      value
    }
  }
}

Command to run and resulting output

Running

dafny build test.dfy --general-traits=datatype --target:java

fails with

Dafny program verifier finished with 1 verified, 0 errors
/test-java/Test/Broken.java:7: error: Broken is not abstract and does not override abstract method hey() in Something
public class Broken implements Something<Boolean> {
       ^
/test-java/Test/Broken.java:57: error: hey() in Broken cannot implement hey() in Something
  public boolean hey() {
                 ^
  return type boolean is not compatible with Boolean
  where T is a type-variable:
    T extends Object declared in interface Something
2 errors
Error while compiling Java files. Process exited with exit code 1

What happened?

When compiling a Dafny datatype that implements a generic trait with bool as the type argument, the resulting Java code uses a primitive return type where a boxed type is required.

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

Mac