Move “Wildcard Types” to a subsection of “Parameterized Types”, and describe them independently of forSome.

Author: julienrf

docs/_spec/03-types.md

@@ -8,13 +8,9 @@ chapter: 3
 
 ```ebnf
   Type              ::=  FunctionArgTypes ‘=>’ Type
-                      |  InfixType [ExistentialClause]
+                      |  InfixType
   FunctionArgTypes  ::=  InfixType
                       |  ‘(’ [ ParamType {‘,’ ParamType } ] ‘)’
-  ExistentialClause ::=  ‘forSome’ ‘{’ ExistentialDcl
-                             {semi ExistentialDcl} ‘}’
-  ExistentialDcl    ::=  ‘type’ TypeDcl
-                      |  ‘val’ ValDcl
   InfixType         ::=  CompoundType {id [nl] CompoundType}
   CompoundType      ::=  AnnotType {‘with’ AnnotType} [Refinement]
                       |  Refinement
@@ -163,13 +159,14 @@ SimpleType      ::=  SimpleType TypeArgs
 TypeArgs        ::=  ‘[’ Types ‘]’
 ```
 
-A _parameterized type_ ´T[ T_1, ..., T_n ]´ consists of a type designator ´T´ and type parameters ´T_1, ..., T_n´ where ´n \geq 1´.
+A _parameterized type_ ´T[ T_1, ..., T_n ]´ consists of a type designator ´T´ and type arguments ´T_1, ..., T_n´ where ´n \geq 1´.
 ´T´ must refer to a type constructor which takes ´n´ type parameters ´a_1, ..., a_n´.
 
+<!-- TODO Mention well-kinded conformance when we introduce kind-polymorphism -->
 Say the type parameters have lower bounds ´L_1, ..., L_n´ and upper bounds ´U_1, ..., U_n´.
-The parameterized type is well-formed if each actual type parameter _conforms to its bounds_, i.e. ´\sigma L_i <: T_i <: \sigma U_i´ where ´\sigma´ is the substitution ´[ a_1 := T_1, ..., a_n := T_n ]´.
+The parameterized type is well-formed if each type argument _conforms to its bounds_, i.e. ´\sigma L_i <: T_i <: \sigma U_i´ where ´\sigma´ is the substitution ´[ a_1 := T_1, ..., a_n := T_n ]´.
 
-###### Example Parameterized Types
+#### Example Parameterized Types
 
 Given the partial type definitions:
 
@@ -178,9 +175,9 @@ class TreeMap[A <: Comparable[A], B] { ... }
 class List[A] { ... }
 class I extends Comparable[I] { ... }
 
-class F[M[_], X] { ... }
+class F[M[A], X] { ... }
 class S[K <: String] { ... }
-class G[M[ Z <: I ], I] { ... }
+class G[M[Z <: I], I] { ... }
 ```
 
 the following parameterized types are well-formed:
@@ -194,9 +191,7 @@ F[List, Int]
 G[S, String]
 ```
 
