Skip to content

Commit 5ffe2dc

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 2b709e7 commit 5ffe2dc

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
@@ -2763,26 +2763,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
27632763
false
27642764
} || tycon.derivesFrom(defn.PairClass)
27652765

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

32323213
def toText(p: Printer): Text = this match
3233-
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3234-
case Disjoint => "Disjoint"
3235-
case Stuck => "Stuck"
3236-
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
3214+
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
3215+
case Disjoint => "Disjoint"
3216+
case ReducedAndDisjoint => "ReducedAndDisjoint"
3217+
case Stuck => "Stuck"
3218+
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
32373219

32383220
class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
32393221
import TrackingTypeComparer.*
@@ -3328,9 +3310,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
33283310
}
33293311

33303312
def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult =
3313+
val disjoint = provablyDisjoint(scrut, spec.pattern)
33313314
if necessarySubType(scrut, spec.pattern) then
3332-
MatchResult.Reduced(spec.body)
3333-
else if provablyDisjoint(scrut, spec.pattern) then
3315+
if disjoint then
3316+
MatchResult.ReducedAndDisjoint
3317+
else
3318+
MatchResult.Reduced(spec.body)
3319+
else if disjoint then
33343320
MatchResult.Disjoint
33353321
else
33363322
MatchResult.Stuck
@@ -3464,9 +3450,12 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34643450
// This might not be needed
34653451
val constrainedCaseLambda = constrained(spec.origMatchCase, ast.tpd.EmptyTree)._1.asInstanceOf[HKTypeLambda]
34663452

3467-
def tryDisjoint: MatchResult =
3453+
val disjoint =
34683454
val defn.MatchCase(origPattern, _) = constrainedCaseLambda.resultType: @unchecked
3469-
if provablyDisjoint(scrut, origPattern) then
3455+
provablyDisjoint(scrut, origPattern)
3456+
3457+
def tryDisjoint: MatchResult =
3458+
if disjoint then
34703459
MatchResult.Disjoint
34713460
else
34723461
MatchResult.Stuck
@@ -3482,7 +3471,10 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
34823471
val defn.MatchCase(instantiatedPat, reduced) =
34833472
instantiateParamsSpec(instances, constrainedCaseLambda)(constrainedCaseLambda.resultType): @unchecked
34843473
if scrut <:< instantiatedPat then
3485-
MatchResult.Reduced(reduced)
3474+
if disjoint then
3475+
MatchResult.ReducedAndDisjoint
3476+
else
3477+
MatchResult.Reduced(reduced)
34863478
else
34873479
tryDisjoint
34883480
else
@@ -3506,6 +3498,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35063498
this.poisoned = savedPoisoned
35073499
this.canWidenAbstract = saved
35083500

3501+
val disjoint = provablyDisjoint(scrut, pat)
3502+
35093503
def redux(canApprox: Boolean): MatchResult =
35103504
val instances = paramInstances(canApprox)(Array.fill(caseLambda.paramNames.length)(NoType), pat)
35113505
instantiateParams(instances)(body) match
@@ -3516,13 +3510,16 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
35163510
}
35173511
}
35183512
case redux =>
3519-
MatchResult.Reduced(redux)
3513+
if disjoint then
3514+
MatchResult.ReducedAndDisjoint
3515+
else
3516+
MatchResult.Reduced(redux)
35203517

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

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