Skip to content

Commit c653793

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 f432d08 commit c653793

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
@@ -2771,26 +2771,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
27712771
false
27722772
} || tycon.derivesFrom(defn.PairClass)
27732773

2774-
/** Is `tp` an empty type?
2775-
*
2776-
* `true` implies that we found a proof; uncertainty defaults to `false`.
2777-
*/
2778-
def provablyEmpty(tp: Type): Boolean =
2779-
tp.dealias match {
2780-
case tp if tp.isExactlyNothing => true
2781-
case AndType(tp1, tp2) => provablyDisjoint(tp1, tp2)
2782-
case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2)
2783-
case at @ AppliedType(tycon, args) =>
2784-
args.lazyZip(tycon.typeParams).exists { (arg, tparam) =>
2785-
tparam.paramVarianceSign >= 0
2786-
&& provablyEmpty(arg)
2787-
&& typeparamCorrespondsToField(tycon, tparam)
2788-
}
2789-
case tp: TypeProxy =>
2790-
provablyEmpty(tp.underlying)
2791-
case _ => false
2792-
}
2793-
27942774
/** Are `tp1` and `tp2` provablyDisjoint types?
27952775
*
27962776
* `true` implies that we found a proof; uncertainty defaults to `false`.
@@ -3234,14 +3214,16 @@ object TrackingTypeComparer:
32343214
enum MatchResult extends Showable:
32353215
case Reduced(tp: Type)
32363216
case Disjoint
3217+
case ReducedAndDisjoint
32373218
case Stuck
32383219
case NoInstance(fails: List[(Name, TypeBounds)])
32393220

32403221
def toText(p: Printer): Text = this match
3241-
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3242-
case Disjoint => "Disjoint"
3243-
case Stuck => "Stuck"
3244-
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
3222+
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3223+
case Disjoint => "Disjoint"
3224+
case ReducedAndDisjoint => "ReducedAndDisjoint"
3225+
case Stuck => "Stuck"
3226+
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
32453227

32463228
class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
32473229
import TrackingTypeComparer.*
@@ -3336,9 +3318,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
33363318
}
33373319

33383320
def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult =
3321+
val disjoint = provablyDisjoint(scrut, spec.pattern)
33393322
if necessarySubType(scrut, spec.pattern) then
3340-
MatchResult.Reduced(spec.body)
3341-
else if provablyDisjoint(scrut, spec.pattern) then
3323+
if disjoint then
3324+
MatchResult.ReducedAndDisjoint
3325+
else
3326+
MatchResult.Reduced(spec.body)
3327+
else if disjoint then
33423328
MatchResult.Disjoint
33433329
else
33443330
MatchResult.Stuck
@@ -3472,9 +3458,12 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34723458
// This might not be needed
34733459
val constrainedCaseLambda = constrained(spec.origMatchCase, ast.tpd.EmptyTree)._1.asInstanceOf[HKTypeLambda]
34743460

3475-
def tryDisjoint: MatchResult =
3461+
val disjoint =
34763462
val defn.MatchCase(origPattern, _) = constrainedCaseLambda.resultType: @unchecked
3477-
if provablyDisjoint(scrut, origPattern) then
3463+
provablyDisjoint(scrut, origPattern)
3464+
3465+
def tryDisjoint: MatchResult =
3466+
if disjoint then
34783467
MatchResult.Disjoint
34793468
else
34803469
MatchResult.Stuck
@@ -3490,7 +3479,10 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34903479
val defn.MatchCase(instantiatedPat, reduced) =
34913480
instantiateParamsSpec(instances, constrainedCaseLambda)(constrainedCaseLambda.resultType): @unchecked
34923481
if scrut <:< instantiatedPat then
3493-
MatchResult.Reduced(reduced)
3482+
if disjoint then
3483+
MatchResult.ReducedAndDisjoint
3484+
else
3485+
MatchResult.Reduced(reduced)
34943486
else
34953487
tryDisjoint
34963488
else
@@ -3514,6 +3506,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35143506
this.poisoned = savedPoisoned
35153507
this.canWidenAbstract = saved
35163508

3509+
val disjoint = provablyDisjoint(scrut, pat)
3510+
35173511
def redux(canApprox: Boolean): MatchResult =
35183512
val instances = paramInstances(canApprox)(Array.fill(caseLambda.paramNames.length)(NoType), pat)
35193513
instantiateParams(instances)(body) match
@@ -3524,13 +3518,16 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35243518
}
35253519
}
35263520
case redux =>
3527-
MatchResult.Reduced(redux)
3521+
if disjoint then
3522+
MatchResult.ReducedAndDisjoint
3523+
else
3524+
MatchResult.Reduced(redux)
35283525

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

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