I disagree, to understand the differences one needs to define semantics for the terms first. To be concrete, what is an existential, a compile time existential, existential containers, existential values, existential types, existential box, opaqueness.

Then, differences between the meaning of these terms can be inferred and reoccurring discussions about them can be eliminated.

What does that mean?

Did you refer to the point of assigning an `any P`

to `some P`

?

And if `some P`

types can be defined in terms of existential quantification, why aren't these existential types then?

Agree

Disagree, as this would imply `some P`

!= `some P`

at the type level, which is a contradiction.

I think you are talking about three entities here:

**opaque type**: `some P`

**underlying type transparent to the type system**: `(global1(),Int)`

**underlying type opaque to the type system**: `Int`

And yes, between the "underlying type transparent to the type system" and "the underlying type opaque to the type system" we have a many-to-one mapping, e.g. `Int`

can be mapped to type `(global1(),Int)`

and `(global2(),Int)`

but `Float`

can't be mapped to `(global1(),Int)`

as changing function `global1`

to return Float would also change the transparent type to `(global1(),Float)`

.

The mapping from `some P`

to the "underlying type transparent to the type system" as well as to the "underlying type opaque to the type system" is one-to-many.

To see this, just change `return 2`

to `return 2.0`

in a function with `some Number`

as return type and the function is still sound.