From c96d8478ed70f4ff42aa1ce04133c867376e6b4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Thu, 20 Jul 2023 18:34:09 +0200 Subject: [PATCH 01/17] Introduce MatchTypeCaseSpec to categorize match type cases. For now, we only have `SubTypeTest` and `LegacyPatMat`. * `SubTypeTest` is used when there is no type capture. * `LegacyPatMat` is used when there are captures. In the match type reduction algorithm, we already have a simpler path for `SubTypeTest`. The `LegacyPatMat` path is basically the same as before, but with static knowledge that we have an `HKTypeLambda`. --- .../tools/dotc/core/MatchTypeTrace.scala | 15 +++-- .../dotty/tools/dotc/core/TypeComparer.scala | 60 ++++++++++--------- .../src/dotty/tools/dotc/core/Types.scala | 20 ++++++- 3 files changed, 61 insertions(+), 34 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala index 5fc1b3137e90..7bdcba19c99b 100644 --- a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala +++ b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala @@ -12,8 +12,8 @@ object MatchTypeTrace: private enum TraceEntry: case TryReduce(scrut: Type) - case Stuck(scrut: Type, stuckCase: Type, otherCases: List[Type]) - case NoInstance(scrut: Type, stuckCase: Type, fails: List[(Name, TypeBounds)]) + case Stuck(scrut: Type, stuckCase: MatchTypeCaseSpec, otherCases: List[MatchTypeCaseSpec]) + case NoInstance(scrut: Type, stuckCase: MatchTypeCaseSpec, fails: List[(Name, TypeBounds)]) case EmptyScrutinee(scrut: Type) import TraceEntry.* @@ -54,10 +54,10 @@ object MatchTypeTrace: * not disjoint from it either, which means that the remaining cases `otherCases` * cannot be visited. Only the first failure is recorded. */ - def stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])(using Context) = + def stuck(scrut: Type, stuckCase: MatchTypeCaseSpec, otherCases: List[MatchTypeCaseSpec])(using Context) = matchTypeFail(Stuck(scrut, stuckCase, otherCases)) - def noInstance(scrut: Type, stuckCase: Type, fails: List[(Name, TypeBounds)])(using Context) = + def noInstance(scrut: Type, stuckCase: MatchTypeCaseSpec, fails: List[(Name, TypeBounds)])(using Context) = matchTypeFail(NoInstance(scrut, stuckCase, fails)) /** Record a failure that scrutinee `scrut` is provably empty. @@ -80,13 +80,16 @@ object MatchTypeTrace: case _ => op + def caseText(spec: MatchTypeCaseSpec)(using Context): String = + caseText(spec.origMatchCase) + def caseText(tp: Type)(using Context): String = tp match case tp: HKTypeLambda => caseText(tp.resultType) case defn.MatchCase(any, body) if any eq defn.AnyType => i"case _ => $body" case defn.MatchCase(pat, body) => i"case $pat => $body" case _ => i"case $tp" - private def casesText(cases: List[Type])(using Context) = + private def casesText(cases: List[MatchTypeCaseSpec])(using Context) = i"${cases.map(caseText)}%\n %" private def explainEntry(entry: TraceEntry)(using Context): String = entry match @@ -116,7 +119,7 @@ object MatchTypeTrace: | ${fails.map((name, bounds) => i"$name$bounds")}%\n %""" /** The failure message when the scrutinee `scrut` does not match any case in `cases`. */ - def noMatchesText(scrut: Type, cases: List[Type])(using Context): String = + def noMatchesText(scrut: Type, cases: List[MatchTypeCaseSpec])(using Context): String = i"""failed since selector $scrut |matches none of the cases | diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 9ed631a7359c..c0fecce7d15e 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3197,7 +3197,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { super.typeVarInstance(tvar) } - def matchCases(scrut: Type, cases: List[Type])(using Context): Type = { + def matchCases(scrut: Type, cases: List[MatchTypeCaseSpec])(using Context): Type = { // a reference for the type parameters poisoned during matching // for use during the reduction step var poisoned: Set[TypeParamRef] = Set.empty @@ -3238,16 +3238,26 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { } /** Match a single case. */ - def matchCase(cas: Type): MatchResult = trace(i"$scrut match ${MatchTypeTrace.caseText(cas)}", matchTypes, show = true) { - val cas1 = cas match { - case cas: HKTypeLambda => - caseLambda = constrained(cas, ast.tpd.EmptyTree)._1 - caseLambda.resultType - case _ => - cas - } + def matchCase(cas: MatchTypeCaseSpec): MatchResult = trace(i"$scrut match ${MatchTypeTrace.caseText(cas)}", matchTypes, show = true) { + cas match + case cas: MatchTypeCaseSpec.SubTypeTest => matchSubTypeTest(cas) + case cas: MatchTypeCaseSpec.LegacyPatMat => matchLegacyPatMat(cas) + } + + def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult = + if necessarySubType(scrut, spec.pattern) then + MatchResult.Reduced(spec.body) + else if provablyDisjoint(scrut, spec.pattern) then + MatchResult.Disjoint + else + MatchResult.Stuck + end matchSubTypeTest - val defn.MatchCase(pat, body) = cas1: @unchecked + def matchLegacyPatMat(spec: MatchTypeCaseSpec.LegacyPatMat): MatchResult = + val caseLambda = constrained(spec.origMatchCase, ast.tpd.EmptyTree)._1.asInstanceOf[HKTypeLambda] + this.caseLambda = caseLambda + + val defn.MatchCase(pat, body) = caseLambda.resultType: @unchecked def matches(canWidenAbstract: Boolean): Boolean = val saved = this.canWidenAbstract @@ -3261,22 +3271,18 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { this.canWidenAbstract = saved def redux(canApprox: Boolean): MatchResult = - caseLambda match - case caseLambda: HKTypeLambda => - val instances = paramInstances(canApprox)(Array.fill(caseLambda.paramNames.length)(NoType), pat) - instantiateParams(instances)(body) match - case Range(lo, hi) => - MatchResult.NoInstance { - caseLambda.paramNames.zip(instances).collect { - case (name, Range(lo, hi)) => (name, TypeBounds(lo, hi)) - } - } - case redux => - MatchResult.Reduced(redux) - case _ => - MatchResult.Reduced(body) + val instances = paramInstances(canApprox)(Array.fill(caseLambda.paramNames.length)(NoType), pat) + instantiateParams(instances)(body) match + case Range(lo, hi) => + MatchResult.NoInstance { + caseLambda.paramNames.zip(instances).collect { + case (name, Range(lo, hi)) => (name, TypeBounds(lo, hi)) + } + } + case redux => + MatchResult.Reduced(redux) - if caseLambda.exists && matches(canWidenAbstract = false) then + if matches(canWidenAbstract = false) then redux(canApprox = true) else if matches(canWidenAbstract = true) then redux(canApprox = false) @@ -3286,9 +3292,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { MatchResult.Disjoint else MatchResult.Stuck - } + end matchLegacyPatMat - def recur(remaining: List[Type]): Type = remaining match + def recur(remaining: List[MatchTypeCaseSpec]): Type = remaining match case cas :: remaining1 => matchCase(cas) match case MatchResult.Disjoint => diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index e5c166f28d78..c17d33fc6bef 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -5036,7 +5036,7 @@ object Types extends TypeUtils { trace(i"reduce match type $this $hashCode", matchTypes, show = true)(inMode(Mode.Type) { def matchCases(cmp: TrackingTypeComparer): Type = val saved = ctx.typerState.snapshot() - try cmp.matchCases(scrutinee.normalized, cases) + try cmp.matchCases(scrutinee.normalized, cases.map(MatchTypeCaseSpec.analyze(_))) catch case ex: Throwable => handleRecursive("reduce type ", i"$scrutinee match ...", ex) finally @@ -5088,6 +5088,24 @@ object Types extends TypeUtils { case _ => None } + enum MatchTypeCaseSpec: + case SubTypeTest(origMatchCase: Type, pattern: Type, body: Type) + case LegacyPatMat(origMatchCase: HKTypeLambda) + + def origMatchCase: Type + end MatchTypeCaseSpec + + object MatchTypeCaseSpec: + def analyze(cas: Type)(using Context): MatchTypeCaseSpec = + cas match + case cas: HKTypeLambda => + LegacyPatMat(cas) + case _ => + val defn.MatchCase(pat, body) = cas: @unchecked + SubTypeTest(cas, pat, body) + end analyze + end MatchTypeCaseSpec + // ------ ClassInfo, Type Bounds -------------------------------------------------- type TypeOrSymbol = Type | Symbol From 5260c6023fb24d0362e55c5fedc320b562cb553f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 24 Nov 2023 17:06:05 +0100 Subject: [PATCH 02/17] Use new specced match types for class type constructors. This is the first step in using the new specified algorithm for match type reduction. When the pattern of a case satisfies elibility conditions, we use the new algorithm. Otherwise, we fall back on the legacy algorithm. To be eligible, a pattern with at least one capture must be: an applied *class* type constructor whose arguments are all: - either a type capture, - or a fully defined type that contains no inner capture, - or the argument must be in covariant position and recursively qualify to the elibility conditions. With those criteria, all the type captures can be *computed* using `baseType`, instead of inferred through the full `TypeComparer` machinery. The new algorithm directly handles preventing widening abstract types, when doing so leads to captures being under-defined. With the legacy algorithm, this prevention is scattered elsewhere in the type comparer. Making it centralized improves the error messages in those situations; it seems they were previously entirely misleading (see changed check files). --- .../dotty/tools/dotc/core/TypeComparer.scala | 137 +++++++++++++++++- .../src/dotty/tools/dotc/core/Types.scala | 67 ++++++++- tests/neg/6570-1.check | 2 +- tests/neg/i11982a.check | 6 +- tests/neg/i12049.check | 4 +- tests/neg/i13780.check | 12 +- tests/neg/wildcard-match.check | 94 ++++++++++++ tests/neg/wildcard-match.scala | 15 ++ 8 files changed, 321 insertions(+), 16 deletions(-) create mode 100644 tests/neg/wildcard-match.check diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index c0fecce7d15e..4cd97cb6ef75 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3237,11 +3237,22 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { } } + def instantiateParamsSpec(insts: Array[Type], caseLambda: HKTypeLambda) = new TypeMap { + variance = 0 + + def apply(t: Type) = t match { + case t @ TypeParamRef(b, n) if b `eq` caseLambda => insts(n) + case t: LazyRef => apply(t.ref) + case _ => mapOver(t) + } + } + /** Match a single case. */ def matchCase(cas: MatchTypeCaseSpec): MatchResult = trace(i"$scrut match ${MatchTypeTrace.caseText(cas)}", matchTypes, show = true) { cas match - case cas: MatchTypeCaseSpec.SubTypeTest => matchSubTypeTest(cas) - case cas: MatchTypeCaseSpec.LegacyPatMat => matchLegacyPatMat(cas) + case cas: MatchTypeCaseSpec.SubTypeTest => matchSubTypeTest(cas) + case cas: MatchTypeCaseSpec.SpeccedPatMat => matchSpeccedPatMat(cas) + case cas: MatchTypeCaseSpec.LegacyPatMat => matchLegacyPatMat(cas) } def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult = @@ -3253,6 +3264,128 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { MatchResult.Stuck end matchSubTypeTest + def matchSpeccedPatMat(spec: MatchTypeCaseSpec.SpeccedPatMat): MatchResult = + /* Concreteness checking + * + * When following a baseType and reaching a non-wildcard, in-variant-pos type capture, + * we have to make sure that the scrutinee is concrete enough to uniquely determine + * the values of the captures. This comes down to checking that we do not follow any + * upper bound of an abstract type. + * + * See notably neg/wildcard-match.scala for examples of this. + */ + + def followEverythingConcrete(tp: Type): Type = + val widenedTp = tp.widenDealias + val tp1 = widenedTp.normalized + + def followTp1: Type = + // If both widenDealias and normalized did something, start again + if (tp1 ne widenedTp) && (widenedTp ne tp) then followEverythingConcrete(tp1) + else tp1 + + tp1 match + case tp1: TypeRef => + tp1.info match + case TypeAlias(tl: HKTypeLambda) => tl + case MatchAlias(tl: HKTypeLambda) => tl + case _ => followTp1 + case tp1 @ AppliedType(tycon, args) => + val concreteTycon = followEverythingConcrete(tycon) + if concreteTycon eq tycon then followTp1 + else followEverythingConcrete(concreteTycon.applyIfParameterized(args)) + case _ => + followTp1 + end followEverythingConcrete + + def isConcrete(tp: Type): Boolean = + followEverythingConcrete(tp) match + case tp1: AndOrType => isConcrete(tp1.tp1) && isConcrete(tp1.tp2) + case tp1 => tp1.underlyingClassRef(refinementOK = true).exists + + // Actual matching logic + + val instances = Array.fill[Type](spec.captureCount)(NoType) + + def rec(pattern: MatchTypeCasePattern, scrut: Type, variance: Int, scrutIsWidenedAbstract: Boolean): Boolean = + pattern match + case MatchTypeCasePattern.Capture(num, isWildcard) => + instances(num) = scrut match + case scrut: TypeBounds => + if isWildcard then + // anything will do, as long as it conforms to the bounds for the subsequent `scrut <:< instantiatedPat` test + scrut.hi + else if scrutIsWidenedAbstract then + // always keep the TypeBounds so that we can report the correct NoInstances + scrut + else + variance match + case 1 => scrut.hi + case -1 => scrut.lo + case 0 => scrut + case _ => + if !isWildcard && scrutIsWidenedAbstract && variance != 0 then + // force a TypeBounds to report the correct NoInstances + // the Nothing and Any bounds are used so that they are not displayed; not for themselves in particular + if variance > 0 then TypeBounds(defn.NothingType, scrut) + else TypeBounds(scrut, defn.AnyType) + else + scrut + !instances(num).isError + + case MatchTypeCasePattern.TypeTest(tpe) => + // The actual type test is handled by `scrut <:< instantiatedPat` + true + + case MatchTypeCasePattern.BaseTypeTest(classType, argPatterns, needsConcreteScrut) => + val cls = classType.classSymbol.asClass + scrut.baseType(cls) match + case base @ AppliedType(baseTycon, baseArgs) if baseTycon =:= classType => + val innerScrutIsWidenedAbstract = + scrutIsWidenedAbstract + || (needsConcreteScrut && !isConcrete(scrut)) // no point in checking concreteness if it does not need to be concrete + + def matchArgs(argPatterns: List[MatchTypeCasePattern], baseArgs: List[Type], tparams: List[TypeParamInfo]): Boolean = + if argPatterns.isEmpty then + true + else + rec(argPatterns.head, baseArgs.head, tparams.head.paramVarianceSign, innerScrutIsWidenedAbstract) + && matchArgs(argPatterns.tail, baseArgs.tail, tparams.tail) + + matchArgs(argPatterns, baseArgs, classType.typeParams) + + case _ => + false + end rec + + // This might not be needed + val constrainedCaseLambda = constrained(spec.origMatchCase, ast.tpd.EmptyTree)._1.asInstanceOf[HKTypeLambda] + + def tryDisjoint: MatchResult = + val defn.MatchCase(origPattern, _) = constrainedCaseLambda.resultType: @unchecked + if provablyDisjoint(scrut, origPattern) then + MatchResult.Disjoint + else + MatchResult.Stuck + + if rec(spec.pattern, scrut, variance = 1, scrutIsWidenedAbstract = false) then + if instances.exists(_.isInstanceOf[TypeBounds]) then + MatchResult.NoInstance { + constrainedCaseLambda.paramNames.zip(instances).collect { + case (name, bounds: TypeBounds) => (name, bounds) + } + } + else + val defn.MatchCase(instantiatedPat, reduced) = + instantiateParamsSpec(instances, constrainedCaseLambda)(constrainedCaseLambda.resultType): @unchecked + if scrut <:< instantiatedPat then + MatchResult.Reduced(reduced) + else + tryDisjoint + else + tryDisjoint + end matchSpeccedPatMat + def matchLegacyPatMat(spec: MatchTypeCaseSpec.LegacyPatMat): MatchResult = val caseLambda = constrained(spec.origMatchCase, ast.tpd.EmptyTree)._1.asInstanceOf[HKTypeLambda] this.caseLambda = caseLambda diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index c17d33fc6bef..72d83afbff87 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -7,7 +7,7 @@ import Flags.* import Names.* import StdNames.*, NameOps.* import NullOpsDecorator.* -import NameKinds.SkolemName +import NameKinds.{SkolemName, WildcardParamName} import Scopes.* import Constants.* import Contexts.* @@ -5088,8 +5088,23 @@ object Types extends TypeUtils { case _ => None } + enum MatchTypeCasePattern: + case Capture(num: Int, isWildcard: Boolean) + case TypeTest(tpe: Type) + case BaseTypeTest(classType: TypeRef, argPatterns: List[MatchTypeCasePattern], needsConcreteScrut: Boolean) + + def isTypeTest: Boolean = + this.isInstanceOf[TypeTest] + + def needsConcreteScrutInVariantPos: Boolean = this match + case Capture(_, isWildcard) => !isWildcard + case TypeTest(_) => false + case _ => true + end MatchTypeCasePattern + enum MatchTypeCaseSpec: case SubTypeTest(origMatchCase: Type, pattern: Type, body: Type) + case SpeccedPatMat(origMatchCase: HKTypeLambda, captureCount: Int, pattern: MatchTypeCasePattern, body: Type) case LegacyPatMat(origMatchCase: HKTypeLambda) def origMatchCase: Type @@ -5099,11 +5114,59 @@ object Types extends TypeUtils { def analyze(cas: Type)(using Context): MatchTypeCaseSpec = cas match case cas: HKTypeLambda => - LegacyPatMat(cas) + val defn.MatchCase(pat, body) = cas.resultType: @unchecked + val specPattern = tryConvertToSpecPattern(cas, pat) + if specPattern != null then + SpeccedPatMat(cas, cas.paramNames.size, specPattern, body) + else + LegacyPatMat(cas) case _ => val defn.MatchCase(pat, body) = cas: @unchecked SubTypeTest(cas, pat, body) end analyze + + private def tryConvertToSpecPattern(caseLambda: HKTypeLambda, pat: Type)(using Context): MatchTypeCasePattern | Null = + var typeParamRefsAccountedFor: Int = 0 + + def rec(pat: Type, variance: Int): MatchTypeCasePattern | Null = + pat match + case pat @ TypeParamRef(binder, num) if binder eq caseLambda => + typeParamRefsAccountedFor += 1 + MatchTypeCasePattern.Capture(num, isWildcard = pat.paramName.is(WildcardParamName)) + + case pat @ AppliedType(tycon: TypeRef, args) if variance == 1 => + val tyconSym = tycon.symbol + if tyconSym.isClass then + val cls = tyconSym.asClass + if cls.name.startsWith("Tuple") && defn.isTupleNType(pat) then + rec(pat.toNestedPairs, variance) + else + val tparams = tycon.typeParams + val argPatterns = args.zip(tparams).map { (arg, tparam) => + rec(arg, tparam.paramVarianceSign) + } + if argPatterns.exists(_ == null) then + null + else + val argPatterns1 = argPatterns.asInstanceOf[List[MatchTypeCasePattern]] // they are not null + if argPatterns1.forall(_.isTypeTest) then + MatchTypeCasePattern.TypeTest(pat) + else + val needsConcreteScrut = argPatterns1.zip(tparams).exists { + (argPattern, tparam) => tparam.paramVarianceSign != 0 && argPattern.needsConcreteScrutInVariantPos + } + MatchTypeCasePattern.BaseTypeTest(tycon, argPatterns1, needsConcreteScrut) + else + null + + case _ => + MatchTypeCasePattern.TypeTest(pat) + end rec + + val result = rec(pat, variance = 1) + if typeParamRefsAccountedFor == caseLambda.paramNames.size then result + else null + end tryConvertToSpecPattern end MatchTypeCaseSpec // ------ ClassInfo, Type Bounds -------------------------------------------------- diff --git a/tests/neg/6570-1.check b/tests/neg/6570-1.check index bdbadd0f752a..0abf96e2d350 100644 --- a/tests/neg/6570-1.check +++ b/tests/neg/6570-1.check @@ -27,6 +27,6 @@ | does not uniquely determine parameter x in | case Cov[x] => N[x] | The computed bounds for the parameter are: - | x >: Box[Int] + | x <: Box[Int] | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i11982a.check b/tests/neg/i11982a.check index 1977aa30e8b5..5433688447f7 100644 --- a/tests/neg/i11982a.check +++ b/tests/neg/i11982a.check @@ -10,7 +10,7 @@ | does not uniquely determine parameter xs in | case _ *: xs => xs | The computed bounds for the parameter are: - | xs >: Any *: EmptyTuple.type <: Tuple + | xs <: Any *: EmptyTuple.type | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:10:38 ----------------------------------------------------------- @@ -25,7 +25,7 @@ | does not uniquely determine parameter xs in | case _ *: xs => xs | The computed bounds for the parameter are: - | xs >: Any *: EmptyTuple.type <: Tuple + | xs <: Any *: EmptyTuple.type | | longer explanation available when compiling with `-explain` -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:12:25 ----------------------------------------------------------- @@ -40,6 +40,6 @@ | does not uniquely determine parameter xs in | case _ *: xs => xs | The computed bounds for the parameter are: - | xs >: Any *: EmptyTuple.type <: Tuple + | xs <: Any *: EmptyTuple.type | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i12049.check b/tests/neg/i12049.check index e2ed9e584fa3..b44eb612f627 100644 --- a/tests/neg/i12049.check +++ b/tests/neg/i12049.check @@ -18,7 +18,7 @@ -- [E184] Type Error: tests/neg/i12049.scala:14:23 --------------------------------------------------------------------- 14 |val y3: String = ??? : Last[Int *: Int *: Boolean *: String *: EmptyTuple] // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Match type reduction failed since selector EmptyTuple.type + | Match type reduction failed since selector EmptyTuple | matches none of the cases | | case _ *: _ *: t => Last[t] @@ -48,7 +48,7 @@ -- [E184] Type Error: tests/neg/i12049.scala:25:26 --------------------------------------------------------------------- 25 |val _ = summon[String =:= Last[Int *: Int *: Boolean *: String *: EmptyTuple]] // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Match type reduction failed since selector EmptyTuple.type + | Match type reduction failed since selector EmptyTuple | matches none of the cases | | case _ *: _ *: t => Last[t] diff --git a/tests/neg/i13780.check b/tests/neg/i13780.check index 63ba7dec6142..69537d8a3f3b 100644 --- a/tests/neg/i13780.check +++ b/tests/neg/i13780.check @@ -14,8 +14,8 @@ | does not uniquely determine parameters a, b in | case (a, b) => a | The computed bounds for the parameters are: - | a >: Any - | b >: Any + | a + | b | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------ @@ -34,8 +34,8 @@ | does not uniquely determine parameters a, b in | case (a, b) => a | The computed bounds for the parameters are: - | a >: Int - | b >: Int + | a <: Int + | b <: Int | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------ @@ -54,7 +54,7 @@ | does not uniquely determine parameters a, b in | case (a, b) => a | The computed bounds for the parameters are: - | a >: String - | b >: String + | a <: String + | b <: String | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/wildcard-match.check b/tests/neg/wildcard-match.check new file mode 100644 index 000000000000..d405326c3d2b --- /dev/null +++ b/tests/neg/wildcard-match.check @@ -0,0 +1,94 @@ +-- [E007] Type Mismatch Error: tests/neg/wildcard-match.scala:31:13 ---------------------------------------------------- +31 | val _: C = a1 // error + | ^^ + | Found: CovElem[Y] + | Required: C + | + | where: Y is a type in method f with bounds <: Cov[C] + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce CovElem[Y] + | failed since selector Y + | does not uniquely determine parameter a in + | case Cov[a] => a + | The computed bounds for the parameter are: + | a <: C + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/wildcard-match.scala:34:13 ---------------------------------------------------- +34 | val _: C = a2 // error + | ^^ + | Found: ContravElem[Z] + | Required: C + | + | where: Z is a type in method f with bounds <: Contrav[C] + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce ContravElem[Z] + | failed since selector Z + | does not uniquely determine parameter a in + | case Contrav[a] => a + | The computed bounds for the parameter are: + | a >: C + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/wildcard-match.scala:40:19 ---------------------------------------------------- +40 | val _: List[C] = b1 // error + | ^^ + | Found: CovToList[Y] + | Required: List[C] + | + | where: Y is a type in method f with bounds <: Cov[C] + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce CovToList[Y] + | failed since selector Y + | does not uniquely determine parameter a in + | case Cov[a] => List[a] + | The computed bounds for the parameter are: + | a <: C + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/wildcard-match.scala:43:19 ---------------------------------------------------- +43 | val _: List[C] = b2 // error + | ^^ + | Found: ContravElem[Z] + | Required: List[C] + | + | where: Z is a type in method f with bounds <: Contrav[C] + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce ContravElem[Z] + | failed since selector Z + | does not uniquely determine parameter a in + | case Contrav[a] => a + | The computed bounds for the parameter are: + | a >: C + | + | longer explanation available when compiling with `-explain` +-- [E172] Type Error: tests/neg/wildcard-match.scala:61:33 ------------------------------------------------------------- +61 | summon[tuples.length[T2] =:= 3] // error + | ^ + | Cannot prove that shapeless.tuples.length[T2] =:= (3 : Int). + | + | where: T2 is a type in method testShapeless with bounds <: (Int, Int, Int) + | + | + | Note: a match type could not be fully reduced: + | + | trying to reduce shapeless.tuples.length[T2] + | trying to reduce Tuple.Size[shapeless.tuples.to[T2]] + | failed since selector shapeless.tuples.to[T2] + | does not uniquely determine parameters x, xs in + | case x *: xs => scala.compiletime.ops.int.S[Tuple.Size[xs]] + | The computed bounds for the parameters are: + | x <: Int + | xs <: (Int, Int) diff --git a/tests/neg/wildcard-match.scala b/tests/neg/wildcard-match.scala index 326a97485bd2..c220428f4f85 100644 --- a/tests/neg/wildcard-match.scala +++ b/tests/neg/wildcard-match.scala @@ -42,5 +42,20 @@ def f[X <: Box[C], Y <: Cov[C], Z <: Contrav[C]] = def b2: ContravElem[Z] = ??? val _: List[C] = b2 // error +// found in shapeless +object shapeless: + trait Monoidal: + type to[_] <: Tuple + type length[m] = Tuple.Size[to[m]] + object tuples extends Monoidal: + type to[t] = t & Tuple +end shapeless + +def testShapeless[T2 <: (Int, Int, Int)](): Unit = + import shapeless.* + + type T1 = (Int, Int, Int) + summon[tuples.length[T1] =:= 3] // OK + summon[tuples.length[T2] =:= 3] // error From cc41d4890a0e0e2e1766869770a31ca5d2aaa0a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 4 Aug 2023 14:05:51 +0200 Subject: [PATCH 03/17] Use new specced match types for `scala.compiletime.int.S[n]`. --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 7 +++++++ compiler/src/dotty/tools/dotc/core/Types.scala | 9 +++++++++ 2 files changed, 16 insertions(+) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 4cd97cb6ef75..b2c70914d034 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3356,6 +3356,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { case _ => false + + case MatchTypeCasePattern.CompileTimeS(argPattern) => + natValue(scrut) match + case Some(scrutValue) if scrutValue > 0 => + rec(argPattern, ConstantType(Constant(scrutValue - 1)), variance, scrutIsWidenedAbstract) + case _ => + false end rec // This might not be needed diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 72d83afbff87..047e370ff3e8 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -5092,6 +5092,7 @@ object Types extends TypeUtils { case Capture(num: Int, isWildcard: Boolean) case TypeTest(tpe: Type) case BaseTypeTest(classType: TypeRef, argPatterns: List[MatchTypeCasePattern], needsConcreteScrut: Boolean) + case CompileTimeS(argPattern: MatchTypeCasePattern) def isTypeTest: Boolean = this.isInstanceOf[TypeTest] @@ -5156,6 +5157,14 @@ object Types extends TypeUtils { (argPattern, tparam) => tparam.paramVarianceSign != 0 && argPattern.needsConcreteScrutInVariantPos } MatchTypeCasePattern.BaseTypeTest(tycon, argPatterns1, needsConcreteScrut) + else if defn.isCompiletime_S(tyconSym) && args.sizeIs == 1 then + val argPattern = rec(args.head, variance) + if argPattern == null then + null + else if argPattern.isTypeTest then + MatchTypeCasePattern.TypeTest(pat) + else + MatchTypeCasePattern.CompileTimeS(argPattern) else null From 067b828e864b736e68c87e3ccc1ad86b0c118b51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 24 Nov 2023 14:46:12 +0100 Subject: [PATCH 04/17] Short-circuit match type cases with missing captures in their patterns. So that they do not fall into the legacy fallback. --- .../dotty/tools/dotc/core/TypeComparer.scala | 10 +++-- .../src/dotty/tools/dotc/core/Types.scala | 37 +++++++++++++++++-- 2 files changed, 40 insertions(+), 7 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index b2c70914d034..1abcf5e2c6ea 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3250,9 +3250,10 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { /** Match a single case. */ def matchCase(cas: MatchTypeCaseSpec): MatchResult = trace(i"$scrut match ${MatchTypeTrace.caseText(cas)}", matchTypes, show = true) { cas match - case cas: MatchTypeCaseSpec.SubTypeTest => matchSubTypeTest(cas) - case cas: MatchTypeCaseSpec.SpeccedPatMat => matchSpeccedPatMat(cas) - case cas: MatchTypeCaseSpec.LegacyPatMat => matchLegacyPatMat(cas) + case cas: MatchTypeCaseSpec.SubTypeTest => matchSubTypeTest(cas) + case cas: MatchTypeCaseSpec.SpeccedPatMat => matchSpeccedPatMat(cas) + case cas: MatchTypeCaseSpec.LegacyPatMat => matchLegacyPatMat(cas) + case cas: MatchTypeCaseSpec.MissingCaptures => matchMissingCaptures(cas) } def matchSubTypeTest(spec: MatchTypeCaseSpec.SubTypeTest): MatchResult = @@ -3434,6 +3435,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { MatchResult.Stuck end matchLegacyPatMat + def matchMissingCaptures(spec: MatchTypeCaseSpec.MissingCaptures): MatchResult = + MatchResult.Stuck + def recur(remaining: List[MatchTypeCaseSpec]): Type = remaining match case cas :: remaining1 => matchCase(cas) match diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 047e370ff3e8..b6afd5f445d8 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -5107,6 +5107,7 @@ object Types extends TypeUtils { case SubTypeTest(origMatchCase: Type, pattern: Type, body: Type) case SpeccedPatMat(origMatchCase: HKTypeLambda, captureCount: Int, pattern: MatchTypeCasePattern, body: Type) case LegacyPatMat(origMatchCase: HKTypeLambda) + case MissingCaptures(origMatchCase: HKTypeLambda, missing: collection.BitSet) def origMatchCase: Type end MatchTypeCaseSpec @@ -5116,16 +5117,44 @@ object Types extends TypeUtils { cas match case cas: HKTypeLambda => val defn.MatchCase(pat, body) = cas.resultType: @unchecked - val specPattern = tryConvertToSpecPattern(cas, pat) - if specPattern != null then - SpeccedPatMat(cas, cas.paramNames.size, specPattern, body) + val missing = checkCapturesPresent(cas, pat) + if !missing.isEmpty then + MissingCaptures(cas, missing) else - LegacyPatMat(cas) + val specPattern = tryConvertToSpecPattern(cas, pat) + if specPattern != null then + SpeccedPatMat(cas, cas.paramNames.size, specPattern, body) + else + LegacyPatMat(cas) case _ => val defn.MatchCase(pat, body) = cas: @unchecked SubTypeTest(cas, pat, body) end analyze + /** Checks that all the captures of the case are present in the case. + * + * Sometimes, because of earlier substitutions of an abstract type constructor, + * we can end up with patterns that do not mention all their captures anymore. + * This can happen even when the body still refers to these missing captures. + * In that case, we must always consider the case to be unmatchable, i.e., to + * become `Stuck`. + * + * See pos/i12127.scala for an example. + */ + def checkCapturesPresent(cas: HKTypeLambda, pat: Type)(using Context): collection.BitSet = + val captureCount = cas.paramNames.size + val missing = new mutable.BitSet(captureCount) + missing ++= (0 until captureCount) + new CheckCapturesPresent(cas).apply(missing, pat) + + private class CheckCapturesPresent(cas: HKTypeLambda)(using Context) extends TypeAccumulator[mutable.BitSet]: + def apply(missing: mutable.BitSet, tp: Type): mutable.BitSet = tp match + case TypeParamRef(binder, num) if binder eq cas => + missing -= num + case _ => + foldOver(missing, tp) + end CheckCapturesPresent + private def tryConvertToSpecPattern(caseLambda: HKTypeLambda, pat: Type)(using Context): MatchTypeCasePattern | Null = var typeParamRefsAccountedFor: Int = 0 From aa8d348232d25ed0e473ae86999d68b46012766d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 4 Aug 2023 17:30:33 +0200 Subject: [PATCH 05/17] Use the specced match types for abstract tycons in patterns. An abstract tycon can be matched if it is exactly equal to the scrutinee's tycon. --- .../dotty/tools/dotc/core/TypeComparer.scala | 23 ++++---- .../src/dotty/tools/dotc/core/Types.scala | 52 +++++++++++++------ 2 files changed, 49 insertions(+), 26 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 1abcf5e2c6ea..e943989b7eb0 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3345,16 +3345,14 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { val innerScrutIsWidenedAbstract = scrutIsWidenedAbstract || (needsConcreteScrut && !isConcrete(scrut)) // no point in checking concreteness if it does not need to be concrete + matchArgs(argPatterns, baseArgs, classType.typeParams, innerScrutIsWidenedAbstract) + case _ => + false - def matchArgs(argPatterns: List[MatchTypeCasePattern], baseArgs: List[Type], tparams: List[TypeParamInfo]): Boolean = - if argPatterns.isEmpty then - true - else - rec(argPatterns.head, baseArgs.head, tparams.head.paramVarianceSign, innerScrutIsWidenedAbstract) - && matchArgs(argPatterns.tail, baseArgs.tail, tparams.tail) - - matchArgs(argPatterns, baseArgs, classType.typeParams) - + case MatchTypeCasePattern.AbstractTypeConstructor(tycon, argPatterns) => + scrut.dealias match + case scrutDealias @ AppliedType(scrutTycon, args) if scrutTycon =:= tycon => + matchArgs(argPatterns, args, tycon.typeParams, scrutIsWidenedAbstract) case _ => false @@ -3366,6 +3364,13 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { false end rec + def matchArgs(argPatterns: List[MatchTypeCasePattern], args: List[Type], tparams: List[TypeParamInfo], scrutIsWidenedAbstract: Boolean): Boolean = + if argPatterns.isEmpty then + true + else + rec(argPatterns.head, args.head, tparams.head.paramVarianceSign, scrutIsWidenedAbstract) + && matchArgs(argPatterns.tail, args.tail, tparams.tail, scrutIsWidenedAbstract) + // This might not be needed val constrainedCaseLambda = constrained(spec.origMatchCase, ast.tpd.EmptyTree)._1.asInstanceOf[HKTypeLambda] diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index b6afd5f445d8..b11a6720d358 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -5093,6 +5093,7 @@ object Types extends TypeUtils { case TypeTest(tpe: Type) case BaseTypeTest(classType: TypeRef, argPatterns: List[MatchTypeCasePattern], needsConcreteScrut: Boolean) case CompileTimeS(argPattern: MatchTypeCasePattern) + case AbstractTypeConstructor(tycon: Type, argPatterns: List[MatchTypeCasePattern]) def isTypeTest: Boolean = this.isInstanceOf[TypeTest] @@ -5167,25 +5168,15 @@ object Types extends TypeUtils { case pat @ AppliedType(tycon: TypeRef, args) if variance == 1 => val tyconSym = tycon.symbol if tyconSym.isClass then - val cls = tyconSym.asClass - if cls.name.startsWith("Tuple") && defn.isTupleNType(pat) then + if tyconSym.name.startsWith("Tuple") && defn.isTupleNType(pat) then rec(pat.toNestedPairs, variance) else - val tparams = tycon.typeParams - val argPatterns = args.zip(tparams).map { (arg, tparam) => - rec(arg, tparam.paramVarianceSign) + recArgPatterns(pat) { argPatterns => + val needsConcreteScrut = argPatterns.zip(tycon.typeParams).exists { + (argPattern, tparam) => tparam.paramVarianceSign != 0 && argPattern.needsConcreteScrutInVariantPos + } + MatchTypeCasePattern.BaseTypeTest(tycon, argPatterns, needsConcreteScrut) } - if argPatterns.exists(_ == null) then - null - else - val argPatterns1 = argPatterns.asInstanceOf[List[MatchTypeCasePattern]] // they are not null - if argPatterns1.forall(_.isTypeTest) then - MatchTypeCasePattern.TypeTest(pat) - else - val needsConcreteScrut = argPatterns1.zip(tparams).exists { - (argPattern, tparam) => tparam.paramVarianceSign != 0 && argPattern.needsConcreteScrutInVariantPos - } - MatchTypeCasePattern.BaseTypeTest(tycon, argPatterns1, needsConcreteScrut) else if defn.isCompiletime_S(tyconSym) && args.sizeIs == 1 then val argPattern = rec(args.head, variance) if argPattern == null then @@ -5195,12 +5186,39 @@ object Types extends TypeUtils { else MatchTypeCasePattern.CompileTimeS(argPattern) else - null + tycon.info match + case _: RealTypeBounds => recAbstractTypeConstructor(pat) + case _ => null + + case pat @ AppliedType(tycon: TypeParamRef, _) if variance == 1 => + recAbstractTypeConstructor(pat) case _ => MatchTypeCasePattern.TypeTest(pat) end rec + def recAbstractTypeConstructor(pat: AppliedType): MatchTypeCasePattern | Null = + recArgPatterns(pat) { argPatterns => + MatchTypeCasePattern.AbstractTypeConstructor(pat.tycon, argPatterns) + } + end recAbstractTypeConstructor + + def recArgPatterns(pat: AppliedType)(whenNotTypeTest: List[MatchTypeCasePattern] => MatchTypeCasePattern | Null): MatchTypeCasePattern | Null = + val AppliedType(tycon, args) = pat + val tparams = tycon.typeParams + val argPatterns = args.zip(tparams).map { (arg, tparam) => + rec(arg, tparam.paramVarianceSign) + } + if argPatterns.exists(_ == null) then + null + else + val argPatterns1 = argPatterns.asInstanceOf[List[MatchTypeCasePattern]] // they are not null + if argPatterns1.forall(_.isTypeTest) then + MatchTypeCasePattern.TypeTest(pat) + else + whenNotTypeTest(argPatterns1) + end recArgPatterns + val result = rec(pat, variance = 1) if typeParamRefsAccountedFor == caseLambda.paramNames.size then result else null From 97725d76473dd4d3bb4362cdc6e7c43ead39631a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Tue, 8 Aug 2023 15:49:13 +0200 Subject: [PATCH 06/17] Handle type member extractors as specced match types. --- .../dotty/tools/dotc/core/TypeComparer.scala | 23 +++++++++++ .../src/dotty/tools/dotc/core/Types.scala | 38 ++++++++++++++++++- tests/pos/i17395-spec.scala | 29 ++++++++++++++ 3 files changed, 88 insertions(+), 2 deletions(-) create mode 100644 tests/pos/i17395-spec.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index e943989b7eb0..7e83fd1b22da 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3362,6 +3362,29 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { rec(argPattern, ConstantType(Constant(scrutValue - 1)), variance, scrutIsWidenedAbstract) case _ => false + + case MatchTypeCasePattern.TypeMemberExtractor(typeMemberName, capture) => + val stableScrut: SingletonType = scrut match + case scrut: SingletonType => scrut + case _ => SkolemType(scrut) + stableScrut.member(typeMemberName) match + case denot: SingleDenotation if denot.exists => + val info = denot.info match + case TypeAlias(alias) => alias + case info => info // Notably, RealTypeBounds, which will eventually give a MatchResult.NoInstances + if info.isInstanceOf[ClassInfo] then + /* The member is not an alias (we'll get Stuck instead of NoInstances, + * which is not ideal, but we cannot make a RealTypeBounds of ClassInfo). + */ + false + else + val infoRefersToSkolem = stableScrut.isInstanceOf[SkolemType] && stableScrut.occursIn(info) + val info1 = + if infoRefersToSkolem && !info.isInstanceOf[TypeBounds] then RealTypeBounds(info, info) // to trigger a MatchResult.NoInstances + else info + rec(capture, info1, variance = 0, scrutIsWidenedAbstract) + case _ => + false end rec def matchArgs(argPatterns: List[MatchTypeCasePattern], args: List[Type], tparams: List[TypeParamInfo], scrutIsWidenedAbstract: Boolean): Boolean = diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index b11a6720d358..8522fa6a0e06 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -5094,6 +5094,7 @@ object Types extends TypeUtils { case BaseTypeTest(classType: TypeRef, argPatterns: List[MatchTypeCasePattern], needsConcreteScrut: Boolean) case CompileTimeS(argPattern: MatchTypeCasePattern) case AbstractTypeConstructor(tycon: Type, argPatterns: List[MatchTypeCasePattern]) + case TypeMemberExtractor(typeMemberName: TypeName, capture: Capture) def isTypeTest: Boolean = this.isInstanceOf[TypeTest] @@ -5187,12 +5188,45 @@ object Types extends TypeUtils { MatchTypeCasePattern.CompileTimeS(argPattern) else tycon.info match - case _: RealTypeBounds => recAbstractTypeConstructor(pat) - case _ => null + case _: RealTypeBounds => + recAbstractTypeConstructor(pat) + case TypeAlias(tl @ HKTypeLambda(onlyParam :: Nil, resType: RefinedType)) => + /* Unlike for eta-expanded classes, the typer does not automatically + * dealias poly type aliases to refined types. So we have to give them + * a chance here. + * We are quite specific about the shape of type aliases that we are willing + * to dealias this way, because we must not dealias arbitrary type constructors + * that could refine the bounds of the captures; those would amount of + * type-test + capture combos, which are out of the specced match types. + */ + rec(pat.superType, variance) + case _ => + null case pat @ AppliedType(tycon: TypeParamRef, _) if variance == 1 => recAbstractTypeConstructor(pat) + case pat @ RefinedType(parent, refinedName: TypeName, TypeAlias(alias @ TypeParamRef(binder, num))) + if variance == 1 && (binder eq caseLambda) => + parent.member(refinedName) match + case refinedMember: SingleDenotation if refinedMember.exists => + // Check that the bounds of the capture contain the bounds of the inherited member + val refinedMemberBounds = refinedMember.info + val captureBounds = caseLambda.paramInfos(num) + if captureBounds.contains(refinedMemberBounds) then + /* In this case, we know that any member we eventually find during reduction + * will have bounds that fit in the bounds of the capture. Therefore, no + * type-test + capture combo is necessary, and we can apply the specced match types. + */ + val capture = rec(alias, variance = 0).asInstanceOf[MatchTypeCasePattern.Capture] + MatchTypeCasePattern.TypeMemberExtractor(refinedName, capture) + else + // Otherwise, a type-test + capture combo might be necessary, and we are out of spec + null + case _ => + // If the member does not refine a member of the `parent`, we are out of spec + null + case _ => MatchTypeCasePattern.TypeTest(pat) end rec diff --git a/tests/pos/i17395-spec.scala b/tests/pos/i17395-spec.scala new file mode 100644 index 000000000000..0adeda703b99 --- /dev/null +++ b/tests/pos/i17395-spec.scala @@ -0,0 +1,29 @@ +trait TC[T] + +object TC { + def optionTCForPart[T](implicit tc: TC[ExtractPart[T]]): TC[Option[ExtractPart[T]]] = new TC[Option[ExtractPart[T]]] {} +} + +trait ThingWithPart { + type Part +} + +type ExtractPart[T] = T match { + case PartField[t] => t +} +type PartField[T] = ThingWithPart { type Part = T } + +class ValuePartHolder extends ThingWithPart { + type Part = Value +} + +class Value +object Value { + implicit val tcValue: TC[Value] = new {} +} + +@main def main(): Unit = { +// import Value.tcValue // explicit import works around the issue, but shouldn't be necessary + val tc = TC.optionTCForPart[ValuePartHolder] + println(tc) +} From 7ab7b0fc856f9297e88f4d73fcb44a44da6531b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 24 Nov 2023 15:15:29 +0100 Subject: [PATCH 07/17] Report a compile error on illegal match types. The error can be silenced with `-source:3.3`. In that case, illegal match types are reduced using the legacy matching algorithm, as before. --- .../tools/dotc/core/MatchTypeTrace.scala | 5 +++ .../dotty/tools/dotc/core/TypeComparer.scala | 6 ++- .../tools/dotc/reporting/ErrorMessageID.scala | 1 + .../dotty/tools/dotc/reporting/messages.scala | 4 ++ tests/neg/6570.scala | 2 + tests/neg/illegal-match-types.check | 42 +++++++++++++++++++ tests/neg/illegal-match-types.scala | 41 ++++++++++++++++++ tests/pos/10747-shapeless-min-spec.scala | 13 ++++++ tests/pos/10747-shapeless-min.scala | 2 + tests/pos/8647.scala | 2 + tests/pos/9757.scala | 2 + tests/pos/i10242.scala | 4 +- tests/pos/i15155.scala | 4 +- tests/pos/i16408.min1.scala | 2 + tests/pos/i16408.scala | 2 + tests/pos/i16706.scala | 4 +- tests/pos/i17395.scala | 2 + tests/pos/i5625b.scala | 4 +- .../tasty-simplified/quoted_2.scala | 2 + 19 files changed, 139 insertions(+), 5 deletions(-) create mode 100644 tests/neg/illegal-match-types.check create mode 100644 tests/neg/illegal-match-types.scala create mode 100644 tests/pos/10747-shapeless-min-spec.scala diff --git a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala index 7bdcba19c99b..fb278ab92dc9 100644 --- a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala +++ b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala @@ -125,4 +125,9 @@ object MatchTypeTrace: | | ${casesText(cases)}""" + def illegalPatternText(scrut: Type, cas: MatchTypeCaseSpec.LegacyPatMat)(using Context): String = + i"""The match type contains an illegal case: + | ${caseText(cas)} + |(this error can be ignored for now with `-source:3.3`)""" + end MatchTypeTrace diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 7e83fd1b22da..6f1e334ccc95 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -10,8 +10,9 @@ import TypeOps.refineUsingParent import collection.mutable import util.{Stats, NoSourcePosition, EqHashMap} import config.Config -import config.Feature.migrateTo3 +import config.Feature.{migrateTo3, sourceVersion} import config.Printers.{subtyping, gadts, matchTypes, noPrinter} +import config.SourceVersion import TypeErasure.{erasedLub, erasedGlb} import TypeApplications.* import Variances.{Variance, variancesConform} @@ -3467,6 +3468,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { MatchResult.Stuck def recur(remaining: List[MatchTypeCaseSpec]): Type = remaining match + case (cas: MatchTypeCaseSpec.LegacyPatMat) :: _ if sourceVersion.isAtLeast(SourceVersion.`3.4`) => + val errorText = MatchTypeTrace.illegalPatternText(scrut, cas) + ErrorType(reporting.MatchTypeLegacyPattern(errorText)) case cas :: remaining1 => matchCase(cas) match case MatchResult.Disjoint => diff --git a/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala b/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala index 8e583509cd98..89fd071137cf 100644 --- a/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala +++ b/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala @@ -204,6 +204,7 @@ enum ErrorMessageID(val isActive: Boolean = true) extends java.lang.Enum[ErrorMe case VarArgsParamCannotBeGivenID // errorNumber: 188 case ExtractorNotFoundID // errorNumber: 189 case PureUnitExpressionID // errorNumber: 190 + case MatchTypeLegacyPatternID // errorNumber: 191 def errorNumber = ordinal - 1 diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala index b6622d67f36a..033376a9ab09 100644 --- a/compiler/src/dotty/tools/dotc/reporting/messages.scala +++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala @@ -3073,6 +3073,10 @@ class MatchTypeScrutineeCannotBeHigherKinded(tp: Type)(using Context) def msg(using Context) = i"the scrutinee of a match type cannot be higher-kinded" def explain(using Context) = "" +class MatchTypeLegacyPattern(errorText: String)(using Context) extends TypeMsg(MatchTypeLegacyPatternID): + def msg(using Context) = errorText + def explain(using Context) = "" + class ClosureCannotHaveInternalParameterDependencies(mt: Type)(using Context) extends TypeMsg(ClosureCannotHaveInternalParameterDependenciesID): def msg(using Context) = diff --git a/tests/neg/6570.scala b/tests/neg/6570.scala index f36471868d9b..cd6016a164c8 100644 --- a/tests/neg/6570.scala +++ b/tests/neg/6570.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + object Base { trait Trait1 trait Trait2 diff --git a/tests/neg/illegal-match-types.check b/tests/neg/illegal-match-types.check new file mode 100644 index 000000000000..f5f0f2d07c51 --- /dev/null +++ b/tests/neg/illegal-match-types.check @@ -0,0 +1,42 @@ +-- [E191] Type Error: tests/neg/illegal-match-types.scala:7:23 --------------------------------------------------------- +7 |type InvNesting[X] = X match // error + | ^ + | The match type contains an illegal case: + | case Inv[Cov[t]] => t + | (this error can be ignored for now with `-source:3.3`) +8 | case Inv[Cov[t]] => t +-- [E191] Type Error: tests/neg/illegal-match-types.scala:10:26 -------------------------------------------------------- +10 |type ContraNesting[X] = X match // error + | ^ + | The match type contains an illegal case: + | case Contra[Cov[t]] => t + | (this error can be ignored for now with `-source:3.3`) +11 | case Contra[Cov[t]] => t +-- [E191] Type Error: tests/neg/illegal-match-types.scala:15:22 -------------------------------------------------------- +15 |type AndTypeMT[X] = X match // error + | ^ + | The match type contains an illegal case: + | case t & Seq[Any] => t + | (this error can be ignored for now with `-source:3.3`) +16 | case t & Seq[Any] => t +-- [E191] Type Error: tests/neg/illegal-match-types.scala:22:33 -------------------------------------------------------- +22 |type TypeAliasWithBoundMT[X] = X match // error + | ^ + | The match type contains an illegal case: + | case IsSeq[t] => t + | (this error can be ignored for now with `-source:3.3`) +23 | case IsSeq[t] => t +-- [E191] Type Error: tests/neg/illegal-match-types.scala:29:34 -------------------------------------------------------- +29 |type TypeMemberExtractorMT[X] = X match // error + | ^ + | The match type contains an illegal case: + | case TypeMemberAux[t] => t + | (this error can be ignored for now with `-source:3.3`) +30 | case TypeMemberAux[t] => t +-- [E191] Type Error: tests/neg/illegal-match-types.scala:40:35 -------------------------------------------------------- +40 |type TypeMemberExtractorMT2[X] = X match // error + | ^ + | The match type contains an illegal case: + | case TypeMemberAux2[t] => t + | (this error can be ignored for now with `-source:3.3`) +41 | case TypeMemberAux2[t] => t diff --git a/tests/neg/illegal-match-types.scala b/tests/neg/illegal-match-types.scala new file mode 100644 index 000000000000..51b0aab6301a --- /dev/null +++ b/tests/neg/illegal-match-types.scala @@ -0,0 +1,41 @@ +class Inv[T] +class Cov[+T] +class Contra[-T] + +// Nesting captures in non-covariant position + +type InvNesting[X] = X match // error + case Inv[Cov[t]] => t + +type ContraNesting[X] = X match // error + case Contra[Cov[t]] => t + +// Intersection type to type-test and capture at the same time + +type AndTypeMT[X] = X match // error + case t & Seq[Any] => t + +// Poly type alias with a bound to type-test and capture at the same time + +type IsSeq[X <: Seq[Any]] = X + +type TypeAliasWithBoundMT[X] = X match // error + case IsSeq[t] => t + +// Poly type alias with an unknown type member refinement + +type TypeMemberAux[X] = { type TypeMember = X } + +type TypeMemberExtractorMT[X] = X match // error + case TypeMemberAux[t] => t + +// Poly type alias with a refined member of stronger bounds than in the parent + +class Base { + type TypeMember +} + +type TypeMemberAux2[X <: Seq[Any]] = Base { type TypeMember = X } + +type TypeMemberExtractorMT2[X] = X match // error + case TypeMemberAux2[t] => t diff --git a/tests/pos/10747-shapeless-min-spec.scala b/tests/pos/10747-shapeless-min-spec.scala new file mode 100644 index 000000000000..a0dce79a7830 --- /dev/null +++ b/tests/pos/10747-shapeless-min-spec.scala @@ -0,0 +1,13 @@ +trait Monoidal { + type to[_] <: Tuple +} + +object eithers extends Monoidal { + class Wrap[T] + + type to[t] <: Tuple = Wrap[t] match { + case Wrap[Nothing] => EmptyTuple + case Wrap[other] => other match + case Either[hd, tl] => hd *: to[tl] + } +} diff --git a/tests/pos/10747-shapeless-min.scala b/tests/pos/10747-shapeless-min.scala index fbb8012fc9f2..3599dd2db469 100644 --- a/tests/pos/10747-shapeless-min.scala +++ b/tests/pos/10747-shapeless-min.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + trait Monoidal { type to[_] <: Tuple } diff --git a/tests/pos/8647.scala b/tests/pos/8647.scala index 5e8f839b27ca..f597caef4484 100644 --- a/tests/pos/8647.scala +++ b/tests/pos/8647.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + final class Two[A, B]() final class Blaaa diff --git a/tests/pos/9757.scala b/tests/pos/9757.scala index aeecfa0a472f..8f4af92c20ef 100644 --- a/tests/pos/9757.scala +++ b/tests/pos/9757.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + type RemoveFrom[R, A] = R match { case A & newType => newType } diff --git a/tests/pos/i10242.scala b/tests/pos/i10242.scala index 707c4c9f0a0c..10883633971e 100644 --- a/tests/pos/i10242.scala +++ b/tests/pos/i10242.scala @@ -1,4 +1,6 @@ -// https://github.com/lampepfl/dotty/issues/10242 +//> using options -source:3.3 + +// https://github.com/lampepfl/dotty/issues/10242 type Foo[A, B <: A] = A type Bar[A] = A match { diff --git a/tests/pos/i15155.scala b/tests/pos/i15155.scala index a00ca742b5d3..ac23409bd0c5 100644 --- a/tests/pos/i15155.scala +++ b/tests/pos/i15155.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + import scala.reflect.ClassTag // https://github.com/json4s/json4s/blob/355d8751391773e0d79d04402a4f9fb7bfc684ec/ext/src/main/scala-3/org/json4s/ext/package.scala#L4-L8 type Aux[A] = { type Value = A } @@ -8,4 +10,4 @@ type EnumValue[A <: Enumeration] = A match { // https://github.com/json4s/json4s/blob/355d8751391773e0d79d04402a4f9fb7bfc684ec/ext/src/main/scala/org/json4s/ext/EnumSerializer.scala#L25-L26 class EnumSerializer[E <: Enumeration: ClassTag](enumeration: E) { val EnumerationClass = classOf[EnumValue[E]] -} \ No newline at end of file +} diff --git a/tests/pos/i16408.min1.scala b/tests/pos/i16408.min1.scala index 8c45fbaa9783..b35199edbfcd 100644 --- a/tests/pos/i16408.min1.scala +++ b/tests/pos/i16408.min1.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + object Helpers: type NodeFun[R] = Matchable // compiles without [R] parameter diff --git a/tests/pos/i16408.scala b/tests/pos/i16408.scala index 10e8b16bab72..fc894baeb958 100644 --- a/tests/pos/i16408.scala +++ b/tests/pos/i16408.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + import scala.util.Try trait RDF: diff --git a/tests/pos/i16706.scala b/tests/pos/i16706.scala index 87fd015c69bb..e94ce37c0c86 100644 --- a/tests/pos/i16706.scala +++ b/tests/pos/i16706.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + import scala.deriving.Mirror import scala.reflect.ClassTag @@ -14,4 +16,4 @@ transparent inline given derived[A]( sealed trait Foo case class FooA(a: Int) extends Foo -val instance = derived[Foo] // error \ No newline at end of file +val instance = derived[Foo] // error diff --git a/tests/pos/i17395.scala b/tests/pos/i17395.scala index 87c0a45a9ff5..dbe1b08ab2d1 100644 --- a/tests/pos/i17395.scala +++ b/tests/pos/i17395.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + trait TC[T] object TC { diff --git a/tests/pos/i5625b.scala b/tests/pos/i5625b.scala index b2621f9020a8..db2092c18bbc 100644 --- a/tests/pos/i5625b.scala +++ b/tests/pos/i5625b.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + object Test { type AV[t <: AnyVal] = t @@ -13,4 +15,4 @@ object Test { summon[LeafElem[Array[Int]] =:= Int] summon[LeafElem[Iterable[Int]] =:= Int] summon[LeafElem[Int] =:= Int] -} \ No newline at end of file +} diff --git a/tests/run-macros/tasty-simplified/quoted_2.scala b/tests/run-macros/tasty-simplified/quoted_2.scala index dcf100d6e8bb..b6bb99bf7cf9 100644 --- a/tests/run-macros/tasty-simplified/quoted_2.scala +++ b/tests/run-macros/tasty-simplified/quoted_2.scala @@ -1,3 +1,5 @@ +//> using options -source:3.3 + import Macros.simplified object Test { From ec94ff5f061f9abc66eda0a207438ae228f05300 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 24 Nov 2023 16:35:10 +0100 Subject: [PATCH 08/17] Allow to reduce type member extractors when the member is a class. --- .../dotty/tools/dotc/core/TypeComparer.scala | 22 ++++++++----------- .../match-type-enumeration-value-hack.check | 13 +++++++++++ .../match-type-enumeration-value-hack.scala | 12 ++++++++++ .../match-type-enumeration-value-hack.scala | 11 ++++++++++ 4 files changed, 45 insertions(+), 13 deletions(-) create mode 100644 tests/neg/match-type-enumeration-value-hack.check create mode 100644 tests/neg/match-type-enumeration-value-hack.scala create mode 100644 tests/pos/match-type-enumeration-value-hack.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 6f1e334ccc95..027aa569b063 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3371,19 +3371,15 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { stableScrut.member(typeMemberName) match case denot: SingleDenotation if denot.exists => val info = denot.info match - case TypeAlias(alias) => alias - case info => info // Notably, RealTypeBounds, which will eventually give a MatchResult.NoInstances - if info.isInstanceOf[ClassInfo] then - /* The member is not an alias (we'll get Stuck instead of NoInstances, - * which is not ideal, but we cannot make a RealTypeBounds of ClassInfo). - */ - false - else - val infoRefersToSkolem = stableScrut.isInstanceOf[SkolemType] && stableScrut.occursIn(info) - val info1 = - if infoRefersToSkolem && !info.isInstanceOf[TypeBounds] then RealTypeBounds(info, info) // to trigger a MatchResult.NoInstances - else info - rec(capture, info1, variance = 0, scrutIsWidenedAbstract) + case TypeAlias(alias) => alias // Extract the alias + case ClassInfo(prefix, cls, _, _, _) => prefix.select(cls) // Re-select the class from the prefix + case info => info // Notably, RealTypeBounds, which will eventually give a MatchResult.NoInstances + val infoRefersToSkolem = stableScrut.isInstanceOf[SkolemType] && stableScrut.occursIn(info) + val info1 = info match + case info: TypeBounds => info // Will already trigger a MatchResult.NoInstances + case _ if infoRefersToSkolem => RealTypeBounds(info, info) // Explicitly trigger a MatchResult.NoInstances + case _ => info // We have a match + rec(capture, info1, variance = 0, scrutIsWidenedAbstract) case _ => false end rec diff --git a/tests/neg/match-type-enumeration-value-hack.check b/tests/neg/match-type-enumeration-value-hack.check new file mode 100644 index 000000000000..13e425b80dbf --- /dev/null +++ b/tests/neg/match-type-enumeration-value-hack.check @@ -0,0 +1,13 @@ +-- [E172] Type Error: tests/neg/match-type-enumeration-value-hack.scala:11:40 ------------------------------------------ +11 | summon[Suit#Value =:= EnumValue[Suit]] // error + | ^ + | Cannot prove that Suit#Value =:= EnumValue[Suit]. + | + | Note: a match type could not be fully reduced: + | + | trying to reduce EnumValue[Suit] + | failed since selector Suit + | does not uniquely determine parameter t in + | case EnumValueAux[t] => t + | The computed bounds for the parameter are: + | t >: ?1.Value <: ?1.Value diff --git a/tests/neg/match-type-enumeration-value-hack.scala b/tests/neg/match-type-enumeration-value-hack.scala new file mode 100644 index 000000000000..4c6176b9b637 --- /dev/null +++ b/tests/neg/match-type-enumeration-value-hack.scala @@ -0,0 +1,12 @@ +type EnumValueAux[A] = ({ type Value }) { type Value = A } + +type EnumValue[E <: Enumeration] = E match + case EnumValueAux[t] => t + +// A class extending Enumeration does not yet define a concrete enumeration +class Suit extends Enumeration: + val Hearts, Diamonds, Clubs, Spades = Val() + +object Test: + summon[Suit#Value =:= EnumValue[Suit]] // error +end Test diff --git a/tests/pos/match-type-enumeration-value-hack.scala b/tests/pos/match-type-enumeration-value-hack.scala new file mode 100644 index 000000000000..b1f0146c012d --- /dev/null +++ b/tests/pos/match-type-enumeration-value-hack.scala @@ -0,0 +1,11 @@ +type EnumValueAux[A] = ({ type Value }) { type Value = A } + +type EnumValue[E <: Enumeration] = E match + case EnumValueAux[t] => t + +object Suit extends Enumeration: + val Hearts, Diamonds, Clubs, Spades = Val() + +object Test: + summon[Suit.Value =:= EnumValue[Suit.type]] +end Test From 1b2a16ee043140826f697f2e10c8da7e7cb6df39 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Thu, 17 Aug 2023 11:41:53 +0200 Subject: [PATCH 09/17] New implementation of `provablyDisjoint` to match SIP-56. --- .../dotty/tools/dotc/core/TypeComparer.scala | 352 +++++++++++------- tests/neg/6314-1.scala | 9 +- tests/neg/6314-6.check | 16 + tests/neg/6314-6.scala | 12 +- tests/neg/6314.check | 44 +++ tests/neg/6314.scala | 37 +- tests/neg/i13190.check | 15 + tests/{pos => neg}/i13190/A_1.scala | 2 +- tests/{pos => neg}/i13190/B_2.scala | 2 +- tests/neg/i13190b.check | 14 + tests/neg/i13190b.scala | 19 + tests/neg/i15312.check | 17 + tests/{pos => neg}/i15312.scala | 2 +- tests/{pos => pos-deep-subtype}/i15677.scala | 0 .../match-type-disjoint-transitivity.scala | 56 +++ 15 files changed, 430 insertions(+), 167 deletions(-) create mode 100644 tests/neg/6314-6.check create mode 100644 tests/neg/6314.check create mode 100644 tests/neg/i13190.check rename tests/{pos => neg}/i13190/A_1.scala (96%) rename tests/{pos => neg}/i13190/B_2.scala (88%) create mode 100644 tests/neg/i13190b.check create mode 100644 tests/neg/i13190b.scala create mode 100644 tests/neg/i15312.check rename tests/{pos => neg}/i15312.scala (58%) rename tests/{pos => pos-deep-subtype}/i15677.scala (100%) create mode 100644 tests/pos/match-type-disjoint-transitivity.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 027aa569b063..860bdf10b3a1 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2807,159 +2807,225 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling * property that in all possible contexts, the same match type expression * is either stuck or reduces to the same case. */ - def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean = trace(i"provable disjoint $tp1, $tp2", matchTypes) { - // println(s"provablyDisjoint(${tp1.show}, ${tp2.show})") + def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean = + provablyDisjoint(tp1, tp2, null) - def isEnumValue(ref: TermRef): Boolean = - val sym = ref.termSymbol - sym.isAllOf(EnumCase, butNot=JavaDefined) + def provablyDisjoint(tp1: Type, tp2: Type, pending: util.HashSet[(Type, Type)] | Null)( + using Context): Boolean = trace(i"provable disjoint $tp1, $tp2", matchTypes) { + // println(s"provablyDisjoint(${tp1.show}, ${tp2.show})") - def isEnumValueOrModule(ref: TermRef): Boolean = - isEnumValue(ref) || ref.termSymbol.is(Module) || (ref.info match { - case tp: TermRef => isEnumValueOrModule(tp) - case _ => false - }) - - def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] { - override def apply(x: Boolean, t: Type) = - x && { - t.dealias match { - case tp: TypeRef if !tp.symbol.isClass => false - case _: SkolemType | _: TypeVar | _: TypeParamRef | _: TypeBounds => false - case _ => foldOver(x, t) - } - } - }.apply(true, tp) - - (tp1.dealias, tp2.dealias) match { - case _ if !ctx.erasedTypes && tp2.isFromJavaObject => - provablyDisjoint(tp1, defn.AnyType) - case _ if !ctx.erasedTypes && tp1.isFromJavaObject => - provablyDisjoint(defn.AnyType, tp2) - case (tp1: TypeRef, _) if tp1.symbol == defn.AnyKindClass => - false - case (_, tp2: TypeRef) if tp2.symbol == defn.AnyKindClass => - false - case (tp1: TypeRef, _) if tp1.symbol == defn.SingletonClass => - false - case (_, tp2: TypeRef) if tp2.symbol == defn.SingletonClass => + @scala.annotation.tailrec + def disjointnessBoundary(tp: Type): Type = tp match + case tp: TypeRef => + tp.symbol match + case cls: ClassSymbol => + if cls == defn.SingletonClass then defn.AnyType + else tp + case sym => + if !ctx.erasedTypes && sym == defn.FromJavaObjectSymbol then defn.AnyType + else + val optGadtBounds = gadtBounds(sym) + if optGadtBounds != null then disjointnessBoundary(optGadtBounds.hi) + else disjointnessBoundary(tp.superTypeNormalized) + case tp @ AppliedType(tycon: TypeRef, _) if tycon.symbol.isClass => + tp + case tp: TermRef => + val isEnumValue = tp.termSymbol.isAllOf(EnumCase, butNot = JavaDefined) + if isEnumValue then tp + else + val optGadtBounds = gadtBounds(tp.symbol) + if optGadtBounds != null then disjointnessBoundary(optGadtBounds.hi) + else disjointnessBoundary(tp.superTypeNormalized) + case tp: AndOrType => + tp + case tp: ConstantType => + tp + case tp: TypeProxy => + disjointnessBoundary(tp.superTypeNormalized) + case tp: WildcardType => + disjointnessBoundary(tp.effectiveBounds.hi) + case tp: ErrorType => + defn.AnyType + end disjointnessBoundary + + (disjointnessBoundary(tp1), disjointnessBoundary(tp2)) match + // Infinite recursion detection + case pair if pending != null && pending.contains(pair) => false + + // Cases where there is an intersection or union on the right + case (tp1, tp2: OrType) => + provablyDisjoint(tp1, tp2.tp1, pending) && provablyDisjoint(tp1, tp2.tp2, pending) + case (tp1, tp2: AndType) => + provablyDisjoint(tp1, tp2.tp1, pending) || provablyDisjoint(tp1, tp2.tp2, pending) + + // Cases where there is an intersection or union on the left but not on the right + case (tp1: OrType, tp2) => + provablyDisjoint(tp1.tp1, tp2, pending) && provablyDisjoint(tp1.tp2, tp2, pending) + case (tp1: AndType, tp2) => + provablyDisjoint(tp1.tp1, tp2, pending) || provablyDisjoint(tp1.tp2, tp2, pending) + + /* Cases where both are unique values (enum cases or constant types) + * + * When both are TermRef's, we look at the symbols. We do not try to + * prove disjointness based on the prefixes. + * + * Otherwise, we know everything there is to know about them our two types. + * Therefore, a direct subtype test is enough to decide disjointness. + */ + case (tp1: TermRef, tp2: TermRef) => + tp1.symbol != tp2.symbol case (tp1: ConstantType, tp2: ConstantType) => - tp1 != tp2 - case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass => - val cls1 = tp1.classSymbol - val cls2 = tp2.classSymbol - val sameKind = tp1.hasSameKindAs(tp2) - def isDecomposable(sym: Symbol): Boolean = - sameKind && sym.is(Sealed) && !sym.hasAnonymousChild - def decompose(sym: Symbol, tp: Type): List[Type] = - val tpSimple = tp.applyIfParameterized(tp.typeParams.map(_ => WildcardType)) - sym.children.map(x => refineUsingParent(tpSimple, x)).filter(_.exists) - if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)) - false - else - if (cls1.is(Final) || cls2.is(Final)) - // One of these types is final and they are not mutually - // subtype, so they must be unrelated. - true - else if (!cls2.is(Trait) && !cls1.is(Trait)) - // Both of these types are classes and they are not mutually - // subtype, so they must be unrelated by single inheritance - // of classes. - true - else if (isDecomposable(cls1)) - // At this point, !cls1.derivesFrom(cls2): we know that direct - // instantiations of `cls1` (terms of the form `new cls1`) are not - // of type `tp2`. Therefore, we can safely decompose `cls1` using - // `.children`, even if `cls1` is non abstract. - decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2)) - else if (isDecomposable(cls2)) - decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1)) + tp1.value != tp2.value + case (tp1: SingletonType, tp2: SingletonType) => + true // a TermRef and a ConstantType, in either direction + + /* Cases where one is a unique value and the other a possibly-parameterized + * class type. Again, we do not look at prefixes, so we test whether the + * unique value derives from the class. + */ + case (tp1: SingletonType, tp2) => + !tp1.derivesFrom(tp2.classSymbol) + case (tp1, tp2: SingletonType) => + !tp2.derivesFrom(tp1.classSymbol) + + /* Now both sides are possibly-parameterized class types `p.C[Ts]` and `q.D[Us]`. + * + * First, we try to show that C and D are entirely disjoint, independently + * of the type arguments, based on their `final` status and `class` status. + * + * Otherwise, we look at all the common baseClasses of tp1 and tp2, and + * try to find one common base class `E` such that `baseType(tp1, E)` and + * `baseType(tp2, E)` can be proven disjoint based on the type arguments. + * + * Regardless, we do not look at prefixes. + */ + case tpPair @ (tp1, tp2) => + val cls1 = tp1.classSymbol.asClass + val cls2 = tp2.classSymbol.asClass + + def isBaseTypeWithDisjointArguments(baseClass: ClassSymbol, pending: util.HashSet[(Type, Type)]): Boolean = + if baseClass.typeParams.isEmpty then + // A common mono base class can never be disjoint thanks to type params + false else + (tp1.baseType(baseClass), tp2.baseType(baseClass)) match + case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) => + provablyDisjointTypeArgs(baseClass, args1, args2, pending) + case _ => + false + end isBaseTypeWithDisjointArguments + + def typeArgsMatch(tp: Type, cls: ClassSymbol): Boolean = + val typeArgs = tp match + case tp: TypeRef => Nil + case AppliedType(_, args) => args + cls.typeParams.sizeCompare(typeArgs) == 0 + + def existsCommonBaseTypeWithDisjointArguments: Boolean = + if !typeArgsMatch(tp1, cls1) || !typeArgsMatch(tp2, cls2) then + /* We have an unapplied polymorphic class type or otherwise not star-kinded one. + * This does not happen with match types, but happens when coming from the Space engine. + * In that case, we cannot prove disjointness based on type arguments. + */ false - case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if isSame(tycon1, tycon2) => - // It is possible to conclude that two types applied are disjoint by - // looking at covariant type parameters if the said type parameters - // are disjoin and correspond to fields. - // (Type parameter disjointness is not enough by itself as it could - // lead to incorrect conclusions for phantom type parameters). - def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = - provablyDisjoint(tp1, tp2) && typeparamCorrespondsToField(tycon1, tparam) - - // In the invariant case, we also use a stronger notion of disjointness: - // we consider fully instantiated types not equal wrt =:= to be disjoint - // (under any context). This is fine because it matches the runtime - // semantics of pattern matching. To implement a pattern such as - // `case Inv[T] => ...`, one needs a type tag for `T` and the compiler - // is used at runtime to check it the scrutinee's type is =:= to `T`. - // Note that this is currently a theoretical concern since Dotty - // doesn't have type tags, meaning that users cannot write patterns - // that do type tests on higher kinded types. - def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = - provablyDisjoint(tp1, tp2) || - !isSameType(tp1, tp2) && - fullyInstantiated(tp1) && // We can only trust a "no" from `isSameType` when - fullyInstantiated(tp2) // both `tp1` and `tp2` are fully instantiated. - - args1.lazyZip(args2).lazyZip(tycon1.typeParams).exists { - (arg1, arg2, tparam) => - val v = tparam.paramVarianceSign - if (v > 0) - covariantDisjoint(arg1, arg2, tparam) - else if (v < 0) - // Contravariant case: a value where this type parameter is - // instantiated to `Any` belongs to both types. - false - else - invariantDisjoint(arg1, arg2, tparam) - } - case (tp1: HKLambda, tp2: HKLambda) => - provablyDisjoint(tp1.resType, tp2.resType) - case (_: HKLambda, _) => - // The intersection of these two types would be ill kinded, they are therefore provablyDisjoint. + else + /* We search among the common base classes of `cls1` and `cls2`. + * We exclude any base class that is an ancestor of one of the other base classes: + * they are useless, since anything discovered at their level would also be discovered at + * the level of the descendant common base class. + */ + val innerPending = + if pending != null then pending + else util.HashSet[(Type, Type)]() + innerPending += tpPair + + val cls2BaseClassSet = SymDenotations.BaseClassSet(cls2.classDenot.baseClasses) + val commonBaseClasses = cls1.classDenot.baseClasses.filter(cls2BaseClassSet.contains(_)) + def isAncestorOfOtherBaseClass(cls: ClassSymbol): Boolean = + commonBaseClasses.exists(other => (other ne cls) && other.derivesFrom(cls)) + val result = commonBaseClasses.exists { baseClass => + !isAncestorOfOtherBaseClass(baseClass) && isBaseTypeWithDisjointArguments(baseClass, innerPending) + } + + innerPending -= tpPair + result + end existsCommonBaseTypeWithDisjointArguments + + provablyDisjointClasses(cls1, cls2) + || existsCommonBaseTypeWithDisjointArguments + end match + } + + private def provablyDisjointClasses(cls1: Symbol, cls2: Symbol)(using Context): Boolean = + def isDecomposable(cls: Symbol): Boolean = + cls.is(Sealed) && !cls.hasAnonymousChild + + def decompose(cls: Symbol): List[Symbol] = + cls.children.map { child => + if child.isTerm then child.info.classSymbol + else child + }.filter(child => child.exists && child != cls) + + // TODO? Special-case for Nothing and Null? We probably need Nothing/Null disjoint from Nothing/Null + def eitherDerivesFromOther(cls1: Symbol, cls2: Symbol): Boolean = + cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1) + + def smallestNonTraitBase(cls: Symbol): Symbol = + cls.asClass.baseClasses.find(!_.is(Trait)).get + + if cls1 == defn.AnyKindClass || cls2 == defn.AnyKindClass then + // For some reason, A.derivesFrom(AnyKind) returns false, so we have to handle it specially + false + else if (eitherDerivesFromOther(cls1, cls2)) + false + else + if (cls1.is(Final) || cls2.is(Final)) + // One of these types is final and they are not mutually + // subtype, so they must be unrelated. true - case (_, _: HKLambda) => + else if (!eitherDerivesFromOther(smallestNonTraitBase(cls1), smallestNonTraitBase(cls2))) then + // The traits extend a pair of non-trait classes that are not mutually subtypes, + // so they must be unrelated by single inheritance of classes. true - case (tp1: OrType, _) => - provablyDisjoint(tp1.tp1, tp2) && provablyDisjoint(tp1.tp2, tp2) - case (_, tp2: OrType) => - provablyDisjoint(tp1, tp2.tp1) && provablyDisjoint(tp1, tp2.tp2) - case (tp1: AndType, _) => - !(tp1 <:< tp2) - && (provablyDisjoint(tp1.tp2, tp2) || provablyDisjoint(tp1.tp1, tp2)) - case (_, tp2: AndType) => - !(tp2 <:< tp1) - && (provablyDisjoint(tp1, tp2.tp2) || provablyDisjoint(tp1, tp2.tp1)) - case (tp1: NamedType, _) if gadtBounds(tp1.symbol) != null => - provablyDisjoint(gadtBounds(tp1.symbol).uncheckedNN.hi, tp2) - || provablyDisjoint(tp1.superTypeNormalized, tp2) - case (_, tp2: NamedType) if gadtBounds(tp2.symbol) != null => - provablyDisjoint(tp1, gadtBounds(tp2.symbol).uncheckedNN.hi) - || provablyDisjoint(tp1, tp2.superTypeNormalized) - case (tp1: TermRef, tp2: TermRef) if isEnumValueOrModule(tp1) && isEnumValueOrModule(tp2) => - tp1.termSymbol != tp2.termSymbol - case (tp1: TermRef, tp2: TypeRef) if isEnumValue(tp1) => - fullyInstantiated(tp2) && !tp1.classSymbols.exists(_.derivesFrom(tp2.symbol)) - case (tp1: TypeRef, tp2: TermRef) if isEnumValue(tp2) => - fullyInstantiated(tp1) && !tp2.classSymbols.exists(_.derivesFrom(tp1.symbol)) - case (tp1: RefinedType, tp2: RefinedType) if tp1.refinedName == tp2.refinedName => - provablyDisjoint(tp1.parent, tp2.parent) || provablyDisjoint(tp1.refinedInfo, tp2.refinedInfo) - case (tp1: TypeAlias, tp2: TypeAlias) => - provablyDisjoint(tp1.alias, tp2.alias) - case (tp1: Type, tp2: Type) if defn.isTupleNType(tp1) => - provablyDisjoint(tp1.toNestedPairs, tp2) - case (tp1: Type, tp2: Type) if defn.isTupleNType(tp2) => - provablyDisjoint(tp1, tp2.toNestedPairs) - case (tp1: TypeProxy, tp2: TypeProxy) => - provablyDisjoint(tp1.superTypeNormalized, tp2) || provablyDisjoint(tp1, tp2.superTypeNormalized) - case (tp1: TypeProxy, _) => - provablyDisjoint(tp1.superTypeNormalized, tp2) - case (_, tp2: TypeProxy) => - provablyDisjoint(tp1, tp2.superTypeNormalized) - case _ => + else if (isDecomposable(cls1)) + // At this point, !cls1.derivesFrom(cls2): we know that direct + // instantiations of `cls1` (terms of the form `new cls1`) are not + // of type `tp2`. Therefore, we can safely decompose `cls1` using + // `.children`, even if `cls1` is non abstract. + decompose(cls1).forall(x => provablyDisjointClasses(x, cls2)) + else if (isDecomposable(cls2)) + decompose(cls2).forall(x => provablyDisjointClasses(cls1, x)) + else false + end provablyDisjointClasses + + private def provablyDisjointTypeArgs(cls: ClassSymbol, args1: List[Type], args2: List[Type], pending: util.HashSet[(Type, Type)])(using Context): Boolean = + // It is possible to conclude that two types applied are disjoint by + // looking at covariant type parameters if the said type parameters + // are disjoint and correspond to fields. + // (Type parameter disjointness is not enough by itself as it could + // lead to incorrect conclusions for phantom type parameters). + def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = + provablyDisjoint(tp1, tp2, pending) && typeparamCorrespondsToField(cls.appliedRef, tparam) + + // In the invariant case, direct type parameter disjointness is enough. + def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = + provablyDisjoint(tp1, tp2, pending) + + args1.lazyZip(args2).lazyZip(cls.typeParams).exists { + (arg1, arg2, tparam) => + val v = tparam.paramVarianceSign + if (v > 0) + covariantDisjoint(arg1, arg2, tparam) + else if (v < 0) + // Contravariant case: a value where this type parameter is + // instantiated to `Any` belongs to both types. + false + else + invariantDisjoint(arg1, arg2, tparam) } - } + end provablyDisjointTypeArgs protected def explainingTypeComparer(short: Boolean) = ExplainingTypeComparer(comparerContext, short) protected def trackingTypeComparer = TrackingTypeComparer(comparerContext) diff --git a/tests/neg/6314-1.scala b/tests/neg/6314-1.scala index 5d5662c338e3..8585b707004d 100644 --- a/tests/neg/6314-1.scala +++ b/tests/neg/6314-1.scala @@ -1,6 +1,7 @@ object G { - final class X - final class Y + trait X + class Y + class Z trait FooSig { type Type @@ -13,14 +14,14 @@ object G { type Foo = Foo.Type type Bar[A] = A match { - case X & Y => String + case X & Z => String case Y => Int } def main(args: Array[String]): Unit = { val a: Bar[X & Y] = "hello" // error val i: Bar[Y & Foo] = Foo.apply[Bar](a) - val b: Int = i // error + val b: Int = i println(b + 1) } } diff --git a/tests/neg/6314-6.check b/tests/neg/6314-6.check new file mode 100644 index 000000000000..7d6bd182173d --- /dev/null +++ b/tests/neg/6314-6.check @@ -0,0 +1,16 @@ +-- Error: tests/neg/6314-6.scala:26:3 ---------------------------------------------------------------------------------- +26 | (new YY {}).boom // error: object creation impossible + | ^ + |object creation impossible, since def apply(fa: String): Int in trait XX in object Test3 is not defined + |(Note that + | parameter String in def apply(fa: String): Int in trait XX in object Test3 does not match + | parameter Test3.Bar[X & Object with Test3.YY {...}#Foo] in def apply(fa: Test3.Bar[X & YY.this.Foo]): Test3.Bar[Y & YY.this.Foo] in trait YY in object Test3 + | ) +-- Error: tests/neg/6314-6.scala:52:3 ---------------------------------------------------------------------------------- +52 | (new YY {}).boom // error: object creation impossible + | ^ + |object creation impossible, since def apply(fa: String): Int in trait XX in object Test4 is not defined + |(Note that + | parameter String in def apply(fa: String): Int in trait XX in object Test4 does not match + | parameter Test4.Bar[X & Object with Test4.YY {...}#FooAlias] in def apply(fa: Test4.Bar[X & YY.this.FooAlias]): Test4.Bar[Y & YY.this.FooAlias] in trait YY in object Test4 + | ) diff --git a/tests/neg/6314-6.scala b/tests/neg/6314-6.scala index 6c400ab46d97..23853e20434d 100644 --- a/tests/neg/6314-6.scala +++ b/tests/neg/6314-6.scala @@ -21,11 +21,9 @@ object Test3 { trait YY extends XX { type Foo = X & Y - def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa // error - // overriding method apply in trait XX of type (fa: String): Int; - // method apply of type (fa: String): String has incompatible type + def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa } - (new YY {}).boom + (new YY {}).boom // error: object creation impossible } object Test4 { @@ -49,9 +47,7 @@ object Test4 { trait YY extends XX { type Foo = X & Y - def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa // error - // overriding method apply in trait XX of type (fa: String): Int; - // method apply of type (fa: String): String has incompatible type + def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa } - (new YY {}).boom + (new YY {}).boom // error: object creation impossible } diff --git a/tests/neg/6314.check b/tests/neg/6314.check new file mode 100644 index 000000000000..2a5e8b68a999 --- /dev/null +++ b/tests/neg/6314.check @@ -0,0 +1,44 @@ +-- [E007] Type Mismatch Error: tests/neg/6314.scala:28:27 -------------------------------------------------------------- +28 | val i: Bar[Y | Type] = 1 // error + | ^ + | Found: (1 : Int) + | Required: Test1Bis.Bar[Test1Bis.Y | Test.this.Type] + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Test1Bis.Bar[Test1Bis.Y | Test.this.Type] + | failed since selector Test1Bis.Y | Test.this.Type + | does not match case Test1Bis.X & Test1Bis.Y => String + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case Any => Int + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/6314.scala:45:33 -------------------------------------------------------------- +45 | def right(fa: Bar[L]): Int = fa // error + | ^^ + | Found: (fa : Wizzle.this.Bar[L]) + | Required: Int + | + | where: L is a type in trait Wizzle with bounds <: Int & Singleton + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/6314.scala:55:33 -------------------------------------------------------------- +55 | def right(fa: Bar[L]): Int = fa // error + | ^^ + | Found: (fa : Wazzlo.this.Bar[L]) + | Required: Int + | + | where: L is a type in trait Wazzlo with bounds <: Int & AnyVal + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg/6314.scala:65:33 -------------------------------------------------------------- +65 | def right(fa: Bar[L]): Int = fa // error + | ^^ + | Found: (fa : Wuzzlu.this.Bar[L]) + | Required: Int + | + | where: L is a type in trait Wuzzlu with bounds <: String & AnyRef + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg/6314.scala b/tests/neg/6314.scala index beee41c48e9a..17adbceef1fd 100644 --- a/tests/neg/6314.scala +++ b/tests/neg/6314.scala @@ -1,22 +1,41 @@ -final class X -final class Y - object Test1 { + // X, Y and Z are unrelated, Y is provably disjoint from Z, but X is not provably disjoint with either + trait X + class Y + class Z + trait Test { type Type // This is testing that both permutations of the types in a & - // are taken into account by the intersection test - val i: Bar[Y & Type] = 1 // error + // are taken into account by the provablyDisjoint test + val i: Bar[Y & Type] = 1 // ok, disjoint from X & Z because Y and Z are disjoint } type Bar[A] = A match { - case X & Y => String + case X & Z => String case Y => Int } } +object Test1Bis { + final class X + final class Y + + trait Test { + type Type + // This is testing that both permutations of the types in a | + // are taken into account by the provablyDisjoint test + val i: Bar[Y | Type] = 1 // error + } + + type Bar[A] = A match { + case X & Y => String + case Any => Int + } +} + object Test2 { - trait Wizzle[L <: Int with Singleton] { + trait Wizzle[L <: Int & Singleton] { type Bar[A] = A match { case 0 => String case L => Int @@ -26,7 +45,7 @@ object Test2 { def right(fa: Bar[L]): Int = fa // error } - trait Wazzlo[L <: Int with AnyVal] { + trait Wazzlo[L <: Int & AnyVal] { type Bar[A] = A match { case 0 => String case L => Int @@ -36,7 +55,7 @@ object Test2 { def right(fa: Bar[L]): Int = fa // error } - trait Wuzzlu[L <: String with AnyRef] { + trait Wuzzlu[L <: String & AnyRef] { type Bar[A] = A match { case "" => String case L => Int diff --git a/tests/neg/i13190.check b/tests/neg/i13190.check new file mode 100644 index 000000000000..d6096eae30e0 --- /dev/null +++ b/tests/neg/i13190.check @@ -0,0 +1,15 @@ + +-- [E172] Type Error: tests/neg/i13190/B_2.scala:14:38 ----------------------------------------------------------------- +14 | summon[FindField[R, "B"] =:= Double] // error + | ^ + | Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double. + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Test.FindField[Test.R, ("B" : String)] + | failed since selector Test.R + | does not match case Opaque.FieldType[("B" : String), f] *: t => f + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case _ *: t => Test.FindField[t, ("B" : String)] diff --git a/tests/pos/i13190/A_1.scala b/tests/neg/i13190/A_1.scala similarity index 96% rename from tests/pos/i13190/A_1.scala rename to tests/neg/i13190/A_1.scala index 9bb9b20f2976..7ab97942eaf9 100644 --- a/tests/pos/i13190/A_1.scala +++ b/tests/neg/i13190/A_1.scala @@ -1,3 +1,3 @@ object Opaque { opaque type FieldType[K, +V] <: V = V -} \ No newline at end of file +} diff --git a/tests/pos/i13190/B_2.scala b/tests/neg/i13190/B_2.scala similarity index 88% rename from tests/pos/i13190/B_2.scala rename to tests/neg/i13190/B_2.scala index 2752778afa04..71b6cac970d3 100644 --- a/tests/pos/i13190/B_2.scala +++ b/tests/neg/i13190/B_2.scala @@ -11,5 +11,5 @@ object Test { //val f2: Int = f type R = FieldType["A", Int] *: FieldType["B", Double] *: FieldType["C", String] *: FieldType["D", Boolean] *: EmptyTuple - summon[FindField[R, "B"] =:= Double] + summon[FindField[R, "B"] =:= Double] // error } diff --git a/tests/neg/i13190b.check b/tests/neg/i13190b.check new file mode 100644 index 000000000000..7708de3769a8 --- /dev/null +++ b/tests/neg/i13190b.check @@ -0,0 +1,14 @@ +-- [E172] Type Error: tests/neg/i13190b.scala:18:38 -------------------------------------------------------------------- +18 | summon[FindField[R, "B"] =:= Double] // error + | ^ + | Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double. + | + | Note: a match type could not be fully reduced: + | + | trying to reduce Test.FindField[Test.R, ("B" : String)] + | failed since selector Test.R + | does not match case Opaque.FieldType[("B" : String), f] *: t => f + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case _ *: t => Test.FindField[t, ("B" : String)] diff --git a/tests/neg/i13190b.scala b/tests/neg/i13190b.scala new file mode 100644 index 000000000000..0791a171c629 --- /dev/null +++ b/tests/neg/i13190b.scala @@ -0,0 +1,19 @@ +object Opaque { + opaque type FieldType[K, +V] <: V = V +} + +import Opaque.* + +object Test { + type FindField[R <: scala.Tuple, K] = R match { + case FieldType[K, f] *: t => f + case _ *: t => FindField[t, K] + } + + val f: FieldType["A", Int] = ??? + val f1: Int = f + //val f2: Int = f + + type R = FieldType["A", Int] *: FieldType["B", Double] *: FieldType["C", String] *: FieldType["D", Boolean] *: EmptyTuple + summon[FindField[R, "B"] =:= Double] // error +} diff --git a/tests/neg/i15312.check b/tests/neg/i15312.check new file mode 100644 index 000000000000..188b03518b43 --- /dev/null +++ b/tests/neg/i15312.check @@ -0,0 +1,17 @@ +-- [E007] Type Mismatch Error: tests/neg/i15312.scala:7:27 ------------------------------------------------------------- +7 |val b: F[{type A = Int}] = "asd" // error + | ^^^^^ + | Found: ("asd" : String) + | Required: F[Object{type A = Int}] + | + | Note: a match type could not be fully reduced: + | + | trying to reduce F[Object{type A = Int}] + | failed since selector Object{type A = Int} + | does not match case Object{type A = Float} => Int + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case Object{type A = Int} => String + | + | longer explanation available when compiling with `-explain` diff --git a/tests/pos/i15312.scala b/tests/neg/i15312.scala similarity index 58% rename from tests/pos/i15312.scala rename to tests/neg/i15312.scala index 28ce2f9bafe2..c3f225aabc74 100644 --- a/tests/pos/i15312.scala +++ b/tests/neg/i15312.scala @@ -4,4 +4,4 @@ type F[t] = case {type A = Int} => String val a: F[{type A = Float}] = 10 -val b: F[{type A = Int}] = "asd" // Found:("asd" : String) Required: F[Object{A = Int}] \ No newline at end of file +val b: F[{type A = Int}] = "asd" // error diff --git a/tests/pos/i15677.scala b/tests/pos-deep-subtype/i15677.scala similarity index 100% rename from tests/pos/i15677.scala rename to tests/pos-deep-subtype/i15677.scala diff --git a/tests/pos/match-type-disjoint-transitivity.scala b/tests/pos/match-type-disjoint-transitivity.scala new file mode 100644 index 000000000000..84872d8d2a3a --- /dev/null +++ b/tests/pos/match-type-disjoint-transitivity.scala @@ -0,0 +1,56 @@ +/* Tests that the following property holds for a chosen set of types (S, T, U): + * + * If S <: T and T provably disjoint from U, then S provably disjoint from U. + */ + +class Parent[T] +class Child[T] extends Parent[T] +trait ChildTrait[T] extends Parent[T] + +class OtherClass + +trait Common[A] +trait Left[A] extends Common[A] +trait Right[A] extends Common[A] + +// Since Parent[Boolean] disjoint from Parent[Int], we must have Child[Boolean] also disjoint from Parent[Int] +object Test1: + type MT[X] = X match + case Parent[Int] => Int + case Parent[Boolean] => Boolean + + def test(): Unit = + summon[MT[Parent[Int]] =:= Int] + summon[MT[Parent[Boolean]] =:= Boolean] + + summon[MT[Child[Int]] =:= Int] + summon[MT[Child[Boolean]] =:= Boolean] + end test +end Test1 + +// Since Parent[Int] disjoint from OtherClass, we must have Child[Int] and ChildTrait[T] also disjoint from OtherClass +object Test2: + type MT[X] = X match + case OtherClass => Int + case Parent[Int] => Boolean + + def test(): Unit = + summon[MT[OtherClass] =:= Int] + summon[MT[Parent[Int]] =:= Boolean] + + summon[MT[Child[Int]] =:= Boolean] + summon[MT[ChildTrait[Int]] =:= Boolean] + end test +end Test2 + +// Since Common[Int] is disjoint from Right[Boolean], we must have Left[Int] disjoint from Right[Boolean] +object Test3: + type MT[X] = X match + case Right[Boolean] => Int + case Any => Boolean + + def test(): Unit = + summon[MT[Common[Int]] =:= Boolean] + summon[MT[Left[Int]] =:= Boolean] + end test +end Test3 From f432d08f98c43e6a1607e48d13212a704e7587fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Tue, 29 Aug 2023 10:13:37 +0200 Subject: [PATCH 10/17] Be more specific about higher-kinded types in provablyDisjoint. Previously the disjointnessBoundary of HKTypeLambda's was implicitly their `resultType`, through the use of `superTypeNormalized`. This was fine as long as both sides of `provablyDisjoint` ended up being HKTypeLambda's at the same time, but this may not always be the case (notably with any-kinded types). It is safer to consider type lambdas as boundaries themselves, and explicitly recurse on the result types when arities match. This change surfaced a weird case in `TypeTestsCasts`, which called `provablyDisjoint` with ill-kinded types. We now explicitly apply what I suspect are partially-erased types to wildcards to recover appropriate kinds. --- .../src/dotty/tools/dotc/core/TypeComparer.scala | 12 ++++++++++++ .../dotty/tools/dotc/transform/TypeTestsCasts.scala | 6 +++++- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 860bdf10b3a1..6ec57ea02c9b 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2820,6 +2820,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling tp.symbol match case cls: ClassSymbol => if cls == defn.SingletonClass then defn.AnyType + else if cls.typeParams.nonEmpty then EtaExpansion(tp) else tp case sym => if !ctx.erasedTypes && sym == defn.FromJavaObjectSymbol then defn.AnyType @@ -2840,6 +2841,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling tp case tp: ConstantType => tp + case tp: HKTypeLambda => + tp case tp: TypeProxy => disjointnessBoundary(tp.superTypeNormalized) case tp: WildcardType => @@ -2865,6 +2868,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling case (tp1: AndType, tp2) => provablyDisjoint(tp1.tp1, tp2, pending) || provablyDisjoint(tp1.tp2, tp2, pending) + // Cases involving type lambdas + case (tp1: HKTypeLambda, tp2: HKTypeLambda) => + tp1.paramNames.sizeCompare(tp2.paramNames) != 0 + || provablyDisjoint(tp1.resultType, tp2.resultType, pending) + case (tp1: HKTypeLambda, tp2) => + !tp2.isDirectRef(defn.AnyKindClass) + case (tp1, tp2: HKTypeLambda) => + !tp1.isDirectRef(defn.AnyKindClass) + /* Cases where both are unique values (enum cases or constant types) * * When both are TermRef's, we look at the symbols. We do not try to diff --git a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala index fb90ea4abfea..74a4845424ea 100644 --- a/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala +++ b/compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala @@ -154,7 +154,11 @@ object TypeTestsCasts { case x => // always false test warnings are emitted elsewhere - TypeComparer.provablyDisjoint(x, tpe.derivedAppliedType(tycon, targs.map(_ => WildcardType))) + // provablyDisjoint wants fully applied types as input; because we're in the middle of erasure, we sometimes get raw types here + val xApplied = + val tparams = x.typeParams + if tparams.isEmpty then x else x.appliedTo(tparams.map(_ => WildcardType)) + TypeComparer.provablyDisjoint(xApplied, tpe.derivedAppliedType(tycon, targs.map(_ => WildcardType))) || typeArgsDeterminable(X, tpe) ||| i"its type arguments can't be determined from $X" } From c653793bbacc919b3a61eddce9f47afdafb89d38 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 24 Nov 2023 16:38:08 +0100 Subject: [PATCH 11/17] Do not use provablyEmpty anymore; use S <: T + provablyDisjoint(S, T) instead. Fundamentally, the `provablyEmpty(scrut)` test was meant to prevent situations where both `scrut <: pattern` and `provablyDisjoint(scrut, pattern)` are true. That is a problem because it allows a match type to reduce in two different ways depending on the context. Instead, we basically use that combination of `scrut <: pattern` and `provablydisjoint(scrut, pattern)` as the *definition* for `provablyEmpty`. When both those conditions arise together, we refuse to reduce the match type. This allows one example to pass that did not pass before, but that particular example does not seem to cause unsoundness. In a sense, `provablyEmpty` was too strong here. --- .../dotty/tools/dotc/core/TypeComparer.scala | 87 ++++++------- tests/neg/12800.scala | 21 ---- tests/neg/6570.check | 116 ++++++++++++++++++ tests/neg/6571.check | 6 +- tests/pos/12800.scala | 19 +++ 5 files changed, 178 insertions(+), 71 deletions(-) delete mode 100644 tests/neg/12800.scala create mode 100644 tests/neg/6570.check create mode 100644 tests/pos/12800.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 6ec57ea02c9b..b129445a4fdb 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2771,26 +2771,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`. @@ -3234,14 +3214,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.* @@ -3336,9 +3318,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 @@ -3472,9 +3458,12 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { // This might not be needed val constrainedCaseLambda = constrained(spec.origMatchCase, ast.tpd.EmptyTree)._1.asInstanceOf[HKTypeLambda] - def tryDisjoint: MatchResult = + val disjoint = val defn.MatchCase(origPattern, _) = constrainedCaseLambda.resultType: @unchecked - if provablyDisjoint(scrut, origPattern) then + provablyDisjoint(scrut, origPattern) + + def tryDisjoint: MatchResult = + if disjoint then MatchResult.Disjoint else MatchResult.Stuck @@ -3490,7 +3479,10 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { val defn.MatchCase(instantiatedPat, reduced) = instantiateParamsSpec(instances, constrainedCaseLambda)(constrainedCaseLambda.resultType): @unchecked if scrut <:< instantiatedPat then - MatchResult.Reduced(reduced) + if disjoint then + MatchResult.ReducedAndDisjoint + else + MatchResult.Reduced(reduced) else tryDisjoint else @@ -3514,6 +3506,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 @@ -3524,13 +3518,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 @@ -3557,28 +3554,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`). +} From 16cf4f269415db7d9613b8e51d18d3a983ea0e8e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Wed, 30 Aug 2023 17:30:50 +0200 Subject: [PATCH 12/17] Add regression tests for old issues fixed with the new match types. Closes #17121. Closes #17944. Closes #18488. --- tests/neg/i17121.check | 24 ++++++++++++++++++++++ tests/neg/i17121.scala | 20 ++++++++++++++++++ tests/neg/i17944.check | 46 ++++++++++++++++++++++++++++++++++++++++++ tests/neg/i17944.scala | 44 ++++++++++++++++++++++++++++++++++++++++ tests/pos/i18488.scala | 15 ++++++++++++++ 5 files changed, 149 insertions(+) create mode 100644 tests/neg/i17121.check create mode 100644 tests/neg/i17121.scala create mode 100644 tests/neg/i17944.check create mode 100644 tests/neg/i17944.scala create mode 100644 tests/pos/i18488.scala diff --git a/tests/neg/i17121.check b/tests/neg/i17121.check new file mode 100644 index 000000000000..59895dd2474a --- /dev/null +++ b/tests/neg/i17121.check @@ -0,0 +1,24 @@ +-- [E191] Type Error: tests/neg/i17121.scala:13:17 --------------------------------------------------------------------- +13 | type G1[X] = X match { case Consumer[List[t]] => t } // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | The match type contains an illegal case: + | case Consumer[List[t]] => t + | (this error can be ignored for now with `-source:3.3`) +-- [E191] Type Error: tests/neg/i17121.scala:15:17 --------------------------------------------------------------------- +15 | type G2[X] = X match { case Consumer[Consumer[t]] => t } // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | The match type contains an illegal case: + | case Consumer[Consumer[t]] => t + | (this error can be ignored for now with `-source:3.3`) +-- [E191] Type Error: tests/neg/i17121.scala:17:17 --------------------------------------------------------------------- +17 | type G3[X] = X match { case Consumer[Consumer[Consumer[t]]] => t } // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | The match type contains an illegal case: + | case Consumer[Consumer[Consumer[t]]] => t + | (this error can be ignored for now with `-source:3.3`) +-- [E191] Type Error: tests/neg/i17121.scala:19:17 --------------------------------------------------------------------- +19 | type G4[X] = X match { case Consumer[List[Consumer[t]]] => t } // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | The match type contains an illegal case: + | case Consumer[List[Consumer[t]]] => t + | (this error can be ignored for now with `-source:3.3`) diff --git a/tests/neg/i17121.scala b/tests/neg/i17121.scala new file mode 100644 index 000000000000..0e845cf3266d --- /dev/null +++ b/tests/neg/i17121.scala @@ -0,0 +1,20 @@ +class Consumer[-T] + +object Test: + type F1[X] = X match { case List[t] => t } // OK + summon[F1[List[?]] =:= Any] + + type F2[X] = X match { case Consumer[t] => t } // OK + summon[F2[Consumer[?]] =:= Nothing] + + type F3[X] = X match { case List[Consumer[t]] => t } // OK + summon[F3[List[Consumer[?]]] =:= Nothing] + + type G1[X] = X match { case Consumer[List[t]] => t } // error + + type G2[X] = X match { case Consumer[Consumer[t]] => t } // error + + type G3[X] = X match { case Consumer[Consumer[Consumer[t]]] => t } // error + + type G4[X] = X match { case Consumer[List[Consumer[t]]] => t } // error +end Test diff --git a/tests/neg/i17944.check b/tests/neg/i17944.check new file mode 100644 index 000000000000..80dfaac8c4c8 --- /dev/null +++ b/tests/neg/i17944.check @@ -0,0 +1,46 @@ +-- [E172] Type Error: tests/neg/i17944.scala:40:87 --------------------------------------------------------------------- +40 | val s = Selector.selectorInst[("s" ->> String) *: ("i" ->> Int) *: EmptyTuple, "i"] // error + | ^ + |No singleton value available for Tuple.Elem[test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)], (1 : Int)]; eligible singleton types for `ValueOf` synthesis include literals and stable paths. + | + |Note: a match type could not be fully reduced: + | + | trying to reduce Tuple.Elem[test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)], (1 : Int)] + | trying to reduce test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)] + | trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)] + | failed since selector (("s" : String) ->> String, ("i" : String) ->> Int) + | does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int)) + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]] + | trying to reduce test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)] + | trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)] + | failed since selector (("s" : String) ->> String, ("i" : String) ->> Int) + | does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int)) + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]] + | trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)] + | failed since selector (("s" : String) ->> String, ("i" : String) ->> Int) + | does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int)) + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]] + | trying to reduce test.FindField[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String)] + | trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)] + | failed since selector (("s" : String) ->> String, ("i" : String) ->> Int) + | does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int)) + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]] + | trying to reduce test.FindField0[(("s" : String) ->> String, ("i" : String) ->> Int), ("i" : String), (0 : Int)] + | failed since selector (("s" : String) ->> String, ("i" : String) ->> Int) + | does not match case (("i" : String) ->> f) *: _ => (f, (0 : Int)) + | and cannot be shown to be disjoint from it either. + | Therefore, reduction cannot advance to the remaining case + | + | case _ *: t => test.FindField0[t, ("i" : String), scala.compiletime.ops.int.S[(0 : Int)]] diff --git a/tests/neg/i17944.scala b/tests/neg/i17944.scala new file mode 100644 index 000000000000..214dfaebbfcf --- /dev/null +++ b/tests/neg/i17944.scala @@ -0,0 +1,44 @@ +package test { + + import types._ + + object types { + opaque type ->>[K, V] = V + extension [K <: Singleton](k: K) def ->>[V](v: V): K ->> V = v.asInstanceOf[K ->> V] + } + + type FindField[T <: Tuple, K] = FindField0[T, K, 0] + + type FindField0[T <: Tuple, K, I <: Int] <: (Any, Int) = T match { + case (K ->> f) *: _ => (f, I) + case _ *: t => FindField0[t, K, compiletime.ops.int.S[I]] + } + + trait Selector[T, Key, Out] { + def apply(t: T): Out + } + + object Selector { + inline def selectorInst[T <: Tuple, K]( + using idx: ValueOf[Tuple.Elem[FindField[T, K], 1]], + ): Selector[T, K, Tuple.Head[FindField[T, K]]] = + new Selector[T, K, Tuple.Head[FindField[T, K]]] { + def apply(t: T): Tuple.Head[FindField[T, K]] = + val i: Int = idx.value.asInstanceOf[Int] + t.productElement(i).asInstanceOf[Tuple.Head[FindField[T, K]]] + } + } + +} + +object Test { + def main(args: Array[String]): Unit = { + import test._ + import test.types._ + + val t = ("s" ->> "foo") *: ("i" ->> 3) *: EmptyTuple + val s = Selector.selectorInst[("s" ->> String) *: ("i" ->> Int) *: EmptyTuple, "i"] // error + val r = s(t) + println(r) + } +} diff --git a/tests/pos/i18488.scala b/tests/pos/i18488.scala new file mode 100644 index 000000000000..c225a2c20711 --- /dev/null +++ b/tests/pos/i18488.scala @@ -0,0 +1,15 @@ +trait AbstractTable[T] + +trait Query[E, U] + +class TableQuery[E <: AbstractTable[?]] extends Query[E, Extract[E]] + +type Extract[E] = E match + case AbstractTable[t] => t + +trait BaseCrudRepository[E[T[_]]]: + + type EntityTable <: AbstractTable[E[Option]] + + def filterById: Query[EntityTable, Extract[EntityTable]] = + new TableQuery[EntityTable] From c8b4da819b14c9c0036f71764b0431a62ee56915 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 24 Nov 2023 16:55:48 +0100 Subject: [PATCH 13/17] Under -source:3.3 and below, always use the legacy match type algorithm. This should improve consistency with the actual earlier compilers, since it means the matching algorithm will be intact. Note that the new behavior of `provablyDisjoint` is always applied, even under `-source:3.3`. This includes using `provablyDisjoint` instead of `provablyEmpty`. So it is still possible that something behaves differently than the actual earlier compilers. --- compiler/src/dotty/tools/dotc/core/Types.scala | 5 +++++ tests/neg/6570.check | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 8522fa6a0e06..7fa99e728f68 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -30,6 +30,8 @@ import Hashable.* import Uniques.* import collection.mutable import config.Config +import config.Feature.sourceVersion +import config.SourceVersion import annotation.{tailrec, constructorOnly} import scala.util.hashing.{ MurmurHash3 => hashing } import config.Printers.{core, typr, matchTypes} @@ -5117,6 +5119,9 @@ object Types extends TypeUtils { object MatchTypeCaseSpec: def analyze(cas: Type)(using Context): MatchTypeCaseSpec = cas match + case cas: HKTypeLambda if !sourceVersion.isAtLeast(SourceVersion.`3.4`) => + // Always apply the legacy algorithm under -source:3.3 and below + LegacyPatMat(cas) case cas: HKTypeLambda => val defn.MatchCase(pat, body) = cas.resultType: @unchecked val missing = checkCapturesPresent(cas, pat) diff --git a/tests/neg/6570.check b/tests/neg/6570.check index f32c3790fb90..e849814449eb 100644 --- a/tests/neg/6570.check +++ b/tests/neg/6570.check @@ -14,7 +14,7 @@ | does not uniquely determine parameter x in | case UpperBoundParametricVariant.Cov[x] => Base.N[x] | The computed bounds for the parameter are: - | x <: Int + | x >: Int | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/6570.scala:29:29 -------------------------------------------------------------- @@ -98,7 +98,7 @@ | does not uniquely determine parameter t in | case UpperBoundVariant.Cov[t] => Base.N[t] | The computed bounds for the parameter are: - | t <: Int + | t >: Int | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/6570.scala:107:29 ------------------------------------------------------------- From 2dd9f45b5a5ecce2e3ee60400089f8aa286b751c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Wed, 29 Nov 2023 10:05:02 +0100 Subject: [PATCH 14/17] In type assigner for Apply, carry ErrorType's from the `fn`. This was already done for `TypeApply` in cecfb61dba312b1e3e658fb523041b367bb19634. We apply the same logic for `Apply` nodes. --- .../dotty/tools/dotc/typer/TypeAssigner.scala | 4 ++-- .../pos/constvalue-of-failed-match-type.scala | 22 +++++++++++++++++++ 2 files changed, 24 insertions(+), 2 deletions(-) create mode 100644 tests/pos/constvalue-of-failed-match-type.scala diff --git a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala index d2b21ea9e4a8..34ac0875696a 100644 --- a/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala +++ b/compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala @@ -297,6 +297,8 @@ trait TypeAssigner { else fntpe.resultType // fast path optimization else errorType(em"wrong number of arguments at ${ctx.phase.prev} for $fntpe: ${fn.tpe}, expected: ${fntpe.paramInfos.length}, found: ${args.length}", tree.srcPos) + case err: ErrorType => + err case t => if (ctx.settings.Ydebug.value) new FatalError("").printStackTrace() errorType(err.takesNoParamsMsg(fn, ""), tree.srcPos) @@ -563,5 +565,3 @@ object TypeAssigner extends TypeAssigner: def seqLitType(tree: untpd.SeqLiteral, elemType: Type)(using Context) = tree match case tree: untpd.JavaSeqLiteral => defn.ArrayOf(elemType) case _ => if ctx.erasedTypes then defn.SeqType else defn.SeqType.appliedTo(elemType) - - diff --git a/tests/pos/constvalue-of-failed-match-type.scala b/tests/pos/constvalue-of-failed-match-type.scala new file mode 100644 index 000000000000..985e8b0c8b56 --- /dev/null +++ b/tests/pos/constvalue-of-failed-match-type.scala @@ -0,0 +1,22 @@ +import scala.compiletime.* + +object Inlines: + inline def testInline[A](): Boolean = + inline erasedValue[A] match + case _: Tuple => + constValue[Tuple.Size[A & Tuple]] == 2 + case _ => + false +end Inlines + +case class Foo2(x: Boolean, y: String) +case class Foo3(x: Boolean, y: String, z: Int) + +object Test: + def main(args: Array[String]): Unit = + // Note: the assert's don't do anything since it's a pos test; they show intent (and pass if we run the test) + assert(!Inlines.testInline[Foo2]()) + assert(!Inlines.testInline[Foo3]()) + assert(Inlines.testInline[(Boolean, String)]()) + assert(!Inlines.testInline[(Boolean, String, Int)]()) +end Test From ec097a948b5a10a0d1d150503cef4d26a8ab527a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Mon, 18 Dec 2023 17:42:53 +0100 Subject: [PATCH 15/17] Fix 1 cause of infinite recursion in the new provablyDisjoint. And add an additional test for another cause of infinite recursion that was fixed earlier. --- .../dotty/tools/dotc/core/TypeComparer.scala | 18 ++++++++++++++++-- ...rovably-disjoint-infinite-recursion-1.scala | 4 ++++ ...rovably-disjoint-infinite-recursion-2.scala | 10 ++++++++++ 3 files changed, 30 insertions(+), 2 deletions(-) create mode 100644 tests/pos/provably-disjoint-infinite-recursion-1.scala create mode 100644 tests/pos/provably-disjoint-infinite-recursion-2.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index b129445a4fdb..a8d27c6448c8 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2808,8 +2808,22 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling val optGadtBounds = gadtBounds(sym) if optGadtBounds != null then disjointnessBoundary(optGadtBounds.hi) else disjointnessBoundary(tp.superTypeNormalized) - case tp @ AppliedType(tycon: TypeRef, _) if tycon.symbol.isClass => - tp + case tp @ AppliedType(tycon: TypeRef, targs) if tycon.symbol.isClass => + /* The theory says we should just return `tp` here. However, due to how + * baseType works (called from `isBaseTypeWithDisjointArguments`), + * it can create infinitely growing towers of `AnnotatedType`s. This + * defeats the infinite recursion detection with the `pending` set. + * Therefore, we eagerly remove all non-refining annotations. We are + * allowed to do that because they don't affect subtyping (so cannot + * create an ill-kinded `AppliedType`) and would anyway be stripped + * later on by the recursive calls to `provablyDisjoint`, though + * `disjointnessBoundary`). + * See tests/pos/provably-disjoint-infinite-recursion-1.scala for an example. + */ + tp.derivedAppliedType( + tycon, + targs.mapConserve(_.stripAnnots(keep = _.symbol.derivesFrom(defn.RefiningAnnotationClass))) + ) case tp: TermRef => val isEnumValue = tp.termSymbol.isAllOf(EnumCase, butNot = JavaDefined) if isEnumValue then tp diff --git a/tests/pos/provably-disjoint-infinite-recursion-1.scala b/tests/pos/provably-disjoint-infinite-recursion-1.scala new file mode 100644 index 000000000000..a6b2e698f5e2 --- /dev/null +++ b/tests/pos/provably-disjoint-infinite-recursion-1.scala @@ -0,0 +1,4 @@ +class Test { + def isTraversableAgain(from: Iterator[Int]): Boolean = + from.isInstanceOf[Iterable[?]] +} diff --git a/tests/pos/provably-disjoint-infinite-recursion-2.scala b/tests/pos/provably-disjoint-infinite-recursion-2.scala new file mode 100644 index 000000000000..204d6bfbbcf3 --- /dev/null +++ b/tests/pos/provably-disjoint-infinite-recursion-2.scala @@ -0,0 +1,10 @@ +type Tupled[A] <: Tuple = A match + case Tuple => A & Tuple + case _ => A *: EmptyTuple + +enum Day: + case Saturday, Sunday + +type Foo = Tupled[Day] + +def foo(): Foo = Day.Saturday *: EmptyTuple 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 16/17] 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 +} From c3b9d9b92d5d2c735fbdb6d16a64ffa326f2712e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= Date: Fri, 15 Dec 2023 14:29:10 +0100 Subject: [PATCH 17/17] Add comments that link to relevant parts of the spec of SIP-56. --- .../dotty/tools/dotc/core/TypeComparer.scala | 21 +++++++++++++++---- .../src/dotty/tools/dotc/core/Types.scala | 10 +++++++++ 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 1b58dd8c1dbc..38f975a8dac8 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2771,9 +2771,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling false } || tycon.derivesFrom(defn.PairClass) - /** Are `tp1` and `tp2` provablyDisjoint types? - * - * `true` implies that we found a proof; uncertainty defaults to `false`. + /** Are `tp1` and `tp2` provablyDisjoint types, i.e., is `tp1 ⋔ tp2` true? * * Proofs rely on the following properties of Scala types: * @@ -2786,14 +2784,28 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling * Note on soundness: the correctness of match types relies on on the * property that in all possible contexts, the same match type expression * is either stuck or reduces to the same case. + * + * This method must adhere to the specification of disjointness in SIP-56: + * https://docs.scala-lang.org/sips/match-types-spec.html#disjointness + * + * The pattern matcher reachability test uses it for its own purposes, so we + * generalize it to *also* handle type variables and their GADT bounds. + * This is fine because match type reduction always operates under frozen + * GADT constraints. + * + * Other than that generalization, `provablyDisjoint` must not depart from + * the specified "provably disjoint" relation. In particular, it is not + * allowed to reply `false` instead of "I don't know". It must say `true` + * iff the spec says `true` and must say `false` iff the spec says `false`. */ def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean = provablyDisjoint(tp1, tp2, null) - def provablyDisjoint(tp1: Type, tp2: Type, pending: util.HashSet[(Type, Type)] | Null)( + private def provablyDisjoint(tp1: Type, tp2: Type, pending: util.HashSet[(Type, Type)] | Null)( using Context): Boolean = trace(i"provable disjoint $tp1, $tp2", matchTypes) { // println(s"provablyDisjoint(${tp1.show}, ${tp2.show})") + // Computes ⌈tp⌉ (see the spec), generalized to handle GADT bounds @scala.annotation.tailrec def disjointnessBoundary(tp: Type): Type = tp match case tp: TypeRef => @@ -3344,6 +3356,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) { MatchResult.Stuck end matchSubTypeTest + // See https://docs.scala-lang.org/sips/match-types-spec.html#matching def matchSpeccedPatMat(spec: MatchTypeCaseSpec.SpeccedPatMat): MatchResult = /* Concreteness checking * diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 7fa99e728f68..5e867e3eee97 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -5162,6 +5162,16 @@ object Types extends TypeUtils { foldOver(missing, tp) end CheckCapturesPresent + /** Tries to convert a match type case pattern in HKTypeLambda form into a spec'ed `MatchTypeCasePattern`. + * + * This method recovers the structure of *legal patterns* as defined in SIP-56 + * from the unstructured `HKTypeLambda` coming from the typer. + * + * It must adhere to the specification of legal patterns defined at + * https://docs.scala-lang.org/sips/match-types-spec.html#legal-patterns + * + * Returns `null` if the pattern in `caseLambda` is a not a legal pattern. + */ private def tryConvertToSpecPattern(caseLambda: HKTypeLambda, pat: Type)(using Context): MatchTypeCasePattern | Null = var typeParamRefsAccountedFor: Int = 0