From 1a8575e81081847de253056d103b41719b09ab09 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] SIP-56-extended: Simpler provablyDisjoint test. --- .../dotty/tools/dotc/core/TypeComparer.scala | 358 ++++++++++++------ 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 | 31 +- 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/i15677.scala | 2 + tests/pos/mytest.scala | 16 + 15 files changed, 418 insertions(+), 141 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%) create mode 100644 tests/pos/mytest.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index a9438ac8561f..cb9a10c64966 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2813,6 +2813,171 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling case _ => false }) + @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 => + if isEnumValue(tp) 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 + // Cases where either is an intersection or union + case (tp1: OrType, tp2) => + provablyDisjoint(tp1.tp1, tp2) && provablyDisjoint(tp1.tp2, tp2) + case (tp1, tp2: OrType) => + provablyDisjoint(tp1, tp2.tp1) && provablyDisjoint(tp1, tp2.tp2) + case (tp1: AndType, tp2) => + provablyDisjoint(tp1.tp1, tp2) || provablyDisjoint(tp1.tp2, tp2) + case (tp1, tp2: AndType) => + provablyDisjoint(tp1, tp2.tp1) || provablyDisjoint(tp1, tp2.tp2) + + /* 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.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 (tp1, tp2) => + val cls1 = tp1.classSymbol.asClass + val cls2 = tp2.classSymbol.asClass + + def isBaseTypeWithDisjointArguments(baseClass: ClassSymbol): 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) + 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 comming from the Space engine. + * In that case, we cannot prove disjointness based on type arguments. + */ + false + 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. + * Moreover, we have to do this to prevent infinite recursion with curiously-recursive + * superclasses: for example `class Seq[A] extends SeqOps[A, Seq[A]]`. + */ + 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)) + commonBaseClasses.exists { baseClass => + !isAncestorOfOtherBaseClass(baseClass) && isBaseTypeWithDisjointArguments(baseClass) + } + 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 + } + + 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).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])(using Context): Boolean = def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] { override def apply(x: Boolean, t: Type) = x && { @@ -2824,129 +2989,82 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling } }.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.SingletonClass => - false - case (_, tp2: TypeRef) if tp2.symbol == defn.SingletonClass => - false - 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 - def isDecomposable(tp: Symbol): Boolean = - tp.is(Sealed) && !tp.hasAnonymousChild - def decompose(sym: Symbol, tp: Type): List[Type] = - sym.children.map(x => refineUsingParent(tp, x)).filter(_.exists) - if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)) + // 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): Boolean = + provablyDisjoint(tp1, tp2) + + // 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): 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(cls.typeParams).exists { + (arg1, arg2, tparam) => + val v = typeParamVarianceStatusForDisjointness(cls, tparam) + if (v.is(Covariant)) + covariantDisjoint(arg1, arg2) + else if (v.is(Contravariant)) 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)) - else - 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. - true - case (_, _: HKLambda) => - 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 _ => - false + invariantDisjoint(arg1, arg2) } - } + end provablyDisjointTypeArgs + + /** The "variance status" of the given type parameter for the purpose of deciding disjointness. + * + * The variance status of a type parameter is its variance if it is "usable for deciding disjointness", + * and `Contravariant` otherwise. + * + * - `Contravariant` means that it is not usable. + * - `Covariant` means that it is usable and requires type arguments to be provably disjoint. + * - `Invariant` means that it is usable and requires type arguments be either a) provably disjoint + * or b) not equivalent and fully defined. + * + * A contravariant type parameter is never usable for deciding disjointness. + * We can always instantiate them to their upper bound to find a common type. + * + * An invariant type parameter is usable if its bounds do not depend on the prefix. + * + * A covariant type parameter is usable if its bounds do not depend on the prefix *and* + * it corresponds to a field. + * (Type parameter disjointness is not enough by itself as it could lead to + * incorrect conclusions for phantom type parameters.) + */ + private def typeParamVarianceStatusForDisjointness(cls: ClassSymbol, tparam: TypeSymbol)(using Context): Variance = + // Should this be cached in `tparam` or its denotation? + + if tparam.is(Contravariant) then + Contravariant + else + val boundsDependOnPrefix = new TypeAccumulator[Boolean] { + override def apply(x: Boolean, t: Type): Boolean = + x || (t match { + case t: ThisType => true + case _ => foldOver(false, t) + }) + }.apply(false, tparam.info) + + if boundsDependOnPrefix then + Contravariant + else if tparam.is(Covariant) && !typeparamCorrespondsToField(cls.appliedRef, tparam) then + Contravariant + else + tparam.variance + end typeParamVarianceStatusForDisjointness protected def explainingTypeComparer = ExplainingTypeComparer(comparerContext) 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..ce24ed6e890b 100644 --- a/tests/neg/6314.scala +++ b/tests/neg/6314.scala @@ -1,20 +1,39 @@ -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] { type Bar[A] = A match { 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/i15677.scala index 2ad2b5283057..66941d6e1e72 100644 --- a/tests/pos/i15677.scala +++ b/tests/pos/i15677.scala @@ -1,3 +1,5 @@ +// scalac: -Yno-deep-subtypes:false + class Inv[A] class Foo[B, M[_]] diff --git a/tests/pos/mytest.scala b/tests/pos/mytest.scala new file mode 100644 index 000000000000..70ad19b95785 --- /dev/null +++ b/tests/pos/mytest.scala @@ -0,0 +1,16 @@ +class Parent[T](val x: T) + +class Child[T](x: T) extends Parent(x) + +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[Parent[Any]] =:= Int] + + summon[MT[Child[Int]] =:= Int] + summon[MT[Child[Boolean]] =:= Boolean] +end test