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