Skip to content

Commit bb257a3

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 a479fa4 commit bb257a3

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`.
@@ -3224,14 +3204,16 @@ object TrackingTypeComparer:
32243204
enum MatchResult extends Showable:
32253205
case Reduced(tp: Type)
32263206
case Disjoint
3207+
case ReducedAndDisjoint
32273208
case Stuck
32283209
case NoInstance(fails: List[(Name, TypeBounds)])
32293210

32303211
def toText(p: Printer): Text = this match
3231-
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3232-
case Disjoint => "Disjoint"
3233-
case Stuck => "Stuck"
3234-
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
3212+
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3213+
case Disjoint => "Disjoint"
3214+
case ReducedAndDisjoint => "ReducedAndDisjoint"
3215+
case Stuck => "Stuck"
3216+
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
32353217

32363218
class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
32373219
import TrackingTypeComparer.*
@@ -3326,9 +3308,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
33263308
}
33273309

33283310
def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult =
3311+
val disjoint = provablyDisjoint(scrut, spec.pattern)
33293312
if necessarySubType(scrut, spec.pattern) then
3330-
MatchResult.Reduced(spec.body)
3331-
else if provablyDisjoint(scrut, spec.pattern) then
3313+
if disjoint then
3314+
MatchResult.ReducedAndDisjoint
3315+
else
3316+
MatchResult.Reduced(spec.body)
3317+
else if disjoint then
33323318
MatchResult.Disjoint
33333319
else
33343320
MatchResult.Stuck
@@ -3469,9 +3455,12 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34693455
// This might not be needed
34703456
val contrainedCaseLambda = constrained(spec.origMatchCase).asInstanceOf[HKTypeLambda]
34713457

3472-
def tryDisjoint: MatchResult =
3458+
val disjoint =
34733459
val defn.MatchCase(origPattern, _) = contrainedCaseLambda.resultType: @unchecked
3474-
if provablyDisjoint(scrut, origPattern) then
3460+
provablyDisjoint(scrut, origPattern)
3461+
3462+
def tryDisjoint: MatchResult =
3463+
if disjoint then
34753464
MatchResult.Disjoint
34763465
else
34773466
MatchResult.Stuck
@@ -3487,7 +3476,10 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34873476
val defn.MatchCase(instantiatedPat, reduced) =
34883477
instantiateParamsSpec(instances, contrainedCaseLambda)(contrainedCaseLambda.resultType): @unchecked
34893478
if scrut <:< instantiatedPat then
3490-
MatchResult.Reduced(reduced)
3479+
if disjoint then
3480+
MatchResult.ReducedAndDisjoint
3481+
else
3482+
MatchResult.Reduced(reduced)
34913483
else
34923484
tryDisjoint
34933485
else
@@ -3511,6 +3503,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35113503
this.poisoned = savedPoisoned
35123504
this.canWidenAbstract = saved
35133505

3506+
val disjoint = provablyDisjoint(scrut, pat)
3507+
35143508
def redux(canApprox: Boolean): MatchResult =
35153509
val instances = paramInstances(canApprox)(Array.fill(caseLambda.paramNames.length)(NoType), pat)
35163510
instantiateParams(instances)(body) match
@@ -3521,13 +3515,16 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35213515
}
35223516
}
35233517
case redux =>
3524-
MatchResult.Reduced(redux)
3518+
if disjoint then
3519+
MatchResult.ReducedAndDisjoint
3520+
else
3521+
MatchResult.Reduced(redux)
35253522

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

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