From 1f9812eba1eaa9679d4c542c9df96b3b696681ac Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 25 Aug 2021 14:05:37 +0800
Subject: [PATCH 1/2] Fix inFrozenGadtIf

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

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index b568cb2c8af8..e46165ac3db3 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/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
   }
 

From c3893895464a8564104e5c8a6e691ade61864701 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 25 Aug 2021 14:09:47 +0800
Subject: [PATCH 2/2] Add neg test

---
 tests/neg/gadt-injectivity-alt-2.scala | 35 ++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 tests/neg/gadt-injectivity-alt-2.scala

diff --git a/tests/neg/gadt-injectivity-alt-2.scala b/tests/neg/gadt-injectivity-alt-2.scala
new file mode 100644
index 000000000000..a48555d557f8
--- /dev/null
+++ b/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
+            ()
+          }
+        }
+      }
+    }
+}