From 9839f09be9ed9185b3acc77641463b4a948cb74c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Wed, 30 Aug 2023 11:57:28 +0200 Subject: [PATCH] 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. --- .../dotty/tools/dotc/core/TypeComparer.scala | 87 ++++++------- tests/neg/12800.scala | 21 ---- tests/neg/6570.check | 116 ++++++++++++++++++ tests/neg/6571.check | 6 +- tests/pos/12800.scala | 19 +++ 5 files changed, 178 insertions(+), 71 deletions(-) delete mode 100644 tests/neg/12800.scala create mode 100644 tests/neg/6570.check create mode 100644 tests/pos/12800.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 94b3d7966f34..2c5372830567 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -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`. @@ -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.* @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/tests/neg/12800.scala b/tests/neg/12800.scala deleted file mode 100644 index 164276396bec..000000000000 --- a/tests/neg/12800.scala +++ /dev/null @@ -1,21 +0,0 @@ -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]] // error - // ^ - // Cannot prove that Main.Extract[Tuple1[Main.FieldType2[("foo" : String), Int]]] =:= Main.FieldType2[("foo" : String), Int]. - // - // Note: a match type could not be fully reduced: - // - // trying to reduce Main.Extract[Tuple1[Main.FieldType2[("foo" : String), Int]]] - // failed since selector Tuple1[Main.FieldType2[("foo" : String), Int]] - // is uninhabited. -} diff --git a/tests/neg/6570.check b/tests/neg/6570.check new file mode 100644 index 000000000000..f32c3790fb90 --- /dev/null +++ b/tests/neg/6570.check @@ -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` diff --git a/tests/neg/6571.check b/tests/neg/6571.check index 4172abb2919b..cb2fc50b86d2 100644 --- a/tests/neg/6571.check +++ b/tests/neg/6571.check @@ -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 --------------------------------------------------------------- @@ -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` diff --git a/tests/pos/12800.scala b/tests/pos/12800.scala new file mode 100644 index 000000000000..be625cb894e0 --- /dev/null +++ b/tests/pos/12800.scala @@ -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`). +}