diff --git a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
index 17deaa5d88e2..0ae3a1ae93c8 100644
--- a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
+++ b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
@@ -123,6 +123,9 @@ class ScalaSettings extends Settings.SettingGroup {
   val YprofileRunGcBetweenPhases = PhasesSetting("-Yprofile-run-gc", "Run a GC between phases - this allows heap size to be accurate at the expense of more time. Specify a list of phases, or *", "_")
       //.withPostSetHook( _ => YprofileEnabled.value = true )
 
+  // Extremely experimental language features
+  val YkindPolymorphism = BooleanSetting("-Ykind-polymorphism", "Enable kind polymorphism (see http://dotty.epfl.ch/docs/reference/kind-polymorphism.html). Potentially unsound.")
+
   /** Area-specific debug output */
   val YexplainLowlevel = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.")
   val YnoDoubleBindings = BooleanSetting("-Yno-double-bindings", "Assert no namedtype is bound twice (should be enabled only if program is error-free).")
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 75a7b560945c..95c5aa94dd37 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -304,6 +304,16 @@ class Definitions {
     def ObjectMethods = List(Object_eq, Object_ne, Object_synchronized, Object_clone,
         Object_finalize, Object_notify, Object_notifyAll, Object_wait, Object_waitL, Object_waitLI)
 
+  lazy val AnyKindClass = {
+    val cls = ctx.newCompleteClassSymbol(ScalaPackageClass, tpnme.AnyKind, AbstractFinal | Permanent, Nil)
+    if (ctx.settings.YkindPolymorphism.value) {
+      // Enable kind-polymorphism by exposing scala.AnyKind
+      cls.entered
+    }
+    cls
+  }
+  def AnyKindType = AnyKindClass.typeRef
+
   /** Marker method to indicate an argument to a call-by-name parameter.
    *  Created by byNameClosures and elimByName, eliminated by Erasure,
    */
@@ -1158,6 +1168,7 @@ class Definitions {
   lazy val syntheticScalaClasses = List(
     AnyClass,
     AnyRefAlias,
+    AnyKindClass,
     RepeatedParamClass,
     ByNameParamClass2x,
     AnyValClass,
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index 1e64ff94d872..3ba81450301e 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -196,6 +196,7 @@ object StdNames {
     final val REIFY_TYPECREATOR_PREFIX: N       = "$typecreator"
 
     final val Any: N                 = "Any"
+    final val AnyKind: N             = "AnyKind"
     final val AnyVal: N              = "AnyVal"
     final val ExprApi: N             = "ExprApi"
     final val Mirror: N              = "Mirror"
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index d3db4845e8b3..c190dfb7262c 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -667,7 +667,7 @@ object SymDenotations {
 
     /** Is this symbol a class references to which that are supertypes of null? */
     final def isNullableClass(implicit ctx: Context): Boolean =
-      isClass && !isValueClass && !(this is ModuleClass) && symbol != defn.NothingClass
+      isClass && !isValueClass && !is(ModuleClass) && symbol != defn.NothingClass
 
     /** Is this definition accessible as a member of tree with type `pre`?
      *  @param pre          The type of the tree from which the selection is made
diff --git a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
index 0eefd44b109e..53b5bede376b 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -197,7 +197,7 @@ class TypeApplications(val self: Type) extends AnyVal {
 
   /** If `self` is a higher-kinded type, its type parameters, otherwise Nil */
   final def hkTypeParams(implicit ctx: Context): List[TypeParamInfo] =
-    if (isHK) typeParams else Nil
+    if (isLambdaSub) typeParams else Nil
 
   /** If `self` is a generic class, its type parameter symbols, otherwise Nil */
   final def typeParamSymbols(implicit ctx: Context): List[TypeSymbol] = typeParams match {
@@ -207,12 +207,19 @@ class TypeApplications(val self: Type) extends AnyVal {
     case _ => Nil
   }
 
-  /** Is self type higher-kinded (i.e. of kind != "*")? */
-  def isHK(implicit ctx: Context): Boolean = hkResult.exists
+  /** Is self type bounded by a type lambda or AnyKind? */
+  def isLambdaSub(implicit ctx: Context): Boolean = hkResult.exists
 
-  /** If self type is higher-kinded, its result type, otherwise NoType */
+  /** Is self type of kind != "*"? */
+  def hasHigherKind(implicit ctx: Context): Boolean =
+    typeParams.nonEmpty || self.isRef(defn.AnyKindClass)
+
+  /** If self type is higher-kinded, its result type, otherwise NoType.
+   *  Note: The hkResult of an any-kinded type is again AnyKind.
+   */
   def hkResult(implicit ctx: Context): Type = self.dealias match {
-    case self: TypeRef => self.info.hkResult
+    case self: TypeRef =>
+      if (self.symbol == defn.AnyKindClass) self else self.info.hkResult
     case self: AppliedType =>
       if (self.tycon.typeSymbol.isClass) NoType else self.superType.hkResult
     case self: HKTypeLambda => self.resultType
@@ -226,17 +233,24 @@ class TypeApplications(val self: Type) extends AnyVal {
     case _ => NoType
   }
 
-  /** Do self and other have the same kinds (not counting bounds and variances) */
+  /** Do self and other have the same kinds (not counting bounds and variances)?
+   *  Note: An any-kinded type "has the same kind" as any other type.
+   */
   def hasSameKindAs(other: Type)(implicit ctx: Context): Boolean = {
-    // println(i"check kind $self $other") // DEBUG
+    def isAnyKind(tp: Type) = tp match {
+      case tp: TypeRef => tp.symbol == defn.AnyKindClass
+      case _ => false
+    }
     val selfResult = self.hkResult
     val otherResult = other.hkResult
-    if (selfResult.exists)
-      otherResult.exists &&
-      selfResult.hasSameKindAs(otherResult) &&
-      self.typeParams.corresponds(other.typeParams)((sparam, oparam) =>
-        sparam.paramInfo.hasSameKindAs(oparam.paramInfo))
-    else !otherResult.exists
+    isAnyKind(selfResult) || isAnyKind(otherResult) ||
+    { if (selfResult.exists)
+        otherResult.exists &&
+        selfResult.hasSameKindAs(otherResult) &&
+        self.typeParams.corresponds(other.typeParams)((sparam, oparam) =>
+          sparam.paramInfo.hasSameKindAs(oparam.paramInfo))
+      else !otherResult.exists
+    }
   }
 
   /** Dealias type if it can be done without forcing the TypeRef's info */
@@ -256,9 +270,9 @@ class TypeApplications(val self: Type) extends AnyVal {
       //.ensuring(res => res.EtaReduce =:= self, s"res = $res, core = ${res.EtaReduce}, self = $self, hc = ${res.hashCode}")
   }
 
-  /** If self is not higher-kinded, eta expand it. */
-  def ensureHK(implicit ctx: Context): Type =
-    if (isHK) self else EtaExpansion(self)
+  /** If self is not lambda-bound, eta expand it. */
+  def ensureLambdaSub(implicit ctx: Context): Type =
+    if (isLambdaSub) self else EtaExpansion(self)
 
   /** Eta expand if `self` is a (non-lambda) class reference and `bound` is a higher-kinded type */
   def EtaExpandIfHK(bound: Type)(implicit ctx: Context): Type = {
@@ -355,7 +369,9 @@ class TypeApplications(val self: Type) extends AnyVal {
                 case _ => false
               }
             }
-            if ((dealiased eq stripped) || followAlias) dealiased.instantiate(args)
+            if ((dealiased eq stripped) || followAlias)
+              try dealiased.instantiate(args)
+              catch { case ex: IndexOutOfBoundsException => AppliedType(self, args) }
             else AppliedType(self, args)
           }
           else dealiased.resType match {
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 2611d96df182..e241a32e6a50 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -48,16 +48,22 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
   private[this] var totalCount = 0
 
   private[this] var myAnyClass: ClassSymbol = null
+  private[this] var myAnyKindClass: ClassSymbol = null
   private[this] var myNothingClass: ClassSymbol = null
   private[this] var myNullClass: ClassSymbol = null
   private[this] var myObjectClass: ClassSymbol = null
   private[this] var myAnyType: TypeRef = null
+  private[this] var myAnyKindType: TypeRef = null
   private[this] var myNothingType: TypeRef = null
 
   def AnyClass = {
     if (myAnyClass == null) myAnyClass = defn.AnyClass
     myAnyClass
   }
+  def AnyKindClass = {
+    if (myAnyKindClass == null) myAnyKindClass = defn.AnyKindClass
+    myAnyKindClass
+  }
   def NothingClass = {
     if (myNothingClass == null) myNothingClass = defn.NothingClass
     myNothingClass
@@ -74,6 +80,10 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     if (myAnyType == null) myAnyType = AnyClass.typeRef
     myAnyType
   }
+  def AnyKindType = {
+    if (myAnyKindType == null) myAnyKindType = AnyKindClass.typeRef
+    myAnyKindType
+  }
   def NothingType = {
     if (myNothingType == null) myNothingType = NothingClass.typeRef
     myNothingType
@@ -367,19 +377,25 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       case _ =>
         val cls2 = tp2.symbol
         if (cls2.isClass) {
-          if (cls2.typeParams.nonEmpty && tp1.isHK)
-            recur(tp1, EtaExpansion(cls2.typeRef))
-          else {
+          if (cls2.typeParams.isEmpty) {
+            if (cls2 eq AnyKindClass) return true
+            if (tp1.isRef(defn.NothingClass)) return true
+            if (tp1.isLambdaSub) return false
+              // Note: We would like to replace this by `if (tp1.hasHigherKind)`
+              // but right now we cannot since some parts of the standard library rely on the
+              // idiom that e.g. `List <: Any`. We have to bootstrap without scalac first.
             val base = tp1.baseType(cls2)
-            if (base.exists) {
-              if (cls2.is(JavaDefined))
-                // If `cls2` is parameterized, we are seeing a raw type, so we need to compare only the symbol
-                return base.typeSymbol == cls2
-              if (base ne tp1)
-                return isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow)
-            }
+            if (base.exists && base.ne(tp1))
+              return isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow)
             if (cls2 == defn.SingletonClass && tp1.isStable) return true
           }
+          else if (cls2.is(JavaDefined)) {
+            // If `cls2` is parameterized, we are seeing a raw type, so we need to compare only the symbol
+            val base = tp1.baseType(cls2)
+            if (base.typeSymbol == cls2) return true
+          }
+          else if (tp1.isLambdaSub && !tp1.isRef(defn.AnyKindClass))
+            return recur(tp1, EtaExpansion(cls2.typeRef))
         }
         fourthTry
     }
@@ -475,13 +491,11 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
               isSubType(tp1.resType, tp2.resType.subst(tp2, tp1))
             finally comparedTypeLambdas = saved
           case _ =>
-            if (tp1.isHK) {
-              val tparams1 = tp1.typeParams
+            val tparams1 = tp1.typeParams
+            if (tparams1.nonEmpty)
               return recur(
                 HKTypeLambda.fromParams(tparams1, tp1.appliedTo(tparams1.map(_.paramRef))),
-                tp2
-              )
-            }
+                tp2)
             else tp2 match {
               case EtaExpansion(tycon2) if tycon2.symbol.isClass =>
                 return recur(tp1, tycon2)
@@ -540,7 +554,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         def compareTypeBounds = tp1 match {
           case tp1 @ TypeBounds(lo1, hi1) =>
             ((lo2 eq NothingType) || isSubType(lo2, lo1)) &&
-            ((hi2 eq AnyType) || isSubType(hi1, hi2))
+            ((hi2 eq AnyType) && !hi1.isLambdaSub || (hi2 eq AnyKindType) || isSubType(hi1, hi2))
           case tp1: ClassInfo =>
             tp2 contains tp1
           case _ =>
@@ -610,7 +624,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
           case EtaExpansion(tycon1) => recur(tycon1, tp2)
           case _ => tp2 match {
             case tp2: HKTypeLambda => false // this case was covered in thirdTry
-            case _ => tp2.isHK && isSubType(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
+            case _ => tp2.isLambdaSub && isSubType(tp1.resultType, tp2.appliedTo(tp1.paramRefs))
           }
         }
         compareHKLambda
@@ -718,7 +732,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
                     tl => tp1base.tycon.appliedTo(args1.take(lengthDiff) ++
                             tparams1.indices.toList.map(tl.paramRefs(_))))
                 (ctx.mode.is(Mode.TypevarsMissContext) ||
-                  tryInstantiate(tycon2, tycon1.ensureHK)) &&
+                  tryInstantiate(tycon2, tycon1.ensureLambdaSub)) &&
                   recur(tp1, tycon1.appliedTo(args2))
               }
             }
@@ -801,7 +815,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         case param1: TypeParamRef =>
           def canInstantiate = tp2 match {
             case AppliedType(tycon2, args2) =>
-              tryInstantiate(param1, tycon2.ensureHK) && isSubArgs(args1, args2, tp1, tycon2.typeParams)
+              tryInstantiate(param1, tycon2.ensureLambdaSub) && isSubArgs(args1, args2, tp1, tycon2.typeParams)
             case _ =>
               false
           }
@@ -1216,8 +1230,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp2
     else if (!tp2.exists) tp1
-    else if ((tp1 isRef AnyClass) || (tp2 isRef NothingClass)) tp2
-    else if ((tp2 isRef AnyClass) || (tp1 isRef NothingClass)) tp1
+    else if ((tp1 isRef AnyClass) && !tp2.isLambdaSub || (tp1 isRef AnyKindClass) || (tp2 isRef NothingClass)) tp2
+    else if ((tp2 isRef AnyClass) && !tp1.isLambdaSub || (tp2 isRef AnyKindClass) || (tp1 isRef NothingClass)) tp1
     else tp2 match {  // normalize to disjunctive normal form if possible.
       case OrType(tp21, tp22) =>
         tp1 & tp21 | tp1 & tp22
@@ -1265,8 +1279,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp1
     else if (!tp2.exists) tp2
-    else if ((tp1 isRef AnyClass) || (tp2 isRef NothingClass)) tp1
-    else if ((tp2 isRef AnyClass) || (tp1 isRef NothingClass)) tp2
+    else if ((tp1 isRef AnyClass) || (tp1 isRef AnyKindClass) || (tp2 isRef NothingClass)) tp1
+    else if ((tp2 isRef AnyClass) || (tp2 isRef AnyKindClass) || (tp1 isRef NothingClass)) tp2
     else {
       val t1 = mergeIfSuper(tp1, tp2, canConstrain)
       if (t1.exists) t1
diff --git a/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala b/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala
index 088b121da737..42ee9cb34db2 100644
--- a/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala
@@ -1462,7 +1462,9 @@ object messages {
 
   case class MissingTypeParameterFor(tpe: Type)(implicit ctx: Context)
     extends Message(MissingTypeParameterForID) {
-    val msg = hl"missing type parameter for ${tpe}"
+    val msg =
+      if (tpe.derivesFrom(defn.AnyKindClass)) hl"${tpe} cannot be used as a value type"
+      else hl"missing type parameter for ${tpe}"
     val kind = "Syntax"
     val explanation = ""
   }
diff --git a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
index 312e2d4093db..0921bfcf58e8 100644
--- a/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
+++ b/compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala
@@ -357,7 +357,7 @@ private class ExtractAPICollector(implicit val ctx: Context) extends ThunkHolder
     // TODO: Never dealias. We currently have to dealias because
     // sbt main class discovery relies on the signature of the main
     // method being fully dealiased. See https://github.com/sbt/zinc/issues/102
-    val tp2 = if (!tp.isHK) tp.dealiasKeepAnnots else tp
+    val tp2 = if (!tp.isLambdaSub) tp.dealiasKeepAnnots else tp
     tp2 match {
       case NoPrefix | NoType =>
         Constants.emptyType
diff --git a/compiler/src/dotty/tools/dotc/typer/Checking.scala b/compiler/src/dotty/tools/dotc/typer/Checking.scala
index 0659b68666dd..698fdaff0c15 100644
--- a/compiler/src/dotty/tools/dotc/typer/Checking.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Checking.scala
@@ -45,7 +45,7 @@ object Checking {
    */
   def checkBounds(args: List[tpd.Tree], boundss: List[TypeBounds], instantiate: (Type, List[Type]) => Type)(implicit ctx: Context): Unit = {
     (args, boundss).zipped.foreach { (arg, bound) =>
-      if (!bound.isHK && arg.tpe.isHK)
+      if (!bound.isLambdaSub && arg.tpe.isLambdaSub)
         // see MissingTypeParameterFor
         ctx.error(ex"missing type parameter(s) for $arg", arg.pos)
     }
@@ -657,7 +657,7 @@ trait Checking {
 
   /** Check that `tpt` does not define a higher-kinded type */
   def checkSimpleKinded(tpt: Tree)(implicit ctx: Context): Tree =
-    if (tpt.tpe.isHK && !ctx.compilationUnit.isJava) {
+    if (tpt.tpe.isLambdaSub && !ctx.compilationUnit.isJava) {
         // be more lenient with missing type params in Java,
         // needed to make pos/java-interop/t1196 work.
       errorTree(tpt, MissingTypeParameterFor(tpt.tpe))
diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
index 0e283cd49e37..61502cddf482 100644
--- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -255,7 +255,7 @@ trait TypeAssigner {
    */
   def accessibleSelectionType(tree: untpd.RefTree, qual1: Tree)(implicit ctx: Context): Type = {
     var qualType = qual1.tpe.widenIfUnstable
-    if (qualType.isHK) qualType = errorType(em"$qualType takes type parameters", qual1.pos)
+    if (qualType.isLambdaSub) qualType = errorType(em"$qualType takes type parameters", qual1.pos)
     val ownType = selectionType(qualType, tree.name, tree.pos)
     ensureAccessible(ownType, qual1.isInstanceOf[Super], tree.pos)
   }
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 754ccddefed2..9a9c78130f65 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1233,7 +1233,24 @@ class Typer extends Namer
                 tparam.ensureCompleted() // This is needed to get the test `compileParSetSubset` to work
               case _ =>
             }
-          if (desugaredArg.isType) typed(desugaredArg, argPt)
+          if (desugaredArg.isType) {
+            var res = typed(desugaredArg, argPt)
+            arg match {
+              case TypeBoundsTree(EmptyTree, EmptyTree)
+              if tparam.paramInfo.isLambdaSub &&
+                 tpt1.tpe.typeParamSymbols.nonEmpty &&
+                 !ctx.mode.is(Mode.Pattern) =>
+                // An unbounded `_` automatically adapts to type parameter bounds. This means:
+                // If we have wildcard application C[_], where `C` is a class replace
+                // with C[_ >: L <: H] where `L` and `H` are the bounds of the corresponding
+                // type parameter in `C`, avoiding any referemces to parameters of `C`.
+                // The transform does not apply for patters, where empty bounds translate to
+                // wildcard identifiers `_` instead.
+                res = res.withType(avoid(tparam.paramInfo, tpt1.tpe.typeParamSymbols))
+              case _ =>
+            }
+            res
+          }
           else desugaredArg.withType(UnspecifiedErrorType)
         }
         args.zipWithConserve(tparams)(typedArg(_, _)).asInstanceOf[List[Tree]]
@@ -2147,7 +2164,7 @@ class Typer extends Namer
 
     def adaptNoArgsImplicitMethod(wtp: MethodType): Tree = {
       assert(wtp.isImplicitMethod)
-      val tvarsToInstantiate = tvarsInParams(tree, locked)
+      val tvarsToInstantiate = tvarsInParams(tree, locked).distinct
       wtp.paramInfos.foreach(instantiateSelected(_, tvarsToInstantiate))
       val constr = ctx.typerState.constraint
 
diff --git a/compiler/test-resources/repl/i2492 b/compiler/test-resources/repl/i2492
deleted file mode 100644
index b459d4feef43..000000000000
--- a/compiler/test-resources/repl/i2492
+++ /dev/null
@@ -1,6 +0,0 @@
-scala> class Map[K, V]
-// defined class Map
-scala> val s: Map {type Map$K = String; type Map$V = Int} = null
-1 | val s: Map {type Map$K = String; type Map$V = Int} = null
-  |        ^^^
-  |        missing type parameter for Map
diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala
index 1c5efcd57de7..5921665f2d7b 100644
--- a/compiler/test/dotty/tools/dotc/CompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala
@@ -102,6 +102,7 @@ class CompilationTests extends ParallelTesting {
     compileFilesInDir("tests/pos", defaultOptions) +
     compileFilesInDir("tests/pos-no-optimise", defaultOptions) +
     compileFilesInDir("tests/pos-deep-subtype", allowDeepSubtypes) +
+    compileFilesInDir("tests/pos-kind-polymorphism", defaultOptions and "-Ykind-polymorphism") +
     compileDir("tests/pos/i1137-1", defaultOptions and "-Yemit-tasty") +
     compileFile(
       // succeeds despite -Xfatal-warnings because of -nowarn
@@ -175,6 +176,7 @@ class CompilationTests extends ParallelTesting {
     compileFilesInDir("tests/neg", defaultOptions) +
     compileFilesInDir("tests/neg-tailcall", defaultOptions) +
     compileFilesInDir("tests/neg-no-optimise", defaultOptions) +
+    compileFilesInDir("tests/neg-kind-polymorphism", defaultOptions and "-Ykind-polymorphism") +
     compileFilesInDir("tests/neg-custom-args/fatal-warnings", defaultOptions.and("-Xfatal-warnings")) +
     compileFilesInDir("tests/neg-custom-args/allow-double-bindings", allowDoubleBindings) +
     compileFile("tests/neg-custom-args/i3246.scala", scala2Mode) +
diff --git a/docs/docs/reference/kind-polymorphism.md b/docs/docs/reference/kind-polymorphism.md
new file mode 100644
index 000000000000..0d520d764641
--- /dev/null
+++ b/docs/docs/reference/kind-polymorphism.md
@@ -0,0 +1,43 @@
+---
+layout: doc-page
+title: "Kind Polymorphism"
+---
+
+Normally type parameters in Scala are partitioned into _kinds_. First-level types are types of values. Higher-kinded types are type constructors
+such as `List` or `Map`. The kind of a type is indicated by the top type of which it is a subtype. Normal types are subtypes of `Any`,
+covariant single argument type constructors such as `List` are subtypes of `[+X] => Any`, and the `Map` type constructor is
+a subtype of `[X, +Y] => Any`.
+
+A type can be used only as prescribed by its kind. Subtypes of `Any` cannot be applied to type arguments whereas subtypes of `[X] => Any`
+_must_ be applied to a type argument, unless they are passed to type parameters of the same kind.
+
+Sometimes we would like to have type parameters that can have more than one kind, for instance to define an implicit
+value that works for parameters of any kind. This is now possible through a form of (_subtype_) kind polymorphism.
+Kind polymorphism relies on the special type `scala.AnyKind` that can be used as an upper bound of a type.
+
+```scala
+def f[T <: AnyKind] = ...
+```
+
+The actual type arguments of `f` can then be types of arbitrary kinds. So the following would all be legal:
+
+```scala
+f[Int]
+f[List]
+f[Map]
+f[[X] => String]
+```
+
+We call type parameters and abstract types with an `AnyKind` upper bound _any-kinded types_`.
+Since the actual kind of an any-kinded type is unknown, its usage must be heavily restricted: An any-kinded type
+can be neither the type of a value, nor can it be instantiated with type parameters. So about the only
+thing one can do with an any-kinded type is to pass it to another any-kinded type argument.
+Nevertheless, this is enough to achieve some interesting generalizations that work across kinds, typically
+through advanced uses of implicits.
+
+(todo: insert good concise example)
+
+Some technical details: `AnyKind` is a synthesized class just like `Any`, but without any members. It extends no other class.
+It is declared `abstract` and `final`, so it can be neither instantiated nor extended.
+
+`AnyKind` plays a special role in Scala's subtype system: It is a supertype of all other types no matter what their kind is. It is also assumed to be kind-compatible with all other types. Furthermore, `AnyKind` is treated as a higher-kinded type (so it cannot be used as a type of values), but at the same time it has no type parameters (so it cannot be instantiated).
diff --git a/docs/sidebar.yml b/docs/sidebar.yml
index 2aed6909d5ef..ca456b11af65 100644
--- a/docs/sidebar.yml
+++ b/docs/sidebar.yml
@@ -55,6 +55,8 @@ sidebar:
               url: docs/reference/named-typeargs.html
             - title: Erased Terms
               url: docs/reference/erased-terms.html
+            - title: Kind Polymorphism
+              url: docs/reference/kind-polymorphism.html
             - title: Local Optimisations
               url: docs/reference/optimisations.html
         - title: Changed Features
diff --git a/tests/neg-kind-polymorphism/anykind.scala b/tests/neg-kind-polymorphism/anykind.scala
new file mode 100644
index 000000000000..95f851fbb571
--- /dev/null
+++ b/tests/neg-kind-polymorphism/anykind.scala
@@ -0,0 +1,26 @@
+object AnyKinds {
+
+  val x: AnyKind = 2   // error
+
+  def f[X <: AnyKind]: Any = {
+    type T0 = AnyKind[String] // error
+    type T1 = X[Int]  // error
+    type T2 = X { type F = Int } // error
+    type T3 <: List & AnyKind // error // error
+    type T4 <: Int & AnyKind // error
+    val x: X = ???   // error
+  }
+
+  f[Int]      // OK
+  f[[X] => X] // OK
+  f[Nothing]  // OK
+
+  def g[X <: Any]: Any = {
+    f[X]      // OK
+  }
+  g[Int]      // OK
+  g[Nothing]  // OK
+
+  trait X[F[_] <: AnyKind] { type L = F[Int]; def a: L = ??? } // error: cannot be used as a value type
+
+}
\ No newline at end of file
diff --git a/tests/neg-kind-polymorphism/anykind1.scala b/tests/neg-kind-polymorphism/anykind1.scala
new file mode 100644
index 000000000000..2a75d1f42fae
--- /dev/null
+++ b/tests/neg-kind-polymorphism/anykind1.scala
@@ -0,0 +1,11 @@
+object Test {
+
+  // Checking edge cases that should not compile with kind-polymorphism
+  trait X[F[_] <: AnyKind] { def a: Int }
+  new X[Int] { }   // error
+  new X[Int] { }.a // error
+  new X[Either] { } // error
+  new X[Either] { }.a // error
+  new X[({ type l[X, Y] = X })#l] { } // error
+
+}
diff --git a/tests/neg-kind-polymorphism/anykind2.scala b/tests/neg-kind-polymorphism/anykind2.scala
new file mode 100644
index 000000000000..19972a686226
--- /dev/null
+++ b/tests/neg-kind-polymorphism/anykind2.scala
@@ -0,0 +1,21 @@
+object AnyKinds {
+
+  def f[X <: AnyKind]: Any = {
+    g[X]             // error
+    g[AnyKind]       // error
+  }
+
+  f[Int]      // OK
+  f[[X] => X] // OK
+  f[Nothing]  // OK
+
+  def g[X <: Any]: Any = {
+    f[X]      // OK
+  }
+  g[Int]      // OK
+  g[List]     // error
+  g[Nothing]  // OK
+
+  1.asInstanceOf[AnyKind] // error
+
+}
\ No newline at end of file
diff --git a/tests/neg-kind-polymorphism/anykind3.scala b/tests/neg-kind-polymorphism/anykind3.scala
new file mode 100644
index 000000000000..d374d2f841df
--- /dev/null
+++ b/tests/neg-kind-polymorphism/anykind3.scala
@@ -0,0 +1,63 @@
+
+object Test {
+
+  def f[X] = ()
+  f[List]
+
+  // Checking edge cases that should not compile with kind-polymorphism
+
+  trait X[A <: AnyKind, F[_ <: AnyKind]] { type B = F[A] }
+
+  val i0: X[Option, Double]#B = Some(5) // error
+
+  val i1: X[Option, List]#B = Some(5) // error
+
+  val i2: X[Option[Double], List]#B = Some(5) // error
+
+  val i3: X[Option[Double], ({ type l[X[_]] = X[Int] })#l]#B = Some(5) // error
+
+  val i4: X[Double, ({ type l[X[_]] = X[Int] })#l]#B = 5.0 // error
+
+  val i6: X[Either, ({ type l[X[_]] = X[Int] })#l]#B = Some(5) // error
+
+  val i7: X[Either, List]#B = Some(5) // error
+
+  trait Foo[A[_[_]]]
+  val i8: X[Foo, ({ type l[X[_]] = X[Int] })#l]#B = Some(5) // error
+
+  trait X2[A <: AnyKind, B <: AnyKind] { def run[F[_ <: AnyKind]]: F[A] => F[B] }
+
+  val x21 = {
+    new X2[Int, Int] { def run[F[_]]: F[Int] => F[Int] = identity[F[Int]] }
+      .asInstanceOf[X2[List, Option[Double]]].run[({ type l[X[_]] = X[Int] })#l]
+  }
+
+  val x22 = {
+    new X2[Int, Int] { def run[F[_]]: F[Int] => F[Int] = identity[F[Int]] }
+      .asInstanceOf[X2[List, Option[Double]]].run[List]
+  }
+
+  trait X3[A <: AnyKind, B <: AnyKind, C <: AnyKind] { def run[F[_ <: AnyKind, _ <: AnyKind]]: F[A, C] => F[B, C] }
+
+  val x31 = {
+    new X3[Int, Int, String] { def run[F[_, _]]: F[Int, String] => F[Int, String] = identity[F[Int, String]] }
+      .asInstanceOf[X3[Option[Double], List, String]].run[Map]
+  }
+  val x32 = {
+    new X3[Int, Int, String] { def run[F[_, _]]: F[Int, String] => F[Int, String] = identity[F[Int, String]] }
+      .asInstanceOf[X3[List, Option[Double], String]].run[Map]
+  }
+
+  trait X4[A <: AnyKind, B <: AnyKind, C] { def run[F[_ <: AnyKind, _]]: F[A, C] => F[B, C] }
+
+  trait Foo2[A]
+  trait Bar[A]
+  trait Bar2[A, B]
+
+  trait Toto[F[_], A]
+
+  val x41 = {
+    new X3[Foo2, Foo2, Int] { def run[F[_[_], A]]: F[Foo2, Int] => F[Foo2, Int] = identity[F[Foo2, Int]] }
+      .asInstanceOf[X3[Bar, Bar, Int]].run[Bar2]
+  }
+}
diff --git a/tests/neg-kind-polymorphism/anykind4.scala b/tests/neg-kind-polymorphism/anykind4.scala
new file mode 100644
index 000000000000..274c79f775c1
--- /dev/null
+++ b/tests/neg-kind-polymorphism/anykind4.scala
@@ -0,0 +1,14 @@
+
+object Test {
+
+  trait Foo[T <: AnyKind]
+
+  def foo[T <: AnyKind](implicit f: Foo[T]): f.type = f
+
+  implicit def c1[T]: Foo[T] = ???
+  implicit def c2[T[_]]: Foo[T] = ???
+
+  foo[List](c1) // error
+
+  foo[List](c2)
+}
\ No newline at end of file
diff --git a/tests/pos-kind-polymorphism/anykind.scala b/tests/pos-kind-polymorphism/anykind.scala
new file mode 100644
index 000000000000..a8f8e2839218
--- /dev/null
+++ b/tests/pos-kind-polymorphism/anykind.scala
@@ -0,0 +1,217 @@
+object Test {
+
+  case class Bar[A](a: A)
+  trait Toto[A, B]
+
+  ////////////////////////////////////////////////
+  // PoC of controlled KindPolymorphism in Scala
+  //
+  // The idea is NOT to provide universal kind-polymorphism that would be a bad idea anyway
+  // but to bring a "controlled" kind-polymorphism relying on accepted kinds defined by typeclass implicits
+  // Thus, kind-polymorphism is strictly scoped to your domain and is what you expect to be, nothing else.
+  //
+  // `Ykind-polymorphism` flag aims at deferring just a bit Scalac type inference when encountering AnyKind higher bounds
+  // without losing any strictness in the final typing.
+  // `<: AnyKind` type-bound is purely technicaland totally eliminated after erasure. There is not type associated to it.
+  //
+  // Here are code-samples that work now:
+  //    - basic kind polymorphism controlled by implicits
+  //    - Kindness proofs based on typeclasses (specially SameKind)
+  //    - Kind-Polymorphic list (on type & value) (2 different implementations)
+  //    - Some weird cases we don't want the compiler to authorize
+
+  ////////////////////////////////////////////////
+  // Basic Kind polymorphism sample
+  trait Foo[T <: AnyKind] { type Out ; def id(t: Out): Out = t }
+
+  object Foo {
+    implicit def foo0[T]: Foo[T] { type Out = T } = new Foo[T] { type Out = T }
+    implicit def foo1[T[_]]: Foo[T] { type Out = T[Any] } = new Foo[T] { type Out = T[Any] }
+    implicit def foo2[T[_, _]]: Foo[T] { type Out = T[Any, Any] } = new Foo[T] { type Out = T[Any, Any] }
+  }
+
+  def foo[T <: AnyKind](implicit f: Foo[T]): f.type = f
+  foo[Int].id(23)
+  foo[List].id(List[Any](1, 2, 3))
+  foo[Map].id(Map[Any, Any](1 -> "toto", 2 -> "tata", 3 -> "tutu"))
+
+  ////////////////////////////////////////////////
+  // Is a type M Kinded as you want ?
+  trait Kinded[M <: AnyKind] { type Out <: AnyKind }
+  object Kinded {
+    type Aux[M <: AnyKind, Out0 <: AnyKind] = Kinded[M] { type Out = Out0 }
+
+    implicit def kinded0[M]: Aux[M, M] = new Kinded[M] { type Out = M }
+    implicit def kinded1[M[_]]: Aux[M, M] = new Kinded[M] { type Out[t] = M[t] }
+    implicit def kinded2[M[_, _]]: Aux[M, M] = new Kinded[M] { type Out[t, u] = M[t, u] }
+  }
+
+  implicitly[Kinded.Aux[Int, Int]]
+  implicitly[Kinded.Aux[List, List]]
+  implicitly[Kinded.Aux[Map, Map]]
+
+  ////////////////////////////////////////////////
+  // Extract Kind from a type
+  trait Kinder[MA] { type M <: AnyKind; type Args <: HList }
+  object Kinder extends KinderLowerImplicits {
+    type Aux[MA, M0 <: AnyKind, Args0 <: HList] = Kinder[MA] { type M = M0; type Args = Args0 }
+
+    implicit def kinder2[M0[_, _], A0, B0]: Kinder.Aux[M0[A0, B0], M0, A0 :: B0 :: HNil] = new Kinder[M0[A0, B0]] { type M[t, u] = M0[t, u]; type Args = A0 :: B0 :: HNil }
+    implicit def kinder1[M0[_], A0]: Kinder.Aux[M0[A0], M0, A0 :: HNil] = new Kinder[M0[A0]] { type M[t] = M0[t]; type Args = A0 :: HNil }
+  }
+
+  trait KinderLowerImplicits {
+    implicit def kinder0[A]: Kinder.Aux[A, A, HNil] = new Kinder[A] { type M = A; type Args = HNil }
+  }
+
+  ////////////////////////////////////////////////
+  //IsoKindness Test
+  trait SameKind[M <: AnyKind, M2 <: AnyKind]
+  object SameKind {
+
+    implicit def sameKind0[A, B]: SameKind[A, B] = new {}
+    implicit def sameKind01[M1[_], M2[_]]: SameKind[M1, M2] = new {}
+    implicit def sameKind02[M1[_, _], M2[_, _]]: SameKind[M1, M2] = new {}
+  }
+
+  def sameKind[M1 <: AnyKind, M2 <: AnyKind](implicit sameKind: SameKind[M1, M2]) = sameKind
+
+  sameKind[Int, String]     // OK
+  sameKind[List, Bar]       // OK
+  sameKind[Map, Toto]       // OK
+
+  // sameKind[List, String] // KO
+  // sameKind[Map, List]    // KO
+  // sameKind[Map, Boolean] // KO
+
+
+
+  ////////////////////////////////////////////////
+  // Kind-Polymorphic List style
+
+  // Classic Heterogenous List used in KindPolymorphic List
+  sealed trait HList
+  final case class ::[+H, +T <: HList](head : H, tail : T) extends HList
+  sealed trait HNil extends HList
+  final case object HNil extends HNil
+
+  object New {
+    // The Kind Polymorphic List
+    sealed trait KPList
+
+    sealed trait KPNil extends KPList
+    case object KPNil extends KPNil {
+      def :::[H, M <: AnyKind, HL <: HList](h:H)(implicit kinder: Kinder.Aux[H, M, HL]) =
+        New.:::(h, KPNil)
+    }
+
+    sealed case class :::[H, T <: KPList, M <: AnyKind, HL0 <: HList](
+      head: H
+    , tail: T
+    )(implicit val kinder: Kinder.Aux[H, M, HL0]) extends KPList
+
+    final case class KPListOps[L <: KPList](l : L) {
+      def :::[H, M <: AnyKind, HL <: HList](h:H)(implicit kinder: Kinder.Aux[H, M, HL]) =
+        New.:::(h, l)
+    }
+
+    implicit def kplistOps[L <: KPList](l: L): KPListOps[L] = new KPListOps(l)
+
+    val kl = Bar(5) ::: "toto" ::: List(1, 2, 3) ::: Map("toto" -> 1L, "tata" -> 2L) ::: KPNil
+
+    val h: Bar[Int] = kl.head
+    val h2: String = kl.tail.head
+    val h3: List[Int] = kl.tail.tail.head
+    val h4: Map[String, Long] = kl.tail.tail.tail.head
+
+  }
+
+
+  ////////////////////////////////////////////////
+  // SPECIAL CASES
+  // def foo0[F <: AnyKind]: F = null.asInstanceOf[F]  // error: F cannot be used as a value type
+  // val i = foo0[Int]
+  // val li = foo0[List[Int]]
+  // foo0[List]                // KO -> neg
+  // val l = foo0[List]        // KO -> neg
+
+  // def foo1[F <: AnyKind, A <: AnyKind]: F[A] = ??? // KO
+
+  // def foo2: AnyKind = ??? // KO
+
+
+  // Older implementation Kind-Polymorphic List but I prefer the one above
+  object Old {
+
+    // The Kind Polymorphic List
+    sealed trait KPList
+
+    sealed trait KPNil extends KPList
+    case object KPNil extends KPNil
+
+    sealed trait :::[H <: AnyKind, T <: KPList] extends KPList
+    trait KPCons[M <: AnyKind, T <: KPList] extends :::[M, T]  {
+      type HL <: HList
+      type H
+      def head: H
+      def tail: T
+    }
+
+    object KPCons {
+      type Aux[M <: AnyKind, T <: KPList, H0, HL0 <: HList] = KPCons[M, T] { type H = H0; type HL = HL0 }
+      // Polymorphic
+      trait Apply[M <: AnyKind, A <: HList] { type Out }
+      object Apply {
+        type Aux[M <: AnyKind, A <: HList, Out0] = Apply[M, A] { type Out = Out0 }
+        implicit def apply0[M]: Aux[M, HNil, M] = new Apply[M, HNil] { type Out = M }
+        implicit def apply1[M[_], A]: Aux[M, A :: HNil, M[A]] = new Apply[M, A :: HNil] { type Out = M[A] }
+        implicit def apply2[M[_, _], A, B]: Aux[M, A :: B :: HNil, M[A, B]] = new Apply[M, A :: B :: HNil] { type Out = M[A, B] }
+      }
+
+      trait Unapply[M <: AnyKind, O] { type Out <: HList }
+      object Unapply {
+        type Aux[M <: AnyKind, O, Out0 <: HList] = Unapply[M, O] { type Out = Out0 }
+
+        implicit def unapply0[M]: Aux[M, M, HNil] = new Unapply[M, M] { type Out = HNil }
+        implicit def unapply1[M[_], A0]: Unapply.Aux[M, M[A0], A0 :: HNil] = new Unapply[M, M[A0]] { type Out = A0 :: HNil }
+        implicit def unapply2[M[_, _], A0, B0]: Aux[M, M[A0, B0], A0 :: B0 :: HNil] = new Unapply[M, M[A0, B0]] { type Out = A0 :: B0 :: HNil }
+      }
+
+      // the list builder
+      trait KPConsBuilder[M <: AnyKind] {
+        def apply[H0, HL0 <: HList, T <: KPList](head0: H0, tail0: T)(implicit unap: Unapply.Aux[M, H0, HL0]): KPCons.Aux[M, T, H0, HL0] = new KPCons[M, T] {
+          type HL = HL0
+          type H = H0
+          val head: H = head0
+          val tail: T = tail0
+        }
+      }
+
+      def apply[M <: AnyKind] = new KPConsBuilder[M] {}
+    }
+
+
+    // Let's create some kind-polymorphic list
+    val kl =
+      KPCons[Bar](
+        Bar(5)
+      , KPCons[String](
+          "toto"
+        , KPCons[List](
+            List(1, 2, 3)
+          , KPCons[Map](
+              Map("toto" -> 1L, "tata" -> 2L)
+            , KPNil
+            )
+          )
+        )
+      )
+
+    val h: Bar[Int] = kl.head
+    val h2: String = kl.tail.head
+    val h3: List[Int] = kl.tail.tail.head
+    val h4: Map[String, Long] = kl.tail.tail.tail.head
+
+  }
+
+}
\ No newline at end of file
diff --git a/tests/pos-kind-polymorphism/kindPolySemiGroup.scala b/tests/pos-kind-polymorphism/kindPolySemiGroup.scala
new file mode 100644
index 000000000000..8ee2db278874
--- /dev/null
+++ b/tests/pos-kind-polymorphism/kindPolySemiGroup.scala
@@ -0,0 +1,85 @@
+// Adapted from github:mandubian/kind-polymorphic-semigroup.scala
+sealed trait HList
+case class HCons[+HD, +TL](hd: HD, tl: TL) extends HList
+case object HNil extends HList
+
+object Test {
+
+  type HNil = HNil.type
+
+  // Kind Extractor
+  trait Kinder[MA] { type M <: AnyKind }
+  object Kinder extends KinderLowerImplicits {
+    type Aux[MA, M0 <: AnyKind] = Kinder[MA] { type M = M0 }
+
+    implicit def kinder1[M0[_], A0]: Kinder.Aux[M0[A0], M0] =
+      new Kinder[M0[A0]] { type M[t] = M0[t] }
+    implicit def kinder2[M0[_, _], A0, B0]: Kinder.Aux[M0[A0, B0], M0] =
+      new Kinder[M0[A0, B0]] { type M[t, u] = M0[t, u]; type Args = HCons[A0, HCons[B0, HNil]] }
+  }
+  trait KinderLowerImplicits {
+    implicit def kinder0[A]: Kinder.Aux[A, A] = new Kinder[A] { type M = A; type Args = HNil }
+  }
+
+  // Kind Polymorphic Semigroup using shapeless "Polymorphic function"-style
+  trait SemiGroup[M <: AnyKind] {
+    // Just a mirror type of itself to ensure the owning of AppendFunction...
+    type Self
+    // the function accepting only monomorphic type MA allowed by this scoped Semigroup AppendFunction
+    def append[MA](m1: MA, m2: MA)(implicit appender: SemiGroup.AppendFunction[Self, MA, M]) = appender(m1, m2)
+  }
+
+  object SemiGroup {
+    type Aux[M <: AnyKind, Self0] = SemiGroup[M] { type Self = Self0 }
+
+    // the monomorphic append function (yes we need to reify monomorphic types sometimes)
+    trait AppendFunction[P, FA, F <: AnyKind] {
+      def apply(m1: FA, m2: FA): FA
+    }
+  }
+
+  // Int SemiGroup instance
+  implicit object SemiGroupInt extends SemiGroup[Int] {
+    type Self = this.type
+    implicit val appender: SemiGroup.AppendFunction[Self, Int, Int]= new SemiGroup.AppendFunction[Self, Int, Int] {
+      def apply(m1: Int, m2: Int) = m1 + m2
+    }
+  }
+
+  // List SemiGroup instance
+  implicit object SemiGroupList extends SemiGroup[List] {
+    type Self = this.type
+    implicit def appender[A]: SemiGroup.AppendFunction[Self, List[A], List] = new  {
+      def apply(m1: List[A], m2: List[A]) = m1 ++ m2
+    }
+  }
+
+  // Map SemiGroup instance
+  implicit object SemiGroupMap extends SemiGroup[Map] {
+    type Self = this.type
+    implicit def appender[A, B]: SemiGroup.AppendFunction[Self, Map[A, B], Map] = new {
+      def apply(m1: Map[A, B], m2: Map[A, B]) = m1 ++ m2
+    }
+  }
+
+  // Searching a semigroup and using it
+  def semiGroup[M <: AnyKind](implicit sg: SemiGroup[M]): SemiGroup.Aux[M, sg.Self] = sg
+
+  semiGroup[Int].append(5, 8)
+  semiGroup[List].append(List(1), List(3))
+  semiGroup[Map].append(Map("toto" -> 1L), Map("tata" -> 3L))
+
+  // higher level append function
+  def append[MA, M <: AnyKind, Self](m1: MA, m2: MA)(
+    implicit kinder: Kinder.Aux[MA, M], semiGroup: SemiGroup.Aux[M, Self], appender: SemiGroup.AppendFunction[Self, MA, M]
+  ): MA = semiGroup.append(m1, m2)
+
+  import SemiGroupList.appender
+  import SemiGroupMap.appender
+
+  val r1: Int = append(5, 8)
+
+  // TODO: Figure igure out why `M` below cannot be inferred
+  val r2: List[Int] = append[M = List](List(1), List(3))
+  val r3: Map[String, Long] = append[M = Map](Map("toto" -> 1L), Map("tata" -> 3L))
+}
\ No newline at end of file
diff --git a/tests/pos/i4167/Test_2.scala b/tests/pos/i4167/Test_2.scala
new file mode 100644
index 000000000000..a0dcf504cf6b
--- /dev/null
+++ b/tests/pos/i4167/Test_2.scala
@@ -0,0 +1,6 @@
+package collection
+
+object Test {
+  type AnyConstr[X] = Any
+  val test: SeqOps[Char, AnyConstr, _] = null.asInstanceOf[StringOps]
+}
diff --git a/tests/pos/i4167/collections_1.scala b/tests/pos/i4167/collections_1.scala
new file mode 100644
index 000000000000..a8bc24d2bac7
--- /dev/null
+++ b/tests/pos/i4167/collections_1.scala
@@ -0,0 +1,11 @@
+package collection
+
+trait Seq[+A] extends SeqOps[A, Seq, Seq[A]]
+trait SeqOps[+A, +CC[_], +C] extends Any
+
+package immutable {
+  trait Seq[+A] extends collection.Seq[A] with SeqOps[A, Seq, Seq[A]]
+  trait SeqOps[+A, +CC[_], +C] extends collection.SeqOps[A, CC, C]
+}
+
+class StringOps extends collection.SeqOps[Char, immutable.Seq, String]
\ No newline at end of file