diff --git a/docs/HigherKinded-v2.md b/docs/HigherKinded-v2.md
new file mode 100644
index 000000000000..3cb722e9848e
--- /dev/null
+++ b/docs/HigherKinded-v2.md
@@ -0,0 +1,375 @@
+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 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 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 parameterized types so we have to interprete
+polymorphic type aliases and abstract types specially.
+
+Modelling polymorphic type aliases: simple case
+-----------------------------------------------
+
+A polymorphic type alias such as
+
+    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 List2D = Lambda$I { type Apply = List[List[$hkArg$0]] }
+
+Here, `Lambda$I` is a standard trait defined as follows:
+
+    trait Lambda$I[type $hkArg$0] { 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:
+
+    trait Lambda$NP[type -$hkArg$0, +$hkArg1] { type +Apply } extends Lambda$IP with Lambda$PI
+
+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
+
+    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 `List2D[String]` would be expanded to
+
+    Lambda$I { type $hkArg$0 = String; type Apply = List[List[String]] } # Apply
+
+which in turn simplifies to `List[List[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  = 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 = 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 for `self1.$hkArg${1,2}` gives:
+
+    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 = 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
+
+    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 <: 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[v1 X1 >: S1 <: U1, ..., vn XN >: S1 <: UN] >: SR <: UR
+
+is encoded as
+
+     type T <: LambdaV1...Vn { self =>
+       type v1 $hkArg$0 >: s(S1) <: s(U1)
+       ...
+       type vn $hkArg$N >: s(SN) <: s(UN)
+       type Apply >: s(SR) <: s(UR)
+     }
+
+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.
+
+    Rep[String]
+
+would expand to
+
+    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
+or class has to be eta-expanded so that it comforms to the `Lambda` bound. For instance,
+
+    type Rep = Set
+
+would expand to
+
+    type Rep = Lambda1 { type Apply = Set[$hkArg$0] }
+
+Or,
+
+    type Rep = Map[String, _]
+
+would expand to
+
+    type Rep = Lambda1 { type Apply = Map[String, $hkArg$0] }
+
+
+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 $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[$hkArg$0] }
+    }
+
+Now, assume we have a value
+
+    val ml: Functor[List]
+
+Then `ml.map` would have type
+
+    s(F { type $hkArg$0 = A } # Apply  =>  F { type $hkArg$0 = B } # Apply)
+
+where `s` is the substitution of `[F := Lambda1 { type Apply = List[$hkArg$0] }]`.
+This gives:
+
+    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:
+
+     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 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.
+
+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:
+
+    _In a type selection `T#x`, `T` is not allowed to have any abstract members different from `X`._
+
+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 this rule formally, trying to verify its soundness.
+
+
+
+
+
+
+
+