Skip to content

Commit

Permalink
Do not use provablyEmpty anymore; use S <: T + provablyDisjoint(S, T)…
Browse files Browse the repository at this point in the history
… 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.
  • Loading branch information
sjrd committed Sep 1, 2023
1 parent 661688f commit 39da0ba
Show file tree
Hide file tree
Showing 5 changed files with 178 additions and 71 deletions.
87 changes: 39 additions & 48 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2764,26 +2764,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
false
} || tycon.derivesFrom(defn.PairClass)

/** Is `tp` an empty type?
*
* `true` implies that we found a proof; uncertainty defaults to `false`.
*/
def provablyEmpty(tp: Type): Boolean =
tp.dealias match {
case tp if tp.isExactlyNothing => true
case AndType(tp1, tp2) => provablyDisjoint(tp1, tp2)
case OrType(tp1, tp2) => provablyEmpty(tp1) && provablyEmpty(tp2)
case at @ AppliedType(tycon, args) =>
args.lazyZip(tycon.typeParams).exists { (arg, tparam) =>
tparam.paramVarianceSign >= 0
&& provablyEmpty(arg)
&& typeparamCorrespondsToField(tycon, tparam)
}
case tp: TypeProxy =>
provablyEmpty(tp.underlying)
case _ => false
}

