From df1bf4d3fd2e80de4bdda120c3426511e3f2435b Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Tue, 16 Apr 2019 16:32:45 +0200
Subject: [PATCH 01/11] Use .zipped.forall instead zip_zip_forall

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 22 ++++---------------
 .../src-3.x/scala/compiletime/package.scala   |  2 +-
 tests/run/tuples1.scala                       |  2 +-
 3 files changed, 6 insertions(+), 20 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index dcf03d4f51c7..6fc19c26ff45 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1945,19 +1945,6 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
             true
         }
       case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
-        // Unboxed xs.zip(ys).zip(zs).forall { case ((a, b), c) => f(a, b, c) }
-        def zip_zip_forall[A, B, C](xs: List[A], ys: List[B], zs: List[C])(f: (A, B, C) => Boolean): Boolean = {
-          xs match {
-            case x :: xs => ys match {
-              case y :: ys => zs match {
-                case z :: zs => f(x, y, z) && zip_zip_forall(xs, ys, zs)(f)
-                case _ => true
-              }
-              case _ => true
-            }
-            case _ => true
-          }
-        }
         def covariantIntersecting(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = {
           intersecting(tp1, tp2) || {
             // We still need to proof that `Nothing` is not a valid
@@ -1981,7 +1968,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
           }
         }
 
-        zip_zip_forall(args1, args2, tycon1.typeParams) {
+        (args1, args2, tycon1.typeParams).zipped.forall {
           (arg1, arg2, tparam) =>
             val v = tparam.paramVariance
             if (v > 0)
@@ -1994,7 +1981,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
               covariantIntersecting(arg1, arg2, tparam) && (isSameType(arg1, arg2) || {
                 // We can only trust a "no" from `isSameType` when both
                 // `arg1` and `arg2` are fully instantiated.
-                val fullyInstantiated = new TypeAccumulator[Boolean] {
+                def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] {
                   override def apply(x: Boolean, t: Type) =
                     x && {
                       t match {
@@ -2003,9 +1990,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
                         case _ => foldOver(x, t)
                       }
                     }
-                }
-                !(fullyInstantiated.apply(true, arg1) &&
-                  fullyInstantiated.apply(true, arg2))
+                }.apply(true, tp)
+                !(fullyInstantiated(arg1) && fullyInstantiated(arg2))
               })
         }
       case (tp1: HKLambda, tp2: HKLambda) =>
diff --git a/library/src-3.x/scala/compiletime/package.scala b/library/src-3.x/scala/compiletime/package.scala
index 4aa2921066d6..da7574d0969a 100644
--- a/library/src-3.x/scala/compiletime/package.scala
+++ b/library/src-3.x/scala/compiletime/package.scala
@@ -11,4 +11,4 @@ package object compiletime {
   inline def constValue[T]: T = ???
 
   type S[X <: Int] <: Int
-}
\ No newline at end of file
+}
diff --git a/tests/run/tuples1.scala b/tests/run/tuples1.scala
index d58371e888c7..6570ebb850b5 100644
--- a/tests/run/tuples1.scala
+++ b/tests/run/tuples1.scala
@@ -94,4 +94,4 @@ object Test extends App {
   val us0: 0 = size(())
   val x3s1: 3 = size0(x3)
   val us1: 0 = size0(())
-}
\ No newline at end of file
+}

From f889bf8e925defe0eb52f40b10c08d86d792ffb9 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Tue, 16 Apr 2019 16:33:17 +0200
Subject: [PATCH 02/11] Don't assume types in & are sorted

---
 .../src/dotty/tools/dotc/core/TypeComparer.scala   |  9 +++++++--
 tests/neg/6314.scala                               | 14 ++++++++++++++
 2 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 tests/neg/6314.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 6fc19c26ff45..6bf3e2edd285 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2005,10 +2005,15 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
         intersecting(tp1.tp1, tp2) || intersecting(tp1.tp2, tp2)
       case (_, tp2: OrType)  =>
         intersecting(tp1, tp2.tp1) || intersecting(tp1, tp2.tp2)
+      case (tp1: AndType, tp2: AndType) =>
+        intersecting(tp1.tp1, tp2.tp1) && intersecting(tp1.tp2, tp2.tp2) ||
+        intersecting(tp1.tp1, tp2.tp2) && intersecting(tp1.tp2, tp2.tp1)
       case (tp1: AndType, _) =>