-###### Example
-
-Given the [above type definitions](#example-parameterized-types), the following types are ill-formed:
+and the following types are ill-formed:
 
 ```scala
 TreeMap[I]            // illegal: wrong number of parameters
@@ -211,6 +206,51 @@ G[S, Int]             // illegal: S constrains its parameter to
                       //   that conforms to Int
 ```
 
+#### Wildcard Type Argument
+
+<!-- TODO Update the syntax to use '?' -->
+```ebnf
+WildcardType   ::=  ‘_’ TypeBounds
+```
+
+A _wildcard type argument_ is of the form `_´\;´>:´\,L\,´<:´\,U´`.
+Both bound clauses may be omitted.
+If a lower bound clause `>:´\,L´` is missing, `>:´\,´scala.Nothing` is assumed.
+If an upper bound clause `<:´\,U´` is missing, `<:´\,´scala.Any` is assumed.
+A wildcard type is a shorthand for an existentially quantified type variable, where the existential quantification is implicit.
+
+A wildcard type must appear as a type argument of a parameterized type.
+The parameterized type to which the wildcard type is applied cannot be an abstract type constructor.
+The wildcard type argument is kind-polymorphic.
+
+Given the [above type definitions](#example-parameterized-types), the following types are well-formed:
+
+```scala
+List[_]
+List[_ <: java.lang.Number]
+S[_ <: String]
+F[_, Boolean]
+```
+
+and the following code contains an ill-formed type:
+
+```scala
+trait H[F[A]]:
+  def f: F[_] // illegal : an abstract type constructor
+              // cannot be applied to wildcard arguments.
+```
+
+Wildcard types may also appear as parts of [infix types](#infix-types), [function types](#function-types), or [tuple types](#tuple-types).
+Their expansion is then the expansion in the equivalent parameterized type.
+
+##### Simplification Rules
+
+Let ´T[T_1, ..., T_n]´ be a parameterized type.
+Then, applying a wildcard type argument ´t´ of the form ´\\_ >: L <: U´ at the ´i´'th position obeys the following equivalences:
+
+- If the type parameter ´T_i´ is declared covariant, then ´t \equiv U´
+- If the type parameter ´T_i´ is declared contravariant, then ´t \equiv L´
+
 ### Tuple Types
 
 ```ebnf
@@ -355,30 +395,6 @@ trait Function´_n´[-´T_1´, ..., -´T_n´, +´R´]:
 
 Their exact supertype and implementation can be consulted in the [function classes section](./12-the-scala-standard-library.md#the-function-classes) of the standard library page in this document.
 
-#### Wildcard Types
-
-```ebnf
-WildcardType   ::=  ‘_’ TypeBounds
-```
-<!-- TODO: Update this to use new mechanism -->
-A _wildcard type_ is of the form `_´\;´>:´\,L\,´<:´\,U´`.
-Both bound clauses may be omitted.
-If a lower bound clause `>:´\,L´` is missing, `>:´\,´scala.Nothing` is assumed.
-If an upper bound clause `<:´\,U´` is missing, `<:´\,´scala.Any` is assumed.
-A wildcard type is a shorthand for an existentially quantified type variable, where the existential quantification is implicit.
-
-A wildcard type must appear as a type argument of a parameterized type.
-Let ´T = p.c[\mathit{targs},T,\mathit{targs}']´ be a parameterized type where ´\mathit{targs}, \mathit{targs}'´ may be empty and ´T´ is a wildcard type `_´\ ´>:´\,L\,´<:´\,U´`.
-Then ´T´ is equivalent to the existential type
-
-```scala
-´p.c[\mathit{targs},t,\mathit{targs}']´ forSome { type ´t´ >: ´L´ <: ´U´ }
-```
-
-where ´t´ is some fresh type variable.
-Wildcard types may also appear as parts of [infix types](#infix-types), [function types](#function-types), or [tuple types](#tuple-types).
-Their expansion is then the expansion in the equivalent parameterized type.
-
 ## Non-Value Types
 
 The types explained in the following do not denote sets of values, nor do they appear explicitly in programs. 
@@ -563,7 +579,6 @@ Equivalence ´(\equiv)´ between types is the smallest congruence [^congruence]
   - corresponding parameters have equivalent types.
     Note that the names of parameters do not matter for method type equivalence.
 - Two [polymorphic method types](#polymorphic-method-types) are equivalent if they have the same number of type parameters, and, after renaming one set of type parameters by another, the result types as well as lower and upper bounds of corresponding type parameters are equivalent.
-- Two [existential types](#existential-types) are equivalent if they have the same number of quantifiers, and, after renaming one list of type quantifiers by another, the quantified types as well as lower and upper bounds of corresponding quantifiers are equivalent.
 - Two [type constructors](#type-constructors) are equivalent if they have the same number of type parameters, and, after renaming one list of type parameters by another, the result types as well as variances, lower and upper bounds of corresponding type parameters are equivalent.
 
 [^congruence]: A congruence is an equivalence relation which is closed under formation of contexts.
@@ -573,7 +588,7 @@ Equivalence ´(\equiv)´ between types is the smallest congruence [^congruence]
 
 The conformance relation ´(<:)´ is the smallest transitive relation that satisfies the following conditions.
 
-- Conformance includes equivalence. If `T \equiv U` then `T <: U`.
+- Conformance includes equivalence. If ´T \equiv U´ then ´T <: U´.
 - For every value type `T`, `scala.Nothing <: ´T´ <: scala.Any`.
 - For every type constructor ´T´ (with any number of type parameters), `scala.Nothing <: ´T´ <: scala.Any`.
 - For every value type ´T´, `scala.Null <: ´T´` unless `´T´ <: scala.AnyVal`.
@@ -582,10 +597,13 @@ The conformance relation ´(<:)´ is the smallest transitive relation that satis
 - A singleton type `´p´.type` conforms to the type of the path ´p´.
 - A singleton type `´p´.type` conforms to the type `scala.Singleton`.
 - A type projection `´T´#´t´` conforms to `´U´#´t´` if ´T´ conforms to ´U´.
-- A parameterized type `´T´[´T_1´, ..., ´T_n´]` conforms to `´T´[´U_1´, ..., ´U_n´]` if the following three conditions hold for ´i \in \{ 1, ..., n \}´:
+- A parameterized type `´T´[´T_1´, ..., ´T_n´]` conforms to `´T´[´U_1´, ..., ´U_n´]` if the following conditions hold for ´i \in \{ 1, ..., n \}´:
   1. If the ´i´'th type parameter of ´T´ is declared covariant, then ´T_i <: U_i´.
   1. If the ´i´'th type parameter of ´T´ is declared contravariant, then ´U_i <: T_i´.
   1. If the ´i´'th type parameter of ´T´ is declared neither covariant nor contravariant, then ´U_i \equiv T_i´.
+  1. If ´U_i´ is a wildcard type argument of the form ´\\_ >: L <: U´, then ´T_i >: L´ and ´T_i <: U´.
+  1. If ´U_i´ is a wildcard type argument of the form ´\\_ >: L_1 <: U_1´ and ´T_i´ is a wildcard argument of the form ´\\_ >: L_2 <: U_2´, then ´L_1 <: L_2´ and ´H_2 <: H_1´.
+  1. If ´U_i´ is a wildcard type argument of the form ´\\_ >: L <: U´ and the ´i´'th type parameter is declared covariant, then 
 - A compound type `´T_1´ with ... with ´T_n´ {´R\,´}` conforms to each of its component types ´T_i´.
 - If ´T <: U_i´ for ´i \in \{ 1, ..., n \}´ and for every binding ´d´ of a type or value ´x´ in ´R´ there exists a member binding of ´x´ in ´T´ which subsumes ´d´, then ´T´ conforms to the compound type `´U_1´ with ... with ´U_n´ {´R\,´}`.
 - If ´T_i \equiv T_i'´ for ´i \in \{ 1, ..., n\}´ and ´U´ conforms to ´U'´ then the method type ´(p_1:T_1, ..., p_n:T_n) U´ conforms to ´(p_1':T_1', ..., p_n':T_n') U'´.