Spec: Opaque type aliases. (#17947)

[skip ci]

Based on #17940.

Author: sjrd

docs/_spec/03-types.md

@@ -1012,7 +1012,11 @@ We define `memberType(´T´, ´id´, ´p´)` as follows:
   - If ´m´ is not defined, the result is undefined.
   - If ´m´ is a class declaration, the result is a class result with class ´m´.
   - If ´m´ is a term definition in class ´D´ with declared type ´U´, the result is a term result with underlying type [`asSeenFrom`](#as-seen-from)`(´U´, ´D´, ´p´)` and stable flag true if and only if ´m´ is stable.
-  - If ´m´ is a type member definition in class ´D´ with declared type definition ´U´, the result is a type result with underlying type definition [`asSeenFrom`](#as-seen-from)`(´U´, ´D´, ´p´)`.
+  - If ´m´ is a type member definition in class ´D´, the result is a type result with underlying type definition [`asSeenFrom`](#as-seen-from)`(´U´, ´D´, ´p´)` where ´U´ is defined as follows:
+      - If ´m´ is an opaque type alias member definition with declared definition ´>: L <: H = V´, then
+          - ´U´ is ´= V´ if `´p = D.´this` or if we are computing `memberType` in a [_transparent mode_](#type-erasure),
+          - ´U´ is ´>: L <: H´ otherwise.
+      - ´U´ is the declared type definition of ´m´ otherwise.
 - If ´T´ is another monomorphic type designator of the form ´q.X´:
   - Let ´U´ be `memberType(´q´, ´X´)`
   - Let ´H´ be the upper bound of ´U´
@@ -1228,6 +1232,7 @@ A type is called _generic_ if it contains type arguments or type variables.
 _Type erasure_ is a mapping from (possibly generic) types to non-generic types.
 We write ´|T|´ for the erasure of type ´T´.
 The erasure mapping is defined as follows.
+Internal computations are performed in a _transparent mode_, which has an effect on how [`memberType`](#member-type) behaves for opaque type aliases.
 
 - The erasure of `AnyKind` is `Object`.
 - The erasure of a non-class type designator is the erasure of its underlying upper bound.

docs/_spec/04-basic-declarations-and-definitions.md

@@ -16,6 +16,7 @@ PatVarDef   ::=  ‘val’ PatDef
 Def         ::=  PatVarDef
               |  ‘def’ FunDef
               |  ‘type’ {nl} TypeDef
+              |  ‘opaque‘ ‘type‘ {nl} OpaqueTypeDef
               |  TmplDef
 ```
 
@@ -218,17 +219,21 @@ A variable definition `var ´x_1, ..., x_n: T´ = ´e´` is a shorthand for the
 ## Type Declarations and Type Aliases
 
 ```ebnf
-Dcl        ::=  ‘type’ {nl} TypeDcl
-TypeDcl    ::=  id [TypeParamClause] [‘>:’ Type] [‘<:’ Type]
-Def        ::=  ‘type’ {nl} TypeDef
-TypeDef    ::=  id [TypeParamClause] ‘=’ Type
+Dcl             ::=  ‘type’ {nl} TypeDcl
+TypeDcl         ::=  id [TypeParamClause] [‘>:’ Type] [‘<:’ Type]
+Def             ::=  ‘type’ {nl} TypeDef
+                  |  ‘opaque‘ ‘type‘ {nl} OpaqueTypeDef
+TypeDef         ::=  id [TypeParamClause] ‘=’ Type
+OpaqueTypeDef   ::=  id [TypeParamClause] [‘>:’ Type] [‘<:’ Type] ‘=’ Type
 ```
 
 A possibly parameterized _type declaration_ `type ´t´[´\mathit{tps}\,´] >: ´L´ <: ´H´` declares ´t´ to be an abstract type.
 If omitted, ´L´ and ´H´ are implied to be `Nothing` and `scala.Any`, respectively.
 
 A possibly parameterized _type alias_ `type ´t´[´\mathit{tps}\,´] = ´T´` defines ´t´ to be a concrete type member.
 
+A possibly parameterized _opaque type alias_ `opaque type ´t´[´\mathit{tps}\,´] >: ´L´ <: ´H´ = ´T´` defines ´t´ to be an opaque type alias with public bounds `>: ´L´ <: ´H´` and a private alias `= ´T´`.
+
 If a type parameter clause `[´\mathit{tps}\,´]` is present, it is desugared away according to the rules in the following section.
 
 ### Desugaring of parameterized type declarations
@@ -248,7 +253,7 @@ A parameterized abstract type
 ```scala
 type ´t´[´\mathit{tps}\,´] >: ´L´ <: ´H´
 ```
-is desugared into an unparameterized abstract type as follow:
+is desugared into an unparameterized abstract type as follows:
 - If `L` conforms to `Nothing`, then,
 
   ```scala
@@ -286,6 +291,25 @@ type ´t´ = [´\mathit{tps'}\,´] =>> ´T´
 ```
 where ´\mathit{tps'}´ is computed as in the previous case.
 
+#### Opaque Type Alias
+
+A parameterized type alias
+```scala
+type ´t´[´\mathit{tps}\,´] >: ´L´ <: ´H´ = ´T´
+```
+is desugared into an unparameterized opaque type alias as follows:
+- If `L` conforms to `Nothing`, then,
+
+  ```scala
+type ´t´ >: Nothing <: [´\mathit{tps'}\,´] =>> ´H´ = [´\mathit{tps'}\,´] =>> ´T´
+  ```
+- otherwise,
+
+  ```scala
+type ´t´ >: [´\mathit{tps'}\,´] =>> ´L´ <: [´\mathit{tps'}\,´] =>> ´H´ = [´\mathit{tps'}\,´] =>> ´T´
+  ```
+where ´\mathit{tps'}´ is computed as in the previous cases.
+
 ### Non-Parameterized Type Declarations and Type Aliases
 
 A _type declaration_ `type ´t´ >: ´L´ <: ´H´` declares ´t´ to be an abstract type whose [type definition](03-types.html#type-definitions) has the lower bound type ´L´ and upper bound type ´H´.
@@ -295,6 +319,19 @@ It is a compile-time error if ´L´ does not conform to ´H´.
 
 A _type alias_ `type ´t´ = ´T´` defines ´t´ to be an alias name for the type ´T´.
 
+An _opaque type alias_ `opaque type ´t´ >: ´L´ <: ´H´ = ´T´` defines ´t´ to be an opaque type alias with public bounds `>: ´L´ <: ´H´` and a private alias `= ´T´`.
+An opaque type alias can only be declared within a [template](./05-classes-and-objects.html#templates).
+It cannot be `private` and cannot be overridden in subclasses.
+In order for the definition to be valid, ´T´ must satisfy some constraints:
+
+- ´L <: T´ and ´T <: H´ must be true,
+- ´T´ must not be a context function type, and
+- If ´T´ is a type lambda, its result must be a proper type (i.e., it cannot be a curried type lambda).
+
+When viewed from within its enclosing template, an opaque type alias behaves as a type alias with type definition `= ´T´`.
+When viewed from anywhere else, it behaves as a type declaration with type definition `>: ´L´ <: ´H´`.
+See [`memberType`](./03-types.html#member-type) for the precise mechanism that governs this dual view.
+
 The scope rules for [definitions](#basic-declarations-and-definitions) and [type parameters](#method-declarations-and-definitions) make it possible that a type name appears in its own bounds or in its right-hand side.
 However, it is a static error if a type alias refers recursively to the defined type itself.
 That is, the type ´T´ in a type alias `type ´t´[´\mathit{tps}\,´] = ´T´` may not refer directly or indirectly to the name ´t´.

docs/_spec/TODOreference/other-new-features/opaques.md renamed to docs/_spec/APPLIEDreference/other-new-features/opaques.md

@@ -176,4 +176,28 @@ l1.mul(x, z) // error: found l2.Logarithm, required l1.Logarithm
 ```
 In general, one can think of an opaque type as being only transparent in the scope of `private[this]`.
 
-[More details](opaques-details.md)
+## Top-level Opaque Types
+
+An opaque type alias on the top-level is transparent in all other top-level definitions in the sourcefile where it appears, but is opaque in nested
+objects and classes and in all other source files. Example:
+```scala
+// in test1.scala
+opaque type A = String
+val x: A = "abc"
+
+object obj:
+  val y: A = "abc"  // error: found: "abc", required: A
+
+// in test2.scala
+def z: String = x   // error: found: A, required: String
+```
+This behavior becomes clear if one recalls that top-level definitions are placed in their own synthetic object. For instance, the code in `test1.scala` would expand to
+```scala
+object test1$package:
+  opaque type A = String
+  val x: A = "abc"
+
+object obj:
+  val y: A = "abc"  // error: cannot assign "abc" to opaque type alias A
+```
+The opaque type alias `A` is transparent in its scope, which includes the definition of `x`, but not the definitions of `obj` and `y`.