I've written the attached program while thinking about method type
variable substitution in a proof I was doing and think that I found a
problem in javac

class D<Z> {
    Z f;
}
class E {}
class F {}

class C<Xc> {
    Xc dirty;
    
    <Xm> D<Xm> m(Xc pxc, Xm pxm, boolean rec) {
System.out.println("----\nthis: " + this + " pxc: " + pxc + " pxm: " + pxm );
if (rec) System.out.println("this is a C<D<F>>, pxc is a D<F>, pxm is an F");
if (!rec) System.out.println("this is another C<D<F>>, pxc is a D<E>, pxm is an E");

dirty = pxc; System.out.println("dirty: " + dirty + ", a " + (rec?"D<F>":"D<E>"));

C< D<Xm> > cdm = new C< D<Xm> >();
if( rec ) {
D<E> de = new D<E>();
de.f = new E();
cdm.m( de, new E(), false );
}
        System.out.println("Returning cdm.dirty: " + cdm.dirty +
(rec?" (a D<F>, allegedly)":" (a D<E>)") + "\n---");
return cdm.dirty;
    }
}

public class MTVDemo {
    public static void main( String[] args ) {
C< D<F> > cdf = new C< D<F> >();

D<F> df;
df = cdf.m( new D<F>(), new F(), true );

// Exception in thread "main" java.lang.ClassCastException:
// E cannot be cast to F
F x = df.f;

System.out.println("x: " + x);
    }
}

I then also tried the compiler coming with Eclipse 3.3 and got a type
error:


$ ecj -version
Eclipse Java Compiler v_774_R33x, 3.3.1, Copyright IBM Corp 2000, 2007.
All rights reserved.

$ ecj -5 MTVDemo.java ----------
1. ERROR in MTVDemo.java (at line 36)
    cdm.m( de, new E(), false );
        ^
The method m(D<Xm>, Xm, boolean) in the type C<D<Xm>> is not applicable
for the arguments (D<E>, E, boolean)
----------
1 problem (1 error)