From d25f03c3c188aa23af278fa2d471588e785e2fea Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Wed, 22 May 2019 15:57:55 +0200
Subject: [PATCH 1/9] Rework how GADT constraints are inferred

GADT constraints are now inferred with an intersection-inspired
algorithm.

Inferencing.constrainPatternType was moved to PatternTypeConstrainer
to organize the code better.
---
 .../dotc/core/PatternTypeConstrainer.scala    | 206 ++++++++++++++++++
 .../dotty/tools/dotc/core/TypeComparer.scala  |   4 +-
 .../dotty/tools/dotc/typer/Applications.scala |  27 +--
 .../dotty/tools/dotc/typer/Inferencing.scala  |  60 -----
 .../src/dotty/tools/dotc/typer/Typer.scala    |   2 +-
 tests/neg/nontrivial-intersection-gadt.scala  |  22 ++
 .../overconstrained-abstract-type-gadt.scala  |  14 ++
 .../overconstrained-type-variables-gadt.scala |  17 ++
 tests/neg/unsound-covariant-gadt.scala        |  10 +
 tests/neg/unsound-union-gadt.scala            |  13 ++
 tests/pos/nontrivial-intersection-gadt.scala  |  22 ++
 tests/pos/precise-pattern-type.scala          |  16 ++
 tests/pos/pseudo-thistype-constraints.scala   |  12 +
 13 files changed, 340 insertions(+), 85 deletions(-)
 create mode 100644 compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
 create mode 100644 tests/neg/nontrivial-intersection-gadt.scala
 create mode 100644 tests/neg/overconstrained-abstract-type-gadt.scala
 create mode 100644 tests/neg/overconstrained-type-variables-gadt.scala
 create mode 100644 tests/neg/unsound-covariant-gadt.scala
 create mode 100644 tests/neg/unsound-union-gadt.scala
 create mode 100644 tests/pos/nontrivial-intersection-gadt.scala
 create mode 100644 tests/pos/pseudo-thistype-constraints.scala