-        intersecting(tp1.tp1, tp2) && intersecting(tp1.tp2, tp2) && intersecting(tp1.tp1, tp1.tp2)
+        intersecting(tp1.tp1, tp2) && intersecting(tp1.tp2, tp2) ||
+        intersecting(tp1.tp2, tp2) && intersecting(tp1.tp1, tp2)
       case (_, tp2: AndType) =>
-        intersecting(tp1, tp2.tp1) && intersecting(tp1, tp2.tp2) && intersecting(tp2.tp1, tp2.tp2)
+        intersecting(tp1, tp2.tp1) && intersecting(tp1, tp2.tp2) ||
+        intersecting(tp1, tp2.tp2) && intersecting(tp1, tp2.tp1)
       case (tp1: TypeProxy, tp2: TypeProxy) =>
         intersecting(tp1.underlying, tp2) && intersecting(tp1, tp2.underlying)
       case (tp1: TypeProxy, _) =>
diff --git a/tests/neg/6314.scala b/tests/neg/6314.scala
new file mode 100644
index 000000000000..003ed3a0ede1
--- /dev/null
+++ b/tests/neg/6314.scala
@@ -0,0 +1,14 @@
+object G {
+  final class X
+  final class Y
+
+  trait Test {
+    type Type
+    val i: Bar[Y & Type] = 1 // error
+  }
+
+  type Bar[A] = A match {
+    case X & Y => String
+    case Y => Int
+  }
+}

From 992150b27a974e02c342c4a6fe16ff85babb4f15 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Tue, 16 Apr 2019 16:48:30 +0200
Subject: [PATCH 03/11] Update exhaustivity tests for loosen rules

---
 tests/patmat/andtype-opentype-interaction.check    | 1 +
 tests/patmat/andtype-refinedtype-interaction.check | 1 +
 2 files changed, 2 insertions(+)

diff --git a/tests/patmat/andtype-opentype-interaction.check b/tests/patmat/andtype-opentype-interaction.check
index a9d8618adad0..d42d03bb240c 100644
--- a/tests/patmat/andtype-opentype-interaction.check
+++ b/tests/patmat/andtype-opentype-interaction.check
@@ -2,5 +2,6 @@
 27: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2
 31: Pattern Match Exhaustivity: _: Trait & OpenClass
 35: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClass
+39: Pattern Match Exhaustivity: _: Trait & OpenClass & (OpenTrait & OpenClass2)
 43: Pattern Match Exhaustivity: _: Trait & OpenAbstractClass
 47: Pattern Match Exhaustivity: _: Trait & OpenClass & (OpenTrait & OpenClassSubclass)
diff --git a/tests/patmat/andtype-refinedtype-interaction.check b/tests/patmat/andtype-refinedtype-interaction.check
index b4bf99c88274..9f57c5ba4867 100644
--- a/tests/patmat/andtype-refinedtype-interaction.check
+++ b/tests/patmat/andtype-refinedtype-interaction.check
@@ -1,6 +1,7 @@
 32: Pattern Match Exhaustivity: _: Trait & C1{x: Int}
 48: Pattern Match Exhaustivity: _: Trait & (C1 | (C2 | T1)){x: Int} & (C3 | (C4 | T2)){x: Int}, _: Clazz & (C1 | (C2 | T1)){x: Int} & (C3 | (C4 | T2)){x: Int}
 54: Pattern Match Exhaustivity: _: Trait & (C1 | (C2 | T1)){x: Int} & C3{x: Int}
+59: Pattern Match Exhaustivity: _: Trait & (C1 & C2){x: Int}
 65: Pattern Match Exhaustivity: _: Trait & (C1 | C2){x: Int} & (C3 | SubC1){x: Int}
 72: Pattern Match Exhaustivity: _: Trait & (T1 & (C1 | SubC2)){x: Int} & (T2 & (C2 | C3 | SubC1)){x: Int} &
   SubSubC1{x: Int}

From be29f14a3d9347599e7f996625e610a1967b15d0 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 18 Apr 2019 10:10:34 +0200
Subject: [PATCH 04/11] Remove EqualsPatternClass

