JLS3 8.4.5 defines return-type-substitutability in such a way that a supertype can be generified (and hence return type variables) while a subtype continues to use a ground type. This is the R1=|R2| requirement. Consider:

class AAA<X> { X m() { return null; } }
class BBB<Y> extends AAA<Y> { Y m() { return null; } }

javac accepts this, and it is legal in the JLS because BBB<Y> has a member 'Y m()' that overrides a member of its supertype AAA<Y>, 'Y m()'. Namely, the return type of 'Y m()' is a subtype of the return type of 'Y m()'. It is crucial to remember to compute membership of BBB<..> before considering whether 'Y m()' in BBB<..> overrides anything.