SI-6895 Test cases to explain the limitations in tcpoly inference

I've determined that the failure in this bug report boils down
to SI-2712. Submitting my working as neg tests for posterity.

The type error disabmiguator develops a serious stutter with this
example. I'll fix that in the following commit.

4 files changed, 80 insertions, 0 deletions

diff --git a/test/files/neg/t6895.check b/test/files/neg/t6895.check
new file mode 100644
index 0000000000..df01031fff
--- /dev/null
+++ b/test/files/neg/t6895.check
@@ -0,0 +1,6 @@
+t6895.scala:19: error: polymorphic expression cannot be instantiated to expected type;
+ found   : [F3[F3_P]]Foo[F3]
+ required: Foo[[X3]Bar[[X1]String]]
+  val nok: Foo[({type L[X3] = Bar[M]})#L] = barFoo /* Type inference can't unify F with L */
+                                            ^
+one error found
diff --git a/test/files/neg/t6895.scala b/test/files/neg/t6895.scala
new file mode 100644
index 0000000000..5fb20d8c61
--- /dev/null
+++ b/test/files/neg/t6895.scala
@@ -0,0 +1,26 @@
+trait Foo[F1[F1_P]]
+trait Bar[F2[F2_P]]
+
+class Test {
+  def barFoo[F3[F3_P]]: Foo[F3] = ???
+
+  // Now we can define a couple of type aliases:
+  type M[X1] = String
+  type N[X2] = Bar[M]
+
+  // val ok1: Foo[N] = barFoo
+  // Foo[?F3] <:< Foo[Test.this.N]
+  //   [X2]Test.this.N[X2] <:< [F3_P]?F3[F3_P]
+  //      Test.this.N[X2] <:< ?F3[X2]
+  //        true, ?F3=N
+
+  // val ok2: Foo[({type L[X] = Bar[M]})#L] = barFoo[N]
+
+  val nok: Foo[({type L[X3] = Bar[M]})#L] = barFoo /* Type inference can't unify F with L */
+  // Foo[?F3] <:< Foo[[X3]Bar[[X1]String]]
+  //   [X3]Bar[[X1]String] <:< ?F3
+  //     [X3]Bar[[X1]String] <:< [F3_P]?F3[F3_P]
+  //        Bar[[X1]String] <:< ?F3[X3]
+  //          X3 <:< [X1]String
+  //            false
+}
diff --git a/test/files/neg/t6895b.check b/test/files/neg/t6895b.check
new file mode 100644
index 0000000000..3ebdb69309
--- /dev/null
+++ b/test/files/neg/t6895b.check
@@ -0,0 +1,9 @@
+t6895b.scala:20: error: could not find implicit value for parameter e: Foo[[X]Bar[[X]Or[String,X],X]]
+  implicitly[Foo[({type L[X] = Bar[StringOr, X]})#L]]
+            ^
+t6895b.scala:23: error: polymorphic expression cannot be instantiated to expected type;
+ found   : [F[_]]Foo[[X(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)]Bar[F,X(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)]]
+ required: Foo[[X(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)]Bar[[X]Or[String,X],X(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)(in type L)]]
+  barFoo(null) : Foo[({type L[X] = Bar[StringOr, X]})#L]
+        ^
+two errors found
diff --git a/test/files/neg/t6895b.scala b/test/files/neg/t6895b.scala
new file mode 100644
index 0000000000..c465065011
--- /dev/null
+++ b/test/files/neg/t6895b.scala
@@ -0,0 +1,39 @@
+trait Foo[F[_]]
+trait Bar[F[_], A]
+
+trait Or[A, B]
+
+class Test {
+  implicit def orFoo[A]: Foo[({type L[X] = Or[A, X]})#L] = ???
+  implicit def barFoo[F[_]](implicit f: Foo[F]): Foo[({type L[X] = Bar[F, X]})#L] = ???
+
+  // Now we can define a couple of type aliases:
+  type StringOr[X] = Or[String, X]
+  type BarStringOr[X] = Bar[StringOr, X]
+
+  // ok
+  implicitly[Foo[BarStringOr]]
+  barFoo[StringOr](null) : Foo[BarStringOr]
+  barFoo(null) : Foo[BarStringOr]
+
+  // nok
+  implicitly[Foo[({type L[X] = Bar[StringOr, X]})#L]]
+  // Let's write the application explicitly, and then
+  // compile with just this line enabled and -explaintypes.
+  barFoo(null) : Foo[({type L[X] = Bar[StringOr, X]})#L]
+
+  // Foo[[X]Bar[F,X]] <: Foo[[X]Bar[[X]Or[String,X],X]]?
+  //   Bar[[X]Or[String,X],X] <: Bar[F,X]?
+  //     F[_] <: Or[String,_]?
+  //     false
+  //   false
+  // false
+
+  // Note that the type annotation above is typechecked as
+  // Foo[[X]Bar[[X]Or[String,X],X]], ie the type alias `L`
+  // is eta expanded.
+  //
+  // This is done so that it does not escape its defining scope.
+  // However, one this is done, higher kinded inference
+  // no longer is able to unify F with `StringOr` (SI-2712)
+}