Merge pull request #13380 from Linyxus/fix/frozen-gadt

Fix unsound injectivity assumption when inferring GADT bounds

Author: abgruszecki

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -172,7 +172,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
 
   private inline def inFrozenGadtIf[T](cond: Boolean)(inline op: T): T = {
     val savedFrozenGadt = frozenGadt
-    frozenGadt = cond
+    frozenGadt ||= cond
     try op finally frozenGadt = savedFrozenGadt
   }
 

tests/neg/gadt-injectivity-alt-2.scala

@@ -0,0 +1,35 @@
+/** A modified version of gadt-injectivity-alt.scala. */
+object test {
+
+  enum SUB[-F, +G] {
+    case Refl[S]() extends SUB[S, S]
+  }
+
+  enum KSUB[-F[_], +G[_]] {
+    case Refl[S[_]]() extends KSUB[S, S]
+  }
+
+  def foo[F[_], G[_], A](
+    keq: (F KSUB Option, Option KSUB F),
+    ksub: Option KSUB G,
+    sub: F[Option[A]] SUB G[Option[Int]],
+    a: A
+  ) =
+    keq._1 match { case KSUB.Refl() =>
+      keq._2 match { case KSUB.Refl() =>
+        ksub match { case KSUB.Refl() =>
+          sub match { case SUB.Refl() =>
+            //        F        =  Option
+            // &      G       >: Option
+            // & F[Option[A]] <: G[Option[Int]]
+            // =X=>
+            // A <: Int
+            //
+            // counterexample: G = [T] => Any
+            val i: Int = a // error
+            ()
+          }
+        }
+      }
+    }
+}