why is specified equivalence between wildcard and existential types not observed in REPL

Question

According to THE Java Programming Language 4th ed. section 15.7.1 "Type Tokens":

getClass receives special treatment by the compiler: If getClass is invoked on a reference with static type T, then the compiler treats the return type of getClass as being Class. So this works:

String str = "Hello";
Class<? extends String> c2 = str.getClass(); // compiler magic

The javadocs for the getClass method in class Object give more detail:

The actual result type [of getClass()] is Class<? extends |X|> where |X| is the erasure of the static type of the expression on which getClass is called. For example, no cast is required in this code fragment:

Number n = 0; 
Class<? extends Number> c = n.getClass();

That's Java and the getClass() method of class Object. Switching attention to Scala, SLS 3.2.10 reads,

Placeholder Syntax for Existential Types

Syntax:

WildcardType ::= ‘_’ TypeBounds

Scala supports a placeholder syntax for existential types. A wildcard type is of the form _ >: L <: U...A wildcard type is a shorthand for an existentially quantified type variable, where the existential quantification is implicit.

...Let T = p.c[targs, T, targs'] be a parameterized type where targs, targs' may be empty and T is a wildcard type _ >: L <: U . Then T is equivalent to the existential type

p.c[targs, t , targs ] forSome { type t >: L <: U }

where t is some fresh type variable.

I emphasized "T is equivalent to the existential type..." above because the behavior I am observing seems to be inconsistent with that statement.

What I did

In the Scala repl I try the wildcard syntax of SLS 3.2.10:

scala> val c: Class[_ >: scala.Nothing <: String] = "foo".getClass
c: Class[_ <: String] = class java.lang.String

That works as I expect. But if I rely on the equivalence claimed in SLS 3.2.10 that "A wildcard type is a shorthand for an existentially quantified type variable," I get unexpected failure.

scala> val c: Class[t forSome { type t >: scala.Nothing <: String }] = "foo".getClass
<console>:7: error: type mismatch;
 found   : java.lang.Class[?0] where type ?0 <: java.lang.String
 required: Class[t forSome { type t <: String }]
Note: ?0 <: t forSome { type t <: String }, but Java-defined class Class is invariant in type T.
You may wish to investigate a wildcard type such as `_ <: t forSome { type t <: String }`. (SLS 3.2.10)
       val c: Class[t forSome { type t >: scala.Nothing <: String }] = "foo".getClass
                                                                         ^

The error message appears to be guiding me recursively back to SLS 3.2.10, suggesting I use both the wildcard syntax along with the express existential quantification. I don't understand what that means. In any event, I observe the same dichotomy using the example from the Object javadocs that I quoted above:

scala> val n: Number = 0
n: java.lang.Number = 0

Works:

scala> val c: Class[_ >: scala.Nothing <: Number] = n.getClass
c: Class[_ <: java.lang.Number] = class java.lang.Integer

Not works:

scala> val c: Class[t forSome { type t >: scala.Nothing <: Number }] = n.getClass
<console>:8: error: type mismatch;
 found   : java.lang.Class[?0] where type ?0 <: java.lang.Number
 required: Class[t forSome { type t <: java.lang.Number }]
Note: ?0 <: t forSome { type t <: java.lang.Number }, but Java-defined class Class is invariant in type T.
You may wish to investigate a wildcard type such as `_ <: t forSome { type t <: java.lang.Number }`. (SLS 3.2.10)
       val c: Class[t forSome { type t >: scala.Nothing <: Number }] = n.getClass

The Questions

Primarily

If a particular wildcard type is "equivalent" to a particular existential type, does that mean that one can be substituted for the other? Is that not the meaning of equivalence? Assuming I am correctly understanding the meaning "equivalence" as used in SLS 3.2.10, is there an error in my attempt to make that equivalent substitution according to the rules set forth in SLS 3.2.10? How are the failures of the repl to process the two statements I quoted above containing existential types consistent with SLS 3.2.10, according to which the failing statements are equivalent to the statements using wildcard types that succeed?

Additionally

What is the difference between the types specified in the required and found lines of the error messages in question? Namely, how is this:

java.lang.Class[?0] where type ?0 <: java.lang.String

different from

Class[t forSome { type t <: String }]

And what is that question mark in the first one? Obviously ?0 means something, it seems to be a type variable, but using a question mark like that is not Scala, is it? What language is that and where is it specified so I can understand that error message?

Answer 1

Look again at the part of the spec that you quoted:

Let T = p.c[targs, T, targs'] be a parameterized type where targs, targs' may be empty and T is a wildcard type _ >: L <: U . Then T is equivalent to the existential type p.c[targs, t , targs ] forSome { type t >: L <: U } where t is some fresh type variable.

In particular, notice that it says p.c[targs, t , targs ] forSome { type t >: L <: U } and not p.c[targs, t forSome { type t >: L <: U } , targs ]. Those two types are different.

Going back to the context of Class it means that Class[_ >: scala.Nothing <: String] is equivalent to Class[t] forSome { type t >: scala.Nothing <: String} , and not Class[t forSome { type t >: scala.Nothing <: String }].

And sure enough, if you enter the following in the REPL, it commpiles fine:

val c: Class[t] forSome { type t >: scala.Nothing <: String } = "foo".getClass

Answer 2

I don't know Scala, but I'd wager a guess based on my understanding of Java's wildcards.

If the type of an expression contains wildcard, java does "wildcard capture" on it

expr: "foo".getClass()
type: Class<? extends String>

after wildcard capture
type: Class<X>, for some X that X<:String

The two types are not exactly the same, the 2nd type is more specific (which is the reason to do wildcard capture in the first place, so that we get more type info on the expression)

"Wildcard capture" is applied extensively, on any expression. Therefore in almost all cases, a type containing a wildcard can be said to be equivalent to the type after capture conversion. For example the type of expression "foo".getClass() is Class<? extends String>, but we can equivalently think of its type as Class<X>, for some X that X<:String

But the two types are not always exchangeable. In Java, the 2nd type is not denotable; suppose it is, meaning we can declare a type like that

Class<Y>(for some Y<:String) var = "foo".getClass();

That line should not compile, because the right hand side, after capture conversion, gets a different, unrelated type variable, say X. So the line tries to assign Class<X> to Class<Y>.

This works

Class<? extends String> var = "foo".getClass();

because Class<X>(where X<:String) is a subtype of Class<? extends String>. As a matter of fact,

for any X<:String,  Class<X>  <:  Class<? extends String>

which can be considered the definition of the wildcarded type, which is essentially a union.

o instanceof Class<? extends String> 
iff 
there exists X<:String and o instanceof Class<X>

(Java type system does not consider the fact that, String is final so all these types are pretty much the same, since they all contain the same element, String.class)

We can say the two types are equivalent when we talk about expression types; they are not equivalent when we talk about variable types.