Make HKT GADT constraints actually work

Fix gadt-uninjectivity test, as it wasn't clear what it was actually
testing.

Author: abgruszecki

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

@@ -146,12 +146,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    */
   private [this] var leftRoot: Type = _
 
-  /** Are we forbidden from recording GADT constraints?
-   *
-   *  This flag is set when we're already in [[Mode.GadtConstraintInference]],
-   *  to signify that we temporarily cannot record any GADT constraints.
-   */
+  /** Are we forbidden from recording GADT constraints? */
   private var frozenGadt = false
+  private inline def inFrozenGadt[T](op: => T): T = {
+    val savedFrozenGadt = frozenGadt
+    frozenGadt = true
+    try op finally frozenGadt = savedFrozenGadt
+  }
 
   protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = {
     val savedApprox = approx
@@ -852,30 +853,33 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
                   val tycon2sym = tycon2.symbol
 
                   var touchedGADTs = false
-                  def gadtBoundsContain(sym: Symbol, tp: Type): Boolean = {
+                  var gadtIsInstantiated = false
+                  def byGadtBounds(sym: Symbol, tp: Type, fromAbove: Boolean): Boolean = {
                     touchedGADTs = true
                     val b = gadtBounds(sym)
-                    b != null && inFrozenConstraint {
-                      (b.lo =:= tp) && (b.hi =:= tp)
+                    def boundsDescr = if b == null then "null" else b.show
+                    b != null && inFrozenGadt {
+                      if fromAbove then isSubType(b.hi, tp) else isSubType(tp, b.lo)
+                    } && {
+                      gadtIsInstantiated = b.isInstanceOf[TypeAlias]
+                      true
                     }
                   }
 
                   val res = (
-                    tycon1sym == tycon2sym ||
-                    gadtBoundsContain(tycon1sym, tycon2) ||
-                    gadtBoundsContain(tycon2sym, tycon1)
-                  ) &&
-                  isSubType(tycon1.prefix, tycon2.prefix) && {
+                    tycon1sym == tycon2sym
+                      && isSubType(tycon1.prefix, tycon2.prefix)
+                      || 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
-                    val tyconIsInjective = tycon1sym.isClass || tycon2sym.isClass
+                    val tyconIsInjective =
+                      (tycon1sym.isClass || tycon2sym.isClass)
+                        && (if touchedGADTs then gadtIsInstantiated else true)
                     def checkSubArgs() = isSubArgs(args1, args2, tp1, tparams)
-                    // we only record GADT constraints if tycon is guaranteed to be injective
+                    // we only record GADT constraints if *both* tycons are effectively injective
                     if (tyconIsInjective) checkSubArgs()
-                    else {
-                      val savedFrozenGadt = frozenGadt
-                      frozenGadt = true
-                      try checkSubArgs() finally frozenGadt = savedFrozenGadt
-                    }
+                    else inFrozenGadt { checkSubArgs() }
                   }
                   if (res && touchedGADTs) GADTused = true
                   res

tests/neg/gadt-uninjectivity.scala

@@ -7,18 +7,16 @@ object uninjectivity {
       x // error
   }
 
-  def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fi: F[Int], fs: F[String]): G[Int] = eq match {
+  def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fs: F[String]) = eq match {
     case Refl() =>
       val gs: G[String] = fs // error
-      // fi
-      ???
+      ()
   }
 
-  def absurd3[F[_], G[_], X, Y](eq: EQ[F[X], G[Y]], fx: F[X]): G[Y] = eq match {
+  def absurd3[F[_], G[_], X, Y](eq: EQ[F[X], G[Y]], fx: F[X]) = eq match {
     case Refl() =>
       val gx: G[X] = fx // error
       val fy: F[Y] = fx // error
-      // fx
-      ???
+      ()
   }
 }

tests/neg/gadt-variant-hkt.scala

@@ -0,0 +1,39 @@
+object test {
+
+  enum SUB[T, U] {
+    case Refl[S]() extends SUB[S, S]
+  }
+
+  // injective(G) & f[S] <: G[S]  =X=> \forall t. f[t] <: Option[t]
+  def foo[F[_]](fi: F[Int], sub: F[String] SUB Option[String]): Option[Int] =
+    sub match {
+      case SUB.Refl() =>
+        fi // error
+    }
+
+  // injective(G) & f[x] <: G[S]  =X=> x <: S
+  def bar[F[_], X](x: X, fi: F[Int], sub: F[X] SUB Option[Int]): Option[Int] =
+    sub match {
+      case SUB.Refl() =>
+        val i: Int = x // error
+        val y: X = (0: Int) // error
+        fi // error
+    }
+
+  enum KSUB[-F[_], +G[_]] {
+    case Refl[S[_]]() extends KSUB[S, S]
+  }
+
+  // injective(G) & f <: G & f[x] <: G[T] =X=> x <: T
+  def baz[F[_], X](x: X, ksub: F KSUB Option, sub: F[X] SUB Option[Int]) =
+    ksub match {
+      case KSUB.Refl() =>
+        sub match {
+          case SUB.Refl() =>
+            val i: Int = x // error
+            val y: X = (0: Int) // error
+            ()
+        }
+    }
+
+}

tests/pos/gadt-hkt-usage.scala

@@ -0,0 +1,13 @@
+object test {
+  class Foo[A]
+  class Inv[M[_]]
+  class InvFoo extends Inv[Foo]
+
+  object Test {
+    def foo[F[_]](x: Inv[F]) = x match {
+      case x: InvFoo =>
+        val z: F[Int] = ??? : Foo[Int]
+      case _ =>
+    }
+  }
+}

tests/pos/gadt-variant-hkt.scala

@@ -0,0 +1,32 @@
+object test {
+
+  enum KSUB[-F[_], +G[_]] {
+    case Refl[S[_]]() extends KSUB[S, S]
+  }
+
+  trait Mkr[F[_]] {
+    def mk[T](t: T): F[T]
+  }
+
+  def foo[F[_]](mkr: Mkr[F], sub: F KSUB Option): Option[Int] =
+    sub match {
+      case KSUB.Refl() =>
+        mkr.mk(0)
+    }
+
+  enum SUB[T, U] {
+    case Refl[S]() extends SUB[S, S]
+  }
+
+  // f <: g & x <: T ==> f[x] <: g[T]
+  def bar[F[_], G[_], X](fx: F[X], ksub: F KSUB G, sub: X SUB Int) =
+    ksub match {
+      case _: KSUB.Refl[s] =>
+        sub match {
+          case SUB.Refl() =>
+            val gi: G[Int] = fx : s[X]
+            ()
+        }
+    }
+
+}