One more test for new injectivity logic

And a comment to boot.

Author: abgruszecki

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

@@ -872,7 +872,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
                       || byGadtBounds(tycon1sym, tycon2, fromAbove = true)
                       || byGadtBounds(tycon2sym, tycon1, fromAbove = false)
                   ) && {
-                    // check both tycons to deal with the case when they are equal b/c of GADT constraint
+                    // There are two cases in which we can assume injectivity.
+                    // First we check if either sym is a class.
+                    // Then:
+                    // 1) if we didn't touch GADTs, then both symbols are the same
+                    //    (b/c of an earlier condition) and both are the same class
+                    // 2) if we touched GADTs, then the _other_ symbol (class syms
+                    //    cannot have GADT constraints), the one w/ GADT cstrs,
+                    //    must be instantiated, making the two tycons equal
                     val tyconIsInjective =
                       (tycon1sym.isClass || tycon2sym.isClass)
                         && (if touchedGADTs then gadtIsInstantiated else true)

tests/neg/gadt-injectivity-alt.scala

@@ -0,0 +1,33 @@
+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[A] SUB G[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[a] <: g[I]
+            // =X=>
+            // a <: I
+            // counterexample: g = [t] => Any
+            val i: Int = a // error
+            ()
+          }
+        }
+      }
+    }
+}

tests/pos/gadt-hk-ordering.scala

@@ -4,11 +4,6 @@ object test {
     case Refl[S[_]]() extends KSUB[S, S]
   }
 
-  enum Thing[+F[_]] {
-    case LBOption() extends Thing[Option];
-    case
-  }
-
   def foo[F[_]](ksub: Option KSUB F) =
     ksub match {
       case KSUB.Refl() =>