Use Skolems to infer GADT constraints

The rationale for using a Skolem here is: we want to record that there
is at least one value that is both of the pattern type and the scrutinee
type.

All symbols are now considered valid for adding GADT constraints -
the rationale is that set of constrainable symbols should be either
selected on a per-(sub)pattern basis, or be the same for all matches.
Previously, symbols which were only appearing variantly in a scrutinee
type could be considered constrainable anyway because of an outer
pattern match.

Author: abgruszecki

compiler/src/dotty/tools/dotc/typer/Applications.scala

@@ -1036,7 +1036,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)

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -599,7 +599,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)
       }

tests/neg/int-extractor.scala

@@ -0,0 +1,17 @@
+object Test {
+  object EssaInt {
+    def unapply(i: Int): Some[Int] = Some(i)
+  }
+
+  def foo1[T](t: T): T = t match {
+    case EssaInt(_) =>
+      0 // error
+  }
+
+  case class Inv[T](t: T)
+
+  def bar1[T](t: T): T = Inv(t) match {
+    case Inv(EssaInt(_)) =>
+      0 // error
+  }
+}

tests/neg/invariant-gadt.scala

@@ -0,0 +1,20 @@
+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
+    }
+  }
+}

tests/neg/typeclass-derivation2.scala

@@ -111,6 +111,13 @@ object TypeLevel {
    *  It informs that type `T` has shape `S` and also implements runtime reflection on `T`.
    */
   abstract class Shaped[T, S <: Shape] extends Reflected[T]
+
+  // substitute for erasedValue that allows precise matching
+  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] = ???
 }
 
 // An algebraic datatype
@@ -203,7 +210,7 @@ trait Show[T] {
   def show(x: T): String
 }
 object Show {
-  import scala.compiletime.erasedValue
+  import scala.compiletime.{erasedValue, error}
   import TypeLevel._
 
   inline def tryShow[T](x: T): String = implicit match {
@@ -229,9 +236,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)

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
+  }
+}

tests/run/typeclass-derivation2.scala

@@ -113,6 +113,13 @@ object TypeLevel {
    *  It informs that type `T` has shape `S` and also implements runtime reflection on `T`.
    */
   abstract class Shaped[T, S <: Shape] extends Reflected[T]
+
+  // substitute for erasedValue that allows precise matching
+  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] = ???
 }
 
 // An algebraic datatype
@@ -217,7 +224,7 @@ trait Eq[T] {
 }
 
 object Eq {
-  import scala.compiletime.erasedValue
+  import scala.compiletime.{erasedValue, error}
   import TypeLevel._
 
   inline def tryEql[T](x: T, y: T) = implicit match {
@@ -239,8 +246,13 @@ object Eq {
   inline def eqlCases[T, Alts <: Tuple](xm: Mirror, ym: Mirror, ordinal: Int, n: Int): Boolean =
     inline erasedValue[Alts] match {
       case _: (Shape.Case[alt, elems] *: alts1) =>
-        if (n == ordinal) eqlElems[elems](xm, ym, 0)
-        else eqlCases[T, alts1](xm, ym, ordinal, n + 1)
+        inline typeOf[alt] match {
+          case _: Subtype[T] =>
+            if (n == ordinal) eqlElems[elems](xm, ym, 0)
+            else eqlCases[T, alts1](xm, ym, ordinal, n + 1)
+          case _ =>
+            error("invalid call to eqlCases: one of Alts is not a subtype of T")
+        }
      case _: Unit =>
         false
     }
@@ -271,7 +283,7 @@ trait Pickler[T] {
 }
 
 object Pickler {
-  import scala.compiletime.{erasedValue, constValue}
+  import scala.compiletime.{erasedValue, constValue, error}
   import TypeLevel._
 
   def nextInt(buf: mutable.ListBuffer[Int]): Int = try buf.head finally buf.trimStart(1)
@@ -294,12 +306,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 =>
     }
@@ -362,7 +379,7 @@ trait Show[T] {
   def show(x: T): String
 }
 object Show {
-  import scala.compiletime.erasedValue
+  import scala.compiletime.{erasedValue, error}
   import TypeLevel._
 
   inline def tryShow[T](x: T): String = implicit match {
@@ -388,9 +405,15 @@ 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)