diff --git a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
index ef97028efd75..2faf721a9da8 100644
--- a/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/GadtConstraint.scala
@@ -124,7 +124,7 @@ final class ProperGadtConstraint private(
 
     // The replaced symbols are picked up here.
     addToConstraint(poly1, tvars)
-      .reporting(i"added to constraint: $params%, %\n$debugBoundsDescription", gadts)
+      .reporting(i"added to constraint: [$poly1] $params%, %\n$debugBoundsDescription", gadts)
   }
 
   override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = {
@@ -237,8 +237,11 @@ final class ProperGadtConstraint private(
      }
 
    override def fullUpperBound(param: TypeParamRef)(implicit ctx: Context): Type =
-     constraint.minUpper(param).foldLeft(nonParamBounds(param).hi) {
-       (t, u) => t & externalize(u)
+     constraint.minUpper(param).foldLeft(nonParamBounds(param).hi) { (t, u) =>
+       val eu = externalize(u)
+       // Any as the upper bound means "no bound", but if F is higher-kinded,
+       // Any & F = F[_]; this is wrong for us so we need to short-circuit
+       if t.isAny then eu else t & eu
      }
 
   // ---- Private ----------------------------------------------------------
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 8b38b489983c..0e4dd994a286 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/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,40 @@ 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) && {
-                    // check both tycons to deal with the case when they are equal b/c of GADT constraint
-                    val tyconIsInjective = tycon1sym.isClass || tycon2sym.isClass
+                    tycon1sym == tycon2sym
+                      && isSubType(tycon1.prefix, tycon2.prefix)
+                      || byGadtBounds(tycon1sym, tycon2, fromAbove = true)
+                      || byGadtBounds(tycon2sym, tycon1, fromAbove = false)
+                  ) && {
+                    // 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)
                     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
diff --git a/tests/neg/gadt-injectivity-alt.scala b/tests/neg/gadt-injectivity-alt.scala
new file mode 100644
index 000000000000..4e8574c7bba5
--- /dev/null
+++ b/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
+            ()
+          }
+        }
+      }
+    }
+}
diff --git a/tests/neg/gadt-uninjectivity.scala b/tests/neg/gadt-uninjectivity.scala
index 30ebac32b735..ca305031556d 100644
--- a/tests/neg/gadt-uninjectivity.scala
+++ b/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
-      ???
+      ()
   }
 }
diff --git a/tests/neg/gadt-variant-hkt.scala b/tests/neg/gadt-variant-hkt.scala
new file mode 100644
index 000000000000..a8279ed7868f
--- /dev/null
+++ b/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
+            ()
+        }
+    }
+
+}
diff --git a/tests/pos/gadt-hk-ordering.scala b/tests/pos/gadt-hk-ordering.scala
new file mode 100644
index 000000000000..f2b17a917c71
--- /dev/null
+++ b/tests/pos/gadt-hk-ordering.scala
@@ -0,0 +1,16 @@
+object test {
+
+  enum KSUB[-F[_], +G[_]] {
+    case Refl[S[_]]() extends KSUB[S, S]
+  }
+
+  def foo[F[_]](ksub: Option KSUB F) =
+    ksub match {
+      case KSUB.Refl() =>
+        // we have (s is type parameter of KSUB.Refl):
+        // f >: Option
+        // s <: f
+        val fi: F[Int] = Option(0)
+        ()
+    }
+}
diff --git a/tests/pos/gadt-hkt-usage.scala b/tests/pos/gadt-hkt-usage.scala
new file mode 100644
index 000000000000..3dcb127f1590
--- /dev/null
+++ b/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 _ =>
+    }
+  }
+}
diff --git a/tests/pos/gadt-variant-hkt.scala b/tests/pos/gadt-variant-hkt.scala
new file mode 100644
index 000000000000..22c94393ef40
--- /dev/null
+++ b/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]
+            ()
+        }
+    }
+
+}