From c2147daf63155e5b8fc94dfce3cf7a73822c1f94 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Tue, 13 Apr 2021 18:34:26 +0200
Subject: [PATCH 1/2] Fix i11545

---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 23 ++++++++++++-------
 tests/neg/i11545.scala                        | 13 +++++++++++
 tests/neg/i11545a.scala                       | 20 ++++++++++++++++
 3 files changed, 48 insertions(+), 8 deletions(-)
 create mode 100644 tests/neg/i11545.scala
 create mode 100644 tests/neg/i11545a.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 62b06aea39a7..22bd900913bc 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -736,14 +736,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         fourthTry
     }
 
-    def tryBaseType(cls2: Symbol) = {
-      val base = nonExprBaseType(tp1, cls2)
-      if (base.exists && (base `ne` tp1))
-        isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) ||
-        base.isInstanceOf[OrType] && fourthTry
-          // if base is a disjunction, this might have come from a tp1 type that
-          // expands to a match type. In this case, we should try to reduce the type
-          // and compare the redux. This is done in fourthTry
+    def tryBaseType(cls2: Symbol): Boolean = {
+      // nonExprBaseType approximates its result in ways that are unsound for GADTs
+      // when it handles intersections. See neg/i11545a.scala for a specific example.
+      // Note that we can't simply freeze GADTs at this point. PatternTypeConstrainer
+      // passes a Skolem here and we _need_ to calculate its base type. Only intersection
+      // types are a problem.
+      if !(ctx.mode.is(Mode.GadtConstraintInference) && tp1.isInstanceOf[AndType]) then
+        val base = nonExprBaseType(tp1, cls2)
+        if (base.exists && (base `ne` tp1))
+          isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) ||
+          base.isInstanceOf[OrType] && fourthTry
+            // if base is a disjunction, this might have come from a tp1 type that
+            // expands to a match type. In this case, we should try to reduce the type
+            // and compare the redux. This is done in fourthTry
+        else fourthTry
       else fourthTry
     }
 
diff --git a/tests/neg/i11545.scala b/tests/neg/i11545.scala
new file mode 100644
index 000000000000..566a4105538f
--- /dev/null
+++ b/tests/neg/i11545.scala
@@ -0,0 +1,13 @@
+@main def test: Unit = {
+  trait S[A]
+  trait Inv[A]
+
+  class P[X] extends S[Inv[X] & Inv[String]]
+
+  def patmat[A, Y](s: S[Inv[A] & Y]): A = s match {
+    case p: P[x] =>
+      "Hello" // error
+  }
+
+  val got: Int = patmat[Int, Inv[String]](new P) // ClassCastException: String cannot be cast to Integer
+}
diff --git a/tests/neg/i11545a.scala b/tests/neg/i11545a.scala
new file mode 100644
index 000000000000..0be54e59d1ed
--- /dev/null
+++ b/tests/neg/i11545a.scala
@@ -0,0 +1,20 @@
+@main def test: Unit = {
+  trait Inv[A]
+
+  trait S[+A]
+  final class P[+X] extends S[Inv[String] & X]
+
+
+  def patmat[A](s: S[Inv[A]]): A = s match {
+    // When inferring the GADT cstr here, we need to infer cstr following from:
+    //   Inv[String] & a <: Inv[A]
+    // We end up invoking nonExprBaseType(`Inv[String] & a`, `Inv`),
+    // which returns just `Inv[String]`. After that we approximate with:
+    //   Inv[String] <: Inv[A]
+    // Which is simply wrong.
+    case p: P[a] => "Hello" // error
+  }
+
+  val i: Int = patmat[Int](P[Inv[Int]]())
+  i
+}

From c06739be0f49cf5acdc0e4183359db7dfac077a9 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Sat, 1 May 2021 16:15:24 +0200
Subject: [PATCH 2/2] Consider useNecessaryEither

---
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 22bd900913bc..0aa0e1d4383d 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -742,7 +742,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       // Note that we can't simply freeze GADTs at this point. PatternTypeConstrainer
       // passes a Skolem here and we _need_ to calculate its base type. Only intersection
       // types are a problem.
-      if !(ctx.mode.is(Mode.GadtConstraintInference) && tp1.isInstanceOf[AndType]) then
+      if !((ctx.mode.is(Mode.GadtConstraintInference) || useNecessaryEither)
+           && tp1.isInstanceOf[AndType]) then
         val base = nonExprBaseType(tp1, cls2)
         if (base.exists && (base `ne` tp1))
           isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) ||