Merge pull request #1343 from dotty-staging/change-hk-direct2

Direct representation of higher-kinded types 

44 files changed, 404 insertions, 76 deletions

diff --git a/tests/neg/named-params.scala b/tests/disabled/neg/named-params.scala
index 5a2375b15..5a2375b15 100644
--- a/tests/neg/named-params.scala
+++ b/tests/disabled/neg/named-params.scala
diff --git a/tests/disabled/not-representable/pos/t2066.scala b/tests/disabled/not-representable/pos/t2066.scala
index 30cb99d45..d175769fa 100644
--- a/tests/disabled/not-representable/pos/t2066.scala
+++ b/tests/disabled/not-representable/pos/t2066.scala
@@ -3,7 +3,7 @@ trait A1 {
 }
 
 trait B1 extends A1 {
-  override def f[T[_]] = ()
+  override def f[T[+_]] = ()
 }
 
 
@@ -12,12 +12,12 @@ trait A2 {
 }
 
 trait B2 extends A2 {
-  override def f[T[_]] = ()
+  override def f[T[-_]] = ()
 }
 
 
 trait A3 {
-  def f[T[X[_]]] = ()
+  def f[T[X[+_]]] = ()
 }
 
 trait B3 extends A3 {
diff --git a/tests/pos/CollectionStrawMan3.scala b/tests/disabled/pos/CollectionStrawMan3.scala
index c21a73f00..c21a73f00 100644
--- a/tests/pos/CollectionStrawMan3.scala
+++ b/tests/disabled/pos/CollectionStrawMan3.scala
diff --git a/tests/pos/flowops.scala b/tests/disabled/pos/flowops.scala
index 6aead26be..6aead26be 100644
--- a/tests/pos/flowops.scala
+++ b/tests/disabled/pos/flowops.scala
diff --git a/tests/pos/flowops1.scala b/tests/disabled/pos/flowops1.scala
index 649a9b18c..649a9b18c 100644
--- a/tests/pos/flowops1.scala
+++ b/tests/disabled/pos/flowops1.scala
diff --git a/tests/pos/hk-named.scala b/tests/disabled/pos/hk-named.scala
index 5f2cb6c74..5f2cb6c74 100644
--- a/tests/pos/hk-named.scala
+++ b/tests/disabled/pos/hk-named.scala
diff --git a/tests/pos/named-params.scala b/tests/disabled/pos/named-params.scala
index 3fab24cd2..3fab24cd2 100644
--- a/tests/pos/named-params.scala
+++ b/tests/disabled/pos/named-params.scala
diff --git a/tests/neg/boundspropagation.scala b/tests/neg/boundspropagation.scala
index b545b09da..dd4ebf513 100644
--- a/tests/neg/boundspropagation.scala
+++ b/tests/neg/boundspropagation.scala
@@ -40,5 +40,5 @@ object test4 {
 }
 
 class Test5 {
-"": ({ type U = this.type })#U                        // error // error
+"": ({ type U = this.type })#U                        // error
 }
diff --git a/tests/neg/existentials.scala b/tests/neg/existentials.scala
new file mode 100644
index 000000000..4798504d9
--- /dev/null
+++ b/tests/neg/existentials.scala
@@ -0,0 +1,61 @@
+object TestList {
+
+  var x: ([X] -> List[List[X]])[_] = List(List(1)) // error: unreducible
+  var y: ([X] -> List[Seq[X]])[_] = List(List(1)) // error: unreducible
+
+  x = x
+  y = y
+  y = x
+
+  val h = x.head
+  val x1: List[_] = h
+
+  var z: List[_] = x
+
+}
+object TestSet {
+
+  var x: ([Y] -> Set[Set[Y]])[_] = Set(Set("a")) // error: unreducible
+  var y: ([Y] -> Set[Iterable[Y]])[_] = Set(Set("a")) // error: unreducible
+
+  x = x
+  y = y
+
+  val h = x.head
+  val h1: Set[_] = h
+
+  // val p = x.+ // infinite loop in implicit search
+
+  var z: Set[_] = x
+
+}
+class TestX {
+
+  class C[T](x: T) {
+    def get: T = x
+    def cmp: T => Boolean = (x == _)
+  }
+
+  val x: ([Y] -> C[C[Y]])[_] = new C(new C("a")) // error: unreducible
+
+  type CC[X] = C[C[X]]
+  val y: CC[_] = ??? // error: unreducible
+
+  type D[X] <: C[X]
+
+  type DD = [X] -> D[D[X]]
+  val z: DD[_] = ??? // error: unreducible
+
+  val g = x.get
+
+  val c = x.cmp
+}
+
+object Test6014 {
+  case class CC[T](key: T)
+  type Alias[T] = Seq[CC[T]]
+
+  def f(xs: Seq[CC[_]]) = xs map { case CC(x) => CC(x) }    // ok
+  def g(xs: Alias[_])   = xs map { case CC(x) => CC(x) }    // error: unreducible application
+}
+
diff --git a/tests/neg/hk-bounds.scala b/tests/neg/hk-bounds.scala
new file mode 100644
index 000000000..db6712d72
--- /dev/null
+++ b/tests/neg/hk-bounds.scala
@@ -0,0 +1,31 @@
+class Foo[A]
+class Bar[B]
+class Baz[C] extends Bar[C]
+
+object Test1 {
+  type Alias[F[X] <: Foo[X]] = F[Int]
+
+  val x: Alias[Bar] = new Bar[Int] // error: Type argument [X0] -> Bar[X0] does not conform to upper bound [X0] -> Foo[X0]
+
+  def foo[F[X] <: Foo[X]] = ()
+  foo[Bar] // error: Type argument [X0] -> Bar[X0] does not conform to upper bound [X0] -> Foo[X0]
+
+  def bar[B[X] >: Bar[X]] = ()
+  bar[Bar] // ok
+  bar[Baz] // // error: Type argument [X0] -> Baz[X0] does not conform to lower bound [X0] -> Bar[X0]
+  bar[Foo] // error: Type argument [X0] -> Foo[X0] does not conform to lower bound [X0] -> Bar[X0]
+
+  def baz[B[X] >: Baz[X]] = ()
+  baz[Bar] //ok
+  baz[Baz] //ok
+  baz[Foo] // error: Type argument [X0] -> Foo[X0] does not conform to lower bound [X0] -> Baz[X0]
+
+}
+object Test2 {
+  type Alias[F[X] <: Foo[X]] = F[Int]
+
+  def foo[M[_[_]], A[_]]: M[A] = null.asInstanceOf[M[A]]
+
+  val x = foo[Alias, Bar] // error: Type argument Test2.Alias does not conform to upper bound [X0 <: [X0] -> Any] -> Any
+
+}
diff --git a/tests/neg/hk-variance.scala b/tests/neg/hk-variance.scala
new file mode 100644
index 000000000..fec5cc366
--- /dev/null
+++ b/tests/neg/hk-variance.scala
@@ -0,0 +1,11 @@
+object Test {
+
+  def f[C[+X]] = ()
+
+  class D[X] {}
+
+  f[D] // error
+
+  def g[E[-Y]] = f[E] // error
+
+}
diff --git a/tests/neg/hklower.scala b/tests/neg/hklower.scala
deleted file mode 100644
index 5c1ba27ba..000000000
--- a/tests/neg/hklower.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-class Test { // error conflicting bounds
-
-  type T[X] // OK
-  type U[X] = T[X] // OK
-
-  type V[X] >: T[X] // error
-  type W[X] >: T[X] <: T[X] // error
-
-  def f[C[X] >: T[X]]() = ??? // error
-
-}
diff --git a/tests/neg/hklower2.scala b/tests/neg/hklower2.scala
new file mode 100644
index 000000000..8268bf09f
--- /dev/null
+++ b/tests/neg/hklower2.scala
@@ -0,0 +1,4 @@
+class Test { // error: conflicting bounds
+  trait T[X]
+  type Z[X] >: String <: T[X]
+}
diff --git a/tests/neg/i39.scala b/tests/neg/i39.scala
index df53d9816..8a13a7d06 100644
--- a/tests/neg/i39.scala
+++ b/tests/neg/i39.scala
@@ -1,7 +1,7 @@
 object i39neg {
 
   trait B {
-    type D <: { type T }           // error
+    type D <: { type T }
     def d: D
   }
 
diff --git a/tests/neg/i50-volatile.scala b/tests/neg/i50-volatile.scala
index f6fa3466d..fcfc9592b 100644
--- a/tests/neg/i50-volatile.scala
+++ b/tests/neg/i50-volatile.scala
@@ -3,10 +3,10 @@ class Test {
     class Inner
   }
   type A <: Base {
-    type X = String                                     // error
+    type X = String                                     // old-error
   }
   type B <: {
-    type X = Int                                        // error
+    type X = Int                                        // old-error
   }
   lazy val o: A & B = ???
 
diff --git a/tests/neg/kinds.scala b/tests/neg/kinds.scala
new file mode 100644
index 000000000..312c5d45e
--- /dev/null
+++ b/tests/neg/kinds.scala
@@ -0,0 +1,18 @@
+object Test {
+
+  class C[T]
+  class C2[T[X]]
+
+  class B
+
+  val x: C[C] = ??? // error: missing type parameter(s)
+  val y: C2[C] = ???
+
+  def f[T] = ???
+
+  def f2[T[X]] = ???
+
+  f[C] // error: missing type parameter(s)
+  f2[C]
+
+}
diff --git a/tests/neg/ski.scala b/tests/neg/ski.scala
index b192dc9e2..90a43039a 100644
--- a/tests/neg/ski.scala
+++ b/tests/neg/ski.scala
@@ -17,8 +17,8 @@ trait S2[x <: Term, y <: Term] extends Term {
   type eval = S2[x, y]
 }
 trait S3[x <: Term, y <: Term, z <: Term] extends Term {
-  type ap[v <: Term] = eval#ap[v] // error
-  type eval = x#ap[z]#ap[y#ap[z]]#eval // error // error
+  type ap[v <: Term] = eval#ap[v] // error: not a legal path
+  type eval = x#ap[z]#ap[y#ap[z]]#eval // error: not a legal path // error: not a legal path
 }
 
 // The K combinator
@@ -31,8 +31,8 @@ trait K1[x <: Term] extends Term {
   type eval = K1[x]
 }
 trait K2[x <: Term, y <: Term] extends Term {
-  type ap[z <: Term] = eval#ap[z] // error
-  type eval = x#eval // error
+  type ap[z <: Term] = eval#ap[z] // error: not a legal path
+  type eval = x#eval // error: not a legal path
 }
 
 // The I combinator
@@ -41,8 +41,8 @@ trait I extends Term {
   type eval = I
 }
 trait I1[x <: Term] extends Term {
-  type ap[y <: Term] = eval#ap[y] // error
-  type eval = x#eval // error
+  type ap[y <: Term] = eval#ap[y] // error: not a legal path
+  type eval = x#eval // error: not a legal path
 }
 
 // Constants
@@ -64,9 +64,10 @@ case class Equals[A >: B <:B , B]()
 
 object Test {
   type T1 = Equals[Int, Int]     // compiles fine
-  type T2 = Equals[String, Int]  // error
+  type T2 = Equals[String, Int]  // error: Type argument String does not conform to upper bound Int
+
   type T3 = Equals[I#ap[c]#eval, c]
-  type T3a = Equals[I#ap[c]#eval, d] // error
+  type T3a = Equals[I#ap[c]#eval, d] // error: Type argument I1[c]#eval does not conform to upper bound d
 
   // Ic -> c
   type T4 = Equals[I#ap[c]#eval, c]
@@ -106,11 +107,11 @@ object Test {
     type eval = A0
   }
   trait A1 extends Term {
-    type ap[x <: Term] = x#ap[A0]#eval // error
+    type ap[x <: Term] = x#ap[A0]#eval // error: not a legal path
     type eval = A1
   }
   trait A2 extends Term {
-    type ap[x <: Term] = x#ap[A1]#eval // error
+    type ap[x <: Term] = x#ap[A1]#eval // error: not a legal path
     type eval = A2
   }
 
@@ -126,7 +127,7 @@ object Test {
   type T15 = Equals[NN3#eval, c]
 
   trait An extends Term {
-    type ap[x <: Term] = x#ap[An]#eval // error
+    type ap[x <: Term] = x#ap[An]#eval // error: not a legal path
     type eval = An
   }
 
diff --git a/tests/neg/subtyping.scala b/tests/neg/subtyping.scala
index 27cc0568e..351fa0ecd 100644
--- a/tests/neg/subtyping.scala
+++ b/tests/neg/subtyping.scala
@@ -8,7 +8,7 @@ object Test {
     implicitly[B#X <:< A#X] // error: no implicit argument
   }
   def test2(): Unit = {
-    val a : { type T; type U } = ??? // error // error
+    val a : { type T; type U } = ???
     implicitly[a.T <:< a.U] // error: no implicit argument
   }
 }
diff --git a/tests/neg/t2994.scala b/tests/neg/t2994.scala
index 23a3b6a8b..e19397a3d 100644
--- a/tests/neg/t2994.scala
+++ b/tests/neg/t2994.scala
@@ -7,7 +7,7 @@ object Naturals {
     type a[s[_ <: NAT] <: NAT, z <: NAT] = z
   }
   final class SUCC[n <: NAT] extends NAT {
-    type a[s[_ <: NAT] <: NAT, z <: NAT] = s[n#a[s, z]] // old-error: not a legal path
+    type a[s[_ <: NAT] <: NAT, z <: NAT] = s[n#a[s, z]] // error: not a legal path
   }
   type _0 = ZERO
   type _1 = SUCC[_0]
@@ -20,8 +20,8 @@ object Naturals {
 
   // crashes scala-2.8.0 beta1
   trait MUL[n <: NAT, m <: NAT] extends NAT {
-    trait curry[n[_[_], _], s[_]] { type f[z <: NAT] = n[s, z] } // can't do double param lists: // error: `]' expected but `[` found. // error: wrong number of type arguments
-    type a[s[_ <: NAT] <: NAT, z <: NAT] = n#a[curry[m#a, s]#f, z] // old-error: not a legal path // old-error: not a legal path
+    trait curry[n[_[_], _], s[_]] { type f[z <: NAT] = n[s, z] }
+    type a[s[_ <: NAT] <: NAT, z <: NAT] = n#a[curry[m#a, s]#f, z] // error: not a legal path // error: not a legal path // error: arg does not conform to bound // error: arg does not conform to bound
   }
 
 }
diff --git a/tests/neg/t7278.scala b/tests/neg/t7278.scala
index 7aafbb76f..643a3c858 100644
--- a/tests/neg/t7278.scala
+++ b/tests/neg/t7278.scala
@@ -13,8 +13,8 @@ object Test {
 
   def fail1(): Unit = {
     val b = new B
-    var x1: EE[A] = null
-    var x2: EE[B] = new b.E // old-error: found: B#E, required: A#E
+    var x1: EE[A] = null // error: Type argument A does not conform to upper bound EC
+    var x2: EE[B] = new b.E // error: Type argument B does not conform to upper bound EC
 //    x1 = x2  // gives a prior type error: B#E, required: A#E, masked to get at the real thing.
   }
 
@@ -27,8 +27,8 @@ object Test {
   }
 */
   def fail3(): Unit = {
-    var x1: EE[C] = 5
-    var x2: EE[C & D] = ""
+    var x1: EE[C] = 5       // error: Type argument C does not conform to upper bound EC
+    var x2: EE[C & D] = ""  // error: Type argument C & D does not conform to upper bound EC
     x1 = x2
   }
 
diff --git a/tests/neg/zoo.scala b/tests/neg/zoo.scala
index 3d9b77b72..19efcc1d7 100644
--- a/tests/neg/zoo.scala
+++ b/tests/neg/zoo.scala
@@ -1,23 +1,23 @@
 object Test {
 type Meat = {
-  type IsMeat = Any            // error
+  type IsMeat = Any
 }
 type Grass = {
-  type IsGrass = Any           // error
+  type IsGrass = Any
 }
 type Animal = {
-  type Food                    // error
+  type Food
   def eats(food: Food): Unit   // error
   def gets: Food               // error
 }
 type Cow = {
-  type IsMeat = Any            // error
-  type Food <: Grass           // error
+  type IsMeat = Any
+  type Food <: Grass
   def eats(food: Grass): Unit  // error
   def gets: Grass              // error
 }
 type Lion = {
-  type Food = Meat             // error
+  type Food = Meat
   def eats(food: Meat): Unit   // error
   def gets: Meat               // error
 }
diff --git a/tests/pos/apply-equiv.scala b/tests/pending/pos/apply-equiv.scala
index f53b8b5ab..f53b8b5ab 100644
--- a/tests/pos/apply-equiv.scala
+++ b/tests/pending/pos/apply-equiv.scala
diff --git a/tests/pickling/i94-nada.scala b/tests/pickling/i94-nada.scala
index ce8dc98ad..cf39ee2ae 100644
--- a/tests/pickling/i94-nada.scala
+++ b/tests/pickling/i94-nada.scala
@@ -27,7 +27,7 @@ trait Test1 {
   case class Left[A,B](x: A) extends Either[A,B] with Monad[A]
   case class Right[A,B](x: B) extends Either[A,B] with Monad[B]
   def flatMap[X,Y,M[X]<:Monad[X]](m: M[X], f: X => M[Y]): M[Y] = f(m.x)
-  println(flatMap(Left(1), {x: Int => Left(x)}))
+  println(flatMap(Right(1), {x: Int => Right(x)}))
 }
 trait Test2 {
   trait Monad[X] {
@@ -37,7 +37,7 @@ trait Test2 {
   case class Left[A,B](x: A) extends Either[A,B] with Monad[A]
   case class Right[A,B](x: B) extends Either[A,B] with Monad[B]
   def flatMap[X,Y,M[X]](m: M[X], f: X => M[Y]): M[Y]
-  println(flatMap(Left(1), {x: Int => Left(x)}))
+  println(flatMap(Right(1), {x: Int => Right(x)}))
 }
 trait Test3 {
   def flatMap[X,Y,M[X]](m: M[X], f: X => M[Y]): M[Y]
diff --git a/tests/pos/GenTraversableFactory.scala b/tests/pos-scala2/GenTraversableFactory.scala
index 2f93ab27b..2f93ab27b 100644
--- a/tests/pos/GenTraversableFactory.scala
+++ b/tests/pos-scala2/GenTraversableFactory.scala
diff --git a/tests/pos-scala2/t2994.scala b/tests/pos-scala2/t2994.scala
index c7421c42a..f3009b12f 100644
--- a/tests/pos-scala2/t2994.scala
+++ b/tests/pos-scala2/t2994.scala
@@ -20,7 +20,7 @@ object Naturals {
 
   // crashes scala-2.8.0 beta1
   trait MUL[n <: NAT, m <: NAT] extends NAT {
-    trait curry[n[_, _], s[_]] { type f[z <: NAT] = n[s, z] }
+    trait curry[n[_[_], _], s[_]] { type f[z <: NAT] = n[s, z] }
     type a[s[_ <: NAT] <: NAT, z <: NAT] = n#a[curry[m#a, s]#f, z]
   }
 
diff --git a/tests/pos/t6014.scala b/tests/pos-scala2/t6014.scala
index 26e258a27..02535f377 100644
--- a/tests/pos/t6014.scala
+++ b/tests/pos-scala2/t6014.scala
@@ -3,7 +3,7 @@ object Test {
   type Alias[T] = Seq[CC[T]]
 
   def f(xs: Seq[CC[_]]) = xs map { case CC(x) => CC(x) }    // ok
-  def g(xs: Alias[_])   = xs map { case CC(x) => CC(x) }    // fails
+  def g(xs: Alias[_])   = xs map { case CC(x) => CC(x) }    // migration warning: unreducible application
   // ./a.scala:11: error: missing parameter type for expanded function
   // The argument types of an anonymous function must be fully known. (SLS 8.5)
   // Expected type was: ?
diff --git a/tests/pos/hk-subtyping.scala b/tests/pos/hk-subtyping.scala
new file mode 100644
index 000000000..a004c2618
--- /dev/null
+++ b/tests/pos/hk-subtyping.scala
@@ -0,0 +1,13 @@
+object Test {
+
+  def compare[S <: T, T] = ()
+
+  compare[Int, Int]
+  compare[Int, Any]
+
+  def f[C <: List] = {
+    compare[C[Int], List[Int]]
+  }
+
+
+}
diff --git a/tests/pos/hklower.scala b/tests/pos/hklower.scala
new file mode 100644
index 000000000..90aa343ba
--- /dev/null
+++ b/tests/pos/hklower.scala
@@ -0,0 +1,41 @@
+class Test {
+
+  type T[X]
+  type U[X] = T[X]
+
+  type V[X] >: T[X]
+  type W[X] >: T[X] <: T[X]
+
+  def f[C[X] >: T[X]](x: C[Int]) = ???
+
+  val v: V[Int] = ???
+  val t: T[Int] = ???
+
+  f[V](v)
+
+  f[V](t)
+
+
+}
+class Test2 {
+
+  class T[X]
+  type U[X] = T[X]
+
+  type V[X] >: T[X]
+  type W[X] >: T[X] <: T[X]
+
+  def f[C[X] >: T[X]](x: C[Int]) = ???
+
+  val v: V[Int] = ???
+  val t: T[Int] = ???
+
+  f[V](v)
+
+  f[V](t)
+
+  var x: V[Int] = _
+  x = t
+
+
+}
diff --git a/tests/pending/pos/i1181.scala b/tests/pos/i1181.scala
index 057c938d3..057c938d3 100644
--- a/tests/pending/pos/i1181.scala
+++ b/tests/pos/i1181.scala
diff --git a/tests/pos/i94-nada.scala b/tests/pos/i94-nada.scala
index f8263ccf2..2c3cf895c 100644
--- a/tests/pos/i94-nada.scala
+++ b/tests/pos/i94-nada.scala
@@ -25,7 +25,7 @@ trait Test1 {
   case class Left[A,B](x: A) extends Either[A,B] with Monad[A]
   case class Right[A,B](x: B) extends Either[A,B] with Monad[B]
   def flatMap[X,Y,M[X]<:Monad[X]](m: M[X], f: X => M[Y]): M[Y] = f(m.x)
-  println(flatMap(Left(1), {x: Int => Left(x)}))
+  println(flatMap(Right(1), {x: Int => Right(x)}))
 }
 trait Test2 {
   trait Monad[X] {
diff --git a/tests/pos/jon.scala b/tests/pos/jon.scala
index d4ea74f02..224486945 100644
--- a/tests/pos/jon.scala
+++ b/tests/pos/jon.scala
@@ -4,5 +4,5 @@ object Test {
 
   val x = List(List, Vector)
 
-  val y: List[scala.collection.generic.SeqFactory] = x
+  val y: List[scala.collection.generic.SeqFactory[_]] = x
 }
diff --git a/tests/pos/lookuprefined.scala b/tests/pos/lookuprefined.scala
index f7e7f7337..9dd2b4abb 100644
--- a/tests/pos/lookuprefined.scala
+++ b/tests/pos/lookuprefined.scala
@@ -2,7 +2,9 @@ class C { type T; type U }
 
 trait Test {
 
-  val x: (C { type U = T } { type T = String }) # U
-  val y: String = x
+  val x1: (C { type U = T; type T = String }) # U
+  val x2: (C { type U = T } {type T = String }) # U
 
+  val y1: String = x1
+  val y2: String = x2
 }
diff --git a/tests/pos/range.scala b/tests/pos/range.scala
index 9e7b5d1c9..a33f7fcee 100644
--- a/tests/pos/range.scala
+++ b/tests/pos/range.scala
@@ -1,8 +1,8 @@
 import scala.math._
 import collection.immutable.NumericRange
 object Test {
-  val r1: scala.collection.immutable.Range.Partial = ???
-  val r2: scala.Range.Partial = r1
+  val r1: scala.collection.immutable.Range.Partial[_, _] = ???
+  val r2: scala.Range.Partial[_, _] = r1
   def until(d: BigDecimal, end: BigDecimal): Range.Partial[BigDecimal, NumericRange.Exclusive[BigDecimal]] =
     new Range.Partial(until(d, end, _))
   def until(d: BigDecimal, end: BigDecimal, step: BigDecimal) = Range.BigDecimal(d, end, step)
diff --git a/tests/pos/t2066.scala b/tests/pos/t2066.scala
new file mode 100644
index 000000000..d175769fa
--- /dev/null
+++ b/tests/pos/t2066.scala
@@ -0,0 +1,25 @@
+trait A1 {
+  def f[T[+_]] = ()
+}
+
+trait B1 extends A1 {
+  override def f[T[+_]] = ()
+}
+
+
+trait A2 {
+  def f[T[-_]] = ()
+}
+
+trait B2 extends A2 {
+  override def f[T[-_]] = ()
+}
+
+
+trait A3 {
+  def f[T[X[+_]]] = ()
+}
+
+trait B3 extends A3 {
+  override def f[T[X[+_]]] = ()
+}
diff --git a/tests/pos/t2613.scala b/tests/pos/t2613.scala
index c234d4c0d..17ebe2d7e 100644
--- a/tests/pos/t2613.scala
+++ b/tests/pos/t2613.scala
@@ -5,7 +5,7 @@ object Test {
 
   abstract class MyRelation [R <: Row, +Relation <: MyRelation[R, Relation]]
 
-  type M = MyRelation[_ <: Row, _ <: MyRelation]
+  type M = MyRelation[_ <: Row, _ <: MyRelation[_, _]]
 
   val (x,y): (String, M) = null
 }
diff --git a/tests/pos/t2712-1.scala b/tests/pos/t2712-1.scala
new file mode 100644
index 000000000..4f84c9df5
--- /dev/null
+++ b/tests/pos/t2712-1.scala
@@ -0,0 +1,9 @@
+package test
+
+// Original test case from,
+//
+//   https://issues.scala-lang.org/browse/SI-2712
+object Test {
+  def meh[M[_], A](x: M[A]): M[A] = x
+  meh{(x: Int) => x} // solves ?M = [X] Int => X and ?A = Int ...
+}
diff --git a/tests/pos/t2712-2.scala b/tests/pos/t2712-2.scala
new file mode 100644
index 000000000..95172545d
--- /dev/null
+++ b/tests/pos/t2712-2.scala
@@ -0,0 +1,25 @@
+package test
+
+// See: https://github.com/milessabin/si2712fix-demo/issues/3
+object Test {
+  trait A[T1, T2] { }
+  trait B[T1, T2] { }
+  class C[T] extends A[T, Long] with B[T, Double]
+  class CB extends A[Boolean, Long] with B[Boolean, Double]
+
+  trait A2[T]
+  trait B2[T]
+  class C2[T] extends A2[T] with B2[T]
+  class CB2 extends A2[Boolean] with B2[Boolean]
+
+  def meh[M[_], A](x: M[A]): M[A] = x
+
+  val m0 = meh(new C[Boolean])
+  m0: C[Boolean]
+  val m1 = meh(new CB)
+  m1: B[Boolean, Double] // note: different order in which parents are visited for hk type inference. Dotty picks libearization order.
+  val m2 = meh(new C2[Boolean])
+  m2: C2[Boolean]
+  val m3 = meh(new CB2)
+  m3: B2[Boolean] // note: different order in which parents are visited for hk type inference. Dotty picks libearization order.
+}
diff --git a/tests/pos/t2712-3.scala b/tests/pos/t2712-3.scala
new file mode 100644
index 000000000..dd599f40f
--- /dev/null
+++ b/tests/pos/t2712-3.scala
@@ -0,0 +1,24 @@
+package test
+
+object Test1 {
+  class Foo[T, F[_]]
+  def meh[M[_[_]], F[_]](x: M[F]): M[F] = x
+  meh(new Foo[Int, List]) // solves ?M = [X[_]]Foo[Int, X[_]] ?A = List ...
+}
+
+object Test2 {
+  trait TC[T]
+  class Foo[F[_], G[_]]
+  def meh[GG[_[_]]](g: GG[TC]) = ???
+  meh(new Foo[TC, TC]) // solves ?G = [X[_]]Foo[TC, X]
+}
+
+object Test3 {
+  trait TC[F[_]]
+  trait TC2[F[_]]
+  class Foo[F[_[_]], G[_[_]]]
+  new Foo[TC, TC2]
+
+  def meh[G[_[_[_]]]](g: G[TC2]) = ???
+  meh(new Foo[TC, TC2]) // solves ?G = [X[_[_]]]Foo[TC, X]
+}
diff --git a/tests/pos/t2712-4.scala b/tests/pos/t2712-4.scala
new file mode 100644
index 000000000..3e2e5cdda
--- /dev/null
+++ b/tests/pos/t2712-4.scala
@@ -0,0 +1,17 @@
+package test
+
+object Test1 {
+  trait X
+  trait Y extends X
+  class Foo[T, U <: X]
+  def meh[M[_ <: A], A](x: M[A]): M[A] = x
+  meh(new Foo[Int, Y])
+}
+
+object Test2 {
+  trait X
+  trait Y extends X
+  class Foo[T, U >: Y]
+  def meh[M[_ >: A], A](x: M[A]): M[A] = x
+  meh(new Foo[Int, X])
+}
diff --git a/tests/pos/t2712-5.scala b/tests/pos/t2712-5.scala
new file mode 100644
index 000000000..ed96d4c06
--- /dev/null
+++ b/tests/pos/t2712-5.scala
@@ -0,0 +1,29 @@
+package test
+
+import scala.language.higherKinds
+
+trait Functor[F[_]] {
+  def map[A, B](f: A => B, fa: F[A]): F[B]
+}
+
+object Functor {
+  implicit def function[A]: Functor[({ type l[B] = A => B })#l] =
+    new Functor[({ type l[B] = A => B })#l] {
+      def map[C, B](cb: C => B, ac: A => C): A => B = cb compose ac
+    }
+}
+
+object FunctorSyntax {
+  implicit class FunctorOps[F[_], A](fa: F[A])(implicit F: Functor[F]) {
+    def map[B](f: A => B): F[B] = F.map(f, fa)
+  }
+}
+
+object Test {
+
+  val f: Int => String = _.toString
+
+  import FunctorSyntax._
+
+  f.map((s: String) => s.reverse)
+}
diff --git a/tests/pos/t2712-6.scala b/tests/pos/t2712-6.scala
new file mode 100644
index 000000000..dbba60472
--- /dev/null
+++ b/tests/pos/t2712-6.scala
@@ -0,0 +1,12 @@
+package test
+
+object Tags {
+  type Tagged[A, T] = {type Tag = T; type Self = A}
+
+  type @@[T, Tag] = Tagged[T, Tag]
+
+  trait Disjunction
+
+  def meh[M[_], A](ma: M[A]): M[A] = ma
+  meh(null: Int @@ Disjunction)//.asInstanceOf[Int @@ Disjunction])
+}
diff --git a/tests/pos/t2712-7.scala b/tests/pos/t2712-7.scala
new file mode 100644
index 000000000..d9c5243f1
--- /dev/null
+++ b/tests/pos/t2712-7.scala
@@ -0,0 +1,15 @@
+package test
+
+// Cats Xor, Scalaz \/, scala.util.Either
+sealed abstract class Xor[+A, +B] extends Product with Serializable
+object Xor {
+  final case class Left[+A](a: A) extends (A Xor Nothing)
+  final case class Right[+B](b: B) extends (Nothing Xor B)
+}
+
+object TestXor {
+  import Xor._
+  def meh[F[_], A, B](fa: F[A])(f: A => B): F[B] = ???
+  meh(new Right(23): Xor[Boolean, Int])(_ < 13)
+  meh(new Left(true): Xor[Boolean, Int])(_ < 13)
+}
diff --git a/tests/pos/t5683.scala b/tests/pos/t5683.scala
new file mode 100644
index 000000000..05ab03579
--- /dev/null
+++ b/tests/pos/t5683.scala
@@ -0,0 +1,23 @@
+object Test {
+  trait NT[X]
+  trait W[W, A] extends NT[Int]
+  type StringW[T] = W[String, T]
+  trait K[M[_], A, B]
+
+  def k[M[_], B](f: Int => M[B]): K[M, Int, B] = null
+
+  val okay1: K[StringW,Int,Int] = k{ (y: Int) => null: StringW[Int] }
+  val okay2 = k[StringW,Int]{ (y: Int) => null: W[String, Int] }
+
+  val crash: K[StringW,Int,Int] = k{ (y: Int) => null: W[String, Int] }
+
+  // remove `extends NT[Int]`, and the last line gives an inference error
+  // rather than a crash.
+  //   test/files/pos/t5683.scala:12: error: no type parameters for method k: (f: Int => M[B])Test.K[M,Int,B] exist so that it can be applied to arguments (Int => Test.W[String,Int])
+  //  --- because ---
+  // argument expression's type is not compatible with formal parameter type;
+  //  found   : Int => Test.W[String,Int]
+  //  required: Int => ?M[?B]
+  //   val crash: K[StringW,Int,Int] = k{ (y: Int) => null: W[String, Int] }
+  //                                   ^
+}
diff --git a/tests/pos/tycons.scala b/tests/pos/tycons.scala
deleted file mode 100644
index 1ed4d2855..000000000
--- a/tests/pos/tycons.scala
+++ /dev/null
@@ -1,22 +0,0 @@
-class TypeConstructor {
-  type TypeArg
-}
-
-trait List[+T] extends TypeConstructor { type TypeArg <: T }
-
-trait Set[T] extends TypeConstructor { type TypeArg <: T }
-
-object obj extends List[Number] with Set[Exception] {
-  val x: TypeArg = ???
-  val n: Number = x
-  val e: Exception = x
-}
-
-abstract class Functor[F <: TypeConstructor] {
-  def map[A, B](f: F { type TypeArg <: A }): F { type TypeArg <: B }
-}
-
-object ListFunctor extends Functor[List] {
-  override def map[A, B](f: List { type TypeArg <: A }): List { type TypeArg <: B } = ???
-}
-