Test runner generator produces malformed Java code

[ssomayyajula]

Dafny version

latest

Code to produce this issue

datatype Option<U> = None() | Some(val: U) {
  predicate IsFailure() {
    None?
  }

  function PropagateFailure<U>(): Option<U>
    requires None?
  {
    None()
  }

  function Extract(): U
    requires Some?
  {
    val
  }
}

function foobar(): Option<()> { Some(()) }

// run 'dafny test --target java bug.dfy'
method {:test} Funky() returns (out: Option<()>) {
  for i := 0 to 100 {
    var fizz :- foobar();
  }
  return Some(());
}

Command to run and resulting output

bug-java/_System/__default.java:41: error: method IsFailure in class Option<U> cannot be applied to given types;
        if ((_2_result0).IsFailure()) {
                        ^
  required: TypeDescriptor<Tuple0>
  found: no arguments
  reason: actual and formal argument lists differ in length
  where U is a type-variable:
    U extends Object declared in class Option
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

(filing on behalf of @codyroux)

Because this error does not occur with dafny build --target java (or by removing the {:test} attribute from Funky()), it appears that the test runner generator is producing malformed target code (not passing a type descriptor when necessary).

It's likely has to do with how the elephant operator is inlined.

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

Mac