Java support for variance on type parameters

[robin-aws]

Dafny version

master, not yet released (edab6cc)

Code to produce this issue

module Repro {

    trait Foo {}
    class Bar extends Foo {
        constructor() {}
    }

    datatype Option<+T> = Some(value: T) | None
    datatype D = D(Option<Foo>)

    method Main() {
        var b: Bar := new Bar();
        var d := D(Some(b));
    }
}

Command to run and resulting output

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

Dafny program verifier finished with 1 verified, 0 errors
/Users/salkeldr/Documents/GitHub/libraries/src/Scratch-java/Repro_Compile/__default.java:17: error: incompatible types: Option<Bar> cannot be converted to Option<Foo>
    _1_d = Repro_Compile.D.create(Repro_Compile.Option.<Bar>create_Some(_0_b));
                                                                       ^
Note: Some messages have been simplified; recompile with -Xdiags:verbose to get full output
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

Root case is that the D data constructor creation method D.create has the following signature:

public static D create(Option<Foo> _a0) {
    return new D(_a0);
}

But given Option's type parameter is covariant, it should be:

public static D create(Option<? extends Foo> _a0) {
    return new D(_a0);
}

Or perhaps the intent was to insert an explicit unchecked (Option<Foo>) cast before passing the Option<Bar> value to the constructor.

This works correctly if the data constructor parameter is a seq<T> instead, which is also implicitly covariant.

@RustanLeino This looks like a missing case from #3072?

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

Mac