diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala
index b212e3cbfcfb..a0a8d7e705cc 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -779,6 +779,13 @@ object Contexts {
         }, gadts)
       }
 
+      bound match {
+        case _: SkolemType =>
+          val TypeBounds(lo, hi) = bounds(sym)
+          return if (isUpper) lo <:< (hi & bound) else (lo | bound) <:< hi
+        case _ => ;
+      }
+
       val symTvar: TypeVar = stripInternalTypeVar(tvar(sym)) match {
         case tv: TypeVar => tv
         case inst =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 438249f89124..20c7235dd8a7 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1039,7 +1039,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
      *   - If a type proxy P is not a reference to a class, P's supertype is in G
      */
     def isSubTypeOfParent(subtp: Type, tp: Type)(implicit ctx: Context): Boolean =
-      if (constrainPatternType(subtp, tp)) true
+      if (constrainPatternType(SkolemType(subtp), tp)) true
       else tp match {
         case tp: TypeRef if tp.symbol.isClass => isSubTypeOfParent(subtp, tp.firstParent)
         case tp: TypeProxy => isSubTypeOfParent(subtp, tp.superType)
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index f426aa1562ad..593cc2e83394 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -584,7 +584,7 @@ class Typer extends Namer
       def handlePattern: Tree = {
         val tpt1 = typedTpt
         if (!ctx.isAfterTyper && pt != defn.ImplicitScrutineeTypeRef)
-          constrainPatternType(tpt1.tpe, pt)(ctx.addMode(Mode.GADTflexible))
+          constrainPatternType(SkolemType(tpt1.tpe), pt)(ctx.addMode(Mode.GADTflexible))
         // special case for an abstract type that comes with a class tag
         tryWithClassTag(ascription(tpt1, isWildcard = true), pt)
       }
@@ -1026,7 +1026,7 @@ class Typer extends Namer
     val accu = new TypeAccumulator[Set[Symbol]] {
       def apply(tsyms: Set[Symbol], t: Type): Set[Symbol] = {
         val tsyms1 = t match {
-          case tr: TypeRef if (tr.symbol is TypeParam) && tr.symbol.owner.isTerm && variance == 0 =>
+          case tr: TypeRef if (tr.symbol is TypeParam) && tr.symbol.owner.isTerm =>
             tsyms + tr.symbol
           case _ =>
             tsyms
@@ -1041,7 +1041,11 @@ class Typer extends Namer
   def gadtContext(gadtSyms: Set[Symbol])(implicit ctx: Context): Context = {
     val gadtCtx = ctx.fresh.setFreshGADTBounds
     for (sym <- gadtSyms)
-      if (!gadtCtx.gadt.contains(sym)) gadtCtx.gadt.addEmptyBounds(sym)
+      if (!gadtCtx.gadt.contains(sym)) {
+        val TypeBounds(lo, hi) = sym.info.bounds
+        gadtCtx.gadt.addBound(sym, lo, isUpper = false)
+        gadtCtx.gadt.addBound(sym, hi, isUpper = true)
+      }
     gadtCtx
   }
 
diff --git a/tests/neg/int-extractor.scala b/tests/neg/int-extractor.scala
new file mode 100644
index 000000000000..a31ef9cc1c36
--- /dev/null
+++ b/tests/neg/int-extractor.scala
@@ -0,0 +1,31 @@
+object Test {
+  object EssaInt {
+    def unapply(i: Int): Some[Int] = Some(i)
+  }
+
+  def foo1[T](t: T) = t match {
+    case EssaInt(_) =>
+      0 // error
+  }
+
+  def foo2[T](t: T) = t match {
+    case EssaInt(_) => t match {
+      case EssaInt(_) =>
+        0 // error
+    }
+  }
+
+  case class Inv[T](t: T)
+
+  def bar1[T](t: T) = Inv(t) match {
+    case Inv(EssaInt(_)) =>
+      0 // error
+  }
+
+  def bar2[T](t: T) = t match {
+    case Inv(EssaInt(_)) => t match {
+      case Inv(EssaInt(_)) =>
+        0 // error
+    }
+  }
+}
diff --git a/tests/neg/invariant-gadt.scala b/tests/neg/invariant-gadt.scala
new file mode 100644
index 000000000000..ac335f57743f
--- /dev/null
+++ b/tests/neg/invariant-gadt.scala
@@ -0,0 +1,27 @@
+object `invariant-gadt` {
+  case class Invariant[T](value: T)
+
+  def unsound0[T](t: T): T = Invariant(t) match {
+    case Invariant(_: Int) =>
+      (0: Any) // error
+  }
+
+  def unsound1[T](t: T): T = Invariant(t) match {
+    case Invariant(_: Int) =>
+      0 // error
+  }
+
+  def unsound2[T](t: T): T = Invariant(t) match {
+    case Invariant(value) => value match {
+      case _: Int =>
+        0 // error
+    }
+  }
+
+  def unsoundTwice[T](t: T): T = Invariant(t) match {
+    case Invariant(_: Int) => Invariant(t) match {
+      case Invariant(_: Int) =>
+        0 // error
+    }
+  }
+}
diff --git a/tests/pos/precise-pattern-type.scala b/tests/pos/precise-pattern-type.scala
new file mode 100644
index 000000000000..856672fafbf2
--- /dev/null
+++ b/tests/pos/precise-pattern-type.scala
@@ -0,0 +1,16 @@
+object `precise-pattern-type` {
+  class Type {
+    def isType: Boolean = true
+  }
+
+  class Tree[-T >: Null] {
+    def tpe: T @annotation.unchecked.uncheckedVariance = ???
+  }
+
+  case class Select[-T >: Null](qual: Tree[T]) extends Tree[T]
+
+  def test[T <: Tree[Type]](tree: T) = tree match {
+    case Select(q) =>
+      q.tpe.isType
+  }
+}
diff --git a/tests/run/typeclass-derivation2.scala b/tests/run/typeclass-derivation2.scala
index 69863715976f..83cce0261817 100644
--- a/tests/run/typeclass-derivation2.scala
+++ b/tests/run/typeclass-derivation2.scala
@@ -1,6 +1,14 @@
 import scala.collection.mutable
 import scala.annotation.tailrec
 
+object _typelevel {
+  final abstract class Type[-A, +B]
+  type Subtype[t] = Type[_, t]
+  type Supertype[t] = Type[t, _]
+  type Exactly[t] = Type[t, t]
+  erased def typeOf[T]: Type[T, T] = ???
+}
+
 trait Deriving {
   import Deriving._
 
@@ -177,6 +185,7 @@ trait Eq[T] {
 object Eq {
   import scala.typelevel._
   import Deriving._
+  import _typelevel._
 
   inline def tryEql[T](x: T, y: T) = implicit match {
     case eq: Eq[T] => eq.eql(x, y)
@@ -197,14 +206,19 @@ object Eq {
   inline def eqlCases[T, Alts <: Tuple](r: Reflected[T], x: T, y: T): Boolean =
     inline erasedValue[Alts] match {
       case _: (Shape.Case[alt, elems] *: alts1) =>
-        x match {
-          case x: `alt` =>
-            y match {
-              case y: `alt` => eqlCase[T, elems](r, x, y)
-              case _ => false
+        inline typeOf[alt] match {
+          case _: Subtype[T] =>
+            x match {
+              case x: `alt` =>
+                y match {
+                  case y: `alt` => eqlCase[T, elems](r, x, y)
+                  case _ => false
+                }
+              case _ => eqlCases[T, alts1](r, x, y)
             }
-          case _ => eqlCases[T, alts1](r, x, y)
-      }
+          case _ =>
+            error("invalid call to eqlCases: one of Alts is not a subtype of T")
+        }
     case _: Unit =>
       false
   }
@@ -232,6 +246,7 @@ trait Pickler[T] {
 object Pickler {
   import scala.typelevel._
   import Deriving._
+  import _typelevel._
 
   def nextInt(buf: mutable.ListBuffer[Int]): Int = try buf.head finally buf.trimStart(1)
 
@@ -253,12 +268,17 @@ object Pickler {
   inline def pickleCases[T, Alts <: Tuple](r: Reflected[T], buf: mutable.ListBuffer[Int], x: T, n: Int): Unit =
     inline erasedValue[Alts] match {
       case _: (Shape.Case[alt, elems] *: alts1) =>
-        x match {
-          case x: `alt` =>
-            buf += n
-            pickleCase[T, elems](r, buf, x)
+        inline typeOf[alt] match {
+          case _: Subtype[T] =>
+            x match {
+              case x: `alt` =>
+                buf += n
+                pickleCase[T, elems](r, buf, x)
+              case _ =>
+                pickleCases[T, alts1](r, buf, x, n + 1)
+            }
           case _ =>
-            pickleCases[T, alts1](r, buf, x, n + 1)
+            error("invalid pickleCases call: one of Alts is not a subtype of T")
         }
       case _: Unit =>
     }
@@ -323,6 +343,7 @@ trait Show[T] {
 object Show {
   import scala.typelevel._
   import Deriving._
+  import _typelevel._
 
   inline def tryShow[T](x: T): String = implicit match {
     case s: Show[T] => s.show(x)
@@ -347,9 +368,14 @@ object Show {
   inline def showCases[T, Alts <: Tuple](r: Reflected[T], x: T): String =
     inline erasedValue[Alts] match {
       case _: (Shape.Case[alt, elems] *: alts1) =>
-        x match {
-          case x: `alt` => showCase[T, elems](r, x)
-          case _ => showCases[T, alts1](r, x)
+        inline typeOf[alt] match {
+          case _: Subtype[T] =>
+            x match {
+              case x: `alt` => showCase[T, elems](r, x)
+              case _ => showCases[T, alts1](r, x)
+            }
+          case _ =>
+            error("invalid call to showCases: one of Alts is not a subtype of T")
         }
       case _: Unit =>
         throw new MatchError(x)
@@ -424,4 +450,4 @@ object Test extends App {
     println(implicitly[Show[T]].show(x))
   showPrintln(xs)
   showPrintln(xss)
-}
\ No newline at end of file
+}