SI-2712 Add support for higher order unification

35 files changed, 509 insertions, 6 deletions

diff --git a/bincompat-forward.whitelist.conf b/bincompat-forward.whitelist.conf
index c6cffee846..411989fd4b 100644
--- a/bincompat-forward.whitelist.conf
+++ b/bincompat-forward.whitelist.conf
@@ -387,6 +387,10 @@ filter {
     {
         matchName="scala.concurrent.impl.Promise.toString"
         problemName=MissingMethodProblem
+    },
+    {
+        matchName="scala.reflect.runtime.Settings.YpartialUnification"
+        problemName=MissingMethodProblem
     }
   ]
 }
diff --git a/project/ScalaOptionParser.scala b/project/ScalaOptionParser.scala
index da8a3bf460..b907045cb4 100644
--- a/project/ScalaOptionParser.scala
+++ b/project/ScalaOptionParser.scala
@@ -86,7 +86,7 @@ object ScalaOptionParser {
     "-Yeta-expand-keeps-star", "-Yide-debug", "-Yinfer-argument-types", "-Yinfer-by-name", "-Yinfer-debug", "-Yinline", "-Yinline-handlers",
     "-Yinline-warnings", "-Yissue-debug", "-Ylog-classpath", "-Ymacro-debug-lite", "-Ymacro-debug-verbose", "-Ymacro-no-expand",
     "-Yno-completion", "-Yno-generic-signatures", "-Yno-imports", "-Yno-load-impl-class", "-Yno-predef", "-Ynooptimise",
-    "-Yoverride-objects", "-Yoverride-vars", "-Ypatmat-debug", "-Yno-adapted-args", "-Ypos-debug", "-Ypresentation-debug",
+    "-Yoverride-objects", "-Yoverride-vars", "-Ypatmat-debug", "-Yno-adapted-args", "-Ypartial-unification", "-Ypos-debug", "-Ypresentation-debug",
     "-Ypresentation-strict", "-Ypresentation-verbose", "-Yquasiquote-debug", "-Yrangepos", "-Yreify-copypaste", "-Yreify-debug", "-Yrepl-class-based",
     "-Yrepl-sync", "-Yshow-member-pos", "-Yshow-symkinds", "-Yshow-symowners", "-Yshow-syms", "-Yshow-trees", "-Yshow-trees-compact", "-Yshow-trees-stringified", "-Ytyper-debug",
     "-Ywarn-adapted-args", "-Ywarn-dead-code", "-Ywarn-inaccessible", "-Ywarn-infer-any", "-Ywarn-nullary-override", "-Ywarn-nullary-unit", "-Ywarn-numeric-widen", "-Ywarn-unused", "-Ywarn-unused-import", "-Ywarn-value-discard",
diff --git a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
index 1817cfa25a..8e5c064e1f 100644
--- a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
+++ b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
@@ -218,6 +218,7 @@ trait ScalaSettings extends AbsScalaSettings
   val inferByName     = BooleanSetting    ("-Yinfer-by-name", "Allow inference of by-name types. This is a temporary option to ease transition. See SI-7899.").withDeprecationMessage(removalIn212)
   val YclasspathImpl  = ChoiceSetting     ("-YclasspathImpl", "implementation", "Choose classpath scanning method.", List(ClassPathRepresentationType.Recursive, ClassPathRepresentationType.Flat), ClassPathRepresentationType.Recursive)
   val YdisableFlatCpCaching  = BooleanSetting    ("-YdisableFlatCpCaching", "Do not cache flat classpath representation of classpath elements from jars across compiler instances.")
+  val YpartialUnification = BooleanSetting ("-Ypartial-unification", "Enable partial unification in type constructor inference")
 
   val YvirtClasses    = false // too embryonic to even expose as a -Y //BooleanSetting    ("-Yvirtual-classes", "Support virtual classes")
   val YdisableUnreachablePrevention = BooleanSetting("-Ydisable-unreachable-prevention", "Disable the prevention of unreachable blocks in code generation.")
diff --git a/src/reflect/scala/reflect/internal/Types.scala b/src/reflect/scala/reflect/internal/Types.scala
index 9697e16da7..98510825c0 100644
--- a/src/reflect/scala/reflect/internal/Types.scala
+++ b/src/reflect/scala/reflect/internal/Types.scala
@@ -3076,13 +3076,43 @@ trait Types
        */
       def unifyFull(tpe: Type): Boolean = {
         def unifySpecific(tp: Type) = {
-          sameLength(typeArgs, tp.typeArgs) && {
-            val lhs = if (isLowerBound) tp.typeArgs else typeArgs
-            val rhs = if (isLowerBound) typeArgs else tp.typeArgs
+          val tpTypeArgs = tp.typeArgs
+          val arityDelta = compareLengths(typeArgs, tpTypeArgs)
+          if (arityDelta == 0) {
+            val lhs = if (isLowerBound) tpTypeArgs else typeArgs
+            val rhs = if (isLowerBound) typeArgs else tpTypeArgs
             // This is a higher-kinded type var with same arity as tp.
             // If so (see SI-7517), side effect: adds the type constructor itself as a bound.
-            isSubArgs(lhs, rhs, params, AnyDepth) && { addBound(tp.typeConstructor); true }
-          }
+            isSubArgs(lhs, rhs, params, AnyDepth) && {addBound(tp.typeConstructor); true}
+          } else if (settings.YpartialUnification && arityDelta < 0 && typeArgs.nonEmpty) {
+            // Simple algorithm as suggested by Paul Chiusano in the comments on SI-2712
+            //
+            //   https://issues.scala-lang.org/browse/SI-2712?focusedCommentId=61270
+            //
+            // Treat the type constructor as curried and partially applied, we treat a prefix
+            // as constants and solve for the suffix. For the example in the ticket, unifying
+            // M[A] with Int => Int this unifies as,
+            //
+            //   M[t] = [t][Int => t]  --> abstract on the right to match the expected arity
+            //   A = Int               --> capture the remainder on the left
+            //
+            // A more "natural" unifier might be M[t] = [t][t => t]. There's lots of scope for
+            // experimenting with alternatives here.
+            val numCaptured = tpTypeArgs.length - typeArgs.length
+            val (captured, abstractedArgs) = tpTypeArgs.splitAt(numCaptured)
+
+            val (lhs, rhs) =
+              if (isLowerBound) (abstractedArgs, typeArgs)
+              else (typeArgs, abstractedArgs)
+
+            isSubArgs(lhs, rhs, params, AnyDepth) && {
+              val tpSym = tp.typeSymbolDirect
+              val abstractedTypeParams = tpSym.typeParams.drop(numCaptured).map(_.cloneSymbol(tpSym))
+
+              addBound(PolyType(abstractedTypeParams, appliedType(tp.typeConstructor, captured ++ abstractedTypeParams.map(_.tpeHK))))
+              true
+            }
+          } else false
         }
         // The type with which we can successfully unify can be hidden
         // behind singleton types and type aliases.
diff --git a/src/reflect/scala/reflect/internal/settings/MutableSettings.scala b/src/reflect/scala/reflect/internal/settings/MutableSettings.scala
index 38893d8db3..3de720da11 100644
--- a/src/reflect/scala/reflect/internal/settings/MutableSettings.scala
+++ b/src/reflect/scala/reflect/internal/settings/MutableSettings.scala
@@ -53,6 +53,7 @@ abstract class MutableSettings extends AbsSettings {
   def printtypes: BooleanSetting
   def uniqid: BooleanSetting
   def verbose: BooleanSetting
+  def YpartialUnification: BooleanSetting
 
   def Yrecursion: IntSetting
   def maxClassfileName: IntSetting
diff --git a/src/reflect/scala/reflect/runtime/Settings.scala b/src/reflect/scala/reflect/runtime/Settings.scala
index 27d574b1de..1081218a70 100644
--- a/src/reflect/scala/reflect/runtime/Settings.scala
+++ b/src/reflect/scala/reflect/runtime/Settings.scala
@@ -47,6 +47,7 @@ private[reflect] class Settings extends MutableSettings {
   val printtypes        = new BooleanSetting(false)
   val uniqid            = new BooleanSetting(false)
   val verbose           = new BooleanSetting(false)
+  val YpartialUnification = new BooleanSetting(false)
 
   val Yrecursion        = new IntSetting(0)
   val maxClassfileName  = new IntSetting(255)
diff --git a/test/files/neg/t2712-1.check b/test/files/neg/t2712-1.check
new file mode 100644
index 0000000000..61e4b6b149
--- /dev/null
+++ b/test/files/neg/t2712-1.check
@@ -0,0 +1,13 @@
+t2712-1.scala:7: error: no type parameters for method foo: (m: M[A])Unit exist so that it can be applied to arguments (test.Two[Int,String])
+ --- because ---
+argument expression's type is not compatible with formal parameter type;
+ found   : test.Two[Int,String]
+ required: ?M[?A]
+  def test(ma: Two[Int, String]) = foo(ma) // should fail with -Ypartial-unification *disabled*
+                                   ^
+t2712-1.scala:7: error: type mismatch;
+ found   : test.Two[Int,String]
+ required: M[A]
+  def test(ma: Two[Int, String]) = foo(ma) // should fail with -Ypartial-unification *disabled*
+                                       ^
+two errors found
diff --git a/test/files/neg/t2712-1.scala b/test/files/neg/t2712-1.scala
new file mode 100644
index 0000000000..f7967d71b6
--- /dev/null
+++ b/test/files/neg/t2712-1.scala
@@ -0,0 +1,8 @@
+package test
+
+trait Two[A, B]
+
+object Test {
+  def foo[M[_], A](m: M[A]) = ()
+  def test(ma: Two[Int, String]) = foo(ma) // should fail with -Ypartial-unification *disabled*
+}
diff --git a/test/files/neg/t2712-2.check b/test/files/neg/t2712-2.check
new file mode 100644
index 0000000000..ea19e33e2c
--- /dev/null
+++ b/test/files/neg/t2712-2.check
@@ -0,0 +1,13 @@
+t2712-2.scala:16: error: type mismatch;
+ found   : test.Foo
+ required: test.Two[test.X1,Object]
+Note: test.X2 <: Object (and test.Foo <: test.Two[test.X1,test.X2]), but trait Two is invariant in type B.
+You may wish to define B as +B instead. (SLS 4.5)
+  test1(foo): One[X3]     // fails with -Ypartial-unification enabled
+        ^
+t2712-2.scala:16: error: type mismatch;
+ found   : test.Two[test.X1,Object]
+ required: test.One[test.X3]
+  test1(foo): One[X3]     // fails with -Ypartial-unification enabled
+       ^
+two errors found
diff --git a/test/files/neg/t2712-2.flags b/test/files/neg/t2712-2.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/neg/t2712-2.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/neg/t2712-2.scala b/test/files/neg/t2712-2.scala
new file mode 100644
index 0000000000..85ed523489
--- /dev/null
+++ b/test/files/neg/t2712-2.scala
@@ -0,0 +1,18 @@
+package test
+
+class X1
+class X2
+class X3
+
+trait One[A]
+trait Two[A, B]
+
+class Foo extends Two[X1, X2] with One[X3]
+object Test {
+  def test1[M[_], A](x: M[A]): M[A] = x
+
+  val foo = new Foo
+
+  test1(foo): One[X3]     // fails with -Ypartial-unification enabled
+  test1(foo): Two[X1, X2] // fails without -Ypartial-unification
+}
diff --git a/test/files/neg/t2712-3.check b/test/files/neg/t2712-3.check
new file mode 100644
index 0000000000..a84d96bf09
--- /dev/null
+++ b/test/files/neg/t2712-3.check
@@ -0,0 +1,6 @@
+t2712-3.scala:17: error: type mismatch;
+ found   : test.One[test.X3]
+ required: test.Two[test.X1,test.X2]
+  test1(foo): Two[X1, X2] // fails without -Ypartial-unification
+       ^
+one error found
diff --git a/test/files/neg/t2712-3.scala b/test/files/neg/t2712-3.scala
new file mode 100644
index 0000000000..85ed523489
--- /dev/null
+++ b/test/files/neg/t2712-3.scala
@@ -0,0 +1,18 @@
+package test
+
+class X1
+class X2
+class X3
+
+trait One[A]
+trait Two[A, B]
+
+class Foo extends Two[X1, X2] with One[X3]
+object Test {
+  def test1[M[_], A](x: M[A]): M[A] = x
+
+  val foo = new Foo
+
+  test1(foo): One[X3]     // fails with -Ypartial-unification enabled
+  test1(foo): Two[X1, X2] // fails without -Ypartial-unification
+}
diff --git a/test/files/neg/t2712.flags b/test/files/neg/t2712.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/neg/t2712.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/pos/t2712-1.flags b/test/files/pos/t2712-1.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/pos/t2712-1.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/pos/t2712-1.scala b/test/files/pos/t2712-1.scala
new file mode 100644
index 0000000000..4f84c9df5e
--- /dev/null
+++ b/test/files/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/test/files/pos/t2712-2.flags b/test/files/pos/t2712-2.flags
new file mode 100644
index 0000000000..7d49efbb8e
--- /dev/null
+++ b/test/files/pos/t2712-2.flags
@@ -0,0 +1,2 @@
+-Ypartial-unification
+
diff --git a/test/files/pos/t2712-2.scala b/test/files/pos/t2712-2.scala
new file mode 100644
index 0000000000..39f22dd92a
--- /dev/null
+++ b/test/files/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: A[Boolean, Long]
+  val m2 = meh(new C2[Boolean])
+  m2: C2[Boolean]
+  val m3 = meh(new CB2)
+  m3: A2[Boolean]
+}
diff --git a/test/files/pos/t2712-3.flags b/test/files/pos/t2712-3.flags
new file mode 100644
index 0000000000..7d49efbb8e
--- /dev/null
+++ b/test/files/pos/t2712-3.flags
@@ -0,0 +1,2 @@
+-Ypartial-unification
+
diff --git a/test/files/pos/t2712-3.scala b/test/files/pos/t2712-3.scala
new file mode 100644
index 0000000000..46445f9289
--- /dev/null
+++ b/test/files/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[G[_[_]]](g: G[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/test/files/pos/t2712-4.flags b/test/files/pos/t2712-4.flags
new file mode 100644
index 0000000000..7d49efbb8e
--- /dev/null
+++ b/test/files/pos/t2712-4.flags
@@ -0,0 +1,2 @@
+-Ypartial-unification
+
diff --git a/test/files/pos/t2712-4.scala b/test/files/pos/t2712-4.scala
new file mode 100644
index 0000000000..3e2e5cddae
--- /dev/null
+++ b/test/files/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/test/files/pos/t2712-5.flags b/test/files/pos/t2712-5.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/pos/t2712-5.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/pos/t2712-5.scala b/test/files/pos/t2712-5.scala
new file mode 100644
index 0000000000..ed96d4c06f
--- /dev/null
+++ b/test/files/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/test/files/pos/t2712-6.flags b/test/files/pos/t2712-6.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/pos/t2712-6.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/pos/t2712-6.scala b/test/files/pos/t2712-6.scala
new file mode 100644
index 0000000000..eefe769ad6
--- /dev/null
+++ b/test/files/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.asInstanceOf[Int @@ Disjunction])
+}
diff --git a/test/files/pos/t2712-7.flags b/test/files/pos/t2712-7.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/pos/t2712-7.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/pos/t2712-7.scala b/test/files/pos/t2712-7.scala
new file mode 100644
index 0000000000..d9c5243f13
--- /dev/null
+++ b/test/files/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/test/files/pos/t5683.flags b/test/files/pos/t5683.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/pos/t5683.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/pos/t5683.scala b/test/files/pos/t5683.scala
new file mode 100644
index 0000000000..05ab035792
--- /dev/null
+++ b/test/files/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/test/files/pos/t6895b.flags b/test/files/pos/t6895b.flags
new file mode 100644
index 0000000000..7d49efbb8e
--- /dev/null
+++ b/test/files/pos/t6895b.flags
@@ -0,0 +1,2 @@
+-Ypartial-unification
+
diff --git a/test/files/pos/t6895b.scala b/test/files/pos/t6895b.scala
new file mode 100644
index 0000000000..c465065011
--- /dev/null
+++ b/test/files/pos/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)
+}
diff --git a/test/files/run/inferred-type-constructors-hou.check b/test/files/run/inferred-type-constructors-hou.check
new file mode 100644
index 0000000000..6b09823341
--- /dev/null
+++ b/test/files/run/inferred-type-constructors-hou.check
@@ -0,0 +1,56 @@
+warning: there were two feature warnings; re-run with -feature for details
+                p.Iterable[Int]
+                p.Set[Int]
+                p.Seq[Int]
+                p.m.Set[Int]
+                p.m.Seq[Int]
+     private[m] p.m.ASet[Int]
+                p.i.Seq[Int]
+     private[i] p.i.ASet[Int]
+     private[i] p.i.ASeq[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Set[Int]
+                p.Iterable[Int]
+                p.Set[Int]
+                p.Iterable[Int]
+                p.Set[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Seq[Int]
+                p.Iterable[Int]
+                p.Seq[Int]
+                p.Iterable[Int]
+                p.Seq[Int]
+                p.Iterable[Int]
+                p.m.Set[Int]
+                p.Iterable[Int]
+                p.Set[Int]
+                p.Iterable[Int]
+                p.Iterable[Int]
+                p.Seq[Int]
+                p.Iterable[Int]
+                p.Seq[Int]
+                p.Iterable[Int]
+     private[p] p.ASet[Int]
+     private[p] p.AIterable[Int]
+                p.Iterable[Int]
+                p.i.Seq[Int]
+     private[p] p.AIterable[Int]
+                List[Nothing]
+                scala.collection.immutable.Vector[Nothing]
+                scala.collection.immutable.Map[Int,Int]
+                scala.collection.immutable.Set[Int]
+                Seq[Int]
+                Array[Int]
+                scala.collection.AbstractSet[Int]
+                Comparable[java.lang.String]
+                scala.collection.immutable.LinearSeq[Int]
+                Iterable[Int]
diff --git a/test/files/run/inferred-type-constructors-hou.flags b/test/files/run/inferred-type-constructors-hou.flags
new file mode 100644
index 0000000000..41565c7e32
--- /dev/null
+++ b/test/files/run/inferred-type-constructors-hou.flags
@@ -0,0 +1 @@
+-Ypartial-unification
diff --git a/test/files/run/inferred-type-constructors-hou.scala b/test/files/run/inferred-type-constructors-hou.scala
new file mode 100644
index 0000000000..79a8653f68
--- /dev/null
+++ b/test/files/run/inferred-type-constructors-hou.scala
@@ -0,0 +1,125 @@
+package p {
+  trait TCon[+CC[X]] {
+    def fPublic: CC[Int]                        = ???
+    private[p] def fPackagePrivate: CC[Int]     = ???
+    protected[p] def fPackageProtected: CC[Int] = ???
+  }
+  trait Iterable[+A] extends TCon[Iterable]
+  trait Set[A] extends Iterable[A] with TCon[Set]
+  trait Seq[+A] extends Iterable[A] with TCon[Seq]
+
+  private[p] abstract class AIterable[+A] extends Iterable[A]
+  private[p] abstract class ASeq[+A] extends AIterable[A] with Seq[A]
+  private[p] abstract class ASet[A] extends AIterable[A] with Set[A]
+
+  package m {
+    private[m] abstract class ASeq[A] extends p.ASeq[A] with Seq[A]
+    private[m] abstract class ASet[A] extends p.ASet[A] with Set[A]
+    trait Set[A] extends p.Set[A] with TCon[Set]
+    trait Seq[A] extends p.Seq[A] with TCon[Seq]
+    trait BitSet extends ASet[Int]
+    trait IntSeq extends ASeq[Int]
+  }
+
+  package i {
+    private[i] abstract class ASeq[+A] extends p.ASeq[A] with Seq[A]
+    private[i] abstract class ASet[A] extends p.ASet[A] with Set[A]
+    trait Set[A] extends p.Set[A] with TCon[Set]
+    trait Seq[+A] extends p.Seq[A] with TCon[Seq]
+    trait BitSet extends ASet[Int]
+    trait IntSeq extends ASeq[Int]
+  }
+}
+
+object Test {
+  import scala.reflect.runtime.universe._
+  // Complicated by the absence of usable type constructor type tags.
+  def extract[A, CC[X]](xs: CC[A]): CC[A] = xs
+  def whatis[T: TypeTag](x: T): Unit = {
+    val tpe = typeOf[T]
+    val access = tpe.typeSymbol.asInstanceOf[scala.reflect.internal.HasFlags].accessString.replaceAllLiterally("package ", "")
+    println(f"$access%15s $tpe")
+  }
+
+  trait IntIterable extends p.Iterable[Int]
+  trait IntSet extends p.Set[Int]
+  trait IntSeq extends p.Seq[Int]
+
+  trait MutableIntSet extends p.m.Set[Int]
+  trait MutableIntSeq extends p.m.Seq[Int]
+
+  trait ImmutableIntSet extends p.i.Set[Int]
+  trait ImmutableIntSeq extends p.i.Seq[Int]
+
+  def f1: IntIterable = null
+  def f2: IntSet = null
+  def f3: IntSeq = null
+
+  def g1: MutableIntSet = null
+  def g2: MutableIntSeq = null
+  def g3: p.m.BitSet = null
+
+  def h1: ImmutableIntSeq = null
+  def h2: p.i.BitSet = null
+  def h3: p.i.IntSeq = null
+
+  def main(args: Array[String]): Unit = {
+    whatis(extract(f1))
+    whatis(extract(f2))
+    whatis(extract(f3))
+    whatis(extract(g1))
+    whatis(extract(g2))
+    whatis(extract(g3))
+    whatis(extract(h1))
+    whatis(extract(h2))
+    whatis(extract(h3))
+
+    whatis(extract(if (true) f1 else f2))
+    whatis(extract(if (true) f1 else f3))
+    whatis(extract(if (true) f1 else g1))
+    whatis(extract(if (true) f1 else g2))
+    whatis(extract(if (true) f1 else g3))
+    whatis(extract(if (true) f1 else h1))
+    whatis(extract(if (true) f1 else h2))
+    whatis(extract(if (true) f1 else h3))
+    whatis(extract(if (true) f2 else f3))
+    whatis(extract(if (true) f2 else g1))
+    whatis(extract(if (true) f2 else g2))
+    whatis(extract(if (true) f2 else g3))
+    whatis(extract(if (true) f2 else h1))
+    whatis(extract(if (true) f2 else h2))
+    whatis(extract(if (true) f2 else h3))
+    whatis(extract(if (true) f3 else g1))
+    whatis(extract(if (true) f3 else g2))
+    whatis(extract(if (true) f3 else g3))
+    whatis(extract(if (true) f3 else h1))
+    whatis(extract(if (true) f3 else h2))
+    whatis(extract(if (true) f3 else h3))
+    whatis(extract(if (true) g1 else g2))
+    whatis(extract(if (true) g1 else g3))
+    whatis(extract(if (true) g1 else h1))
+    whatis(extract(if (true) g1 else h2))
+    whatis(extract(if (true) g1 else h3))
+    whatis(extract(if (true) g2 else g3))
+    whatis(extract(if (true) g2 else h1))
+    whatis(extract(if (true) g2 else h2))
+    whatis(extract(if (true) g2 else h3))
+    whatis(extract(if (true) g3 else h1))
+    whatis(extract(if (true) g3 else h2))
+    whatis(extract(if (true) g3 else h3))
+    whatis(extract(if (true) h1 else h2))
+    whatis(extract(if (true) h1 else h3))
+    whatis(extract(if (true) h2 else h3))
+
+    whatis(extract(Nil))
+    whatis(extract(Vector()))
+    whatis(extract(Map[Int,Int]()))
+    whatis(extract(Set[Int]()))
+    whatis(extract(Seq[Int]()))
+    whatis(extract(Array[Int]()))
+    whatis(extract(scala.collection.immutable.BitSet(1)))
+    whatis(extract("abc"))
+    whatis(extract(if (true) Stream(1) else List(1)))
+    whatis(extract(if (true) Seq(1) else Set(1)))
+  }
+}