From b5a4ca50a34984acb82e931beb88511ffa2ddf95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 8 Dec 2023 11:18:04 +0100 Subject: [PATCH] Demonstrate more potential unsoundness with a CCE reproducer. This additional test demonstrates that relaxing the `isConcrete` in a particular way around `AndType`s would also cause unsoundness. This justifies new failures in the Open Community Build. --- .../dotty/tools/dotc/core/TypeComparer.scala | 3 + tests/neg/i13780-1.check | 39 +++++++++++ tests/neg/i13780-1.scala | 69 +++++++++++++++++++ 3 files changed, 111 insertions(+) create mode 100644 tests/neg/i13780-1.check create mode 100644 tests/neg/i13780-1.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index a8d27c6448c8..1b58dd8c1dbc 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3353,6 +3353,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { * upper bound of an abstract type. * * See notably neg/wildcard-match.scala for examples of this. + * + * See neg/i13780.scala and neg/i13780-1.scala for ClassCastException + * reproducers if we disable this check. */ def followEverythingConcrete(tp: Type): Type = diff --git a/tests/neg/i13780-1.check b/tests/neg/i13780-1.check new file mode 100644 index 000000000000..029ef3f3ac4b --- /dev/null +++ b/tests/neg/i13780-1.check @@ -0,0 +1,39 @@ +-- [E007] Type Mismatch Error: tests/neg/i13780-1.scala:38:24 ---------------------------------------------------------- +38 | case x: (h *: t) => x.head // error + | ^^^^^^ + | Found: Tuple.Head[VS & h *: t] + | Required: h + | + | where: VS is a type in method foo with bounds <: Tuple + | h is a type in method foo with bounds + | t is a type in method foo with bounds <: Tuple + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Tuple.Head[VS & h *: t] + | failed since selector VS & h *: t + | does not uniquely determine parameter x in + | case x *: _ => x + | The computed bounds for the parameter are: + | x <: h + | Note that implicit conversions were not tried because the result of an implicit conversion + | must be more specific than h + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/i13780-1.scala:52:31 ---------------------------------------------------------- +52 | def unpair: SelectH[Y & W] = "" // error + | ^^ + | Found: ("" : String) + | Required: SelectH[A.this.Y & A.this.W] + | + | Note: a match type could not be fully reduced: + | + | trying to reduce SelectH[A.this.Y & A.this.W] + | failed since selector A.this.Y & A.this.W + | does not uniquely determine parameter h in + | case h *: _ => h + | The computed bounds for the parameter are: + | h + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i13780-1.scala b/tests/neg/i13780-1.scala new file mode 100644 index 000000000000..39f06e520797 --- /dev/null +++ b/tests/neg/i13780-1.scala @@ -0,0 +1,69 @@ +/* It is tempting to relax the `isConcrete` test of match types for `AndType` + * in the following way: + * + * (isConcrete(tp.tp1) || !tp.tp1.derivesFrom(targetClass)) && (... same for tp.tp2) + * + * but the test in this file shows that this would be unsound. + * + * If we did relax the rule, it would help usages of match types applied to the + * singleton type of term pattern match scrutinees. For example: + * + * def foo[VS <: Tuple](x: VS): SelectH[VS] = x match + * case x: (h *: t) => x.head + * + * The type of `x` in the branch body is `(VS & (h *: t))`. The result of + * `x.head` is therefore a `Tuple.Head[VS & (h *: t)]`, which does not reduce + * according to the current rules, but would reduce to `h` with the relaxed + * rule. + * + * Note that the code can be fixed with an explicit type argument to `.head`: + * + * def foo[VS <: Tuple](x: VS): SelectH[VS] = x match + * case x: (h *: t) => x.head[h *: t] + * + * So it *seems* like it would be fine to relax the rule, based on the insight + * that `VS` in `Tuple.Head[VS & (h *: t)]` does not contribute anything to the + * computed type capture in `Tuple.Head`. + * + * The test is this file demonstrates that relaxing the rule can cause + * unsoundness. So don't do it. + */ + +type SelectH[VS <: Tuple] = VS match + case h *: ? => h + +// The original example found in the fingo/spata library +object ExampleFromSpata: + def foo[VS <: Tuple](x: VS): SelectH[VS] = x match + case x: (h *: t) => x.head // error + + def bar[VS <: Tuple](x: VS): SelectH[VS] = x match + case x: (h *: t) => x.head[h *: t] // ok +end ExampleFromSpata + +trait Z { + type Y <: Tuple + type W <: Tuple + def unpair: SelectH[Y & W] +} + +class A extends Z { + type Y = Tuple2[Any, Any] + def unpair: SelectH[Y & W] = "" // error + def any: Any = unpair +} + +class B extends A { this: Z => + type W = Tuple2[Int, Int] + def int: Int = unpair +} + +class C extends A { this: Z => + type W = Tuple2[String, String] + def string: String = unpair +} + +object Main { + def main(args: Array[String]): Unit = + println((new B).int + 1) // would give ClassCastException +}