Skip to content

Commit

Permalink
Fix spurious subtype check pruning when both sides have unions (#18213)
Browse files Browse the repository at this point in the history
Fixes #17465.

In TypeComparer, `fourthTry` calls `isNewSubType` and `isCovered` to
detect the subtype queries that have been covered by previous attempts
and prune them. However, the pruning is spurious when both sides contain
union types, as exemplified by the following subtype trace before the
PR:
```
==> isSubType (test1 : (Int | String){def foo(x: Int): Int}) <:< Int | String?
  ==> isSubType (Int | String){def foo(x: Int): Int} <:< Int | String?
    ==> isSubType (Int | String){def foo(x: Int): Int} <:< Int?
    <== isSubType (Int | String){def foo(x: Int): Int} <:< Int = false
    ==> isSubType (Int | String){def foo(x: Int): Int} <:< String?
      ==> isSubType (Int | String){def foo(x: Int): Int} <:< String?
      <== isSubType (Int | String){def foo(x: Int): Int} <:< String = false
    <== isSubType (Int | String){def foo(x: Int): Int} <:< String = false
    // (1): follow-up subtype checks are pruned here by isNewSubType
  <== isSubType (Int | String){def foo(x: Int): Int} <:< Int | String = false
<== isSubType (test1 : (Int | String){def foo(x: Int): Int}) <:< Int | String = false
```
At `(1)`, the pruning condition is met, and follow-up recursions are
skipped. However, in this case, only after `(1)` are the refinement on
LHS dropped and the subtype between two identical OrTypes are accepted.
The pruning is spurious.

This PR tempers the pruning conditions specified in `isCovered` and
`isNewSubType` to fix these false negatives.
  • Loading branch information
Linyxus authored Jul 20, 2023
2 parents aac8ba7 + 13c87ba commit 78e7163
Show file tree
Hide file tree
Showing 2 changed files with 77 additions and 14 deletions.
46 changes: 32 additions & 14 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1487,9 +1487,30 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling

/** Like tp1 <:< tp2, but returns false immediately if we know that
* the case was covered previously during subtyping.
*
* A type has been covered previously in subtype checking if it
* is some combination of TypeRefs that point to classes, where the
* combiners are AppliedTypes, RefinedTypes, RecTypes, And/Or-Types or AnnotatedTypes.
*
* The exception is that if both sides contain OrTypes, the check hasn't been covered.
* See #17465.
*/
def isNewSubType(tp1: Type): Boolean =
if (isCovered(tp1) && isCovered(tp2))
def isCovered(tp: Type): CoveredStatus =
tp.dealiasKeepRefiningAnnots.stripTypeVar match
case tp: TypeRef =>
if tp.symbol.isClass && tp.symbol != NothingClass && tp.symbol != NullClass
then CoveredStatus.Covered
else CoveredStatus.Uncovered
case tp: AppliedType => isCovered(tp.tycon)
case tp: RefinedOrRecType => isCovered(tp.parent)
case tp: AndType => isCovered(tp.tp1) min isCovered(tp.tp2)
case tp: OrType => isCovered(tp.tp1) min isCovered(tp.tp2) min CoveredStatus.CoveredWithOr
case _ => CoveredStatus.Uncovered

val covered1 = isCovered(tp1)
val covered2 = isCovered(tp2)
if (covered1 min covered2) >= CoveredStatus.CoveredWithOr && (covered1 max covered2) == CoveredStatus.Covered then
//println(s"useless subtype: $tp1 <:< $tp2")
false
else isSubType(tp1, tp2, approx.addLow)
Expand Down Expand Up @@ -2099,19 +2120,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
tp1.parent.asInstanceOf[RefinedType],
tp2.parent.asInstanceOf[RefinedType], limit))

/** A type has been covered previously in subtype checking if it
* is some combination of TypeRefs that point to classes, where the
* combiners are AppliedTypes, RefinedTypes, RecTypes, And/Or-Types or AnnotatedTypes.
*/
private def isCovered(tp: Type): Boolean = tp.dealiasKeepRefiningAnnots.stripTypeVar match {
case tp: TypeRef => tp.symbol.isClass && tp.symbol != NothingClass && tp.symbol != NullClass
case tp: AppliedType => isCovered(tp.tycon)
case tp: RefinedOrRecType => isCovered(tp.parent)
case tp: AndType => isCovered(tp.tp1) && isCovered(tp.tp2)
case tp: OrType => isCovered(tp.tp1) && isCovered(tp.tp2)
case _ => false
}

/** Defer constraining type variables when compared against prototypes */
def isMatchedByProto(proto: ProtoType, tp: Type): Boolean = tp.stripTypeVar match {
case tp: TypeParamRef if constraint contains tp => true
Expand Down Expand Up @@ -3000,6 +3008,16 @@ object TypeComparer {
end ApproxState
type ApproxState = ApproxState.Repr

/** Result of `isCovered` check. */
private object CoveredStatus:
type Repr = Int

val Uncovered: Repr = 1 // The type is not covered
val CoveredWithOr: Repr = 2 // The type is covered and contains OrTypes
val Covered: Repr = 3 // The type is covered and free from OrTypes
end CoveredStatus
type CoveredStatus = CoveredStatus.Repr

def topLevelSubType(tp1: Type, tp2: Type)(using Context): Boolean =
comparing(_.topLevelSubType(tp1, tp2))

Expand Down
45 changes: 45 additions & 0 deletions tests/pos/i17465.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
def test1[A, B]: Unit = {
def f[T](x: T{ def *(y: Int): T }): T = ???
def test = f[scala.collection.StringOps | String]("Hello")
locally:
val test1 : (scala.collection.StringOps | String) { def *(y: Int): (scala.collection.StringOps | String) } = ???
val test2 : (scala.collection.StringOps | String) { def *(y: Int): (scala.collection.StringOps | String) } = test1

locally:
val test1 : (Int | String) { def foo(x: Int): Int } = ???
val test2 : (Int | String) { def foo(x: Int): Int } = test1

locally:
val test1 : ((Int | String) & Any) { def foo(): Int } = ???
val test2 : ((Int | String) & Any) { def foo(): Int } = test1

locally:
val test1 : Int { def foo(): Int } = ???
val test2 : Int { def foo(): Int } = test1

locally:
val test1 : (Int | String) { def foo(): Int } = ???
val test2 : (Int | String) & Any = test1

locally:
val test1 : (Int | B) { def *(y: Int): Int } = ???
val test2 : (Int | B) { def *(y: Int): Int } = test1

locally:
val test1 : (Int | String) = ???
val test2 : (Int | String) = test1

type Foo = Int | String
locally:
val test1 : Foo { type T = Int } = ???
val test2 : (Int | String) = test1
}

def test2: Unit = {
import reflect.Selectable.reflectiveSelectable

trait A[T](x: T{ def *(y: Int): T }):
def f: T = x * 2

class B extends A("Hello")
}

0 comments on commit 78e7163

Please sign in to comment.