Seams to be a leftover from scalac old pattern matcher and has always
been dead code in dotty.
---
 compiler/src/dotty/tools/dotc/core/Definitions.scala | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 15bf66caa6bd..db9f12193cab 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -564,7 +564,6 @@ class Definitions {
   lazy val BoxedUnitModule: TermSymbol    = ctx.requiredModule("java.lang.Void")
 
   lazy val ByNameParamClass2x: ClassSymbol = enterSpecialPolyClass(tpnme.BYNAME_PARAM_CLASS, Covariant, Seq(AnyType))
-  lazy val EqualsPatternClass: ClassSymbol = enterSpecialPolyClass(tpnme.EQUALS_PATTERN, EmptyFlags, Seq(AnyType))
 
   lazy val RepeatedParamClass: ClassSymbol = enterSpecialPolyClass(tpnme.REPEATED_PARAM_CLASS, Covariant, Seq(ObjectType, SeqType))
 
@@ -1375,8 +1374,7 @@ class Definitions {
     AnyValClass,
     NullClass,
     NothingClass,
-    SingletonClass,
-    EqualsPatternClass)
+    SingletonClass)
 
   lazy val syntheticCoreClasses: List[Symbol] = syntheticScalaClasses ++ List(
     EmptyPackageVal,

From 1fc0059d99df6aa20a2fc9e4ee94b0b97c5f2dfd Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 18 Apr 2019 13:15:48 +0200
Subject: [PATCH 05/11] Special case intersecting for Singleton

Singleton is not part of the normal type hierarchy, special
treatment in requiered in intersecting to avoid making incorrect
assumptions.
---
 .../dotty/tools/dotc/core/TypeComparer.scala  |  2 +
 tests/neg/6314.scala                          | 40 +++++++++++++++++--
 2 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 6bf3e2edd285..14d312d0ec24 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1920,6 +1920,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       sym.children.map(x => ctx.refineUsingParent(tp, x)).filter(_.exists)
 
     (tp1.dealias, tp2.dealias) match {
+      case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol == defn.SingletonClass || tp2.symbol == defn.SingletonClass =>
+        true
       case (tp1: ConstantType, tp2: ConstantType) =>
         tp1 == tp2
       case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
diff --git a/tests/neg/6314.scala b/tests/neg/6314.scala
index 003ed3a0ede1..beee41c48e9a 100644
--- a/tests/neg/6314.scala
+++ b/tests/neg/6314.scala
@@ -1,9 +1,11 @@
-object G {
-  final class X
-  final class Y
+final class X
+final class Y
 
+object Test1 {
   trait Test {
     type Type
+    // This is testing that both permutations of the types in a &
+    // are taken into account by the intersection test
     val i: Bar[Y & Type] = 1 // error
   }
 
@@ -12,3 +14,35 @@ object G {
     case Y => Int
   }
 }
+
+object Test2 {
+  trait Wizzle[L <: Int with Singleton] {
+    type Bar[A] = A match {
+      case 0 => String
+      case L => Int
+    }
+
+    // This is testing that we don't make wrong assumptions about Singleton
+    def right(fa: Bar[L]): Int = fa // error
+  }
+
+  trait Wazzlo[L <: Int with AnyVal] {
+    type Bar[A] = A match {
+      case 0 => String
+      case L => Int
+    }
+
+    // This is testing that we don't make wrong assumptions about AnyVal
+    def right(fa: Bar[L]): Int = fa // error
+  }
+
+  trait Wuzzlu[L <: String with AnyRef] {
+    type Bar[A] = A match {
+      case "" => String
+      case L => Int
+    }
+
+    // This is testing that we don't make wrong assumptions about AnyRef
+    def right(fa: Bar[L]): Int = fa // error
+  }
+}

From 7e669b7e8eb96474e3a07eae5f79202ff5ec7a66 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 18 Apr 2019 14:14:40 +0200
Subject: [PATCH 06/11] Don't special case bottom

---
 compiler/src/dotty/tools/dotc/core/Types.scala | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index d403aa1dd183..2697abb3ff51 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3823,8 +3823,7 @@ object Types {
         myReduced =
           trace(i"reduce match type $this $hashCode", typr, show = true) {
             try
-              if (defn.isBottomType(scrutinee)) defn.NothingType
-              else typeComparer.matchCases(scrutinee, cases)(trackingCtx)
+              typeComparer.matchCases(scrutinee, cases)(trackingCtx)
             catch {
               case ex: Throwable =>
                 handleRecursive("reduce type ", i"$scrutinee match ...", ex)

From 3f89e4cffb8678e9cf42635e693209bc14e4cec8 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 29 Apr 2019 16:36:23 +0200
Subject: [PATCH 07/11] Speed up runtime test

It timed out on my machine...
---
 tests/run/mapConserve.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/run/mapConserve.scala b/tests/run/mapConserve.scala
index 4c842b0a53e3..c5fa65a186d2 100644
--- a/tests/run/mapConserve.scala
+++ b/tests/run/mapConserve.scala
@@ -10,7 +10,7 @@ object Test {
 
   def checkStackOverflow() = {
     var xs: List[String] = Nil
-    for (i <- 0 until 250000)
+    for (i <- 0 until 250)
         xs = "X" :: xs
 
     val lowers = xs.mapConserve(_.toLowerCase)

From ace48a218099f65865d364b2b095e9562e54c619 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 29 Apr 2019 17:04:08 +0200
Subject: [PATCH 08/11] Add a subtype check with Wildcard types

This breaks tests/run/typeclass-derivation2c.scala
There is no way to statically know that the type passed to constValue reduces.
---
 .../tools/dotc/core/TypeApplications.scala    |  2 +-
 .../dotty/tools/dotc/core/TypeComparer.scala  | 15 +++++++++--
 tests/neg/6314-1.scala                        | 26 +++++++++++++++++++
 tests/run/typeclass-derivation2c.scala        |  5 ++--
 4 files changed, 43 insertions(+), 5 deletions(-)
 create mode 100644 tests/neg/6314-1.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
index 85c24a7dbe10..cb10510871f3 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -405,7 +405,7 @@ class TypeApplications(val self: Type) extends AnyVal {
       case dealiased: LazyRef =>
         LazyRef(c => dealiased.ref(c).appliedTo(args))
       case dealiased: WildcardType =>
-        WildcardType(dealiased.optBounds.appliedTo(args).bounds)
+        WildcardType(dealiased.optBounds.orElse(TypeBounds.empty).appliedTo(args).bounds)
       case dealiased: TypeRef if dealiased.symbol == defn.NothingClass =>
         dealiased
       case dealiased =>
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 14d312d0ec24..18b15e798c08 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2152,6 +2152,15 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
         case _ =>
           cas
       }
+      def widenAbstractTypes(tp: Type) = new TypeMap {
+        def apply(tp: Type) = tp match {
+          case tp: TypeRef if tp.symbol.isAbstractOrParamType | tp.symbol.isOpaqueAlias => WildcardType
+          case tp: TypeVar if !tp.isInstantiated => WildcardType
+          case _: SkolemType | _: TypeParamRef => WildcardType
+          case _ => mapOver(tp)
+        }
+      }.apply(tp)
+
       val defn.MatchCase(pat, body) = cas1
       if (isSubType(scrut, pat))
         // `scrut` is a subtype of `pat`: *It's a Match!*
@@ -2164,12 +2173,14 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
               body
           }
         }
-      else if (intersecting(scrut, pat))
+      else if (isSubType(widenAbstractTypes(scrut), widenAbstractTypes(pat)))
         Some(NoType)
-      else
+      else if (!intersecting(scrut, pat))
         // We found a proof that `scrut` and  `pat` are incompatible.
         // The search continues.
         None
+      else
+        Some(NoType)
     }
 
     def recur(cases: List[Type]): Type = cases match {
diff --git a/tests/neg/6314-1.scala b/tests/neg/6314-1.scala
new file mode 100644
index 000000000000..98adf3d3e644
--- /dev/null
+++ b/tests/neg/6314-1.scala
@@ -0,0 +1,26 @@
+object G {
+  final class X
+  final class Y
+
+  trait FooSig {
+    type Type
+    def apply[F[_]](fa: F[X & Y]): F[Y & Type]
+  }
+  val Foo: FooSig = new FooSig {
+    type Type = X & Y
+    def apply[F[_]](fa: F[X & Y]): F[Y & Type] = fa
+  }
+  type Foo = Foo.Type
+
+  type Bar[A] = A match {
+    case X & Y => String
+    case Y => Int
+  }
+
+  def main(args: Array[String]): Unit = {
+    val a: Bar[X & Y] = "hello"
+    val i: Bar[Y & Foo] = Foo.apply[Bar](a)
+    val b: Int = i // error
+    println(b + 1)
+  }
+}
diff --git a/tests/run/typeclass-derivation2c.scala b/tests/run/typeclass-derivation2c.scala
index eb4db03901df..aa0b5a5f8ece 100644
--- a/tests/run/typeclass-derivation2c.scala
+++ b/tests/run/typeclass-derivation2c.scala
@@ -305,8 +305,9 @@ object Pickler {
     }
 
   inline def unpickleProduct[T](g: Generic.Product[T])(buf: mutable.ListBuffer[Int]): T = {
-    inline val size = constValue[Tuple.Size[g.ElemTypes]]
-    val elems = new Array[Object](size)
+    // inline val size = constValue[Tuple.Size[g.ElemTypes]]
+    // val elems = new Array[Object](size)
+    val elems = new Array[Object](buf.size)
     unpickleElems[g.ElemTypes](0)(buf, elems)
     g.fromProduct(ArrayProduct(elems))
   }

From 0cec0956fea8e4114758a52cc1dbbfc6e9d701fe Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Mon, 29 Apr 2019 17:21:21 +0200
Subject: [PATCH 09/11] Add test cases from #6314

---
 tests/neg/6314-2.scala | 24 ++++++++++++++++++++++++
 tests/neg/6314-3.scala | 24 ++++++++++++++++++++++++
 tests/neg/6314-4.scala | 28 ++++++++++++++++++++++++++++
 tests/neg/6314-5.scala | 29 +++++++++++++++++++++++++++++
 tests/neg/6314.scala   | 25 +++++++++++++++++++++++++
 5 files changed, 130 insertions(+)
 create mode 100644 tests/neg/6314-2.scala
 create mode 100644 tests/neg/6314-3.scala
 create mode 100644 tests/neg/6314-4.scala
 create mode 100644 tests/neg/6314-5.scala

diff --git a/tests/neg/6314-2.scala b/tests/neg/6314-2.scala
new file mode 100644
index 000000000000..c47ae7a2a950
--- /dev/null
+++ b/tests/neg/6314-2.scala
@@ -0,0 +1,24 @@
+object G {
+  final class X
+  final class Y
+
+  opaque type Foo = Nothing // or X & Y
+  object Foo {
+    def apply[F[_]](fa: F[X & Foo]): F[Y & Foo] = fa
+  }
+
+  type Bar[A] = A match {
+    case X => String
+    case Y => Int
+  }
+
+  val a: Bar[X & Foo] = "hello"
+  val b: Bar[Y & Foo] = 1 // error
+
+  def main(args: Array[String]): Unit = {
+    val a: Bar[X & Foo] = "hello"
+    val i: Bar[Y & Foo] = Foo.apply[Bar](a)
+    val b: Int = i // error
+    println(b + 1)
+  }
+}
diff --git a/tests/neg/6314-3.scala b/tests/neg/6314-3.scala
new file mode 100644
index 000000000000..8e6fa390f40f
--- /dev/null
+++ b/tests/neg/6314-3.scala
@@ -0,0 +1,24 @@
+object G {
+    trait Wizzle[L <: Int with Singleton] {
+        type Bar[A] = A match {
+            case 0 => String
+            case L => Int
+        }
+
+        def left(fa: String): Bar[0] = fa
+        def right(fa: Bar[L]): Int = fa // error
+
+        def center[F[_]](fa: F[0]): F[L]
+
+        def run: String => Int = left andThen center[Bar] andThen right
+    }
+
+    class Wozzle extends Wizzle[0] {
+        def center[F[_]](fa: F[0]): F[0] = fa
+    }
+
+    def main(args: Array[String]): Unit = {
+        val coerce: String => Int = (new Wozzle).run
+        println(coerce("hello") + 1)
+    }
+}
diff --git a/tests/neg/6314-4.scala b/tests/neg/6314-4.scala
new file mode 100644
index 000000000000..6b97efd590c2
--- /dev/null
+++ b/tests/neg/6314-4.scala
@@ -0,0 +1,28 @@
+object G {
+    trait Wizzle {
+        type X <: Int with Singleton
+        type Y <: Int with Singleton
+
+        type Bar[A] = A match {
+            case X => String
+            case Y => Int
+        }
+
+        def left(fa: String): Bar[X] = fa
+        def center[F[_]](fa: F[X]): F[Y]
+        def right(fa: Bar[Y]): Int = fa // error
+
+        def run: String => Int = left andThen center[Bar] andThen right
+    }
+
+    class Wozzle extends Wizzle {
+        type X = 0
+        type Y = 0
+        def center[F[_]](fa: F[X]): F[Y] = fa
+    }
+
+    def main(args: Array[String]): Unit = {
+        val coerce: String => Int = (new Wozzle).run
+        println(coerce("hello") + 1)
+    }
+}
diff --git a/tests/neg/6314-5.scala b/tests/neg/6314-5.scala
new file mode 100644
index 000000000000..4dbaf60219b9
--- /dev/null
+++ b/tests/neg/6314-5.scala
@@ -0,0 +1,29 @@
+object G {
+  type Void <: Nothing
+  trait Wizzle {
+    type Razzle[+X >: Void]
+    type X = 0
+    type Y = 1
+
+    type Bar[A] = A match {
+      case Razzle[X] => String
+      case Razzle[Y] => Int
+    }
+
+    def left(fa: String): Bar[Razzle[X]] = fa
+    def center[F[_]](fa: F[Razzle[X]]): F[Razzle[Y]]
+    def right(fa: Bar[Razzle[Y]]): Int = fa // error
+
+    def run: String => Int = left andThen center[Bar] andThen right
+  }
+
+  class Wozzle extends Wizzle {
+    type Razzle[+X >: Void] = Int
+    def center[F[_]](fa: F[Razzle[X]]): F[Razzle[Y]] = fa
+  }
+
+  def main(args: Array[String]): Unit = {
+    val coerce: String => Int = (new Wozzle).run
+    println(coerce("hello") + 1)
+  }
+}
diff --git a/tests/neg/6314.scala b/tests/neg/6314.scala
index beee41c48e9a..c12dc2a5f630 100644
--- a/tests/neg/6314.scala
+++ b/tests/neg/6314.scala
@@ -46,3 +46,28 @@ object Test2 {
     def right(fa: Bar[L]): Int = fa // error
   }
 }
+
+
+object Test3 {
+  type Bar[A] = A match {
+    case X => String
+    case Y => Int
+  }
+
+  trait XX {
+    type Foo
+
+    val a: Bar[X & Foo] = "hello"
+    val b: Bar[Y & Foo] = 1 // error
+
+    def apply(fa: Bar[X & Foo]): Bar[Y & Foo]
+
+    def boom: Int = apply(a) // error
+  }
+
+  trait YY extends XX {
+    type Foo = X & Y
+
+    def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa
+  }
+}

From 96bd9db7a8cd6b07756bc2ed1c97b8703d011a0a Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 9 May 2019 12:01:33 +0200
Subject: [PATCH 10/11] Refactor intersecting as disjoint

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 74 +++++++++----------
 .../tools/dotc/transform/patmat/Space.scala   |  8 +-
 2 files changed, 40 insertions(+), 42 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 18b15e798c08..913f30c1ff19 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1895,9 +1895,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
   /** Returns last check's debug mode, if explicitly enabled. */
   def lastTrace(): String = ""
 
-  /** Do `tp1` and `tp2` share a non-null inhabitant?
+  /** Are `tp1` and `tp2` disjoint types?
    *
-   *  `false` implies that we found a proof; uncertainty default to `true`.
+   *  `true` implies that we found a proof; uncertainty default to `false`.
    *
    *  Proofs rely on the following properties of Scala types:
    *
@@ -1906,8 +1906,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
    *  3. ConstantTypes with distinc values are non intersecting
    *  4. There is no value of type Nothing
    */
-  def intersecting(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
-    // println(s"intersecting(${tp1.show}, ${tp2.show})")
+  def disjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
+    // println(s"disjoint(${tp1.show}, ${tp2.show})")
     /** Can we enumerate all instantiations of this type? */
     def isClosedSum(tp: Symbol): Boolean =
       tp.is(Sealed) && tp.is(AbstractOrTrait) && !tp.hasAnonymousChild
@@ -1921,34 +1921,34 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
 
     (tp1.dealias, tp2.dealias) match {
       case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol == defn.SingletonClass || tp2.symbol == defn.SingletonClass =>
-        true
+        false
       case (tp1: ConstantType, tp2: ConstantType) =>
-        tp1 == tp2
+        tp1 != tp2
       case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
         val cls1 = tp1.classSymbol
         val cls2 = tp2.classSymbol
         if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)) {
-          true
+          false
         } else {
           if (cls1.is(Final) || cls2.is(Final))
             // One of these types is final and they are not mutually
             // subtype, so they must be unrelated.
-            false
+            true
           else if (!cls2.is(Trait) && !cls1.is(Trait))
             // Both of these types are classes and they are not mutually
             // subtype, so they must be unrelated by single inheritance
             // of classes.
-            false
+            true
           else if (isClosedSum(cls1))
-            decompose(cls1, tp1).exists(x => intersecting(x, tp2))
+            decompose(cls1, tp1).forall(x => disjoint(x, tp2))
           else if (isClosedSum(cls2))
-            decompose(cls2, tp2).exists(x => intersecting(x, tp1))
+            decompose(cls2, tp2).forall(x => disjoint(x, tp1))
           else
-            true
+            false
         }
       case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
-        def covariantIntersecting(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = {
-          intersecting(tp1, tp2) || {
+        def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = {
+          disjoint(tp1, tp2) && {
             // We still need to proof that `Nothing` is not a valid
             // instantiation of this type parameter. We have two ways
             // to get to that conclusion:
@@ -1966,21 +1966,21 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
                 case _ =>
                   false
               }
-            lowerBoundedByNothing && !typeUsedAsField
+            !lowerBoundedByNothing || typeUsedAsField
           }
         }
 
-        (args1, args2, tycon1.typeParams).zipped.forall {
+        (args1, args2, tycon1.typeParams).zipped.exists {
           (arg1, arg2, tparam) =>
             val v = tparam.paramVariance
             if (v > 0)
-              covariantIntersecting(arg1, arg2, tparam)
+              covariantDisjoint(arg1, arg2, tparam)
             else if (v < 0)
               // Contravariant case: a value where this type parameter is
               // instantiated to `Any` belongs to both types.
-              true
+              false
             else
-              covariantIntersecting(arg1, arg2, tparam) && (isSameType(arg1, arg2) || {
+              covariantDisjoint(arg1, arg2, tparam) || !isSameType(arg1, arg2) && {
                 // We can only trust a "no" from `isSameType` when both
                 // `arg1` and `arg2` are fully instantiated.
                 def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] {
@@ -1993,37 +1993,35 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
                       }
                     }
                 }.apply(true, tp)
-                !(fullyInstantiated(arg1) && fullyInstantiated(arg2))
-              })
+                fullyInstantiated(arg1) && fullyInstantiated(arg2)
+              }
         }
       case (tp1: HKLambda, tp2: HKLambda) =>
-        intersecting(tp1.resType, tp2.resType)
+        disjoint(tp1.resType, tp2.resType)
       case (_: HKLambda, _) =>
-        // The intersection is ill kinded and therefore empty.
-        false
+        // The intersection of these two types would be ill kinded, they are therefore disjoint.
+        true
       case (_, _: HKLambda) =>
-        false
+        true
       case (tp1: OrType, _)  =>
-        intersecting(tp1.tp1, tp2) || intersecting(tp1.tp2, tp2)
+        disjoint(tp1.tp1, tp2) && disjoint(tp1.tp2, tp2)
       case (_, tp2: OrType)  =>
-        intersecting(tp1, tp2.tp1) || intersecting(tp1, tp2.tp2)
+        disjoint(tp1, tp2.tp1) && disjoint(tp1, tp2.tp2)
       case (tp1: AndType, tp2: AndType) =>
-        intersecting(tp1.tp1, tp2.tp1) && intersecting(tp1.tp2, tp2.tp2) ||
-        intersecting(tp1.tp1, tp2.tp2) && intersecting(tp1.tp2, tp2.tp1)
+        (disjoint(tp1.tp1, tp2.tp1) || disjoint(tp1.tp2, tp2.tp2)) &&
+        (disjoint(tp1.tp1, tp2.tp2) || disjoint(tp1.tp2, tp2.tp1))
       case (tp1: AndType, _) =>
-        intersecting(tp1.tp1, tp2) && intersecting(tp1.tp2, tp2) ||
-        intersecting(tp1.tp2, tp2) && intersecting(tp1.tp1, tp2)
+        disjoint(tp1.tp2, tp2) || disjoint(tp1.tp1, tp2)
       case (_, tp2: AndType) =>
-        intersecting(tp1, tp2.tp1) && intersecting(tp1, tp2.tp2) ||
-        intersecting(tp1, tp2.tp2) && intersecting(tp1, tp2.tp1)
+        disjoint(tp1, tp2.tp2) || disjoint(tp1, tp2.tp1)
       case (tp1: TypeProxy, tp2: TypeProxy) =>
-        intersecting(tp1.underlying, tp2) && intersecting(tp1, tp2.underlying)
+        disjoint(tp1.underlying, tp2) || disjoint(tp1, tp2.underlying)
       case (tp1: TypeProxy, _) =>
-        intersecting(tp1.underlying, tp2)
+        disjoint(tp1.underlying, tp2)
       case (_, tp2: TypeProxy) =>
-        intersecting(tp1, tp2.underlying)
+        disjoint(tp1, tp2.underlying)
       case _ =>
-        true
+        false
     }
   }
 }
@@ -2175,7 +2173,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
         }
       else if (isSubType(widenAbstractTypes(scrut), widenAbstractTypes(pat)))
         Some(NoType)
-      else if (!intersecting(scrut, pat))
+      else if (disjoint(scrut, pat))
         // We found a proof that `scrut` and  `pat` are incompatible.
         // The search continues.
         None
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index 06fcaa907870..c8fb617a65e6 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -299,11 +299,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       // Since projections of types don't include null, intersection with null is empty.
       return Empty
     }