diff --git a/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
new file mode 100644
index 000000000000..f20a9b7906f0
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
@@ -0,0 +1,206 @@
+package dotty.tools
+package dotc
+package core
+
+import Decorators._
+import Symbols._
+import Types._
+import Flags._
+import dotty.tools.dotc.reporting.trace
+import config.Printers._
+
+trait PatternTypeConstrainer { self: TypeComparer =>
+
+  /** Derive type and GADT constraints that necessarily follow from a pattern with the given type matching
+   *  a scrutinee of the given type.
+   *
+   *  We have the following situation in case of a (dynamic) pattern match:
+   *
+   *       StaticScrutineeType           PatternType
+   *                         \            /
+   *                      DynamicScrutineeType
+   *
+   *  In simple cases, it must hold that `PatternType <: StaticScrutineeType`:
+   *
+   *            StaticScrutineeType
+   *                  |         \
+   *                  |          PatternType
+   *                  |         /
+   *               DynamicScrutineeType
+   *
+   *  A good example of a situation where the above must hold is when static scrutinee type is the root of an enum,
+   *  and the pattern is an unapply of a case class, or a case object literal (of that enum).
+   *
+   *  In slightly more complex cases, we may need to upcast `StaticScrutineeType`:
+   *
+   *           SharedPatternScrutineeSuperType
+   *                  /         \
+   *   StaticScrutineeType       PatternType
+   *                  \         /
+   *               DynamicScrutineeType
+   *
+   *  This may be the case if the scrutinee is a singleton type or a path-dependent type. It is also the case
+   *  for the following definitions:
+   *
+   *     trait Expr[T]
+   *     trait IntExpr extends Expr[T]
+   *     trait Const[T] extends Expr[T]
+   *
+   *     StaticScrutineeType = Const[T]
+   *     PatternType = IntExpr
+   *
+   *  Union and intersection types are an additional complication - if either scrutinee or pattern are a union type,
+   *  then the above relationships only need to hold for the "leaves" of the types.
+   *
+   *  Finally, if pattern type contains hk-types applied to concrete types (as opposed to type variables),
+   *  or either scrutinee or pattern type contain type member refinements, the above relationships do not need
+   *  to hold at all. Consider (where `T1`, `T2` are unrelated traits):
+   *
+   *     StaticScrutineeType = { type T <: T1 }
+   *     PatternType = { type T <: T2 }
+   *
+   *  In the above situation, DynamicScrutineeType can equal { type T = T1 & T2 }, but there is no useful relationship
+   *  between StaticScrutineeType and PatternType (nor any of their subcomponents). Similarly:
+   *
+   *     StaticScrutineeType = Option[T1]
+   *     PatternType = Some[T2]
+   *
+   *  Again, DynamicScrutineeType may equal Some[T1 & T2], and there's no useful relationship between the static
+   *  scrutinee and pattern types. This does not apply if the pattern type is only applied to type variables,
+   *  in which case the subtyping relationship "heals" the type.
+   */
+  def constrainPatternType(pat: Type, scrut: Type): Boolean = trace(i"constrainPatternType($scrut, $pat)", gadts) {
+
+    def classesMayBeCompatible: Boolean = {
+      import Flags._
+      val patClassSym = pat.widenSingleton.classSymbol
+      val scrutClassSym = scrut.widenSingleton.classSymbol
+      !patClassSym.exists || !scrutClassSym.exists || {
+        if (patClassSym.is(Final)) patClassSym.derivesFrom(scrutClassSym)
+        else if (scrutClassSym.is(Final)) scrutClassSym.derivesFrom(patClassSym)
+        else if (!patClassSym.is(Flags.Trait) && !scrutClassSym.is(Flags.Trait))
+          patClassSym.derivesFrom(scrutClassSym) || scrutClassSym.derivesFrom(patClassSym)
+        else true
+      }
+    }
+
+    def stripRefinement(tp: Type): Type = tp match {
+      case tp: RefinedOrRecType => stripRefinement(tp.parent)
+      case tp => tp
+    }
+
+    def constrainUpcasted(scrut: Type): Boolean = trace(i"constrainUpcasted($scrut)", gadts) {
+      val upcasted: Type = scrut match {
+        case scrut: TypeRef if scrut.symbol.isClass =>
+          // we do not infer constraints following from all parents for performance reasons
+          // in principle however, if `A extends B, C`, then `A` can be treated as `B & C`
+          scrut.firstParent
+        case scrut @ AppliedType(tycon: TypeRef, _) if tycon.symbol.isClass =>
+          val patClassSym = pat.classSymbol
+          // as above, we do not consider all parents for performance reasons
+          def firstParentSharedWithPat(tp: Type, tpClassSym: ClassSymbol): Symbol = {
+            var parents = tpClassSym.info.parents
+            parents match {
+              case first :: rest =>
+                if (first.classSymbol == defn.ObjectClass) parents = rest
+              case _ => ;
+            }
+            parents match {
+              case first :: _ =>
+                val firstClassSym = first.classSymbol.asClass
+                val res = if (patClassSym.derivesFrom(firstClassSym)) firstClassSym
+                else firstParentSharedWithPat(first, firstClassSym)
+                res
+              case _ => NoSymbol
+            }
+          }
+          val sym = firstParentSharedWithPat(tycon, tycon.symbol.asClass)
+          if (sym.exists) scrut.baseType(sym) else NoType
+        case scrut: TypeProxy => scrut.superType
+        case _ => NoType
+      }
+      if (upcasted.exists)
+        constrainSimplePatternType(pat, upcasted) || constrainUpcasted(upcasted)
+      else true
+    }
+
+    scrut.dealias match {
+      case OrType(scrut1, scrut2) =>
+        either(constrainPatternType(pat, scrut1), constrainPatternType(pat, scrut2))
+      case AndType(scrut1, scrut2) =>
+        constrainPatternType(pat, scrut1) && constrainPatternType(pat, scrut2)
+      case scrut: RefinedOrRecType =>
+        constrainPatternType(pat, stripRefinement(scrut))
+      case scrut => pat.dealias match {
+        case OrType(pat1, pat2) =>
+          either(constrainPatternType(pat1, scrut), constrainPatternType(pat2, scrut))
+        case AndType(pat1, pat2) =>
+          constrainPatternType(pat1, scrut) && constrainPatternType(pat2, scrut)
+        case scrut: RefinedOrRecType =>
+          constrainPatternType(stripRefinement(scrut), pat)
+        case pat =>
+          constrainSimplePatternType(pat, scrut) || classesMayBeCompatible && constrainUpcasted(scrut)
+      }
+    }
+  }
+
+  /** Constrain "simple" patterns (see `constrainPatternType`).
+   *
+   *  This function attempts to modify pattern and scrutinee type s.t. the pattern must be a subtype of the scrutinee,
+   *  or otherwise it cannot possibly match. In order to do that, we:
+   *
+   *  1. Rely on `constrainPatternType` to break the actual scrutinee/pattern types into subcomponents
+   *  2. Widen type parameters of scrutinee type that are not invariantly refined (see below) by the pattern type.
+   *  3. Wrap the pattern type in a skolem to avoid overconstraining top-level abstract types in scrutinee type
+   *  4. Check that `WidenedScrutineeType <: NarrowedPatternType`
+   *
+   *  Importantly, note that the pattern type may contain type variables.
+   *
+   *  ## Invariant refinement
+   *  Essentially, we say that `D[B] extends C[B]` s.t. refines parameter `A` of `trait C[A]` invariantly if
+   *  when `c: C[T]` and `c` is instance of `D`, then necessarily `c: D[T]`. This is violated if `A` is variant:
+   *
+   *     trait C[+A]
+   *     trait D[+B](val b: B) extends C[B]
+   *     trait E extends D[Any](0) with C[String]
+   *
+   *  `E` is a counter-example to the above - if `e: E`, then `e: C[String]` and `e` is instance of `D`, but
+   *  it is false that `e: D[String]`! This is a problem if we're constraining a pattern like the below:
+   *
+   *     def foo[T](c: C[T]): T = c match {
+   *       case d: D[t] => d.b
+   *     }
+   *
+   *  It'd be unsound for us to say that `t <: T`, even though that follows from `D[t] <: C[T]`.
+   *  Note, however, that if `D` was a final class, we *could* rely on that relationship.
+   *  To support typical case classes, we also assume that this relationship holds for them and their parent traits.
+   *  This is enforced by checking that classes inheriting from case classes do not extend the parent traits of those
+   *  case classes without also appropriately extending the relevant case class
+   *  (see `RefChecks#checkCaseClassInheritanceInvariant`).
+   */
+  def constrainSimplePatternType(patternTp: Type, scrutineeTp: Type): Boolean = {
+    def refinementIsInvariant(tp: Type): Boolean = tp match {
+      case tp: ClassInfo => tp.cls.is(Final) || tp.cls.is(Case)
+      case tp: TypeProxy => refinementIsInvariant(tp.underlying)
+      case _ => false
+    }
+
+    def widenVariantParams = new TypeMap {
+      def apply(tp: Type) = mapOver(tp) match {
+        case tp @ AppliedType(tycon, args) =>
+          val args1 = args.zipWithConserve(tycon.typeParams)((arg, tparam) =>
+            if (tparam.paramVariance != 0) TypeBounds.empty else arg
+          )
+          tp.derivedAppliedType(tycon, args1)
+        case tp =>
+          tp
+      }
+    }
+
+    val widePt = if (ctx.scala2Mode || refinementIsInvariant(patternTp)) scrutineeTp else widenVariantParams(scrutineeTp)
+    val narrowTp = SkolemType(patternTp)
+    trace(i"constraining simple pattern type $narrowTp <:< $widePt", gadts, res => s"$res\ngadt = ${ctx.gadt.debugBoundsDescription}") {
+      isSubType(narrowTp, widePt)
+    }
+  }
+}
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 83d1aadf93e9..b5dc30f122e2 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -25,7 +25,7 @@ object AbsentContext {
 
 /** Provides methods to compare types.
  */
-class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
+class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] with PatternTypeConstrainer {
   import TypeComparer._
   implicit def ctx(implicit nc: AbsentContext): Context = initctx
 
@@ -1227,7 +1227,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
    *  @see [[sufficientEither]] for the normal case
    *  @see [[necessaryEither]] for the GADTFlexible case
    */
-  private def either(op1: => Boolean, op2: => Boolean): Boolean =
+  protected def either(op1: => Boolean, op2: => Boolean): Boolean =
     if (ctx.mode.is(Mode.GADTflexible)) necessaryEither(op1, op2) else sufficientEither(op1, op2)
 
   /** Returns true iff the result of evaluating either `op1` or `op2` is true,
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index c9b930b37bbb..c53886aa45ce 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1085,21 +1085,6 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
 
     def fromScala2x = unapplyFn.symbol.exists && (unapplyFn.symbol.owner is Scala2x)
 
-    /** Is `subtp` a subtype of `tp` or of some generalization of `tp`?
-     *  The generalizations of a type T are the smallest set G such that
-     *
-     *   - T is in G
-     *   - If a typeref R in G represents a class or trait, R's superclass is in G.
-     *   - 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
-      else tp match {
-        case tp: TypeRef if tp.symbol.isClass => isSubTypeOfParent(subtp, tp.firstParent)
-        case tp: TypeProxy => isSubTypeOfParent(subtp, tp.superType)
-        case _ => false
-      }
-
     unapplyFn.tpe.widen match {
       case mt: MethodType if mt.paramInfos.length == 1 =>
         val unapplyArgType = mt.paramInfos.head
@@ -1109,17 +1094,15 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
             unapp.println(i"case 1 $unapplyArgType ${ctx.typerState.constraint}")
             fullyDefinedType(unapplyArgType, "pattern selector", tree.span)
             selType.dropAnnot(defn.UncheckedAnnot) // need to drop @unchecked. Just because the selector is @unchecked, the pattern isn't.
-          } else if (isSubTypeOfParent(unapplyArgType, selType)(ctx.addMode(Mode.GADTflexible))) {
+          } else {
+            // note that we simply ignore whether constraining actually succeeded or not
+            // in theory, constraining should only fail if the pattern cannot possibly match
+            // however, during exhaustivity checks, we perform a strictly better check
+            ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(unapplyArgType, selType)
             val patternBound = maximizeType(unapplyArgType, tree.span, fromScala2x)
             if (patternBound.nonEmpty) unapplyFn = addBinders(unapplyFn, patternBound)
             unapp.println(i"case 2 $unapplyArgType ${ctx.typerState.constraint}")
             unapplyArgType
-          } else {
-            unapp.println("Neither sub nor super")
-            unapp.println(TypeComparer.explained(implicit ctx => unapplyArgType <:< selType))
-            errorType(
-              ex"Pattern type $unapplyArgType is neither a subtype nor a supertype of selector type $selType",
-              tree.sourcePos)
           }
         val dummyArg = dummyTreeOfType(ownType)
         val unapplyApp = typedExpr(untpd.TypedSplice(Apply(unapplyFn, dummyArg :: Nil)))
diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
index 1f697678f6ff..fbf04a1bf87c 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -180,66 +180,6 @@ object Inferencing {
   def isSkolemFree(tp: Type)(implicit ctx: Context): Boolean =
     !tp.existsPart(_.isInstanceOf[SkolemType])
 
-  /** Derive information about a pattern type by comparing it with some variant of the
-   *  static scrutinee type. We have the following situation in case of a (dynamic) pattern match:
-   *
-   *       StaticScrutineeType           PatternType
-   *                         \            /
-   *                      DynamicScrutineeType
-   *
-   *  If `PatternType` is not a subtype of `StaticScrutineeType, there's no information to be gained.
-   *  Now let's say we can prove that `PatternType <: StaticScrutineeType`.
-   *
-   *            StaticScrutineeType
-   *                  |         \
-   *                  |          \
-   *                  |           \
-   *                  |            PatternType
-   *                  |          /
-   *               DynamicScrutineeType
-   *
-   *  What can we say about the relationship of parameter types between `PatternType` and
-   *  `DynamicScrutineeType`?
-   *
-   *   - If `DynamicScrutineeType` refines the type parameters of `StaticScrutineeType`
-   *     in the same way as `PatternType` ("invariant refinement"), the subtype test
-   *     `PatternType <:< StaticScrutineeType` tells us all we need to know.
-   *   - Otherwise, if variant refinement is a possibility we can only make predictions
-   *     about invariant parameters of `StaticScrutineeType`. Hence we do a subtype test
-   *     where `PatternType <: widenVariantParams(StaticScrutineeType)`, where `widenVariantParams`
-   *     replaces all type argument of variant parameters with empty bounds.
-   *
-   *  Invariant refinement can be assumed if `PatternType`'s class(es) are final or
-   *  case classes (because of `RefChecks#checkCaseClassInheritanceInvariant`).
-   */
-  def constrainPatternType(tp: Type, pt: Type)(implicit ctx: Context): Boolean = {
-    def refinementIsInvariant(tp: Type): Boolean = tp match {
-      case tp: ClassInfo => tp.cls.is(Final) || tp.cls.is(Case)
-      case tp: TypeProxy => refinementIsInvariant(tp.underlying)
-      case tp: AndType => refinementIsInvariant(tp.tp1) && refinementIsInvariant(tp.tp2)
-      case tp: OrType => refinementIsInvariant(tp.tp1) && refinementIsInvariant(tp.tp2)
-      case _ => false
-    }
-
-    def widenVariantParams = new TypeMap {
-      def apply(tp: Type) = mapOver(tp) match {
-        case tp @ AppliedType(tycon, args) =>
-          val args1 = args.zipWithConserve(tycon.typeParams)((arg, tparam) =>
-            if (tparam.paramVariance != 0) TypeBounds.empty else arg
-          )
-          tp.derivedAppliedType(tycon, args1)
-        case tp =>
-          tp
-      }
-    }
-
-    val widePt = if (ctx.scala2Mode || refinementIsInvariant(tp)) pt else widenVariantParams(pt)
-    val narrowTp = SkolemType(tp)
-    trace(i"constraining pattern type $narrowTp <:< $widePt", gadts, res => s"$res\n${ctx.gadt.debugBoundsDescription}") {
-      narrowTp <:< widePt
-    }
-  }
-
   /** The list of uninstantiated type variables bound by some prefix of type `T` which
    *  occur in at least one formal parameter type of a prefix application.
    *  Considered prefixes are:
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 52b315025376..3fea8ab0eff0 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -607,7 +607,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))
+          ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(tpt1.tpe, pt)
         // special case for an abstract type that comes with a class tag
         tryWithClassTag(ascription(tpt1, isWildcard = true), pt)
       }
diff --git a/tests/neg/nontrivial-intersection-gadt.scala b/tests/neg/nontrivial-intersection-gadt.scala
new file mode 100644
index 000000000000..c8d5aa9975cb
--- /dev/null
+++ b/tests/neg/nontrivial-intersection-gadt.scala
@@ -0,0 +1,22 @@
+object Test {
+  trait Expr[+T]
+  trait IntExpr extends Expr[Int]
+  class Const[+T] extends Expr[T]
+  final class Fin
+
+  def foo1[T](x: Unit | Const[T]): T = x match {
+    case _: IntExpr => 0 // error
+  }
+
+  def bar1[T](x: Const[T]): T = x match {
+    case _: (Unit | IntExpr) => 0 // error
+  }
+
+  def foo2[T](x: Fin | Const[T]): T = x match {
+    case _: IntExpr => 0 // error
+  }
+
+  def bar2[T](x: Const[T]): T = x match {
+    case _: (Fin | IntExpr) => 0 // error
+  }
+}
diff --git a/tests/neg/overconstrained-abstract-type-gadt.scala b/tests/neg/overconstrained-abstract-type-gadt.scala
new file mode 100644
index 000000000000..1d8b08f243d9
--- /dev/null
+++ b/tests/neg/overconstrained-abstract-type-gadt.scala
@@ -0,0 +1,14 @@
+trait Test {
+  type A
+
+  enum Foo[X, Y] {
+    case StrStr() extends Foo[String, String]
+    case IntInt() extends Foo[Int, Int]
+  }
+
+  def foo[T, U](f: Foo[A, T] | Foo[String, U]): Unit =
+    f match { case Foo.StrStr() =>
+      val t: T = "" // error
+      val u: U = "" // error
+    }
+}
diff --git a/tests/neg/overconstrained-type-variables-gadt.scala b/tests/neg/overconstrained-type-variables-gadt.scala
new file mode 100644
index 000000000000..bda23070946c
--- /dev/null
+++ b/tests/neg/overconstrained-type-variables-gadt.scala
@@ -0,0 +1,17 @@
+object Test {
+  trait T1[A] { def a: A }
+  trait T2[B] { def b: B }
+
+  def foo[X, Y](u: T1[X] | T2[Y]): X = u match {
+    case t1: T1[t] =>
+      // consider: foo[Int, String](new T1[String] with T2[String] { ... })
+      t1.a // error
+  }
+
+  class T1Int extends T1[Int] { def a = 0 }
+  def bar[X, Y](u: T1[X] | T2[Y]): X = u match {
+    case t1: T1Int =>
+      // similar reasoning to above applies
+      t1.a // error
+  }
+}
diff --git a/tests/neg/unsound-covariant-gadt.scala b/tests/neg/unsound-covariant-gadt.scala
new file mode 100644
index 000000000000..e8dcb14a5eee
--- /dev/null
+++ b/tests/neg/unsound-covariant-gadt.scala
@@ -0,0 +1,10 @@
+object Test {
+  sealed trait Expr[+T]
+  case class IntVal[+T <: Int]() extends Expr[T]
+  case object ActualInt extends Expr[Int]
+  def eval[T](e: Expr[T]): T = e match {
+    case IntVal() => 0 // error
+    case ActualInt => 0
+  }
+}
+
diff --git a/tests/neg/unsound-union-gadt.scala b/tests/neg/unsound-union-gadt.scala
new file mode 100644
index 000000000000..9412f1581e1a
--- /dev/null
+++ b/tests/neg/unsound-union-gadt.scala
@@ -0,0 +1,13 @@
+object Test {
+  enum Expr[+T] {
+    case StrLit() extends Expr[String]
+    case IntLit() extends Expr[Int]
+  }
+  import Expr._
+
+  def foo[T](e: Expr[T]) = e match {
+    case _: (StrLit | IntLit) =>
+      val str: T = "" // error
+      val int: T = 42 // error
+  }
+}
diff --git a/tests/pos/nontrivial-intersection-gadt.scala b/tests/pos/nontrivial-intersection-gadt.scala
new file mode 100644
index 000000000000..92862080f9ce
--- /dev/null
+++ b/tests/pos/nontrivial-intersection-gadt.scala
@@ -0,0 +1,22 @@
+object Test {
+  trait Expr[T]
+  trait IntExpr extends Expr[Int]
+  class Const[T] extends Expr[T]
+  final class Fin
+
+  def foo1[T](x: Unit | Const[T]): T = x match {
+    case _: IntExpr => 0
+  }
+
+  def bar1[T](x: Const[T]): T = x match {
+    case _: (Unit | IntExpr) => 0
+  }
+
+  def foo2[T](x: Fin | Const[T]): T = x match {
+    case _: IntExpr => 0
+  }
+
+  def bar2[T](x: Const[T]): T = x match {
+    case _: (Fin | IntExpr) => 0
+  }
+}
diff --git a/tests/pos/precise-pattern-type.scala b/tests/pos/precise-pattern-type.scala
index 856672fafbf2..e8c64f019313 100644
--- a/tests/pos/precise-pattern-type.scala
+++ b/tests/pos/precise-pattern-type.scala
@@ -13,4 +13,20 @@ object `precise-pattern-type` {
     case Select(q) =>
       q.tpe.isType
   }
+
+  trait O {
+    type ThisTree <: Tree[Type]
+    val tree: ThisTree
+    def test = tree match {
+      case Select(q) => q.tpe.isType
+      case tree1: Select[t] => (tree1 : Select[Type]).qual.tpe.isType
+    }
+  }
+
+  trait OO {
+    type ThisTree[T >: Null] <: Tree[T]
+    def foo(t: ThisTree[Type]) = t match {
+      case Select(q) => q.tpe.isType
+    }
+  }
 }
diff --git a/tests/pos/pseudo-thistype-constraints.scala b/tests/pos/pseudo-thistype-constraints.scala
new file mode 100644
index 000000000000..8bdb123847b2
--- /dev/null
+++ b/tests/pos/pseudo-thistype-constraints.scala
@@ -0,0 +1,12 @@
+object Test {
+  enum Expr[+T] {
+    case BoolLit(b: Boolean) extends Expr[Boolean]
+    def eval: T = {
+      def go[TT](self: this.type & Expr[TT]): TT = self match {
+        case BoolLit(b) => b
+      }
+
+      go(this)
+    }
+  }
+}

From 54047ba8204b8aa84dd1089438c80abc85c7ae5a Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Wed, 22 May 2019 15:58:46 +0200
Subject: [PATCH 2/9] Add type-member-based GADT test suite

These tests were meant to test inferring GADT constraints based on type
members, which we backed out of.

They are still useful to see if we don't do anything unsound when
type members are present.
---
 tests/neg/structural-gadt.scala               | 56 +++++++++++
 .../neg/structural-recursive-both1-gadt.scala | 93 +++++++++++++++++++
 .../neg/structural-recursive-both2-gadt.scala | 93 +++++++++++++++++++
 .../structural-recursive-pattern-gadt.scala   | 71 ++++++++++++++
 .../structural-recursive-scrutinee-gadt.scala | 81 ++++++++++++++++
 5 files changed, 394 insertions(+)
 create mode 100644 tests/neg/structural-gadt.scala
 create mode 100644 tests/neg/structural-recursive-both1-gadt.scala
 create mode 100644 tests/neg/structural-recursive-both2-gadt.scala
 create mode 100644 tests/neg/structural-recursive-pattern-gadt.scala
 create mode 100644 tests/neg/structural-recursive-scrutinee-gadt.scala

diff --git a/tests/neg/structural-gadt.scala b/tests/neg/structural-gadt.scala
new file mode 100644
index 000000000000..9a14881b5804
--- /dev/null
+++ b/tests/neg/structural-gadt.scala
@@ -0,0 +1,56 @@
+// This file is part of tests for inferring GADT constraints from type members,
+// which needed to be reverted because of soundness issues.
+//
+// Lines with "// limitation" are the ones that we could soundly allow.
+object Test {
+
+  trait Expr { type T }
+  trait IntLit extends Expr { type T <: Int }
+  trait IntExpr extends Expr { type T = Int }
+
+  def foo[A](e: Expr { type T = A }) = e match {
+    case _: IntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: Expr { type T <: Int } =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: Expr { type T = Int } =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+  }
+
+  def bar[A](e: Expr { type T <: A }) = e match {
+    case _: IntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: Expr { type T <: Int } =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: Expr { type T = Int } =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+
+  trait IndirectExprOfIntList extends Expr {
+    type T = U
+    type U <: List[Int]
+  }
+  def baz[A](e: Expr { type T <: List[A] }) = e match {
+    case _: IndirectExprOfIntList =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+  }
+}
diff --git a/tests/neg/structural-recursive-both1-gadt.scala b/tests/neg/structural-recursive-both1-gadt.scala
new file mode 100644
index 000000000000..97df59a92bb5
--- /dev/null
+++ b/tests/neg/structural-recursive-both1-gadt.scala
@@ -0,0 +1,93 @@
+// This file is part of tests for inferring GADT constraints from type members,
+// which needed to be reverted because of soundness issues.
+//
+// Lines with "// limitation" are the ones that we could soundly allow.
+object Test {
+
+  trait Expr { type T }
+  trait IntLit extends Expr { type T <: Int }
+  trait IntExpr extends Expr { type T = Int }
+
+  type ExprSub[+A] = Expr { type T <: A }
+  type ExprExact[A] = Expr { type T = A }
+
+  trait IndirectIntLit extends Expr { type S <: Int; type T = S }
+  trait IndirectIntExpr extends Expr { type S = Int; type T = S }
+
+  type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
+  type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
+  type IndirectExprExact[A] = Expr { type S = A; type T = S }
+
+  trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
+  trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
+
+  type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
+  type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
+  type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
+
+  def foo[A](e: IndirectExprExact[A]) = e match {
+    case _: AltIndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: AltIndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: AltIndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: AltIndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: AltIndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+  }
+
+  def bar[A](e: IndirectExprSub[A]) = e match {
+    case _: AltIndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+
+  def baz[A](e: IndirectExprSub2[A]) = e match {
+    case _: AltIndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: AltIndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+}
diff --git a/tests/neg/structural-recursive-both2-gadt.scala b/tests/neg/structural-recursive-both2-gadt.scala
new file mode 100644
index 000000000000..b58e05f3ed43
--- /dev/null
+++ b/tests/neg/structural-recursive-both2-gadt.scala
@@ -0,0 +1,93 @@
+// This file is part of tests for inferring GADT constraints from type members,
+// which needed to be reverted because of soundness issues.
+//
+// Lines with "// limitation" are the ones that we could soundly allow.
+object Test {
+
+  trait Expr { type T }
+  trait IntLit extends Expr { type T <: Int }
+  trait IntExpr extends Expr { type T = Int }
+
+  type ExprSub[+A] = Expr { type T <: A }
+  type ExprExact[A] = Expr { type T = A }
+
+  trait IndirectIntLit extends Expr { type S <: Int; type T = S }
+  trait IndirectIntExpr extends Expr { type S = Int; type T = S }
+
+  type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
+  type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
+  type IndirectExprExact[A] = Expr { type S = A; type T = S }
+
+  trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
+  trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
+
+  type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
+  type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
+  type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
+
+  def foo[A](e: AltIndirectExprExact[A]) = e match {
+    case _: IndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+  }
+
+  def bar[A](e: AltIndirectExprSub[A]) = e match {
+    case _: IndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+
+  def baz[A](e: AltIndirectExprSub2[A]) = e match {
+    case _: IndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+}
diff --git a/tests/neg/structural-recursive-pattern-gadt.scala b/tests/neg/structural-recursive-pattern-gadt.scala
new file mode 100644
index 000000000000..ea7394b5b66b
--- /dev/null
+++ b/tests/neg/structural-recursive-pattern-gadt.scala
@@ -0,0 +1,71 @@
+// This file is part of tests for inferring GADT constraints from type members,
+// which needed to be reverted because of soundness issues.
+//
+// Lines with "// limitation" are the ones that we could soundly allow.
+object Test {
+
+  trait Expr { type T }
+  trait IntLit extends Expr { type T <: Int }
+  trait IntExpr extends Expr { type T = Int }
+
+  type ExprSub[+A] = Expr { type T <: A }
+  type ExprExact[A] = Expr { type T = A }
+
+  trait IndirectIntLit extends Expr { type S <: Int; type T = S }
+  trait IndirectIntExpr extends Expr { type S = Int; type T = S }
+
+  type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
+  type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
+  type IndirectExprExact[A] = Expr { type S = A; type T = S }
+
+  trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
+  trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
+
+  type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
+  type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
+  type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
+
+  def foo[A](e: ExprExact[A]) = e match {
+    case _: IndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+  }
+
+  def bar[A](e: ExprSub[A]) = e match {
+    case _: IndirectIntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprSub2[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectIntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: IndirectExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+}
diff --git a/tests/neg/structural-recursive-scrutinee-gadt.scala b/tests/neg/structural-recursive-scrutinee-gadt.scala
new file mode 100644
index 000000000000..cd4e2376f49a
--- /dev/null
+++ b/tests/neg/structural-recursive-scrutinee-gadt.scala
@@ -0,0 +1,81 @@
+// This file is part of tests for inferring GADT constraints from type members,
+// which needed to be reverted because of soundness issues.
+//
+// Lines with "// limitation" are the ones that we could soundly allow.
+object Test {
+
+  trait Expr { type T }
+  trait IntLit extends Expr { type T <: Int }
+  trait IntExpr extends Expr { type T = Int }
+
+  type ExprSub[+A] = Expr { type T <: A }
+  type ExprExact[A] = Expr { type T = A }
+
+  trait IndirectIntLit extends Expr { type S <: Int; type T = S }
+  trait IndirectIntExpr extends Expr { type S = Int; type T = S }
+
+  type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
+  type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
+  type IndirectExprExact[A] = Expr { type S = A; type T = S }
+
+  trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
+  trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
+
+  type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
+  type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
+  type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
+
+  def foo[A](e: IndirectExprExact[A]) = e match {
+    case _: IntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: ExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: IntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+
+    case _: ExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // limitation // error
+  }
+
+  def bar[A](e: IndirectExprSub[A]) = e match {
+    case _: IntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: ExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: ExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+
+  def baz[A](e: IndirectExprSub2[A]) = e match {
+    case _: IntLit =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: ExprSub[Int] =>
+      val a: A = 0 // error
+      val i: Int = ??? : A // error
+
+    case _: IntExpr =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+
+    case _: ExprExact[Int] =>
+      val a: A = 0 // limitation // error
+      val i: Int = ??? : A // error
+  }
+}

From 32c4280d67ce1845d2cbc55bd7abcfd2d24475d5 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Wed, 22 May 2019 16:17:46 +0200
Subject: [PATCH 3/9] Do not rely on subtyping to infer constraints for object
 patterns

Fixed soundness problems with abstract types - see test.
---
 .../src/dotty/tools/dotc/typer/Typer.scala    |  2 +-
 tests/neg/unsound-union-object-gadt.scala     | 20 +++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/neg/unsound-union-object-gadt.scala

diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 3fea8ab0eff0..5dc8224d2a15 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -3153,7 +3153,7 @@ class Typer extends Namer
       case _: RefTree | _: Literal
         if !isVarPattern(tree) &&
            !(pt <:< tree.tpe) &&
-           !(tree.tpe <:< pt)(ctx.addMode(Mode.GADTflexible)) =>
+           !ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(tree.tpe, pt) =>
         val cmp =
           untpd.Apply(
             untpd.Select(untpd.TypedSplice(tree), nme.EQ),
diff --git a/tests/neg/unsound-union-object-gadt.scala b/tests/neg/unsound-union-object-gadt.scala
new file mode 100644
index 000000000000..81b55e7dc493
--- /dev/null
+++ b/tests/neg/unsound-union-object-gadt.scala
@@ -0,0 +1,20 @@
+object Test {
+  enum Foo[X] {
+    case Str extends Foo[String]
+    case Int extends Foo[Int]
+  }
+
+  trait Test {
+    type A
+
+    def foo[T](f: Foo[A] | Foo[T]): T =
+      f match { case Foo.Str =>
+        "" // error
+      }
+
+    def bar[T](f: Unit | Foo[T]): T =
+      f match { case Foo.Str =>
+        ""
+      }
+  }
+}

From 483285f2d08dfca87b3201c63ae7475aaf654b5e Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Wed, 22 May 2019 16:40:33 +0200
Subject: [PATCH 4/9] Take HKT injectivity into account when inferring GADT
 constraints

When going into arguments of a HKT, we only infer GADT constraints
if we are certain that tycon is injective.
---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 27 ++++++++---
 tests/neg/gadt-alias-injectivity.scala        | 48 +++++++++++++++++++
 tests/neg/gadt-uninjectivity.scala            |  2 +-
 tests/pos/gadt-EQK.scala                      | 12 -----
 tests/run/gadt-injectivity-unsoundness.scala  | 19 --------
 5 files changed, 70 insertions(+), 38 deletions(-)
 create mode 100644 tests/neg/gadt-alias-injectivity.scala
 delete mode 100644 tests/run/gadt-injectivity-unsoundness.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index b5dc30f122e2..b95659944e91 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -141,6 +141,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    */
   private [this] var leftRoot: Type = _
 
+  /** Are we forbidden from recording GADT constraints? */
+  private[this] var frozenGadt = false
+
   protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = {
     val savedApprox = approx
     val savedLeftRoot = leftRoot
@@ -840,8 +843,11 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
                     gadtBoundsContain(tycon1sym, tycon2) ||
                     gadtBoundsContain(tycon2sym, tycon1)
                   ) &&
-                  isSubType(tycon1.prefix, tycon2.prefix) &&
-                  isSubArgs(args1, args2, tp1, tparams)
+                  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
+                    isSubArgs(args1, args2, tp1, tparams, inferGadtBounds = tyconIsInjective)
+                  }
                   if (res && touchedGADTs) GADTused = true
                   res
                 case _ =>
