Skip to content

Commit 9839f09

Browse files
sjrdsjrd
committed
Do not use provablyEmpty anymore; use S <: T + provablyDisjoint(S, T) instead.
Fundamentally, the `provablyEmpty(scrut)` test was meant to prevent situations where both `scrut <: pattern` and `provablyDisjoint(scrut, pattern)` are true. That is a problem because it allows a match type to reduce in two different ways depending on the context. Instead, we basically use that combination of `scrut <: pattern` and `provablydisjoint(scrut, pattern)` as the *definition* for `provablyEmpty`. When both those conditions arise together, we refuse to reduce the match type. This allows one example to pass that did not pass before, but that particular example does not seem to cause unsoundness. In a sense, `provablyEmpty` was too strong here.
1 parent 3dfdcf7 commit 9839f09

File tree

5 files changed

+178
-71
lines changed

5 files changed

+178
-71
lines changed

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

Lines changed: 39 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -2764,26 +2764,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
27642764
false
27652765
} || tycon.derivesFrom(defn.PairClass)
27662766

2767-
/** Is `tp` an empty type?
2768-
*
2769-
* `true` implies that we found a proof; uncertainty defaults to `false`.
2770-
*/
2771-
def provablyEmpty(tp: Type): Boolean =
2772-
tp.dealias match {
2773-
case tp if tp.isExactlyNothing => true
2774-
case AndType(tp1, tp2) => provablyDisjoint(tp1, tp2)
2775-
case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2)
2776-
case at @ AppliedType(tycon, args) =>
2777-
args.lazyZip(tycon.typeParams).exists { (arg, tparam) =>
2778-
tparam.paramVarianceSign >= 0
2779-
&& provablyEmpty(arg)
2780-
&& typeparamCorrespondsToField(tycon, tparam)
2781-
}
2782-
case tp: TypeProxy =>
2783-
provablyEmpty(tp.underlying)
2784-
case _ => false
2785-
}
2786-
27872767
/** Are `tp1` and `tp2` provablyDisjoint types?
27882768
*
27892769
* `true` implies that we found a proof; uncertainty defaults to `false`.
@@ -3221,14 +3201,16 @@ object TrackingTypeComparer:
32213201
enum MatchResult extends Showable:
32223202
case Reduced(tp: Type)
32233203
case Disjoint
3204+
case ReducedAndDisjoint
32243205
case Stuck
32253206
case NoInstance(fails: List[(Name, TypeBounds)])
32263207

32273208
def toText(p: Printer): Text = this match
3228-
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3229-
case Disjoint => "Disjoint"
3230-
case Stuck => "Stuck"
3231-
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
3209+
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3210+
case Disjoint => "Disjoint"
3211+
case ReducedAndDisjoint => "ReducedAndDisjoint"
3212+
case Stuck => "Stuck"
3213+
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
32323214

32333215
class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
32343216
import TrackingTypeComparer.*
@@ -3323,9 +3305,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
33233305
}
33243306

33253307
def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult =
3308+
val disjoint = provablyDisjoint(scrut, spec.pattern)
33263309
if necessarySubType(scrut, spec.pattern) then
3327-
MatchResult.Reduced(spec.body)
3328-
else if provablyDisjoint(scrut, spec.pattern) then
3310+
if disjoint then
3311+
MatchResult.ReducedAndDisjoint
3312+
else
3313+
MatchResult.Reduced(spec.body)
3314+
else if disjoint then
33293315
MatchResult.Disjoint
33303316
else
33313317
MatchResult.Stuck
@@ -3466,9 +3452,12 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34663452
// This might not be needed
34673453
val contrainedCaseLambda = constrained(spec.origMatchCase).asInstanceOf[HKTypeLambda]
34683454

3469-
def tryDisjoint: MatchResult =
3455+
val disjoint =
34703456
val defn.MatchCase(origPattern, _) = contrainedCaseLambda.resultType: @unchecked
3471-
if provablyDisjoint(scrut, origPattern) then
3457+
provablyDisjoint(scrut, origPattern)
3458+
3459+
def tryDisjoint: MatchResult =
3460+
if disjoint then
34723461
MatchResult.Disjoint
34733462
else
34743463
MatchResult.Stuck
@@ -3484,7 +3473,10 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34843473
val defn.MatchCase(instantiatedPat, reduced) =
34853474
instantiateParamsSpec(instances, contrainedCaseLambda)(contrainedCaseLambda.resultType): @unchecked
34863475
if scrut <:< instantiatedPat then
3487-
MatchResult.Reduced(reduced)
3476+
if disjoint then
3477+
MatchResult.ReducedAndDisjoint
3478+
else
3479+
MatchResult.Reduced(reduced)
34883480
else
34893481
tryDisjoint
34903482
else
@@ -3508,6 +3500,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35083500
this.poisoned = savedPoisoned
35093501
this.canWidenAbstract = saved
35103502

3503+
val disjoint = provablyDisjoint(scrut, pat)
3504+
35113505
def redux(canApprox: Boolean): MatchResult =
35123506
val instances = paramInstances(canApprox)(Array.fill(caseLambda.paramNames.length)(NoType), pat)
35133507
instantiateParams(instances)(body) match
@@ -3518,13 +3512,16 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35183512
}
35193513
}
35203514
case redux =>
3521-
MatchResult.Reduced(redux)
3515+
if disjoint then
3516+
MatchResult.ReducedAndDisjoint
3517+
else
3518+
MatchResult.Reduced(redux)
35223519

35233520
if matches(canWidenAbstract = false) then
35243521
redux(canApprox = true)
35253522
else if matches(canWidenAbstract = true) then
35263523
redux(canApprox = false)
3527-
else if (provablyDisjoint(scrut, pat))
3524+
else if (disjoint)
35283525
// We found a proof that `scrut` and `pat` are incompatible.
35293526
// The search continues.
35303527
MatchResult.Disjoint
@@ -3551,28 +3548,22 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35513548
NoType
35523549
case MatchResult.Reduced(tp) =>
35533550
tp.simplified
3551+
case MatchResult.ReducedAndDisjoint =>
3552+
// Empty types break the basic assumption that if a scrutinee and a
3553+
// pattern are disjoint it's OK to reduce passed that pattern. Indeed,
3554+
// empty types viewed as a set of value is always a subset of any other
3555+
// types. As a result, if a scrutinee both matches a pattern and is
3556+
// probably disjoint from it, we prevent reduction.
3557+
// See `tests/neg/6570.scala` and `6570-1.scala` for examples that
3558+
// exploit emptiness to break match type soundness.
3559+
MatchTypeTrace.emptyScrutinee(scrut)
3560+
NoType
35543561
case Nil =>
35553562
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
35563563
ErrorType(reporting.MatchTypeNoCases(casesText))
35573564

35583565
inFrozenConstraint {
3559-
// Empty types break the basic assumption that if a scrutinee and a
3560-
// pattern are disjoint it's OK to reduce passed that pattern. Indeed,
3561-
// empty types viewed as a set of value is always a subset of any other
3562-
// types. As a result, we first check that the scrutinee isn't empty
3563-
// before proceeding with reduction. See `tests/neg/6570.scala` and
3564-
// `6570-1.scala` for examples that exploit emptiness to break match
3565-
// type soundness.
3566-
3567-
// If we revered the uncertainty case of this empty check, that is,
3568-
// `!provablyNonEmpty` instead of `provablyEmpty`, that would be
3569-
// obviously sound, but quite restrictive. With the current formulation,
3570-
// we need to be careful that `provablyEmpty` covers all the conditions
3571-
// used to conclude disjointness in `provablyDisjoint`.
3572-
if (provablyEmpty(scrut))
3573-
MatchTypeTrace.emptyScrutinee(scrut)
3574-
NoType
3575-
else if scrut.isError then
3566+
if scrut.isError then
35763567
// if the scrutinee is an error type
35773568
// then just return that as the result
35783569
// not doing so will result in the first type case matching

‎tests/neg/12800.scala

Lines changed: 0 additions & 21 deletions
This file was deleted.

‎tests/neg/6570.check

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:26:50 --------------------------------------------------------------
2+
26 | def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing // error
3+
| ^^^^^^^
4+
| Found: UpperBoundParametricVariant.M[T]
5+
| Required: Base.Trait2
6+
|
7+
| where: T is a type in method foo with bounds <: UpperBoundParametricVariant.Cov[Int]
8+
|
9+
|
10+
| Note: a match type could not be fully reduced:
11+
|
12+
| trying to reduce UpperBoundParametricVariant.M[T]
13+
| failed since selector T
14+
| does not uniquely determine parameter x in
15+
| case UpperBoundParametricVariant.Cov[x] => Base.N[x]
16+
| The computed bounds for the parameter are:
17+
| x <: Int
18+
|
19+
| longer explanation available when compiling with `-explain`
20+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:29:29 --------------------------------------------------------------
21+
29 | def thing = new Trait1 {} // error
22+
| ^
23+
| Found: Object with Base.Trait1 {...}
24+
| Required: Base.N[String & Int]
25+
|
26+
| Note: a match type could not be fully reduced:
27+
|
28+
| trying to reduce Base.N[String & Int]
29+
| failed since selector String & Int
30+
| is uninhabited (there are no values of that type).
31+
|
32+
| longer explanation available when compiling with `-explain`
33+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:47:32 --------------------------------------------------------------
34+
47 | def foo(c: Child): Trait2 = c.thing // error
35+
| ^^^^^^^
36+
| Found: InheritanceVariant.M[c.B]
37+
| Required: Base.Trait2
38+
|
39+
| Note: a match type could not be fully reduced:
40+
|
41+
| trying to reduce InheritanceVariant.M[c.B]
42+
| failed since selector c.B
43+
| does not uniquely determine parameter a in
44+
| case InheritanceVariant.Trick[a] => Base.N[a]
45+
| The computed bounds for the parameter are:
46+
| a >: Int
47+
|
48+
| longer explanation available when compiling with `-explain`
49+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:51:29 --------------------------------------------------------------
50+
51 | def thing = new Trait1 {} // error
51+
| ^
52+
| Found: Object with Base.Trait1 {...}
53+
| Required: Base.N[String & Int]
54+
|
55+
| Note: a match type could not be fully reduced:
56+
|
57+
| trying to reduce Base.N[String & Int]
58+
| failed since selector String & Int
59+
| is uninhabited (there are no values of that type).
60+
|
61+
| longer explanation available when compiling with `-explain`
62+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:69:29 --------------------------------------------------------------
63+
69 | def thing = new Trait1 {} // error
64+
| ^
65+
| Found: Object with Base.Trait1 {...}
66+
| Required: Base.N[String & Int]
67+
|
68+
| Note: a match type could not be fully reduced:
69+
|
70+
| trying to reduce Base.N[String & Int]
71+
| failed since selector String & Int
72+
| is uninhabited (there are no values of that type).
73+
|
74+
| longer explanation available when compiling with `-explain`
75+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:86:29 --------------------------------------------------------------
76+
86 | def thing = new Trait1 {} // error
77+
| ^
78+
| Found: Object with Base.Trait1 {...}
79+
| Required: Base.N[String & Int]
80+
|
81+
| Note: a match type could not be fully reduced:
82+
|
83+
| trying to reduce Base.N[String & Int]
84+
| failed since selector String & Int
85+
| is uninhabited (there are no values of that type).
86+
|
87+
| longer explanation available when compiling with `-explain`
88+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:103:32 -------------------------------------------------------------
89+
103 | def foo(c: Child): Trait2 = c.thing // error
90+
| ^^^^^^^
91+
| Found: UpperBoundVariant.M[c.A]
92+
| Required: Base.Trait2
93+
|
94+
| Note: a match type could not be fully reduced:
95+
|
96+
| trying to reduce UpperBoundVariant.M[c.A]
97+
| failed since selector c.A
98+
| does not uniquely determine parameter t in
99+
| case UpperBoundVariant.Cov[t] => Base.N[t]
100+
| The computed bounds for the parameter are:
101+
| t <: Int
102+
|
103+
| longer explanation available when compiling with `-explain`
104+
-- [E007] Type Mismatch Error: tests/neg/6570.scala:107:29 -------------------------------------------------------------
105+
107 | def thing = new Trait1 {} // error
106+
| ^
107+
| Found: Object with Base.Trait1 {...}
108+
| Required: Base.N[String & Int]
109+
|
110+
| Note: a match type could not be fully reduced:
111+
|
112+
| trying to reduce Base.N[String & Int]
113+
| failed since selector String & Int
114+
| is uninhabited (there are no values of that type).
115+
|
116+
| longer explanation available when compiling with `-explain`

‎tests/neg/6571.check

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,8 @@
88
|
99
| trying to reduce Test.M[Test.Inv[Int] & Test.Inv[String]]
1010
| failed since selector Test.Inv[Int] & Test.Inv[String]
11-
| is uninhabited (there are no values of that type).
11+
| does not match case Test.Inv[u] => u
12+
| and cannot be shown to be disjoint from it either.
1213
|
1314
| longer explanation available when compiling with `-explain`
1415
-- [E007] Type Mismatch Error: tests/neg/6571.scala:7:39 ---------------------------------------------------------------
@@ -21,6 +22,7 @@
2122
|
2223
| trying to reduce Test.M[Test.Inv[String] & Test.Inv[Int]]
2324
| failed since selector Test.Inv[String] & Test.Inv[Int]
24-
| is uninhabited (there are no values of that type).
25+
| does not match case Test.Inv[u] => u
26+
| and cannot be shown to be disjoint from it either.
2527
|
2628
| longer explanation available when compiling with `-explain`

‎tests/pos/12800.scala

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
object Test {
2+
type FieldType2[K, +V] = V with KeyTag2[K, V]
3+
trait KeyTag2[K, +V] extends Any
4+
5+
type WrapUpper = Tuple
6+
type Wrap[A] = Tuple1[A]
7+
8+
type Extract[A <: WrapUpper] = A match {
9+
case Wrap[h] => h
10+
}
11+
12+
summon[Extract[Wrap[FieldType2["foo", Int]]] =:= FieldType2["foo", Int]]
13+
14+
// This used to cause an error because `Tuple1[FieldType2["foo", Int]]` was
15+
// "provablyEmpty". Since we switched to testing the combination of
16+
// `scrut <: pattern` *and* `provablyDisjoint(scrut, pattern)` instead, this
17+
// particular example compiles, because `FieldType2["foo", Int]` is not
18+
// `provablyDisjoint` from `h` (`Any`).
19+
}

0 commit comments

Comments
 (0)