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/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 + + () + } +} 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 +} 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)] +}