@@ -1097,7 +1103,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  @param  tp1       The applied type containing `args1`
    *  @param  tparams2  The type parameters of the type constructor applied to `args2`
    */
-  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo]): Boolean = {
+  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo], inferGadtBounds: Boolean = false): Boolean = {
     /** The bounds of parameter `tparam`, where all references to type paramneters
      *  are replaced by corresponding arguments (or their approximations in the case of
      *  wildcard arguments).
@@ -1161,8 +1167,17 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
               case arg1: TypeBounds =>
                 compareCaptured(arg1, arg2)
               case _ =>
-                (v > 0 || isSubType(arg2, arg1)) &&
-                (v < 0 || isSubType(arg1, arg2))
+                def isSub(tp: Type, pt: Type): Boolean = {
+                  if (inferGadtBounds) isSubType(tp, pt)
+                  else {
+                    val savedFrozenGadt = frozenGadt
+                    frozenGadt = true
+                    try isSubType(tp, pt) finally frozenGadt = savedFrozenGadt
+                  }
+                }
+
+                (v > 0 || isSub(arg2, arg1)) &&
+                (v < 0 || isSub(arg1, arg2))
             }
         }
 
@@ -1476,7 +1491,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    */
   private def narrowGADTBounds(tr: NamedType, bound: Type, approx: ApproxState, isUpper: Boolean): Boolean = {
     val boundImprecise = approx.high || approx.low
-    ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && !boundImprecise && {
+    ctx.mode.is(Mode.GADTflexible) && !frozenGadt && !frozenConstraint && !boundImprecise && {
       val tparam = tr.symbol
       gadts.println(i"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.toString} ${bound.isRef(tparam)}")
       if (bound.isRef(tparam)) false
diff --git a/tests/neg/gadt-alias-injectivity.scala b/tests/neg/gadt-alias-injectivity.scala
new file mode 100644
index 000000000000..34203a45f4f8
--- /dev/null
+++ b/tests/neg/gadt-alias-injectivity.scala
@@ -0,0 +1,48 @@
+object Test {
+  enum EQ[A, B] {
+    case Refl[T]() extends EQ[T, T]
+  }
+  import EQ._
+
+  object A {
+    type Foo[+X] = (X, X)
+    def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match {
+      case Refl() => x
+    }
+  }
+
+  object B {
+    type Foo[X] = (X, X)
+    def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match {
+      case Refl() => x
+    }
+  }
+
+  object C {
+    type Foo[+X] = Int | (X, X)
+    def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match {
+      case Refl() => x
+    }
+  }
+
+  object D {
+    type Foo[+X] = (Int, Int)
+    def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match {
+      case Refl() => x // error
+    }
+  }
+
+  trait E {
+    type Foo[+X] <: Int | (X, X)
+    def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match {
+      case Refl() => x // error
+    }
+  }
+
+  trait F {
+    type Foo[X] >: Int | (X, X)
+    def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match {
+      case Refl() => x // error
+    }
+  }
+}
diff --git a/tests/neg/gadt-uninjectivity.scala b/tests/neg/gadt-uninjectivity.scala
index f1d0fc59000a..30ebac32b735 100644
--- a/tests/neg/gadt-uninjectivity.scala
+++ b/tests/neg/gadt-uninjectivity.scala
@@ -4,7 +4,7 @@ object uninjectivity {
 
   def absurd1[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match {
     case Refl() =>
-      x // should be an error
+      x // error
   }
 
   def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fi: F[Int], fs: F[String]): G[Int] = eq match {
diff --git a/tests/pos/gadt-EQK.scala b/tests/pos/gadt-EQK.scala
index b713de2d833b..0c1fbfe03f81 100644
--- a/tests/pos/gadt-EQK.scala
+++ b/tests/pos/gadt-EQK.scala
@@ -18,16 +18,4 @@ object EQK {
           fa : G[Int]
       }
     }
-
-  def m2[F[_], G[_], A](fa: F[A], a: A, eq: EQ[F[A], G[Int]], eqk: EQK[F, G]): Int =
-    eqk match {
-      case ReflK() => eq match {
-        case Refl() =>
-          val r1: F[Int] = fa
-          val r2: G[A] = fa
-          val r3: F[Int] = r2
-          a
-      }
-    }
-
 }
diff --git a/tests/run/gadt-injectivity-unsoundness.scala b/tests/run/gadt-injectivity-unsoundness.scala
deleted file mode 100644
index 192a82afb539..000000000000
--- a/tests/run/gadt-injectivity-unsoundness.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-object Test {
-  sealed trait EQ[A, B]
-  final case class Refl[T]() extends EQ[T, T]
-
-  def absurd[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match {
-    case Refl() => x
-  }
-
-  var ex: Exception = _
-  try {
-    type Unsoundness[X] = Int
-    val s: String = absurd[Unsoundness, Int, String](Refl(), 0)
-  } catch {
-    case e: ClassCastException => ex = e
-  }
-
-  def main(args: Array[String]) =
-    assert(ex != null)
-}

From 609ee7bd3bfa21fd2fe16725681315c55cd5716c Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Thu, 23 May 2019 10:07:55 +0200
Subject: [PATCH 5/9] Fix bias in ConstraintHandling#subsumes

Previously, if c2 had instantiated a variable, it would not be iterated
over and would not be compared with c1.
---
 .../dotty/tools/dotc/core/ConstraintHandling.scala |  2 +-
 .../neg/overconstrained-type-variables-gadt.scala  | 14 ++++++++++++--
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 1e9a8c5e5816..8a86d9abb598 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -345,7 +345,7 @@ trait ConstraintHandling[AbstractContext] {
     else {
       val saved = constraint
       try
-        c2.forallParams(p =>
+        pre.forallParams(p =>
           c1.contains(p) &&
           c2.upper(p).forall(c1.isLess(p, _)) &&
           isSubTypeWhenFrozen(c1.nonParamBounds(p), c2.nonParamBounds(p)))
diff --git a/tests/neg/overconstrained-type-variables-gadt.scala b/tests/neg/overconstrained-type-variables-gadt.scala
index bda23070946c..b8670f28e76b 100644
--- a/tests/neg/overconstrained-type-variables-gadt.scala
+++ b/tests/neg/overconstrained-type-variables-gadt.scala
@@ -2,16 +2,26 @@ object Test {
   trait T1[A] { def a: A }
   trait T2[B] { def b: B }
 
-  def foo[X, Y](u: T1[X] | T2[Y]): X = u match {
+  def foo[X, Y](v: T1[X] | T2[Y]): X = v match {
     case t1: T1[t] =>
       // consider: foo[Int, String](new T1[String] with T2[String] { ... })
       t1.a // error
   }
 
   class T1Int extends T1[Int] { def a = 0 }
-  def bar[X, Y](u: T1[X] | T2[Y]): X = u match {
+  def bar[X, Y](v: T1[X] | T2[Y]): X = v match {
     case t1: T1Int =>
       // similar reasoning to above applies
       t1.a // error
   }
+
+  class T1IntT2String extends T1[Int] with T2[String] {
+    def a = 0
+    def b = ""
+  }
+  def baz[X](v: T1[X] | T2[X]): Unit = v match {
+    case _: T1IntT2String =>
+      val x1: X = 0 // error
+      val x2: X = "" // error
+  }
 }

From a85cce4834dfd21393d65bf3b5cc2afdfdef5124 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Wed, 22 May 2019 19:16:47 +0200
Subject: [PATCH 6/9] Remove now untypeable exhaustivity test

---
 tests/patmat/3469.scala | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 tests/patmat/3469.scala

diff --git a/tests/patmat/3469.scala b/tests/patmat/3469.scala
deleted file mode 100644
index 8abad0252d11..000000000000
--- a/tests/patmat/3469.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-object O {
-  sealed trait Trait[+A] { type T }
-  case class CaseClass[+A](a: A) extends Trait[A] { type T = Nothing }
-
-  def id[TT, A](v: Trait[A] { type T = TT }): Trait[A] { type T = TT } =
-    v match {
-      case CaseClass(a) => CaseClass(a)
-    }
-}
\ No newline at end of file

From 3902ed26b53595f6eb03fb77ef9b3268a08089a3 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Thu, 23 May 2019 10:02:44 +0200
Subject: [PATCH 7/9] Improve comments around constrainPatternType

---
 .../src/dotty/tools/dotc/core/PatternTypeConstrainer.scala  | 4 +++-
 compiler/src/dotty/tools/dotc/typer/Applications.scala      | 6 +++---
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
index f20a9b7906f0..09d8a0f54462 100644
--- a/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
+++ b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
@@ -14,7 +14,9 @@ trait PatternTypeConstrainer { self: TypeComparer =>
   /** Derive type and GADT constraints that necessarily follow from a pattern with the given type matching
    *  a scrutinee of the given type.
    *
-   *  We have the following situation in case of a (dynamic) pattern match:
+   *  This function breaks down scrutinee and pattern types into subcomponents between which there must be
+   *  a subtyping relationship, and derives constraints from those relationships. We have the following situation
+   *  in case of a (dynamic) pattern match:
    *
    *       StaticScrutineeType           PatternType
    *                         \            /
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index c53886aa45ce..7292eac9cca1 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1095,9 +1095,9 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
             fullyDefinedType(unapplyArgType, "pattern selector", tree.span)
             selType.dropAnnot(defn.UncheckedAnnot) // need to drop @unchecked. Just because the selector is @unchecked, the pattern isn't.
           } else {
-            // note that we simply ignore whether constraining actually succeeded or not
-            // in theory, constraining should only fail if the pattern cannot possibly match
-            // however, during exhaustivity checks, we perform a strictly better check
+            // We ignore whether constraining the pattern succeeded.
+            // Constraining only fails if the pattern cannot possibly match,
+            // but useless pattern checks detect more such cases, so we simply rely on them instead.
             ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(unapplyArgType, selType)
             val patternBound = maximizeType(unapplyArgType, tree.span, fromScala2x)
             if (patternBound.nonEmpty) unapplyFn = addBinders(unapplyFn, patternBound)

From 78300699f292b824d9f83aeadc991de5510cb185 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Thu, 6 Jun 2019 11:22:45 +0200
Subject: [PATCH 8/9] Refactor Mode.GADTFlexible and TypeComparer.frozenGadt

---
 compiler/src/dotty/tools/dotc/core/Mode.scala |  7 ++--
 .../dotty/tools/dotc/core/TypeComparer.scala  | 34 ++++++++++---------
 .../dotty/tools/dotc/typer/Applications.scala |  2 +-
 .../src/dotty/tools/dotc/typer/Inliner.scala  |  2 +-
 .../src/dotty/tools/dotc/typer/Typer.scala    |  4 +--
 5 files changed, 27 insertions(+), 22 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala
index 81b9fc5ea5c4..de07aa242c95 100644
--- a/compiler/src/dotty/tools/dotc/core/Mode.scala
+++ b/compiler/src/dotty/tools/dotc/core/Mode.scala
@@ -49,8 +49,11 @@ object Mode {
   /** We are in a pattern alternative */
   val InPatternAlternative: Mode = newMode(7, "InPatternAlternative")
 
-  /** Infer GADT constraints during type comparisons `A <:< B` */
-  val GADTflexible: Mode = newMode(8, "GADTflexible")
+  /** Make subtyping checks instead infer constraints necessarily following from given subtyping relation.
+   *
+   *  This enables changing [[GadtConstraint]] and alters how [[TypeComparer]] approximates constraints.
+   */
+  val GadtConstraintInference: Mode = newMode(8, "GadtConstraintInference")
 
   /** Assume -language:strictEquality */
   val StrictEquality: Mode = newMode(9, "StrictEquality")
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index b95659944e91..bdeb07cf5ea2 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -141,7 +141,11 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    */
   private [this] var leftRoot: Type = _
 
-  /** Are we forbidden from recording GADT constraints? */
+  /** 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.
+   */
   private[this] var frozenGadt = false
 
   protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = {
@@ -846,7 +850,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
                   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
-                    isSubArgs(args1, args2, tp1, tparams, inferGadtBounds = tyconIsInjective)
+                    def checkSubArgs() = isSubArgs(args1, args2, tp1, tparams)
+                    // we only record GADT constraints if tycon is guaranteed to be injective
+                    if (tyconIsInjective) checkSubArgs()
+                    else {
+                      val savedFrozenGadt = frozenGadt
+                      frozenGadt = true
+                      try checkSubArgs() finally frozenGadt = savedFrozenGadt
+                    }
                   }
                   if (res && touchedGADTs) GADTused = true
                   res
@@ -1103,7 +1114,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  @param  tp1       The applied type containing `args1`
    *  @param  tparams2  The type parameters of the type constructor applied to `args2`
    */
-  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo], inferGadtBounds: Boolean = false): Boolean = {
+  def isSubArgs(args1: List[Type], args2: List[Type], tp1: Type, tparams2: List[ParamInfo]): Boolean = {
     /** The bounds of parameter `tparam`, where all references to type paramneters
      *  are replaced by corresponding arguments (or their approximations in the case of
      *  wildcard arguments).
@@ -1167,17 +1178,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
               case arg1: TypeBounds =>
                 compareCaptured(arg1, arg2)
               case _ =>
-                def isSub(tp: Type, pt: Type): Boolean = {
-                  if (inferGadtBounds) isSubType(tp, pt)
-                  else {
-                    val savedFrozenGadt = frozenGadt
-                    frozenGadt = true
-                    try isSubType(tp, pt) finally frozenGadt = savedFrozenGadt
-                  }
-                }
-
-                (v > 0 || isSub(arg2, arg1)) &&
-                (v < 0 || isSub(arg1, arg2))
+                (v > 0 || isSubType(arg2, arg1)) &&
+                (v < 0 || isSubType(arg1, arg2))
             }
         }
 
@@ -1243,7 +1245,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  @see [[necessaryEither]] for the GADTFlexible case
    */
   protected def either(op1: => Boolean, op2: => Boolean): Boolean =
-    if (ctx.mode.is(Mode.GADTflexible)) necessaryEither(op1, op2) else sufficientEither(op1, op2)
+    if (ctx.mode.is(Mode.GadtConstraintInference)) necessaryEither(op1, op2) else sufficientEither(op1, op2)
 
   /** Returns true iff the result of evaluating either `op1` or `op2` is true,
    *  trying at the same time to keep the constraint as wide as possible.
@@ -1491,7 +1493,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    */
   private def narrowGADTBounds(tr: NamedType, bound: Type, approx: ApproxState, isUpper: Boolean): Boolean = {
     val boundImprecise = approx.high || approx.low
-    ctx.mode.is(Mode.GADTflexible) && !frozenGadt && !frozenConstraint && !boundImprecise && {
+    ctx.mode.is(Mode.GadtConstraintInference) && !frozenGadt && !frozenConstraint && !boundImprecise && {
       val tparam = tr.symbol
       gadts.println(i"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.toString} ${bound.isRef(tparam)}")
       if (bound.isRef(tparam)) false
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 7292eac9cca1..741f022ddabe 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1098,7 +1098,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
             // We ignore whether constraining the pattern succeeded.
             // Constraining only fails if the pattern cannot possibly match,
             // but useless pattern checks detect more such cases, so we simply rely on them instead.
-            ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(unapplyArgType, selType)
+            ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(unapplyArgType, selType)
             val patternBound = maximizeType(unapplyArgType, tree.span, fromScala2x)
             if (patternBound.nonEmpty) unapplyFn = addBinders(unapplyFn, patternBound)
             unapp.println(i"case 2 $unapplyArgType ${ctx.typerState.constraint}")
diff --git a/compiler/src/dotty/tools/dotc/typer/Inliner.scala b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
index 8f15fee80625..616a490a956c 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inliner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
@@ -916,7 +916,7 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(implicit ctx: Context) {
           }
 
         if (!isImplicit) caseBindingMap += ((NoSymbol, scrutineeBinding))
-        val gadtCtx = ctx.fresh.setFreshGADTBounds.addMode(Mode.GADTflexible)
+        val gadtCtx = ctx.fresh.setFreshGADTBounds.addMode(Mode.GadtConstraintInference)
         if (reducePattern(caseBindingMap, scrutineeSym.termRef, cdef.pat)(gadtCtx)) {
           val (caseBindings, from, to) = substBindings(caseBindingMap.toList, mutable.ListBuffer(), Nil, Nil)
           val guardOK = cdef.guard.isEmpty || {
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 5dc8224d2a15..aa4a1cea0304 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -607,7 +607,7 @@ class Typer extends Namer
       def handlePattern: Tree = {
         val tpt1 = typedTpt
         if (!ctx.isAfterTyper && pt != defn.ImplicitScrutineeTypeRef)
-          ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(tpt1.tpe, pt)
+          ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(tpt1.tpe, pt)
         // special case for an abstract type that comes with a class tag
         tryWithClassTag(ascription(tpt1, isWildcard = true), pt)
       }
@@ -3153,7 +3153,7 @@ class Typer extends Namer
       case _: RefTree | _: Literal
         if !isVarPattern(tree) &&
            !(pt <:< tree.tpe) &&
-           !ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(tree.tpe, pt) =>
+           !ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(tree.tpe, pt) =>
         val cmp =
           untpd.Apply(
             untpd.Select(untpd.TypedSplice(tree), nme.EQ),

From 01096ffc5b90aa40a0270fa5101ba9d13216e0c2 Mon Sep 17 00:00:00 2001
From: Aleksander Boruch-Gruszecki <aleksander.boruch-gruszecki@epfl.ch>
Date: Thu, 6 Jun 2019 11:32:50 +0200
Subject: [PATCH 9/9] Document ConstraintHandling#subsumes

---
 .../src/dotty/tools/dotc/core/ConstraintHandling.scala   | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 8a86d9abb598..25bf35df6829 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -336,8 +336,8 @@ trait ConstraintHandling[AbstractContext] {
    *     L2 <: L1, and
    *     U1 <: U2
    *
-   *  Both `c1` and `c2` are required to derive from constraint `pre`, possibly
-   *  narrowing it with further bounds.
+   *  Both `c1` and `c2` are required to derive from constraint `pre`, without adding
+   *  any new type variables but possibly narrowing already registered ones with further bounds.
    */
   protected final def subsumes(c1: Constraint, c2: Constraint, pre: Constraint)(implicit actx: AbstractContext): Boolean =
     if (c2 eq pre) true
@@ -345,6 +345,11 @@ trait ConstraintHandling[AbstractContext] {
     else {
       val saved = constraint
       try
+        // We iterate over params of `pre`, instead of `c2` as the documentation may suggest.
+        // As neither `c1` nor `c2` can have more params than `pre`, this only matters in one edge case.
+        // Constraint#forallParams only iterates over params that can be directly constrained.
+        // If `c2` has, compared to `pre`, instantiated a param and we iterated over params of `c2`,
+        // we could miss that param being instantiated to an incompatible type in `c1`.
         pre.forallParams(p =>
           c1.contains(p) &&
           c2.upper(p).forall(c1.isLess(p, _)) &&