A few problems with return-type-substitutable, as defined in JLS 8:

- It talks about adapting type parameters without first asserting that the two signatures are the same (if not, the operation is undefined)

- It performs unchecked conversion *before* widening; javac and assignment perform it *after* widening

- It asserts R1 == |R2|, while javac checks that R1 <: |R2|

- Cosmetically, "does not have the same signature" is (probably?) more general than needed—we're really asserting that d1 is a proper subsignature of d2, rather than being the same.

For the javac discrepancies, it may be that javac needs to be corrected, but we should look more closely and the motivation for the specified rules.