Expressible and Denotable types

Wildcards were added to Java in version 5 to make generics more useable (that is, more powerful and flexible). Whereas most people understand generics pretty quickly ("so its a List of Strings, not just a List"), wildcards seem much more widely misunderstood and confusing. One reason is that they are undoubtedly more complex (compare WildFJ to FGJ). But, I believe another reason they are hard to use (and understand) is that the programmer can create types that can not be defined in the syntax. To quote Erik Meijer (on a different mechanism), Java has types that are "expressible but not denotable". This basically means that the type system can say what they are, but the syntax can't. Here's an example:

<Z> Pair<Z,Z> makePair(List<X> l) {...}
<Z> void usePair(Pair<Z,Z> p) {...}
void m(List<?> x, Pair<?, ?> y)
{
    usePair(y);            //type error
    usePair(makePair(x));  //OK
}

Weird, huh? The type checker knows that makePair(x) has type Pair<?, ?>, but the ? represent the same types, whereas in the type of y they represent different types. Unfortunately this can't be denoted in the syntax (thus the soundbyte: types can be expressed by the programmer but not denoted).

So, Java has expressible but not denotable types, so what? Well you can probably see the kind of ugly situation that occurs from the little example above. Type correctness becomes confusing and surprising (for the programmer, never good). Also, I believe, since there is no syntax for the types, they become harder to reason about by a programmer (they are certainly harder to reason about formally, but more on that another day...).

It seems then, that having 'expressible but not denotable' types is bad language design. Certainly, if I were to design a language (after playing with Wildcards for a year), I'd avoid expressible but not denotable types like the Black Plague. However, is there an alternative? The way to reason about these types formally is to use existential types. So we could replace wildcards with existential types, but to be honest this would probably make it more confusing. The above example becomes:

void m(∃Y.List<Y> x, ∃X,Y.Pair<X,Y> y)
{
    usePair(y);            //type error
    ∃Y.Pair<Y,Y> z = makePair(x);
    usePair(z);            //OK
}

The extra assignment isn't necessary, but shows you the type can be denoted. Not so nice huh? And don't even ask how you'd type '∃' in an ASCII editor. So, can anyone think of an alternative?