diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index e8354dcf5768..f6f2b50c4b0e 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`). +}