/** Are `tp1` and `tp2` provablyDisjoint types?
*
* `true` implies that we found a proof; uncertainty defaults to `false`.
Expand Down Expand Up @@ -3221,14 +3201,16 @@ object TrackingTypeComparer:
enum MatchResult extends Showable:
case Reduced(tp: Type)
case Disjoint
case ReducedAndDisjoint
case Stuck
case NoInstance(fails: List[(Name, TypeBounds)])

def toText(p: Printer): Text = this match
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
case Disjoint => "Disjoint"
case Stuck => "Stuck"
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"
case Reduced(tp) => "Reduced(" ~ p.toText(tp) ~ ")"
case Disjoint => "Disjoint"
case ReducedAndDisjoint => "ReducedAndDisjoint"
case Stuck => "Stuck"
case NoInstance(fails) => "NoInstance(" ~ Text(fails.map(p.toText(_) ~ p.toText(_)), ", ") ~ ")"

class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
import TrackingTypeComparer.*
Expand Down Expand Up @@ -3323,9 +3305,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
}

def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult =
val disjoint = provablyDisjoint(scrut, spec.pattern)
if necessarySubType(scrut, spec.pattern) then
MatchResult.Reduced(spec.body)
else if provablyDisjoint(scrut, spec.pattern) then
if disjoint then
MatchResult.ReducedAndDisjoint
else
MatchResult.Reduced(spec.body)
else if disjoint then
MatchResult.Disjoint
else
MatchResult.Stuck
Expand Down Expand Up @@ -3466,9 +3452,12 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
// This might not be needed
val contrainedCaseLambda = constrained(spec.origMatchCase).asInstanceOf[HKTypeLambda]

def tryDisjoint: MatchResult =
val disjoint =
val defn.MatchCase(origPattern, _) = contrainedCaseLambda.resultType: @unchecked
if provablyDisjoint(scrut, origPattern) then
provablyDisjoint(scrut, origPattern)

def tryDisjoint: MatchResult =
if disjoint then
MatchResult.Disjoint
else
MatchResult.Stuck
Expand All @@ -3484,7 +3473,10 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
val defn.MatchCase(instantiatedPat, reduced) =
instantiateParamsSpec(instances, contrainedCaseLambda)(contrainedCaseLambda.resultType): @unchecked
if scrut <:< instantiatedPat then
MatchResult.Reduced(reduced)
if disjoint then
MatchResult.ReducedAndDisjoint
else
MatchResult.Reduced(reduced)
else
tryDisjoint
else
Expand All @@ -3508,6 +3500,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
this.poisoned = savedPoisoned
this.canWidenAbstract = saved

val disjoint = provablyDisjoint(scrut, pat)

def redux(canApprox: Boolean): MatchResult =
val instances = paramInstances(canApprox)(Array.fill(caseLambda.paramNames.length)(NoType), pat)
instantiateParams(instances)(body) match
Expand All @@ -3518,13 +3512,16 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
}
}
case redux =>
MatchResult.Reduced(redux)
if disjoint then
MatchResult.ReducedAndDisjoint
else
MatchResult.Reduced(redux)

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

inFrozenConstraint {
// Empty types break the basic assumption that if a scrutinee and a
// pattern are disjoint it's OK to reduce passed that pattern. Indeed,
// empty types viewed as a set of value is always a subset of any other
// types. As a result, we first check that the scrutinee isn't empty
// before proceeding with reduction. See `tests/neg/6570.scala` and
// `6570-1.scala` for examples that exploit emptiness to break match
// type soundness.

// If we revered the uncertainty case of this empty check, that is,
// `!provablyNonEmpty` instead of `provablyEmpty`, that would be
// obviously sound, but quite restrictive. With the current formulation,
// we need to be careful that `provablyEmpty` covers all the conditions
// used to conclude disjointness in `provablyDisjoint`.
if (provablyEmpty(scrut))
MatchTypeTrace.emptyScrutinee(scrut)
NoType
else if scrut.isError then
if scrut.isError then
// if the scrutinee is an error type
// then just return that as the result
// not doing so will result in the first type case matching
Expand Down
21 changes: 0 additions & 21 deletions tests/neg/12800.scala

This file was deleted.

116 changes: 116 additions & 0 deletions tests/neg/6570.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,116 @@
-- [E007] Type Mismatch Error: tests/neg/6570.scala:26:50 --------------------------------------------------------------
26 | def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing // error
| ^^^^^^^
| Found: UpperBoundParametricVariant.M[T]
| Required: Base.Trait2
|
| where: T is a type in method foo with bounds <: UpperBoundParametricVariant.Cov[Int]
|
|
| Note: a match type could not be fully reduced:
|
| trying to reduce UpperBoundParametricVariant.M[T]
| failed since selector T
| does not uniquely determine parameter x in
| case UpperBoundParametricVariant.Cov[x] => Base.N[x]
| The computed bounds for the parameter are:
| x <: Int
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:29:29 --------------------------------------------------------------
29 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:47:32 --------------------------------------------------------------
47 | def foo(c: Child): Trait2 = c.thing // error
| ^^^^^^^
| Found: InheritanceVariant.M[c.B]
| Required: Base.Trait2
|
| Note: a match type could not be fully reduced:
|
| trying to reduce InheritanceVariant.M[c.B]
| failed since selector c.B
| does not uniquely determine parameter a in
| case InheritanceVariant.Trick[a] => Base.N[a]
| The computed bounds for the parameter are:
| a >: Int
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:51:29 --------------------------------------------------------------
51 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:69:29 --------------------------------------------------------------
69 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:86:29 --------------------------------------------------------------
86 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:103:32 -------------------------------------------------------------
103 | def foo(c: Child): Trait2 = c.thing // error
| ^^^^^^^
| Found: UpperBoundVariant.M[c.A]
| Required: Base.Trait2
|
| Note: a match type could not be fully reduced:
|
| trying to reduce UpperBoundVariant.M[c.A]
| failed since selector c.A
| does not uniquely determine parameter t in
| case UpperBoundVariant.Cov[t] => Base.N[t]
| The computed bounds for the parameter are:
| t <: Int
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6570.scala:107:29 -------------------------------------------------------------
107 | def thing = new Trait1 {} // error
| ^
| Found: Object with Base.Trait1 {...}
| Required: Base.N[String & Int]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Base.N[String & Int]
| failed since selector String & Int
| is uninhabited (there are no values of that type).
|
| longer explanation available when compiling with `-explain`
6 changes: 4 additions & 2 deletions tests/neg/6571.check
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@
|
| trying to reduce Test.M[Test.Inv[Int] & Test.Inv[String]]
| failed since selector Test.Inv[Int] & Test.Inv[String]
| is uninhabited (there are no values of that type).
| does not match case Test.Inv[u] => u
| and cannot be shown to be disjoint from it either.
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/6571.scala:7:39 ---------------------------------------------------------------
Expand All @@ -21,6 +22,7 @@
|
| trying to reduce Test.M[Test.Inv[String] & Test.Inv[Int]]
| failed since selector Test.Inv[String] & Test.Inv[Int]
| is uninhabited (there are no values of that type).
| does not match case Test.Inv[u] => u
| and cannot be shown to be disjoint from it either.
|
| longer explanation available when compiling with `-explain`
19 changes: 19 additions & 0 deletions tests/pos/12800.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
object Test {
type FieldType2[K, +V] = V with KeyTag2[K, V]
trait KeyTag2[K, +V] extends Any

type WrapUpper = Tuple
type Wrap[A] = Tuple1[A]

type Extract[A <: WrapUpper] = A match {
case Wrap[h] => h
}

summon[Extract[Wrap[FieldType2["foo", Int]]] =:= FieldType2["foo", Int]]

// This used to cause an error because `Tuple1[FieldType2["foo", Int]]` was
// "provablyEmpty". Since we switched to testing the combination of
// `scrut <: pattern` *and* `provablyDisjoint(scrut, pattern)` instead, this
// particular example compiles, because `FieldType2["foo", Int]` is not
// `provablyDisjoint` from `h` (`Any`).
}

0 comments on commit 39da0ba

Please sign in to comment.