From decfade32805bf66e81643b33a963eb981f913f7 Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 12 Jun 2022 10:27:18 +0200 Subject: [PATCH] Refine Matchtype checking Take up #13780 again, but refine it so that abstract types are allowed in match type reduction as long as they uniquely instantiate type parameters of the type pattern. Fixes #11982 --- .../tools/dotc/core/MatchTypeTrace.scala | 9 ++ .../dotty/tools/dotc/core/TypeComparer.scala | 97 +++++++++++++------ .../dotty/tools/dotc/CompilationTests.scala | 1 + tests/neg/6570-1.check | 30 ++++++ tests/neg/6570-1.scala | 2 +- tests/neg/6570.scala | 6 +- tests/neg/i11982.check | 39 ++++++++ tests/neg/i11982.scala | 27 ++++++ tests/neg/i13780.check | 34 +++++++ tests/neg/i13780.scala | 30 ++++++ tests/neg/wildcard-match.scala | 46 +++++++++ .../typeclass-derivation1.scala | 0 12 files changed, 288 insertions(+), 33 deletions(-) create mode 100644 tests/neg/6570-1.check create mode 100644 tests/neg/i11982.check create mode 100644 tests/neg/i11982.scala create mode 100644 tests/neg/i13780.check create mode 100644 tests/neg/i13780.scala create mode 100644 tests/neg/wildcard-match.scala rename tests/{run => run-custom-args}/typeclass-derivation1.scala (100%) diff --git a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala index bc08dbc36eea..7e1326d39a52 100644 --- a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala +++ b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala @@ -4,6 +4,7 @@ package core import Types._, Contexts._, Symbols._, Decorators._ import util.Property +import Names.Name /** A utility module to produce match type reduction traces in error messages. */ @@ -13,6 +14,7 @@ object MatchTypeTrace: case TryReduce(scrut: Type) case NoMatches(scrut: Type, cases: List[Type]) case Stuck(scrut: Type, stuckCase: Type, otherCases: List[Type]) + case NoInstance(scrut: Type, stuckCase: Type, pname: Name, bounds: TypeBounds) case EmptyScrutinee(scrut: Type) import TraceEntry._ @@ -62,6 +64,9 @@ object MatchTypeTrace: def stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])(using Context) = matchTypeFail(Stuck(scrut, stuckCase, otherCases)) + def noInstance(scrut: Type, stuckCase: Type, pname: Name, bounds: TypeBounds)(using Context) = + matchTypeFail(NoInstance(scrut, stuckCase, pname, bounds)) + /** Record a failure that scrutinee `scrut` is provably empty. * Only the first failure is recorded. */ @@ -114,6 +119,10 @@ object MatchTypeTrace: | Therefore, reduction cannot advance to the remaining case$s | | ${casesText(otherCases)}""" + case NoInstance(scrut, stuckCase, pname, bounds) => + i""" failed since selector $scrut + | does not uniquely determine parameter $pname in ${caseText(stuckCase)} + | The computed bounds for the parameter are: $bounds.""" def noMatchesText(scrut: Type, cases: List[Type])(using Context): String = i"""failed since selector $scrut diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 5f9f3e43569b..13d85b57b23c 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -60,6 +60,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling /** Indicates whether the subtype check used GADT bounds */ private var GADTused: Boolean = false + protected var canWidenAbstract: Boolean = true + private var myInstance: TypeComparer = this def currentInstance: TypeComparer = myInstance @@ -757,9 +759,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling def tryBaseType(cls2: Symbol) = { val base = nonExprBaseType(tp1, cls2) - if (base.exists && (base `ne` tp1)) - isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) || - base.isInstanceOf[OrType] && fourthTry + if base.exists && (base ne tp1) + && (!caseLambda.exists || canWidenAbstract || tp1.widen.underlyingClassRef(refinementOK = true).exists) + then + isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) + || base.isInstanceOf[OrType] && fourthTry // if base is a disjunction, this might have come from a tp1 type that // expands to a match type. In this case, we should try to reduce the type // and compare the redux. This is done in fourthTry @@ -776,7 +780,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling || narrowGADTBounds(tp1, tp2, approx, isUpper = true)) && (tp2.isAny || GADTusage(tp1.symbol)) - isSubType(hi1, tp2, approx.addLow) || compareGADT || tryLiftedToThis1 + (!caseLambda.exists || canWidenAbstract) && isSubType(hi1, tp2, approx.addLow) + || compareGADT + || tryLiftedToThis1 case _ => // `Mode.RelaxedOverriding` is only enabled when checking Java overriding // in explicit nulls, and `Null` becomes a bottom type, which allows @@ -2849,7 +2855,16 @@ object TypeComparer { comparing(_.tracked(op)) } +object TrackingTypeComparer: + enum MatchResult: + case Reduced(tp: Type) + case Disjoint + case Stuck + case NoInstance(param: Name, bounds: TypeBounds) + class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { + import TrackingTypeComparer.* + init(initctx) override def trackingTypeComparer = this @@ -2887,15 +2902,25 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { } def matchCases(scrut: Type, cases: List[Type])(using Context): Type = { - def paramInstances = new TypeAccumulator[Array[Type]] { - def apply(inst: Array[Type], t: Type) = t match { - case t @ TypeParamRef(b, n) if b `eq` caseLambda => - inst(n) = approximation(t, fromBelow = variance >= 0).simplified - inst + + def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]: + def apply(insts: Array[Type], t: Type) = t match + case param @ TypeParamRef(b, n) if b eq caseLambda => + insts(n) = { + if canApprox then + approximation(param, fromBelow = variance >= 0) + else constraint.entry(param) match + case entry: TypeBounds => + val lo = fullLowerBound(param) + val hi = fullUpperBound(param) + if isSubType(hi, lo) then lo else TypeBounds(lo, hi) + case inst => + assert(inst.exists, i"param = $param\nconstraint = $constraint") + inst + }.simplified + insts case _ => - foldOver(inst, t) - } - } + foldOver(insts, t) def instantiateParams(inst: Array[Type]) = new TypeMap { def apply(t: Type) = t match { @@ -2911,7 +2936,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { * None if the match fails and we should consider the following cases * because scrutinee and pattern do not overlap */ - def matchCase(cas: Type): Option[Type] = trace(i"match case $cas vs $scrut", matchTypes) { + def matchCase(cas: Type): MatchResult = trace(i"match case $cas vs $scrut", matchTypes) { val cas1 = cas match { case cas: HKTypeLambda => caseLambda = constrained(cas) @@ -2922,34 +2947,48 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { val defn.MatchCase(pat, body) = cas1: @unchecked - if (isSubType(scrut, pat)) - // `scrut` is a subtype of `pat`: *It's a Match!* - Some { - caseLambda match { - case caseLambda: HKTypeLambda => - val instances = paramInstances(new Array(caseLambda.paramNames.length), pat) - instantiateParams(instances)(body).simplified - case _ => - body - } - } + def matches(canWidenAbstract: Boolean): Boolean = + val saved = this.canWidenAbstract + this.canWidenAbstract = canWidenAbstract + try necessarySubType(scrut, pat) + finally this.canWidenAbstract = saved + + def redux(canApprox: Boolean): MatchResult = + caseLambda match + case caseLambda: HKTypeLambda => + val instances = paramInstances(canApprox)(new Array(caseLambda.paramNames.length), pat) + instances.indices.find(instances(_).isInstanceOf[TypeBounds]) match + case Some(i) if !canApprox => + MatchResult.NoInstance(caseLambda.paramNames(i), instances(i).bounds) + case _ => + MatchResult.Reduced(instantiateParams(instances)(body).simplified) + case _ => + MatchResult.Reduced(body) + + if caseLambda.exists && matches(canWidenAbstract = false) then + redux(canApprox = true) + else if matches(canWidenAbstract = true) then + redux(canApprox = false) else if (provablyDisjoint(scrut, pat)) // We found a proof that `scrut` and `pat` are incompatible. // The search continues. - None + MatchResult.Disjoint else - Some(NoType) + MatchResult.Stuck } def recur(remaining: List[Type]): Type = remaining match case cas :: remaining1 => matchCase(cas) match - case None => + case MatchResult.Disjoint => recur(remaining1) - case Some(NoType) => + case MatchResult.Stuck => MatchTypeTrace.stuck(scrut, cas, remaining1) NoType - case Some(tp) => + case MatchResult.NoInstance(pname, bounds) => + MatchTypeTrace.noInstance(scrut, cas, pname, bounds) + NoType + case MatchResult.Reduced(tp) => tp case Nil => val casesText = MatchTypeTrace.noMatchesText(scrut, cases) diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala index 6ad524e07930..e64a06e684a4 100644 --- a/compiler/test/dotty/tools/dotc/CompilationTests.scala +++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala @@ -200,6 +200,7 @@ class CompilationTests { @Test def runAll: Unit = { implicit val testGroup: TestGroup = TestGroup("runAll") aggregateTests( + compileFile("tests/run-custom-args/typeclass-derivation1.scala", defaultOptions.without(yCheckOptions*)), compileFile("tests/run-custom-args/tuple-cons.scala", allowDeepSubtypes), compileFile("tests/run-custom-args/i5256.scala", allowDeepSubtypes), compileFile("tests/run-custom-args/no-useless-forwarders.scala", defaultOptions and "-Xmixin-force-forwarders:false"), diff --git a/tests/neg/6570-1.check b/tests/neg/6570-1.check new file mode 100644 index 000000000000..023d34a4a27d --- /dev/null +++ b/tests/neg/6570-1.check @@ -0,0 +1,30 @@ +-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:23:27 ------------------------------------------------------------ +23 | def thing = new Trait1 {} // error + | ^ + | Found: Object with Trait1 {...} + | Required: N[Box[Int & String]] + | + | Note: a match type could not be fully reduced: + | + | trying to reduce N[Box[Int & String]] + | failed since selector Box[Int & String] + | is uninhabited (there are no values of that type). + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:36:54 ------------------------------------------------------------ +36 | def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing // error + | ^^^^^^^ + | Found: M[T] + | Required: Trait2 + | + | where: T is a type in method foo with bounds <: Cov[Box[Int]] + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce M[T] + | failed since selector T + | does not uniquely determine parameter x in case Cov[x] => N[x] + | The computed bounds for the parameter are: >: Box[Int]. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/6570-1.scala b/tests/neg/6570-1.scala index b24d09782039..0903d188cb16 100644 --- a/tests/neg/6570-1.scala +++ b/tests/neg/6570-1.scala @@ -33,7 +33,7 @@ class Asploder extends Root[Cov[Box[Int & String]]] { } object Main { - def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing + def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing // error def explode = foo(new Asploder) def main(args: Array[String]): Unit = diff --git a/tests/neg/6570.scala b/tests/neg/6570.scala index d0b55fe739de..f36471868d9b 100644 --- a/tests/neg/6570.scala +++ b/tests/neg/6570.scala @@ -21,7 +21,7 @@ object UpperBoundParametricVariant { trait Child[A <: Cov[Int]] extends Root[A] // we reduce `M[T]` to `Trait2`, even though we cannot be certain of that - def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing + def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing // error class Asploder extends Child[Cov[String & Int]] { def thing = new Trait1 {} // error @@ -42,7 +42,7 @@ object InheritanceVariant { trait Child extends Root { type B <: { type A <: Int } } - def foo(c: Child): Trait2 = c.thing + def foo(c: Child): Trait2 = c.thing // error class Asploder extends Child { type B = { type A = String & Int } @@ -98,7 +98,7 @@ object UpperBoundVariant { trait Child extends Root { type A <: Cov[Int] } - def foo(c: Child): Trait2 = c.thing + def foo(c: Child): Trait2 = c.thing // error class Asploder extends Child { type A = Cov[String & Int] diff --git a/tests/neg/i11982.check b/tests/neg/i11982.check new file mode 100644 index 000000000000..b87c9376e91a --- /dev/null +++ b/tests/neg/i11982.check @@ -0,0 +1,39 @@ +-- [E057] Type Mismatch Error: tests/neg/i11982.scala:9:34 ------------------------------------------------------------- +9 | b: ValueOf[Tuple.Head[Tuple.Tail[X]]] // error + | ^ + | Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Tuple.Tail[X] + | failed since selector X + | does not uniquely determine parameter xs in case _ *: xs => xs + | The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple. + | + | longer explanation available when compiling with `-explain` +-- [E057] Type Mismatch Error: tests/neg/i11982.scala:10:38 ------------------------------------------------------------ +10 | ): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] = // error + | ^ + | Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Tuple.Tail[X] + | failed since selector X + | does not uniquely determine parameter xs in case _ *: xs => xs + | The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple. + | + | longer explanation available when compiling with `-explain` +-- [E057] Type Mismatch Error: tests/neg/i11982.scala:12:25 ------------------------------------------------------------ +12 | type BB = Tuple.Head[Tuple.Tail[X]] // error + | ^ + | Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Tuple.Tail[X] + | failed since selector X + | does not uniquely determine parameter xs in case _ *: xs => xs + | The computed bounds for the parameter are: >: Any *: EmptyTuple.type <: Tuple. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i11982.scala b/tests/neg/i11982.scala new file mode 100644 index 000000000000..7a01f84bc157 --- /dev/null +++ b/tests/neg/i11982.scala @@ -0,0 +1,27 @@ +package tuplefun +object Unpair { + + def pair[A, B](using a: ValueOf[A], b: ValueOf[B]): Tuple2[A, B] = + (a.value, b.value) + + def unpair[X <: Tuple2[?, ?]]( + using a: ValueOf[Tuple.Head[X]], + b: ValueOf[Tuple.Head[Tuple.Tail[X]]] // error + ): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] = // error + type AA = Tuple.Head[X] + type BB = Tuple.Head[Tuple.Tail[X]] // error + pair[AA, BB](using a, b) +} + +object UnpairApp { + import Unpair._ + + type Tshape = ("msg", 42) + + // the following won't compile when in the same file as Unpair + val p1: ("msg", 42) = unpair[Tshape] + + @main def pairHello: Unit = + assert(p1 == ("msg", 42)) + println(p1) +} \ No newline at end of file diff --git a/tests/neg/i13780.check b/tests/neg/i13780.check new file mode 100644 index 000000000000..fdb8f0ee6c90 --- /dev/null +++ b/tests/neg/i13780.check @@ -0,0 +1,34 @@ +-- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------ +18 | def int[X <: Y]: Int = unpair[X] // error + | ^^^^^^^^^ + | Found: Head[X] + | Required: Int + | + | where: X is a type in method int with bounds <: B.this.Y + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Head[X] + | failed since selector X + | does not uniquely determine parameter a in case (a, b) => a + | The computed bounds for the parameter are: >: Int. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------ +23 | def string[X <: Y]: String = unpair[X] // error + | ^^^^^^^^^ + | Found: Head[X] + | Required: String + | + | where: X is a type in method string with bounds <: C.this.Y + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Head[X] + | failed since selector X + | does not uniquely determine parameter a in case (a, b) => a + | The computed bounds for the parameter are: >: String. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i13780.scala b/tests/neg/i13780.scala new file mode 100644 index 000000000000..7e7e2e3ecb74 --- /dev/null +++ b/tests/neg/i13780.scala @@ -0,0 +1,30 @@ +type Head[X] = X match { + case Tuple2[a, b] => a +} + +trait Z { + type Y + def unpair[X <: Y]: Head[X] +} + +class A extends Z { + type Y <: Tuple2[Any, Any] + def unpair[X <: Y]: Head[X] = "" + def any[X <: Y]: Any = unpair[X] +} + +class B extends A { this: Z => + type Y = Tuple2[Int, Int] + def int[X <: Y]: Int = unpair[X] // error +} + +class C extends A { this: Z => + type Y = Tuple2[String, String] + def string[X <: Y]: String = unpair[X] // error +} + +object Main { + def main(args: Array[String]): Unit = { + println((new B).int + 1) // would give ClassCastException + } +} \ No newline at end of file diff --git a/tests/neg/wildcard-match.scala b/tests/neg/wildcard-match.scala new file mode 100644 index 000000000000..326a97485bd2 --- /dev/null +++ b/tests/neg/wildcard-match.scala @@ -0,0 +1,46 @@ +class Box[T](x: T) + +class Cov[+T](x: T) +class Contrav[-T](x: T) + +type BoxElem[X] = X match + case Box[a] => a + +type BoxToList[X] = X match + case Box[a] => List[a] + +type CovElem[X] = X match + case Cov[a] => a + +type CovToList[X] = X match + case Cov[a] => List[a] + +type ContravElem[X] = X match + case Contrav[a] => a + +type ContravToList[X] = X match + case Contrav[a] => List[a] + +class C + +def f[X <: Box[C], Y <: Cov[C], Z <: Contrav[C]] = + def a: BoxElem[X] = ??? // OK + val _: C = a + + def a1: CovElem[Y] = ??? + val _: C = a1 // error + + def a2: ContravElem[Z] = ??? + val _: C = a2 // error + + def b: BoxToList[X] = ??? // OK + val _: List[C] = b + + def b1: CovToList[Y] = ??? + val _: List[C] = b1 // error + + def b2: ContravElem[Z] = ??? + val _: List[C] = b2 // error + + + diff --git a/tests/run/typeclass-derivation1.scala b/tests/run-custom-args/typeclass-derivation1.scala similarity index 100% rename from tests/run/typeclass-derivation1.scala rename to tests/run-custom-args/typeclass-derivation1.scala