-    val res = ctx.typeComparer.intersecting(tp1, tp2)
+    val res = ctx.typeComparer.disjoint(tp1, tp2)
 
-    debug.println(s"atomic intersection: ${AndType(tp1, tp2).show} = ${res}")
+    debug.println(s"atomic intersection: ${AndType(tp1, tp2).show} = ${!res}")
 
-    if (!res) Empty
+    if (res) Empty
     else if (tp1.isSingleton) Typ(tp1, true)
     else if (tp2.isSingleton) Typ(tp2, true)
     else Typ(AndType(tp1, tp2), true)
@@ -498,7 +498,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
           def inhabited(tp: Type): Boolean =
             tp.dealias match {
-              case AndType(tp1, tp2) => ctx.typeComparer.intersecting(tp1, tp2)
+              case AndType(tp1, tp2) => !ctx.typeComparer.disjoint(tp1, tp2)
               case OrType(tp1, tp2) => inhabited(tp1) || inhabited(tp2)
               case tp: RefinedType => inhabited(tp.parent)
               case tp: TypeRef => inhabited(tp.prefix)

From 74ca923de5a5986e4be3944e73c178dc06f2f10c Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Thu, 9 May 2019 16:05:01 +0200
Subject: [PATCH 11/11] Follow type aliases in widenAbstractTypes

SeklomType are already mapped over correctly, that is, as .info.
---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 15 ++++++++---
 tests/neg/6314.scala                          | 25 +++++++++++++++++++
 2 files changed, 37 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 913f30c1ff19..8efb2a403e05 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2150,11 +2150,20 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
         case _ =>
           cas
       }
