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/core/ConstraintHandling.scala

@@ -30,6 +30,7 @@ trait ConstraintHandling[AbstractContext] {
 
   protected def isSubType(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean
   protected def isSameType(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean
+  protected def typeLub(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Type
 
   protected def constraint: Constraint
   protected def constraint_=(c: Constraint): Unit
@@ -131,7 +132,7 @@ trait ConstraintHandling[AbstractContext] {
           homogenizeArgs = Config.alignArgsInAnd
           try
             if (isUpper) oldBounds.derivedTypeBounds(lo, hi & bound)
-            else oldBounds.derivedTypeBounds(lo | bound, hi)
+            else oldBounds.derivedTypeBounds(typeLub(lo, bound), hi)
           finally homogenizeArgs = saved
         }
         val c1 = constraint.updateEntry(param, narrowedBounds)

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

@@ -809,6 +809,10 @@ object Contexts {
     override def isSubType(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = ctx.typeComparer.isSubType(tp1, tp2)
     override def isSameType(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = ctx.typeComparer.isSameType(tp1, tp2)
 
+    override protected def typeLub(tp1: Type, tp2: Type)(implicit ctx: Context): Type = {
+      ctx.typeComparer.lub(tp1, tp2, admitSingletons = true)
+    }
+
     override def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit = tvar(sym)
 
     override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = {

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

@@ -34,6 +34,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
 
   override protected def externalize(param: TypeParamRef)(implicit ctx: Context): Type = param
 
+  override protected def typeLub(tp1: Type, tp2: Type)(implicit actx: AbsentContext): Type =
+    lub(tp1, tp2)
+
   private[this] var pendingSubTypes: mutable.Set[(Type, Type)] = null
   private[this] var recCount = 0
   private[this] var monitored = false
@@ -1434,9 +1437,10 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
 
   /** The least upper bound of two types
    *  @param canConstrain  If true, new constraints might be added to simplify the lub.
-   *  @note  We do not admit singleton types in or-types as lubs.
+   *  @param admitSingletons We only admit singletons as parts of lubs when we must maintain necessary conditions,
+   *                         such as when inferring GADT constraints.
    */
-  def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false): Type = /*>|>*/ trace(s"lub(${tp1.show}, ${tp2.show}, canConstrain=$canConstrain)", subtyping, show = true) /*<|<*/ {
+  def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false, admitSingletons: Boolean = false): Type = /*>|>*/ trace(s"lub(${tp1.show}, ${tp2.show}, canConstrain=$canConstrain)", subtyping, show = true) /*<|<*/ {
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp1
     else if (!tp2.exists) tp2
@@ -1448,6 +1452,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       else {
         val t2 = mergeIfSuper(tp2, tp1, canConstrain)
         if (t2.exists) t2
+        else if (admitSingletons) orType(tp1.widenExpr, tp2.widenExpr)
         else {
           val tp1w = tp1.widen
           val tp2w = tp2.widen
@@ -1973,9 +1978,9 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       super.hasMatchingMember(name, tp1, tp2)
     }
 
-  override def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false): Type =
-    traceIndented(s"lub(${show(tp1)}, ${show(tp2)}, canConstrain=$canConstrain)") {
-      super.lub(tp1, tp2, canConstrain)
+  override def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false, admitSingletons: Boolean = false): Type =
+    traceIndented(s"lub(${show(tp1)}, ${show(tp2)}, canConstrain=$canConstrain, admitSingletons=$admitSingletons)") {
+      super.lub(tp1, tp2, canConstrain, admitSingletons)
     }
 
   override def glb(tp1: Type, tp2: Type): Type =

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

@@ -3605,7 +3605,12 @@ object Types {
 
   // ----- Skolem types -----------------------------------------------
 
-  /** A skolem type reference with underlying type `binder`. */
+  /** A skolem type reference with underlying type `info`.
+   *
+   * For Dotty, a skolem type is a singleton type of some unknown value of type `info`.
+   * Note that care is needed when creating them, since not all types need to be inhabited.
+   * A skolem is equal to itself and no other type.
+   */
   case class SkolemType(info: Type) extends UncachedProxyType with ValueType with SingletonType {
     override def underlying(implicit ctx: Context): Type = info
     def derivedSkolemType(info: Type)(implicit ctx: Context): SkolemType =

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(subtp, tp, termPattern = true)) 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/Inferencing.scala

@@ -150,41 +150,22 @@ object Inferencing {
       tree
   }
 
-  /** 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:
+  /** Infer constraints that should be in scope for a case body with given pattern and scrutinee types.
    *
-   *       StaticScrutineeType           PatternType
-   *                         \            /
-   *                      DynamicScrutineeType
+   * If `termPattern`, infer constraints from knowing that there exists a value which of both scrutinee
+   * and pattern types (which is the case for normal pattern matching). If not `termPattern`, instead
+   * infer constraints from knowing that `tp <: pt`.
    *
-   *  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`.
+   * If a pattern matches during normal pattern matching, we can be certain that there exists a value
+   * which is of both scrutinee and pattern types (the value we're matching on). If this value
+   * was in a variable, say `x`, then we could simply infer constraints from `x.type <: pt`. Since we might
+   * be matching on an expression as well, we take a skolem of the scrutinee, which is essentially an existential
+   * singleton type (see [[dotty.tools.dotc.core.Types.SkolemType]]).
    *
-   *            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`).
-   *
-   *  TODO: Update so that GADT symbols can be variant, and we special case final class types in patterns
+   * Note that we need to sometimes widen type parameters of the scrutinee type to avoid unsoundness -
+   * see i3989c.scala and related issue discussion on Github.
    */
-  def constrainPatternType(tp: Type, pt: Type)(implicit ctx: Context): Boolean = {
+  def constrainPatternType(tp: Type, pt: Type, termPattern: Boolean)(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)
@@ -206,8 +187,9 @@ object Inferencing {
     }
 
     val widePt = if (ctx.scala2Mode || refinementIsInvariant(tp)) pt else widenVariantParams(pt)
-    trace(i"constraining pattern type $tp <:< $widePt", gadts, res => s"$res\n${ctx.gadt.debugBoundsDescription}") {
-      tp <:< widePt
+    val narrowTp = if (termPattern) SkolemType(tp) else tp
+    trace(i"constraining pattern type $narrowTp <:< $widePt", gadts, res => s"$res\n${ctx.gadt.debugBoundsDescription}") {
+      narrowTp <:< widePt
     }
   }
 

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(tpt1.tpe, pt, termPattern = true)(ctx.addMode(Mode.GADTflexible))
         // special case for an abstract type that comes with a class tag
         tryWithClassTag(ascription(tpt1, isWildcard = true), pt)
       }
@@ -1095,7 +1095,7 @@ class Typer extends Namer
     def caseRest(implicit ctx: Context) = {
       val pat1 = checkSimpleKinded(typedType(cdef.pat)(ctx.addMode(Mode.Pattern)))
       if (!ctx.isAfterTyper)
-        constrainPatternType(pat1.tpe, selType)(ctx.addMode(Mode.GADTflexible))
+        constrainPatternType(pat1.tpe, selType, termPattern = false)(ctx.addMode(Mode.GADTflexible))
       val pat2 = indexPattern(cdef).transform(pat1)
       val body1 = typedType(cdef.body, pt)
       assignType(cpy.CaseDef(cdef)(pat2, EmptyTree, body1), pat2, body1)

tests/neg/creative-gadt-constraints.scala

@@ -0,0 +1,66 @@
+object buffer {
+  object EssaInt {
+    def unapply(i: Int): Some[Int] = Some(i)
+  }
+
+  case class Inv[T](t: T)
+
+  enum EQ[A, B] { case Refl[T]() extends EQ[T, T] }
+  enum SUB[A, +B] { case Refl[T]() extends SUB[T, T] } // A <: B
+
+  def test_eq1[A, B](eq: EQ[A, B], a: A, b: B): B =
+    Inv(a) match { case Inv(_: Int) => // a >: Sko(Int)
+      Inv(a) match { case Inv(_: Int) => // a >: Sko(Int) | Sko(Int)
+        eq match { case EQ.Refl() => // a = b
+          val success: A = b
+          val fail: A = 0 // error
+          0 // error
+        }
+      }
+    }
+
+  def test_eq2[A, B](eq: EQ[A, B], a: A, b: B): B =
+    Inv(a) match { case Inv(_: Int) => // a >: Sko(Int)
+      Inv(b) match { case Inv(_: Int) => // b >: Sko(Int)
+        eq match { case EQ.Refl() => // a = b
+          val success: A = b
+          val fail: A = 0 // error
+          0 // error
+        }
+      }
+    }
+
+  def test_sub1[A, B](sub: SUB[A, B], a: A, b: B): B =
+    Inv(b) match { case Inv(_: Int) => // b >: Sko(Int)
+      Inv(b) match { case Inv(_: Int) => // b >: Sko(Int) | Sko(Int)
+        sub match { case SUB.Refl() => // b >: a
+          val success: B = a
+          val fail: A = 0 // error
+          0 // error
+        }
+      }
+    }
+
+  def test_sub2[A, B](sub: SUB[A, B], a: A, b: B): B =
+    Inv(a) match { case Inv(_: Int) => // a >: Sko(Int)
+      Inv(b) match { case Inv(_: Int) => // b >: Sko(Int) | Sko(Int)
+        sub match { case SUB.Refl() => // b >: a
+          val success: B = a
+          val fail: A = 0 // error
+          0 // error
+        }
+      }
+    }
+
+
+  def test_sub_eq[A, B, C](sub: SUB[A|B, C], eqA: EQ[A, 5], eqB: EQ[B, 6]): C =
+    sub match { case SUB.Refl() => // C >: A | B
+      eqA match { case EQ.Refl() => // A = 5
+        eqB match { case EQ.Refl() => // B = 6
+          val fail1: A = 0 // error
+          val fail2: B = 0 // error
+          0 // error
+        }
+      }
+    }
+}

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 = t match {
+    case EssaInt(_) =>
+      0 // error
+  }
+
+  def foo2[T](t: T): T = t match {
+    case EssaInt(_) => 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
+  }
+
+  def bar2[T](t: T): T = t match {
+    case Inv(EssaInt(_)) => t match {
+      case Inv(EssaInt(_)) =>
+        0 // error
+    }
+  }
+}

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

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