From 8492c211c2788b93acd2414bea1c8d58fb7ddc29 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 29 May 2014 18:43:53 +0200
Subject: [PATCH 1/4] Version 2, picking up on an idea of Adriaan.

---
 docs/HigherKinded-v2.md | 326 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 326 insertions(+)
 create mode 100644 docs/HigherKinded-v2.md

diff --git a/docs/HigherKinded-v2.md b/docs/HigherKinded-v2.md
new file mode 100644
index 000000000000..1d29b35ea31b
--- /dev/null
+++ b/docs/HigherKinded-v2.md
@@ -0,0 +1,326 @@
+Higher-Kinded Types in Dotty V2
+===============================
+
+This note outlines how we intend to represent higher-kinded types in
+Dotty.  The principal idea is to collapse the four previously
+disparate features of refinements, type parameters, existentials and
+higher-kinded types into just one: refinements of type members. All
+other features will be encoded using these refinements.
+
+The complexity of type systems tends to grow exponentially with the
+number of independent features, because there are an exponential
+number of possible feature interactions. Consequently, a reduction
+from 4 to 1 fundamental features achieves a dramatic reduction of
+complexity. It also adds some nice usablilty improvements, notably in
+the area of partial type application.
+
+This is a second version of the scheme which differs in a key aspect
+from the first one: Following Adriaan's idea, we use traits with type
+members to model type lambdas and type applications. This is both more
+general and more robust than the intersections with type constructor
+traits that we had in the first version.
+
+The duality
+-----------
+
+The core idea: A parameterized class such as
+
+    class Map[K, V]
+
+is treated as equivalent to a type with type members:
+
+    class Map { type Map$K; type Map$V }
+
+The type members are name-mangled (i.e. `Map$K`) so that they do not conflict with other
+members or parameters named `K` or `V`.
+
+A type-instance such as `Map[String, Int]` would then be treated as equivalent to
+
+    Map { type Map$K = String; type Map$V = Int }
+
+Named type parameters
+---------------------
+
+Type parameters can have unmangled names. This is achieved by adding the `type` keyword
+to a type parameter declaration, analogous to how `val` indicates a named field. For instance,
+
+    class Map[type K, type V]
+
+is treated as equivalent to
+
+    class Map { type K; type V }
+
+The parameters are made visible as fields.
+
+Wildcards
+---------
+
+A wildcard type such as `Map[_, Int]` is equivalent to
+
+    Map { type Map$V = Int }
+
+I.e. `_`'s omit parameters from being instantiated. Wildcard arguments
+can have bounds. E.g.
+
+    Map[_ <: AnyRef, Int]
+
+is equivalent to
+
+    Map { type Map$K <: AnyRef; type Map$V = Int }
+
+
+Type parameters in the Encodings
+--------------------------------
+
+The notion of type parameters makes sense even for encoded types,
+which do not contain parameter lists in their syntax. Specifically,
+the type parameters of a type are a sequence of type fields that
+correspond to paraneters in the unencoded type. They are determined as
+follows.
+
+ - The type parameters of a class or trait type are those parameter fields declared in the class
+   that are not yet instantiated, in the order they are given. Type parameter fields of parents
+   are not considered.
+ - The type parameters of an abstract type are the type parameters of its upper bound.
+ - The type parameters of an alias type are the type parameters of its right hand side.
+ - The type parameters of every other type is the empty sequence.
+
+Partial applications
+--------------------
+
+The definition of type parameters in the previous section leads to a simple model of partial applications.
+Consider for instance:
+
+    type Histogram = Map[_, Int]
+
+`Histogram` is a higher-kinded type that still has one type parameter.
+`Histogram[String]`
+would be a possible type instance, and it would be equivalent to `Map[String, Int]`.
+
+
+Modelling polymorphic type declarations
+---------------------------------------
+
+The partial application scheme gives us a new -- and quite elegant --
+way to do higher-kinded types. But how do we interprete the
+poymorphic types that exist in current Scala?
+
+More concretely, current Scala allows us to write parameterize type
+definitions, abstract types, and type parameters. In the new scheme,
+only classes (and traits) can have parameters and these are treated as
+equivalent to type members. Type aliases and abstract types do not
+allow the definition of type members so we have to interprete
+polymorphic type aliases and abstract types specially.
+
+Modelling polymorphic type aliases
+----------------------------------
+
+A polymorphic type alias such as
+
+    type Pair[T] = (T, T)
+
+is represented as a monomorphic type alias of a type lambda. Here's the expanded version of
+the definition above:
+
+    type Pair = Lambda1 { type Apply = (Arg1, Arg1) }
+
+Here, `Lambda1` is a standard trait defined as follows:
+
+    trait Lambda1[type Arg1, type Apply]
+
+According to our definitions of type parameters `Lambda1` has two type parameters
+and `Pair` has one.
+
+There are `LambdaN` traits for higher arities as well. `Lambda` traits are special in that
+they influence how type applications are expanded: If standard type applicatuon `T[X1, ..., Xn]`
+leads to a subtype `S` of a type instance
+
+      LambdaN { type Arg1 = T1; ...; type ArgN = Tn; type Apply ... }
+
+where all argument fields `Arg1, ..., ArgN` are concretely defined
+and the definition of the `Apply` field may be either abstract or concrete, then the application
+is further expanded to `S # Apply`.
+
+For instance, the type instance `Pair[String]` would be expanded to
+
+    Lambda1 { type Arg1 = String; type Apply = (Arg1, Arg1) } # Apply
+
+which turns out to be equal to `(String, String)`.
+
+2nd Example: Consider the two aliases
+
+    type RMap[K, V] = Map[V, K]]
+    type RRMap[K, V] = RMap[V, K]
+
+These expand as follows:
+
+    type RMap  = Lambda2 { self1 => type Apply = Map[self1.Arg2, self1.Arg1] }
+    type RRMap = Lambda2 { self2 => type Apply = RMap[self2.Arg2, self2.Arg1] }
+
+Substituting the definition of `RMap` and expanding the type application gives:
+
+    type RRMap = Lambda2 { self2 => type Apply =
+                   Lambda2 { self1 => type Apply = Map[self1.Arg2, self1.Arg1] }
+                           { type Arg1 = self2.Arg2; type Arg2 = self2.Arg1 } # Apply }
+
+Substituting the definitions `self1.Arg{1,2}` gives:
+
+    type RRMap = Lambda2 { self2 => type Apply =
+                   Lambda2 { self1 => type Apply = Map[self2.Arg1, self2.Arg2] }
+                           { type Arg1 = self2.Arg2; type Arg2 = self2.Arg1 } # Apply }
+
+Simplifiying the `# Apply` selection gives:
+
+    type RRMap = Lambda2 { self2 => type Apply = Map[self2.Arg1, self2.Arg2] }
+
+This can be regarded as the eta-expanded version of `Map`. It has the same expansion as
+
+    type IMap[K, V] = Map[K, V]
+
+
+Modelling higher-kinded types
+-----------------------------
+
+The encoding of higher-kinded types uses again the `Lambda` traits to represent type constructors.
+Consider the higher-kinded type declaration
+
+    type Rep[T]
+
+We expand this to
+
+    type Rep <: Lambda1
+
+The type parameters of `Rep` are the type parameters of its upper bound, so
+`Rep` is a uniary type constructor.
+
+More generally, a higher-kinded type declaration
+
+     type T[X1 >: S1 <: U1, ..., XN >: S1 <: UN] >: SR <: UR
+
+is encoded as
+
+     type T <: LambdaN { self =>
+       type Arg1 >: s(S1) <: s(U1)
+       ...
+       type ArgN >: s(SN) <: s(UN)
+       type Apply >: s(SR) <: s(UR)
+     }
+
+where `s` is the substitution `[XI := self.ArgI | I = 1,...,N]`.
+
+If we instantiate `Rep` with a type argument, this is expanded as was explained before.
+
+    Rep[String]
+
+would expand to
+
+    Rep { type Arg1 = String } # Apply
+
+If we instantiate the higher-kinded type with a concrete type constructor (i.e. a parameterized
+trait or class, we have to do one extra adaptation to make it work. The parameterized trait
+or class has to be eta-expansed so that it comforms to the `Lambda` bound. For instance,
+
+    type Rep = Set
+
+would expand to
+
+    type Rep = Lambda1 { type Apply = Set[Arg1] }
+
+Or,
+
+    type Rep = Map[String, _]
+
+would expand to
+
+    type Rep = Lambda1 { type Apply = Map[String, Arg1] }
+
+
+Full example
+------------
+
+Consider the higher-kinded `Functor` type class
+
+    class Functor[F[_]] {
+       def map[A, B](f: A => B): F[A] => F[B]
+    }
+
+This would be represented as follows:
+
+    class Functor[F <: Lambda1] {
+       def map[A, B](f: A => B): F { type Arg1 = A } # Apply  =>  F { type Arg1 = B } # Apply
+    }
+
+The type `Functor[List]` would be represented as follows
+
+    Functor {
+       type F = Lambda1 { type Apply = List[Arg1] }
+    }
+
+Now, assume we have a value
+
+    val ml: Functor[List]
+
+Then `ml.map` would have type
+
+    s(F { type Arg1 = A } # Apply  =>  F { type Arg1 = B } # Apply)
+
+where `s` is the substitution of `[F := Lambda1 { type Apply = List[Arg1] }]`.
+This gives:
+
+    Lambda1 { type Apply = List[Arg1] } { type Arg1 = A } # Apply
+     =>  Lambda1 { type Apply = List[Arg1] } { type Arg1 = B } # Apply
+
+This type simplifies to:
+
+     List[A] => List[B]
+
+Status of #
+-----------
+
+In the scheme above we have silently assumed that `#` "does the right
+thing", i.e. that the types are well-formed and we can collapse a type
+alias with a `#` projection, thereby giving us a form of beta
+reduction.
+
+In Scala 2.x, this would not work, because `T#X` means `x.X forSome { val x: T }`.
+Hence, two occurrences of `Rep[Int]` say, would not be recognized to be equal because the
+existential would be opened each time afresh.
+
+In pre-existentials Scala, this would not have worked either. There, `T#X` was a fundamental
+type constructor, but was restricted to alias types or classes for both `T` and `X`.
+Roughly, `#` was meant to encode Java's inner classes. In Java, given the classes
+
+    class Outer { class Inner }
+    class Sub1 extends Outer
+    class Sub2 extends Outer
+
+The types `Outer#Inner`, `Sub1#Inner` and `Sub2#Inner` would all exist and be
+regarded as equal to each other. But if `Outer` had abstract type members this would
+not work, since that type member could be instantiated differently in `Sub1` and `Sub2`.
+Assuming that `Sub1#Inner = Sub2#Inner` could then lead to a soundness hole. To avoid soundness
+problems, the types in `X#Y` were restricted so that `Y` was (an alias of) a class type and
+`X` was (an alias of) a class type with no abstract type members.
+
+I believe we can drop this restriction and allow arbitrary type projects `X#Y` if we
+are more careful with the subtyping rules. Specifically:
+
+    A # X  <:  B # X
+
+if either `A = B`, or the following three conditions hold:
+
+  1. `X` is (an alias of) a class type,
+  2. `B` is (an alias of) a class type without abstract type members.
+  3. `A <: B`.
+
+In essence, we allow abstract types `X`, `Y` in a project `X#Y` but we prevent in this
+case hiding conflicting type information in a subtype widening.
+
+It would be good to study these rules formally, trying to verify their soundness.
+
+
+
+
+
+
+
+

From 926b5d911e230b5cbfd78755f872d742a0f4be61 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 29 May 2014 18:55:01 +0200
Subject: [PATCH 2/4] Fixed typos

---
 docs/HigherKinded-v2.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/docs/HigherKinded-v2.md b/docs/HigherKinded-v2.md
index 1d29b35ea31b..5822171e2106 100644
--- a/docs/HigherKinded-v2.md
+++ b/docs/HigherKinded-v2.md
@@ -69,7 +69,7 @@ is equivalent to
     Map { type Map$K <: AnyRef; type Map$V = Int }
 
 
-Type parameters in the Encodings
+Type parameters in the encodings
 --------------------------------
 
 The notion of type parameters makes sense even for encoded types,
@@ -191,7 +191,7 @@ We expand this to
     type Rep <: Lambda1
 
 The type parameters of `Rep` are the type parameters of its upper bound, so
-`Rep` is a uniary type constructor.
+`Rep` is a unary type constructor.
 
 More generally, a higher-kinded type declaration
 
@@ -217,8 +217,8 @@ would expand to
     Rep { type Arg1 = String } # Apply
 
 If we instantiate the higher-kinded type with a concrete type constructor (i.e. a parameterized
-trait or class, we have to do one extra adaptation to make it work. The parameterized trait
-or class has to be eta-expansed so that it comforms to the `Lambda` bound. For instance,
+trait or class), we have to do one extra adaptation to make it work. The parameterized trait
+or class has to be eta-expanded so that it comforms to the `Lambda` bound. For instance,
 
     type Rep = Set
 
@@ -296,7 +296,7 @@ Roughly, `#` was meant to encode Java's inner classes. In Java, given the classe
 
 The types `Outer#Inner`, `Sub1#Inner` and `Sub2#Inner` would all exist and be
 regarded as equal to each other. But if `Outer` had abstract type members this would
-not work, since that type member could be instantiated differently in `Sub1` and `Sub2`.
+not work, since an abstract type member could be instantiated differently in `Sub1` and `Sub2`.
 Assuming that `Sub1#Inner = Sub2#Inner` could then lead to a soundness hole. To avoid soundness
 problems, the types in `X#Y` were restricted so that `Y` was (an alias of) a class type and
 `X` was (an alias of) a class type with no abstract type members.
@@ -306,13 +306,13 @@ are more careful with the subtyping rules. Specifically:
 
     A # X  <:  B # X
 
-if either `A = B`, or the following three conditions hold:
+if either `A =:= B` (i.e. `A <: B` and `B <: A`), or the following three conditions hold:
 
   1. `X` is (an alias of) a class type,
   2. `B` is (an alias of) a class type without abstract type members.
   3. `A <: B`.
 
-In essence, we allow abstract types `X`, `Y` in a project `X#Y` but we prevent in this
+In essence, we allow abstract types `X`, `Y` in a projection `X#Y` but we prevent in this
 case hiding conflicting type information in a subtype widening.
 
 It would be good to study these rules formally, trying to verify their soundness.

From 41e9201d5afe4c15e0020dd9930a31fe87a5183d Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 30 May 2014 14:20:09 +0200
Subject: [PATCH 3/4] fixed typos

---
 docs/HigherKinded-v2.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/docs/HigherKinded-v2.md b/docs/HigherKinded-v2.md
index 5822171e2106..b116bd04ac51 100644
--- a/docs/HigherKinded-v2.md
+++ b/docs/HigherKinded-v2.md
@@ -102,10 +102,10 @@ Modelling polymorphic type declarations
 ---------------------------------------
 
 The partial application scheme gives us a new -- and quite elegant --
-way to do higher-kinded types. But how do we interprete the
+way to do certain higher-kinded types. But how do we interprete the
 poymorphic types that exist in current Scala?
 
-More concretely, current Scala allows us to write parameterize type
+More concretely, current Scala allows us to write parameterized type
 definitions, abstract types, and type parameters. In the new scheme,
 only classes (and traits) can have parameters and these are treated as
 equivalent to type members. Type aliases and abstract types do not
@@ -128,11 +128,11 @@ Here, `Lambda1` is a standard trait defined as follows:
 
     trait Lambda1[type Arg1, type Apply]
 
-According to our definitions of type parameters `Lambda1` has two type parameters
+According to our definitions of type parameters, `Lambda1` has two type parameters
 and `Pair` has one.
 
 There are `LambdaN` traits for higher arities as well. `Lambda` traits are special in that
-they influence how type applications are expanded: If standard type applicatuon `T[X1, ..., Xn]`
+they influence how type applications are expanded: If the standard type application `T[X1, ..., Xn]`
 leads to a subtype `S` of a type instance
 
       LambdaN { type Arg1 = T1; ...; type ArgN = Tn; type Apply ... }
@@ -145,7 +145,7 @@ For instance, the type instance `Pair[String]` would be expanded to
 
     Lambda1 { type Arg1 = String; type Apply = (Arg1, Arg1) } # Apply
 
-which turns out to be equal to `(String, String)`.
+which in turn equals `(String, String)`.
 
 2nd Example: Consider the two aliases
 

From 0d77aaeb2cfbb5b5f36f8895fce1db5cf73b451e Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 14 Jul 2014 17:46:14 +0200
Subject: [PATCH 4/4] Sync with implementation

Adapted docs so that they reflect what has been implemented.
---
 docs/HigherKinded-v2.md | 151 ++++++++++++++++++++++++++--------------
 1 file changed, 100 insertions(+), 51 deletions(-)

diff --git a/docs/HigherKinded-v2.md b/docs/HigherKinded-v2.md
index b116bd04ac51..3cb722e9848e 100644
--- a/docs/HigherKinded-v2.md
+++ b/docs/HigherKinded-v2.md
@@ -109,43 +109,98 @@ More concretely, current Scala allows us to write parameterized type
 definitions, abstract types, and type parameters. In the new scheme,
 only classes (and traits) can have parameters and these are treated as
 equivalent to type members. Type aliases and abstract types do not
-allow the definition of type members so we have to interprete
+allow the definition of parameterized types so we have to interprete
 polymorphic type aliases and abstract types specially.
 
-Modelling polymorphic type aliases
-----------------------------------
+Modelling polymorphic type aliases: simple case
+-----------------------------------------------
 
 A polymorphic type alias such as
 
-    type Pair[T] = (T, T)
+    type Pair[T] = Tuple2[T, T]
+
+where `Tuple2` is declared as
+
+    class Tuple2[T1, T2] ...
+
+is expanded to a monomorphic type alias like this:
+
+    type Pair = Tuple2 { type Tuple2$T2 = Tuple2$T1 }
+
+More generally, each type parameter of the left-hand side must
+appear as a type member of the right hand side type. Type members
+must appear in the same order as their corresponding type parameters.
+References to the type parameter are then translated to references to the
+type member. The type member itself is left uninstantiated.
+
+This technique can expand most polymorphic type aliases appearing
+in Scala codebases but not all of them. For instance, the following
+alias cannot be expanded, because the parameter type `T` is not a
+type member of the right-hand side `List[List[T]]`.
+
+    type List2[T] = List[List[T]]
+
+We scanned the Scala standard library for occurrences of polymorphic
+type aliases and determined that only two occurrences could not be expanded.
+In `io/Codec.scala`:
+
+    type Configure[T] = (T => T, Boolean)
+
+And in `collection/immutable/HashMap.scala`:
+
+    private type MergeFunction[A1, B1] = ((A1, B1), (A1, B1)) => (A1, B1)
+
+For these cases, we use a fall-back scheme that models a parameterized alias as a
+`Lambda` type.
+
+Modelling polymorphic type aliases: general case
+------------------------------------------------
+
+A polymorphic type alias such as
+
+    type List2D[T] = List[List[T]]
 
 is represented as a monomorphic type alias of a type lambda. Here's the expanded version of
 the definition above:
 
-    type Pair = Lambda1 { type Apply = (Arg1, Arg1) }
+    type List2D = Lambda$I { type Apply = List[List[$hkArg$0]] }
+
+Here, `Lambda$I` is a standard trait defined as follows:
 
-Here, `Lambda1` is a standard trait defined as follows:
+    trait Lambda$I[type $hkArg$0] { type +Apply }
 
-    trait Lambda1[type Arg1, type Apply]
+The `I` suffix of the `Lambda` trait indicates that it has one invariant type parameter (named $hkArg$0).
+Other suffixes are `P` for covariant type parameters, and `N` for contravariant type parameters. Lambda traits can
+have more than one type parameter. For instance, here is a trait with contravariant and covariant type parameters:
 
-According to our definitions of type parameters, `Lambda1` has two type parameters
-and `Pair` has one.
+    trait Lambda$NP[type -$hkArg$0, +$hkArg1] { type +Apply } extends Lambda$IP with Lambda$PI
 
-There are `LambdaN` traits for higher arities as well. `Lambda` traits are special in that
+Aside: the `+` prefix in front of `Apply` indicates that `Apply` is a covariant type field. Dotty
+admits variance annotations on type members).
+
+The definition of `Lambda$NP` shows that `Lambda` traits form a subtyping hierarchy: Traits which
+have covariant or contravariant type parameters are subtypes of traits which don't. The supertraits
+of `Lambda$NP` would themselves be written as follows.
+
+    trait Lambda$IP[type $hkArg$0, +$hkArg1] { type +Apply } extends Lambda$II
+    trait Lambda$NI[type -$hkArg$0, $hkArg1] { type +Apply } extends Lambda$II
+    trait Lambda$II[type -hkArg$0, $hkArg1] { type +Apply }
+
+`Lambda` traits are special in that
 they influence how type applications are expanded: If the standard type application `T[X1, ..., Xn]`
 leads to a subtype `S` of a type instance
 
-      LambdaN { type Arg1 = T1; ...; type ArgN = Tn; type Apply ... }
+    LambdaXYZ { type Arg1 = T1; ...; type ArgN = Tn; type Apply ... }
 
 where all argument fields `Arg1, ..., ArgN` are concretely defined
 and the definition of the `Apply` field may be either abstract or concrete, then the application
 is further expanded to `S # Apply`.
 
-For instance, the type instance `Pair[String]` would be expanded to
+For instance, the type instance `List2D[String]` would be expanded to
 
-    Lambda1 { type Arg1 = String; type Apply = (Arg1, Arg1) } # Apply
+    Lambda$I { type $hkArg$0 = String; type Apply = List[List[String]] } # Apply
 
-which in turn equals `(String, String)`.
+which in turn simplifies to `List[List[String]]`.
 
 2nd Example: Consider the two aliases
 
@@ -154,24 +209,24 @@ which in turn equals `(String, String)`.
 
 These expand as follows:
 
-    type RMap  = Lambda2 { self1 => type Apply = Map[self1.Arg2, self1.Arg1] }
-    type RRMap = Lambda2 { self2 => type Apply = RMap[self2.Arg2, self2.Arg1] }
+    type RMap  = Lambda$II { self1 => type Apply = Map[self1.$hkArg$1, self1.$hkArg$0] }
+    type RRMap = Lambda$II { self2 => type Apply = RMap[self2.$hkArg$1, self2.$hkArg$0] }
 
 Substituting the definition of `RMap` and expanding the type application gives:
 
-    type RRMap = Lambda2 { self2 => type Apply =
-                   Lambda2 { self1 => type Apply = Map[self1.Arg2, self1.Arg1] }
-                           { type Arg1 = self2.Arg2; type Arg2 = self2.Arg1 } # Apply }
+    type RRMap = Lambda$II { self2 => type Apply =
+                   Lambda$II { self1 => type Apply = Map[self1.$hkArg$1, self1.$hkArg$0] }
+                     { type $hkArg$0 = self2.$hkArg$1; type $hkArg$1 = self2.$hkArg$0 } # Apply }
 
-Substituting the definitions `self1.Arg{1,2}` gives:
+Substituting the definitions for `self1.$hkArg${1,2}` gives:
 
-    type RRMap = Lambda2 { self2 => type Apply =
-                   Lambda2 { self1 => type Apply = Map[self2.Arg1, self2.Arg2] }
-                           { type Arg1 = self2.Arg2; type Arg2 = self2.Arg1 } # Apply }
+    type RRMap = Lambda$II { self2 => type Apply =
+                   Lambda$II { self1 => type Apply = Map[self2.$hkArg$0, self2.$hkArg$1] }
+                      { type $hkArg$0 = self2.$hkArg$1; type $hkArg$1 = self2.$hkArg$0 } # Apply }
 
 Simplifiying the `# Apply` selection gives:
 
-    type RRMap = Lambda2 { self2 => type Apply = Map[self2.Arg1, self2.Arg2] }
+    type RRMap = Lambda$II { self2 => type Apply = Map[self2.$hkArg$0, self2.$hkArg$1] }
 
 This can be regarded as the eta-expanded version of `Map`. It has the same expansion as
 
@@ -188,25 +243,25 @@ Consider the higher-kinded type declaration
 
 We expand this to
 
-    type Rep <: Lambda1
+    type Rep <: Lambda$I
 
 The type parameters of `Rep` are the type parameters of its upper bound, so
 `Rep` is a unary type constructor.
 
 More generally, a higher-kinded type declaration
 
-     type T[X1 >: S1 <: U1, ..., XN >: S1 <: UN] >: SR <: UR
+     type T[v1 X1 >: S1 <: U1, ..., vn XN >: S1 <: UN] >: SR <: UR
 
 is encoded as
 
-     type T <: LambdaN { self =>
-       type Arg1 >: s(S1) <: s(U1)
+     type T <: LambdaV1...Vn { self =>
+       type v1 $hkArg$0 >: s(S1) <: s(U1)
        ...
-       type ArgN >: s(SN) <: s(UN)
+       type vn $hkArg$N >: s(SN) <: s(UN)
        type Apply >: s(SR) <: s(UR)
      }
 
-where `s` is the substitution `[XI := self.ArgI | I = 1,...,N]`.
+where `s` is the substitution `[XI := self.$hkArg$I | I = 1,...,N]`.
 
 If we instantiate `Rep` with a type argument, this is expanded as was explained before.
 
@@ -214,7 +269,7 @@ If we instantiate `Rep` with a type argument, this is expanded as was explained
 
 would expand to
 
-    Rep { type Arg1 = String } # Apply
+    Rep { type $hkArg$0 = String } # Apply
 
 If we instantiate the higher-kinded type with a concrete type constructor (i.e. a parameterized
 trait or class), we have to do one extra adaptation to make it work. The parameterized trait
@@ -224,7 +279,7 @@ or class has to be eta-expanded so that it comforms to the `Lambda` bound. For i
 
 would expand to
 
-    type Rep = Lambda1 { type Apply = Set[Arg1] }
+    type Rep = Lambda1 { type Apply = Set[$hkArg$0] }
 
 Or,
 
@@ -232,7 +287,7 @@ Or,
 
 would expand to
 
-    type Rep = Lambda1 { type Apply = Map[String, Arg1] }
+    type Rep = Lambda1 { type Apply = Map[String, $hkArg$0] }
 
 
 Full example
@@ -247,13 +302,13 @@ Consider the higher-kinded `Functor` type class
 This would be represented as follows:
 
     class Functor[F <: Lambda1] {
-       def map[A, B](f: A => B): F { type Arg1 = A } # Apply  =>  F { type Arg1 = B } # Apply
+       def map[A, B](f: A => B): F { type $hkArg$0 = A } # Apply  =>  F { type $hkArg$0 = B } # Apply
     }
 
 The type `Functor[List]` would be represented as follows
 
     Functor {
-       type F = Lambda1 { type Apply = List[Arg1] }
+       type F = Lambda1 { type Apply = List[$hkArg$0] }
     }
 
 Now, assume we have a value
@@ -262,13 +317,13 @@ Now, assume we have a value
 
 Then `ml.map` would have type
 
-    s(F { type Arg1 = A } # Apply  =>  F { type Arg1 = B } # Apply)
+    s(F { type $hkArg$0 = A } # Apply  =>  F { type $hkArg$0 = B } # Apply)
 
-where `s` is the substitution of `[F := Lambda1 { type Apply = List[Arg1] }]`.
+where `s` is the substitution of `[F := Lambda1 { type Apply = List[$hkArg$0] }]`.
 This gives:
 
-    Lambda1 { type Apply = List[Arg1] } { type Arg1 = A } # Apply
-     =>  Lambda1 { type Apply = List[Arg1] } { type Arg1 = B } # Apply
+    Lambda1 { type Apply = List[$hkArg$0] } { type $hkArg$0 = A } # Apply
+     =>  Lambda1 { type Apply = List[$hkArg$0] } { type $hkArg$0 = B } # Apply
 
 This type simplifies to:
 
@@ -301,21 +356,15 @@ Assuming that `Sub1#Inner = Sub2#Inner` could then lead to a soundness hole. To
 problems, the types in `X#Y` were restricted so that `Y` was (an alias of) a class type and
 `X` was (an alias of) a class type with no abstract type members.
 
-I believe we can drop this restriction and allow arbitrary type projects `X#Y` if we
-are more careful with the subtyping rules. Specifically:
-
-    A # X  <:  B # X
-
-if either `A =:= B` (i.e. `A <: B` and `B <: A`), or the following three conditions hold:
+I believe we can go back to regarding `T#X` as a fundamental type constructor, the way it
+was done in pre-existential Scala, but with the following relaxed restriction:
 
-  1. `X` is (an alias of) a class type,
-  2. `B` is (an alias of) a class type without abstract type members.
-  3. `A <: B`.
+    _In a type selection `T#x`, `T` is not allowed to have any abstract members different from `X`._
 
-In essence, we allow abstract types `X`, `Y` in a projection `X#Y` but we prevent in this
-case hiding conflicting type information in a subtype widening.
+This would typecheck the higher-kinded types examples, because they only project with `# Apply` once all
+`$hkArg$` type members are fully instantiated.
 
-It would be good to study these rules formally, trying to verify their soundness.
+It would be good to study this rule formally, trying to verify its soundness.