-      def widenAbstractTypes(tp: Type) = new TypeMap {
+      def widenAbstractTypes(tp: Type): Type = new TypeMap {
         def apply(tp: Type) = tp match {
-          case tp: TypeRef if tp.symbol.isAbstractOrParamType | tp.symbol.isOpaqueAlias => WildcardType
+          case tp: TypeRef =>
+            if (tp.symbol.isAbstractOrParamType | tp.symbol.isOpaqueAlias)
+              WildcardType
+            else tp.info match {
+              case TypeAlias(alias) =>
+                val alias1 = widenAbstractTypes(alias)
+                if (alias1 ne alias) alias1 else tp
+              case _ => mapOver(tp)
+            }
+
           case tp: TypeVar if !tp.isInstantiated => WildcardType
-          case _: SkolemType | _: TypeParamRef => WildcardType
+          case _: TypeParamRef => WildcardType
           case _ => mapOver(tp)
         }
       }.apply(tp)
diff --git a/tests/neg/6314.scala b/tests/neg/6314.scala
index c12dc2a5f630..03e3d22a26c0 100644
--- a/tests/neg/6314.scala
+++ b/tests/neg/6314.scala
@@ -71,3 +71,28 @@ object Test3 {
     def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa
   }
 }
+
+object Test4 {
+  type Bar[A] = A match {
+    case X => String
+    case Y => Int
+  }
+
+  trait XX {
+    type Foo
+    type FooAlias = Foo
+
+    val a: Bar[X & FooAlias] = "hello"
+    val b: Bar[Y & FooAlias] = 1 // error
+
+    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias]
+
+    def boom: Int = apply(a) // error
+  }
+
+  trait YY extends XX {
+    type Foo = X & Y
+
+    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa
+  }
+}