Function values generate malformed Java

[RustanLeino]

Dafny version

4.0.0

Code to produce this issue

type Fn<R> = f: int -> R | true witness *

method Arrows() {
  var f: Fn<int>;
}

Command to run and resulting output

% dafny run --target java test.dfy

Dafny program verifier finished with 0 verified, 0 errors
./test-java/_System/Fn.java:13: error: cannot find symbol
    return (dafny.TypeDescriptor<java.util.function.Function<java.math.BigInteger, R>>) (dafny.TypeDescriptor<?>) dafny.TypeDescriptor.referenceWithInitializer(java.util.function.Function.class, () -> ((java.math.BigInteger x0) -> _default_R));
                                                                                                                                                                                                                                       ^
  symbol:   variable _default_R
  location: class Fn<R>
  where R is a type-variable:
    R extends Object declared in class Fn
./test-java/_System/Fn.java:13: error: incompatible types: cannot infer type-variable(s) T
    return (dafny.TypeDescriptor<java.util.function.Function<java.math.BigInteger, R>>) (dafny.TypeDescriptor<?>) dafny.TypeDescriptor.referenceWithInitializer(java.util.function.Function.class, () -> ((java.math.BigInteger x0) -> _default_R));
                                                                                                                                                               ^
    (argument mismatch; bad return type in lambda expression
      incompatible parameter types in lambda expression)
  where T is a type-variable:
    T extends Object declared in method <T>referenceWithInitializer(Class<T>,Initializer<T>)
2 errors
Error while compiling Java files. Process exited with exit code 1

What happened?

Evidently, Java's type inference is not good enough to figure out the desired types. Some casts in the generated code are needed.

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

Mac

[robin-aws]

Similar but slightly different errors if you try to provide a witness (and tweak the subset type to make a witness possible), which #3893 doesn't yet fix:

datatype Option<T> = Some(t: T) | None

type Fn<R> = f: int -> Option<R> | true witness PartialFnWitness

function PartialFnWitness<R>(x: int): Option<R> {
  None
}

% dafny build -t:java src/Scratch.dfy

Dafny program verifier finished with 1 verified, 0 errors
/Users/salkeldr/Documents/GitHub/libraries/src/Scratch-java/_System/Fn.java:13: error: non-static variable _td_R cannot be referenced from a static context
    return (java.math.BigInteger _eta0) -> __default.<R>PartialFnWitness(_td_R, ((java.math.BigInteger)(java.lang.Object)(_eta0)));
                                                                         ^
/Users/salkeldr/Documents/GitHub/libraries/src/Scratch-java/_System/Fn.java:16: error: incompatible types: Function<BigInteger,Option<Object>> cannot be converted to Function<BigInteger,Option<R>>
    return (dafny.TypeDescriptor<java.util.function.Function<java.math.BigInteger, Option<R>>>) (dafny.TypeDescriptor<?>) dafny.TypeDescriptor.referenceWithInitializer(java.util.function.Function.class, () -> (java.util.function.Function<java.math.BigInteger, Option<R>>)Fn.defaultValue());
                                                                                                                                                                                                                                                                                              ^
  where R is a type-variable:
    R extends Object declared in method <R>_typeDescriptor(TypeDescriptor<R>)
Note: Some messages have been simplified; recompile with -Xdiags:verbose to get full output
2 errors
Error while compiling Java files. Process exited with exit code 1

[RustanLeino]

Thanks. I updated #3893 to fix this case, too.