Skip to content

Commit 78e7163

Browse files
authored
Fix spurious subtype check pruning when both sides have unions (#18213)
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.
2 parents aac8ba7 + 13c87ba commit 78e7163

File tree

2 files changed

+77
-14
lines changed

2 files changed

+77
-14
lines changed

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

Lines changed: 32 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1487,9 +1487,30 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
14871487

14881488
/** Like tp1 <:< tp2, but returns false immediately if we know that
14891489
* the case was covered previously during subtyping.
1490+
*
1491+
* A type has been covered previously in subtype checking if it
1492+
* is some combination of TypeRefs that point to classes, where the
1493+
* combiners are AppliedTypes, RefinedTypes, RecTypes, And/Or-Types or AnnotatedTypes.
1494+
*
1495+
* The exception is that if both sides contain OrTypes, the check hasn't been covered.
1496+
* See #17465.
14901497
*/
14911498
def isNewSubType(tp1: Type): Boolean =
1492-
if (isCovered(tp1) && isCovered(tp2))
1499+
def isCovered(tp: Type): CoveredStatus =
1500+
tp.dealiasKeepRefiningAnnots.stripTypeVar match
1501+
case tp: TypeRef =>
1502+
if tp.symbol.isClass && tp.symbol != NothingClass && tp.symbol != NullClass
1503+
then CoveredStatus.Covered
1504+
else CoveredStatus.Uncovered
1505+
case tp: AppliedType => isCovered(tp.tycon)
1506+
case tp: RefinedOrRecType => isCovered(tp.parent)
1507+
case tp: AndType => isCovered(tp.tp1) min isCovered(tp.tp2)
1508+
case tp: OrType => isCovered(tp.tp1) min isCovered(tp.tp2) min CoveredStatus.CoveredWithOr
1509+
case _ => CoveredStatus.Uncovered
1510+
1511+
val covered1 = isCovered(tp1)
1512+
val covered2 = isCovered(tp2)
1513+
if (covered1 min covered2) >= CoveredStatus.CoveredWithOr && (covered1 max covered2) == CoveredStatus.Covered then
14931514
//println(s"useless subtype: $tp1 <:< $tp2")
14941515
false
14951516
else isSubType(tp1, tp2, approx.addLow)
@@ -2099,19 +2120,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
20992120
tp1.parent.asInstanceOf[RefinedType],
21002121
tp2.parent.asInstanceOf[RefinedType], limit))
21012122

2102-
/** A type has been covered previously in subtype checking if it
2103-
* is some combination of TypeRefs that point to classes, where the
2104-
* combiners are AppliedTypes, RefinedTypes, RecTypes, And/Or-Types or AnnotatedTypes.
2105-
*/
2106-
private def isCovered(tp: Type): Boolean = tp.dealiasKeepRefiningAnnots.stripTypeVar match {
2107-
case tp: TypeRef => tp.symbol.isClass && tp.symbol != NothingClass && tp.symbol != NullClass
2108-
case tp: AppliedType => isCovered(tp.tycon)
2109-
case tp: RefinedOrRecType => isCovered(tp.parent)
2110-
case tp: AndType => isCovered(tp.tp1) && isCovered(tp.tp2)
2111-
case tp: OrType => isCovered(tp.tp1) && isCovered(tp.tp2)
2112-
case _ => false
2113-
}
2114-
21152123
/** Defer constraining type variables when compared against prototypes */
21162124
def isMatchedByProto(proto: ProtoType, tp: Type): Boolean = tp.stripTypeVar match {
21172125
case tp: TypeParamRef if constraint contains tp => true
@@ -3000,6 +3008,16 @@ object TypeComparer {
30003008
end ApproxState
30013009
type ApproxState = ApproxState.Repr
30023010

3011+
/** Result of `isCovered` check. */
3012+
private object CoveredStatus:
3013+
type Repr = Int
3014+
3015+
val Uncovered: Repr = 1 // The type is not covered
3016+
val CoveredWithOr: Repr = 2 // The type is covered and contains OrTypes
3017+
val Covered: Repr = 3 // The type is covered and free from OrTypes
3018+
end CoveredStatus
3019+
type CoveredStatus = CoveredStatus.Repr
3020+
30033021
def topLevelSubType(tp1: Type, tp2: Type)(using Context): Boolean =
30043022
comparing(_.topLevelSubType(tp1, tp2))
30053023

tests/pos/i17465.scala

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
def test1[A, B]: Unit = {
2+
def f[T](x: T{ def *(y: Int): T }): T = ???
3+
def test = f[scala.collection.StringOps | String]("Hello")
4+
locally:
5+
val test1 : (scala.collection.StringOps | String) { def *(y: Int): (scala.collection.StringOps | String) } = ???
6+
val test2 : (scala.collection.StringOps | String) { def *(y: Int): (scala.collection.StringOps | String) } = test1
7+
8+
locally:
9+
val test1 : (Int | String) { def foo(x: Int): Int } = ???
10+
val test2 : (Int | String) { def foo(x: Int): Int } = test1
11+
12+
locally:
13+
val test1 : ((Int | String) & Any) { def foo(): Int } = ???
14+
val test2 : ((Int | String) & Any) { def foo(): Int } = test1
15+
16+
locally:
17+
val test1 : Int { def foo(): Int } = ???
18+
val test2 : Int { def foo(): Int } = test1
19+
20+
locally:
21+
val test1 : (Int | String) { def foo(): Int } = ???
22+
val test2 : (Int | String) & Any = test1
23+
24+
locally:
25+
val test1 : (Int | B) { def *(y: Int): Int } = ???
26+
val test2 : (Int | B) { def *(y: Int): Int } = test1
27+
28+
locally:
29+
val test1 : (Int | String) = ???
30+
val test2 : (Int | String) = test1
31+
32+
type Foo = Int | String
33+
locally:
34+
val test1 : Foo { type T = Int } = ???
35+
val test2 : (Int | String) = test1
36+
}
37+
38+
def test2: Unit = {
39+
import reflect.Selectable.reflectiveSelectable
40+
41+
trait A[T](x: T{ def *(y: Int): T }):
42+
def f: T = x * 2
43+
44+
class B extends A("Hello")
45+
}

0 commit comments

Comments
 (0)