From aefb05ad1e933db0e5664de11300949a7332f953 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 4 Jun 2020 12:33:38 +0200 Subject: [PATCH 1/3] Fix #9107: Restore constraints after MT reduction Because of `caseLambda = constrained(cas)` in `def matchCase`, subtyping wrongly things that it's OK to further constrain types introduced in match type patterns. This commit fixes the issue with a stronger version of `inFrozenConstraint` around match type reduction. --- .../dotty/tools/dotc/core/TypeComparer.scala | 43 +++++++++++-------- tests/neg/9107.scala | 14 ++++++ 2 files changed, 39 insertions(+), 18 deletions(-) create mode 100644 tests/neg/9107.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 7daf89a121b6..a6d4aa9a9f6d 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2848,25 +2848,32 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { MatchTypeTrace.noMatches(scrut, cases) NoType - 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)) - NoType - else - recur(cases) + // inFrozenConstraint is not sufficient here as it doesn't prevent + // parameters of type lambdas from being added to `constraint`, see + // ConstraintHandling.canConstrain and tests/neg/9107.scala. + val saved = constraint + try { + 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 reversed 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)) + NoType + else + recur(cases) + } } + finally constraint = saved } } diff --git a/tests/neg/9107.scala b/tests/neg/9107.scala new file mode 100644 index 000000000000..a0cbabd50b4d --- /dev/null +++ b/tests/neg/9107.scala @@ -0,0 +1,14 @@ +trait M[F[_]] +trait Inv[T] + +object Test { + def ev[X] = implicitly[ + (X match { case Inv[t] => Int }) =:= + (X match { case Inv[t] => t }) + ] // error + + def ev2[X] = implicitly[ + (M[[t] =>> runtime.MatchCase[Inv[t], Int]]) =:= + (M[[t] =>> runtime.MatchCase[Inv[t], t]]) + ] // error +} From 74a63011b22e7e04667640837e719f57d923c12d Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 4 Jun 2020 15:28:13 +0200 Subject: [PATCH 2/3] Turn 6697 into a neg test This subtyping check use to work because of the bug in question. Note that 6697 tries to use GADT knowledge that is currently unavailable on expression patterns (as demonstrated in 6697-2.scala), so I don't think we are in a urge to support this with match types. --- tests/{pos/6697.scala => neg/6697-1.scala} | 3 ++- tests/neg/6697-2.scala | 18 ++++++++++++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) rename tests/{pos/6697.scala => neg/6697-1.scala} (61%) create mode 100644 tests/neg/6697-2.scala diff --git a/tests/pos/6697.scala b/tests/neg/6697-1.scala similarity index 61% rename from tests/pos/6697.scala rename to tests/neg/6697-1.scala index 18a59d5b61f4..fbd6e21c1bfd 100644 --- a/tests/pos/6697.scala +++ b/tests/neg/6697-1.scala @@ -3,5 +3,6 @@ object Test { case class Of[sup, sub <: sup]() extends Off type Sup[O <: Off] = O match { case Of[sup, sub] => sup } type Sub[O <: Off] = O match { case Of[sup, sub] => sub } - type Copy[O <: Off] = Of[Sup[O], Sub[O]] + type Copy[O <: Off] = Of[Sup[O], Sub[O]] // error + // Type argument Test.Sub[O] does not conform to upper bound Test.Sup[O] } diff --git a/tests/neg/6697-2.scala b/tests/neg/6697-2.scala new file mode 100644 index 000000000000..588e7a24636f --- /dev/null +++ b/tests/neg/6697-2.scala @@ -0,0 +1,18 @@ +object Test { + sealed trait Off + case class Of[sup, sub <: sup]() extends Off + + def sup[O <: Off](o: O) = o match { + case _: Of[sup, sub] => + val a: sub = null.asInstanceOf + // Even though we know that sub <: sup from Of's bounds, that knowledge + // is lost in the body of pattern matching expressions... + + val b: sup = a // error + // Found: (a : sub) + // Required: sup + // where: sub is a type in method sup with bounds <: Test.Of[?, ?]#sup + + () + } +} From c20a8f99d7b058a6c9352eda9fda1021ee76b954 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Fri, 30 Apr 2021 15:00:44 +0200 Subject: [PATCH 3/3] Fix #9890: Add regression test --- tests/pos/9890.scala | 49 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 tests/pos/9890.scala diff --git a/tests/pos/9890.scala b/tests/pos/9890.scala new file mode 100644 index 000000000000..96d6f1db33b7 --- /dev/null +++ b/tests/pos/9890.scala @@ -0,0 +1,49 @@ +object Test { + import scala.compiletime.ops.int._ + + trait x + + type Range[Min <: Int, Max <: Int] <: Tuple = Min match { + case Max => EmptyTuple + case _ => Min *: Range[Min + 1, Max] + } + + type TupleMap[Tup <: Tuple, Bound, F[_ <: Bound]] <: Tuple = Tup match { + case EmptyTuple => EmptyTuple + case h *: t => F[h] *: TupleMap[t, Bound, F] + } + type TupleDedup[Tup <: Tuple, Mask] <: Tuple = Tup match { + case EmptyTuple => EmptyTuple + case h *: t => h match { + case Mask => TupleDedup[t, Mask] + case _ => h *: TupleDedup[t, h | Mask] + } + } + + type CoordToPos[r <: Int, c <: Int] = r * 9 + c + type Cell[r <: Int, c <: Int, Board <: Tuple] = Tuple.Elem[Board, CoordToPos[r, c]] + type Col[c <: Int, Board <: Tuple] = TupleMap[Range[0, 9], Int, [r <: Int] =>> Cell[r, c, Board]] + + type ColFromPos[Pos <: Int] = Pos % 9 + + type Sudoku1 = ( + x, x, x, x, 1, x, 4, x, 6, + 8, x, 1, 6, 2, x, x, x, 9, + x, 3, x, x, x, 9, x, 2, x, + + 5, x, 9, 1, 3, x, x, 6, x, + x, 6, x, 9, x, 2, x, 4, x, + x, 2, x, x, 6, 7, 8, x, 5, + + x, 9, x, 5, x, x, x, 3, x, + 3, x, x, x, 4, 6, 9, x, 7, + 6, x, 7, x, 9, x, x, x, x, + ) + + //compiles fine + summon[Col[ColFromPos[0], Sudoku1] =:= (x, 8, x, 5, x, x, x, 3, 6)] + + summon[TupleDedup[(x, 8, x, 5, x, x, x, 3, 6), Nothing] =:= (x, 8, 5, 3, 6)] + //but this doesn't + summon[TupleDedup[Col[ColFromPos[0], Sudoku1], Nothing] =:= (x, 8, 5, 3, 6)] +}