diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 1e9a8c5e5816..25bf35df6829 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -336,8 +336,8 @@ trait ConstraintHandling[AbstractContext] { * L2 <: L1, and * U1 <: U2 * - * Both `c1` and `c2` are required to derive from constraint `pre`, possibly - * narrowing it with further bounds. + * Both `c1` and `c2` are required to derive from constraint `pre`, without adding + * any new type variables but possibly narrowing already registered ones with further bounds. */ protected final def subsumes(c1: Constraint, c2: Constraint, pre: Constraint)(implicit actx: AbstractContext): Boolean = if (c2 eq pre) true @@ -345,7 +345,12 @@ trait ConstraintHandling[AbstractContext] { else { val saved = constraint try - c2.forallParams(p => + // We iterate over params of `pre`, instead of `c2` as the documentation may suggest. + // As neither `c1` nor `c2` can have more params than `pre`, this only matters in one edge case. + // Constraint#forallParams only iterates over params that can be directly constrained. + // If `c2` has, compared to `pre`, instantiated a param and we iterated over params of `c2`, + // we could miss that param being instantiated to an incompatible type in `c1`. + pre.forallParams(p => c1.contains(p) && c2.upper(p).forall(c1.isLess(p, _)) && isSubTypeWhenFrozen(c1.nonParamBounds(p), c2.nonParamBounds(p))) diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala index 81b9fc5ea5c4..de07aa242c95 100644 --- a/compiler/src/dotty/tools/dotc/core/Mode.scala +++ b/compiler/src/dotty/tools/dotc/core/Mode.scala @@ -49,8 +49,11 @@ object Mode { /** We are in a pattern alternative */ val InPatternAlternative: Mode = newMode(7, "InPatternAlternative") - /** Infer GADT constraints during type comparisons `A <:< B` */ - val GADTflexible: Mode = newMode(8, "GADTflexible") + /** Make subtyping checks instead infer constraints necessarily following from given subtyping relation. + * + * This enables changing [[GadtConstraint]] and alters how [[TypeComparer]] approximates constraints. + */ + val GadtConstraintInference: Mode = newMode(8, "GadtConstraintInference") /** Assume -language:strictEquality */ val StrictEquality: Mode = newMode(9, "StrictEquality") diff --git a/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala new file mode 100644 index 000000000000..09d8a0f54462 --- /dev/null +++ b/compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala @@ -0,0 +1,208 @@ +package dotty.tools +package dotc +package core + +import Decorators._ +import Symbols._ +import Types._ +import Flags._ +import dotty.tools.dotc.reporting.trace +import config.Printers._ + +trait PatternTypeConstrainer { self: TypeComparer => + + /** Derive type and GADT constraints that necessarily follow from a pattern with the given type matching + * a scrutinee of the given type. + * + * This function breaks down scrutinee and pattern types into subcomponents between which there must be + * a subtyping relationship, and derives constraints from those relationships. We have the following situation + * in case of a (dynamic) pattern match: + * + * StaticScrutineeType PatternType + * \ / + * DynamicScrutineeType + * + * In simple cases, it must hold that `PatternType <: StaticScrutineeType`: + * + * StaticScrutineeType + * | \ + * | PatternType + * | / + * DynamicScrutineeType + * + * A good example of a situation where the above must hold is when static scrutinee type is the root of an enum, + * and the pattern is an unapply of a case class, or a case object literal (of that enum). + * + * In slightly more complex cases, we may need to upcast `StaticScrutineeType`: + * + * SharedPatternScrutineeSuperType + * / \ + * StaticScrutineeType PatternType + * \ / + * DynamicScrutineeType + * + * This may be the case if the scrutinee is a singleton type or a path-dependent type. It is also the case + * for the following definitions: + * + * trait Expr[T] + * trait IntExpr extends Expr[T] + * trait Const[T] extends Expr[T] + * + * StaticScrutineeType = Const[T] + * PatternType = IntExpr + * + * Union and intersection types are an additional complication - if either scrutinee or pattern are a union type, + * then the above relationships only need to hold for the "leaves" of the types. + * + * Finally, if pattern type contains hk-types applied to concrete types (as opposed to type variables), + * or either scrutinee or pattern type contain type member refinements, the above relationships do not need + * to hold at all. Consider (where `T1`, `T2` are unrelated traits): + * + * StaticScrutineeType = { type T <: T1 } + * PatternType = { type T <: T2 } + * + * In the above situation, DynamicScrutineeType can equal { type T = T1 & T2 }, but there is no useful relationship + * between StaticScrutineeType and PatternType (nor any of their subcomponents). Similarly: + * + * StaticScrutineeType = Option[T1] + * PatternType = Some[T2] + * + * Again, DynamicScrutineeType may equal Some[T1 & T2], and there's no useful relationship between the static + * scrutinee and pattern types. This does not apply if the pattern type is only applied to type variables, + * in which case the subtyping relationship "heals" the type. + */ + def constrainPatternType(pat: Type, scrut: Type): Boolean = trace(i"constrainPatternType($scrut, $pat)", gadts) { + + def classesMayBeCompatible: Boolean = { + import Flags._ + val patClassSym = pat.widenSingleton.classSymbol + val scrutClassSym = scrut.widenSingleton.classSymbol + !patClassSym.exists || !scrutClassSym.exists || { + if (patClassSym.is(Final)) patClassSym.derivesFrom(scrutClassSym) + else if (scrutClassSym.is(Final)) scrutClassSym.derivesFrom(patClassSym) + else if (!patClassSym.is(Flags.Trait) && !scrutClassSym.is(Flags.Trait)) + patClassSym.derivesFrom(scrutClassSym) || scrutClassSym.derivesFrom(patClassSym) + else true + } + } + + def stripRefinement(tp: Type): Type = tp match { + case tp: RefinedOrRecType => stripRefinement(tp.parent) + case tp => tp + } + + def constrainUpcasted(scrut: Type): Boolean = trace(i"constrainUpcasted($scrut)", gadts) { + val upcasted: Type = scrut match { + case scrut: TypeRef if scrut.symbol.isClass => + // we do not infer constraints following from all parents for performance reasons + // in principle however, if `A extends B, C`, then `A` can be treated as `B & C` + scrut.firstParent + case scrut @ AppliedType(tycon: TypeRef, _) if tycon.symbol.isClass => + val patClassSym = pat.classSymbol + // as above, we do not consider all parents for performance reasons + def firstParentSharedWithPat(tp: Type, tpClassSym: ClassSymbol): Symbol = { + var parents = tpClassSym.info.parents + parents match { + case first :: rest => + if (first.classSymbol == defn.ObjectClass) parents = rest + case _ => ; + } + parents match { + case first :: _ => + val firstClassSym = first.classSymbol.asClass + val res = if (patClassSym.derivesFrom(firstClassSym)) firstClassSym + else firstParentSharedWithPat(first, firstClassSym) + res + case _ => NoSymbol + } + } + val sym = firstParentSharedWithPat(tycon, tycon.symbol.asClass) + if (sym.exists) scrut.baseType(sym) else NoType + case scrut: TypeProxy => scrut.superType + case _ => NoType + } + if (upcasted.exists) + constrainSimplePatternType(pat, upcasted) || constrainUpcasted(upcasted) + else true + } + + scrut.dealias match { + case OrType(scrut1, scrut2) => + either(constrainPatternType(pat, scrut1), constrainPatternType(pat, scrut2)) + case AndType(scrut1, scrut2) => + constrainPatternType(pat, scrut1) && constrainPatternType(pat, scrut2) + case scrut: RefinedOrRecType => + constrainPatternType(pat, stripRefinement(scrut)) + case scrut => pat.dealias match { + case OrType(pat1, pat2) => + either(constrainPatternType(pat1, scrut), constrainPatternType(pat2, scrut)) + case AndType(pat1, pat2) => + constrainPatternType(pat1, scrut) && constrainPatternType(pat2, scrut) + case scrut: RefinedOrRecType => + constrainPatternType(stripRefinement(scrut), pat) + case pat => + constrainSimplePatternType(pat, scrut) || classesMayBeCompatible && constrainUpcasted(scrut) + } + } + } + + /** Constrain "simple" patterns (see `constrainPatternType`). + * + * This function attempts to modify pattern and scrutinee type s.t. the pattern must be a subtype of the scrutinee, + * or otherwise it cannot possibly match. In order to do that, we: + * + * 1. Rely on `constrainPatternType` to break the actual scrutinee/pattern types into subcomponents + * 2. Widen type parameters of scrutinee type that are not invariantly refined (see below) by the pattern type. + * 3. Wrap the pattern type in a skolem to avoid overconstraining top-level abstract types in scrutinee type + * 4. Check that `WidenedScrutineeType <: NarrowedPatternType` + * + * Importantly, note that the pattern type may contain type variables. + * + * ## Invariant refinement + * Essentially, we say that `D[B] extends C[B]` s.t. refines parameter `A` of `trait C[A]` invariantly if + * when `c: C[T]` and `c` is instance of `D`, then necessarily `c: D[T]`. This is violated if `A` is variant: + * + * trait C[+A] + * trait D[+B](val b: B) extends C[B] + * trait E extends D[Any](0) with C[String] + * + * `E` is a counter-example to the above - if `e: E`, then `e: C[String]` and `e` is instance of `D`, but + * it is false that `e: D[String]`! This is a problem if we're constraining a pattern like the below: + * + * def foo[T](c: C[T]): T = c match { + * case d: D[t] => d.b + * } + * + * It'd be unsound for us to say that `t <: T`, even though that follows from `D[t] <: C[T]`. + * Note, however, that if `D` was a final class, we *could* rely on that relationship. + * To support typical case classes, we also assume that this relationship holds for them and their parent traits. + * This is enforced by checking that classes inheriting from case classes do not extend the parent traits of those + * case classes without also appropriately extending the relevant case class + * (see `RefChecks#checkCaseClassInheritanceInvariant`). + */ + def constrainSimplePatternType(patternTp: Type, scrutineeTp: Type): Boolean = { + def refinementIsInvariant(tp: Type): Boolean = tp match { + case tp: ClassInfo => tp.cls.is(Final) || tp.cls.is(Case) + case tp: TypeProxy => refinementIsInvariant(tp.underlying) + case _ => false + } + + def widenVariantParams = new TypeMap { + def apply(tp: Type) = mapOver(tp) match { + case tp @ AppliedType(tycon, args) => + val args1 = args.zipWithConserve(tycon.typeParams)((arg, tparam) => + if (tparam.paramVariance != 0) TypeBounds.empty else arg + ) + tp.derivedAppliedType(tycon, args1) + case tp => + tp + } + } + + val widePt = if (ctx.scala2Mode || refinementIsInvariant(patternTp)) scrutineeTp else widenVariantParams(scrutineeTp) + val narrowTp = SkolemType(patternTp) + trace(i"constraining simple pattern type $narrowTp <:< $widePt", gadts, res => s"$res\ngadt = ${ctx.gadt.debugBoundsDescription}") { + isSubType(narrowTp, widePt) + } + } +} diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 83d1aadf93e9..bdeb07cf5ea2 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -25,7 +25,7 @@ object AbsentContext { /** Provides methods to compare types. */ -class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] { +class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] with PatternTypeConstrainer { import TypeComparer._ implicit def ctx(implicit nc: AbsentContext): Context = initctx @@ -141,6 +141,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] { */ private [this] var leftRoot: Type = _ + /** Are we forbidden from recording GADT constraints? + * + * This flag is set when we're already in [[Mode.GadtConstraintInference]], + * to signify that we temporarily cannot record any GADT constraints. + */ + private[this] var frozenGadt = false + protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = { val savedApprox = approx val savedLeftRoot = leftRoot @@ -840,8 +847,18 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] { gadtBoundsContain(tycon1sym, tycon2) || gadtBoundsContain(tycon2sym, tycon1) ) && - isSubType(tycon1.prefix, tycon2.prefix) && - isSubArgs(args1, args2, tp1, tparams) + isSubType(tycon1.prefix, tycon2.prefix) && { + // check both tycons to deal with the case when they are equal b/c of GADT constraint + val tyconIsInjective = tycon1sym.isClass || tycon2sym.isClass + def checkSubArgs() = isSubArgs(args1, args2, tp1, tparams) + // we only record GADT constraints if tycon is guaranteed to be injective + if (tyconIsInjective) checkSubArgs() + else { + val savedFrozenGadt = frozenGadt + frozenGadt = true + try checkSubArgs() finally frozenGadt = savedFrozenGadt + } + } if (res && touchedGADTs) GADTused = true res case _ => @@ -1227,8 +1244,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] { * @see [[sufficientEither]] for the normal case * @see [[necessaryEither]] for the GADTFlexible case */ - private def either(op1: => Boolean, op2: => Boolean): Boolean = - if (ctx.mode.is(Mode.GADTflexible)) necessaryEither(op1, op2) else sufficientEither(op1, op2) + protected def either(op1: => Boolean, op2: => Boolean): Boolean = + if (ctx.mode.is(Mode.GadtConstraintInference)) necessaryEither(op1, op2) else sufficientEither(op1, op2) /** Returns true iff the result of evaluating either `op1` or `op2` is true, * trying at the same time to keep the constraint as wide as possible. @@ -1476,7 +1493,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] { */ private def narrowGADTBounds(tr: NamedType, bound: Type, approx: ApproxState, isUpper: Boolean): Boolean = { val boundImprecise = approx.high || approx.low - ctx.mode.is(Mode.GADTflexible) && !frozenConstraint && !boundImprecise && { + ctx.mode.is(Mode.GadtConstraintInference) && !frozenGadt && !frozenConstraint && !boundImprecise && { val tparam = tr.symbol gadts.println(i"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.toString} ${bound.isRef(tparam)}") if (bound.isRef(tparam)) false diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala index c9b930b37bbb..741f022ddabe 100644 --- a/compiler/src/dotty/tools/dotc/typer/Applications.scala +++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala @@ -1085,21 +1085,6 @@ trait Applications extends Compatibility { self: Typer with Dynamic => def fromScala2x = unapplyFn.symbol.exists && (unapplyFn.symbol.owner is Scala2x) - /** Is `subtp` a subtype of `tp` or of some generalization of `tp`? - * The generalizations of a type T are the smallest set G such that - * - * - T is in G - * - If a typeref R in G represents a class or trait, R's superclass is in G. - * - If a type proxy P is not a reference to a class, P's supertype is in G - */ - def isSubTypeOfParent(subtp: Type, tp: Type)(implicit ctx: Context): Boolean = - if (constrainPatternType(subtp, tp)) true - else tp match { - case tp: TypeRef if tp.symbol.isClass => isSubTypeOfParent(subtp, tp.firstParent) - case tp: TypeProxy => isSubTypeOfParent(subtp, tp.superType) - case _ => false - } - unapplyFn.tpe.widen match { case mt: MethodType if mt.paramInfos.length == 1 => val unapplyArgType = mt.paramInfos.head @@ -1109,17 +1094,15 @@ trait Applications extends Compatibility { self: Typer with Dynamic => unapp.println(i"case 1 $unapplyArgType ${ctx.typerState.constraint}") fullyDefinedType(unapplyArgType, "pattern selector", tree.span) selType.dropAnnot(defn.UncheckedAnnot) // need to drop @unchecked. Just because the selector is @unchecked, the pattern isn't. - } else if (isSubTypeOfParent(unapplyArgType, selType)(ctx.addMode(Mode.GADTflexible))) { + } else { + // We ignore whether constraining the pattern succeeded. + // Constraining only fails if the pattern cannot possibly match, + // but useless pattern checks detect more such cases, so we simply rely on them instead. + ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(unapplyArgType, selType) val patternBound = maximizeType(unapplyArgType, tree.span, fromScala2x) if (patternBound.nonEmpty) unapplyFn = addBinders(unapplyFn, patternBound) unapp.println(i"case 2 $unapplyArgType ${ctx.typerState.constraint}") unapplyArgType - } else { - unapp.println("Neither sub nor super") - unapp.println(TypeComparer.explained(implicit ctx => unapplyArgType <:< selType)) - errorType( - ex"Pattern type $unapplyArgType is neither a subtype nor a supertype of selector type $selType", - tree.sourcePos) } val dummyArg = dummyTreeOfType(ownType) val unapplyApp = typedExpr(untpd.TypedSplice(Apply(unapplyFn, dummyArg :: Nil))) diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala index 1f697678f6ff..fbf04a1bf87c 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala +++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala @@ -180,66 +180,6 @@ object Inferencing { def isSkolemFree(tp: Type)(implicit ctx: Context): Boolean = !tp.existsPart(_.isInstanceOf[SkolemType]) - /** Derive information about a pattern type by comparing it with some variant of the - * static scrutinee type. We have the following situation in case of a (dynamic) pattern match: - * - * StaticScrutineeType PatternType - * \ / - * DynamicScrutineeType - * - * If `PatternType` is not a subtype of `StaticScrutineeType, there's no information to be gained. - * Now let's say we can prove that `PatternType <: StaticScrutineeType`. - * - * StaticScrutineeType - * | \ - * | \ - * | \ - * | PatternType - * | / - * DynamicScrutineeType - * - * What can we say about the relationship of parameter types between `PatternType` and - * `DynamicScrutineeType`? - * - * - If `DynamicScrutineeType` refines the type parameters of `StaticScrutineeType` - * in the same way as `PatternType` ("invariant refinement"), the subtype test - * `PatternType <:< StaticScrutineeType` tells us all we need to know. - * - Otherwise, if variant refinement is a possibility we can only make predictions - * about invariant parameters of `StaticScrutineeType`. Hence we do a subtype test - * where `PatternType <: widenVariantParams(StaticScrutineeType)`, where `widenVariantParams` - * replaces all type argument of variant parameters with empty bounds. - * - * Invariant refinement can be assumed if `PatternType`'s class(es) are final or - * case classes (because of `RefChecks#checkCaseClassInheritanceInvariant`). - */ - def constrainPatternType(tp: Type, pt: Type)(implicit ctx: Context): Boolean = { - def refinementIsInvariant(tp: Type): Boolean = tp match { - case tp: ClassInfo => tp.cls.is(Final) || tp.cls.is(Case) - case tp: TypeProxy => refinementIsInvariant(tp.underlying) - case tp: AndType => refinementIsInvariant(tp.tp1) && refinementIsInvariant(tp.tp2) - case tp: OrType => refinementIsInvariant(tp.tp1) && refinementIsInvariant(tp.tp2) - case _ => false - } - - def widenVariantParams = new TypeMap { - def apply(tp: Type) = mapOver(tp) match { - case tp @ AppliedType(tycon, args) => - val args1 = args.zipWithConserve(tycon.typeParams)((arg, tparam) => - if (tparam.paramVariance != 0) TypeBounds.empty else arg - ) - tp.derivedAppliedType(tycon, args1) - case tp => - tp - } - } - - val widePt = if (ctx.scala2Mode || refinementIsInvariant(tp)) pt else widenVariantParams(pt) - val narrowTp = SkolemType(tp) - trace(i"constraining pattern type $narrowTp <:< $widePt", gadts, res => s"$res\n${ctx.gadt.debugBoundsDescription}") { - narrowTp <:< widePt - } - } - /** The list of uninstantiated type variables bound by some prefix of type `T` which * occur in at least one formal parameter type of a prefix application. * Considered prefixes are: diff --git a/compiler/src/dotty/tools/dotc/typer/Inliner.scala b/compiler/src/dotty/tools/dotc/typer/Inliner.scala index 8f15fee80625..616a490a956c 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inliner.scala +++ b/compiler/src/dotty/tools/dotc/typer/Inliner.scala @@ -916,7 +916,7 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(implicit ctx: Context) { } if (!isImplicit) caseBindingMap += ((NoSymbol, scrutineeBinding)) - val gadtCtx = ctx.fresh.setFreshGADTBounds.addMode(Mode.GADTflexible) + val gadtCtx = ctx.fresh.setFreshGADTBounds.addMode(Mode.GadtConstraintInference) if (reducePattern(caseBindingMap, scrutineeSym.termRef, cdef.pat)(gadtCtx)) { val (caseBindings, from, to) = substBindings(caseBindingMap.toList, mutable.ListBuffer(), Nil, Nil) val guardOK = cdef.guard.isEmpty || { diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 52b315025376..aa4a1cea0304 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -607,7 +607,7 @@ class Typer extends Namer def handlePattern: Tree = { val tpt1 = typedTpt if (!ctx.isAfterTyper && pt != defn.ImplicitScrutineeTypeRef) - constrainPatternType(tpt1.tpe, pt)(ctx.addMode(Mode.GADTflexible)) + ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(tpt1.tpe, pt) // special case for an abstract type that comes with a class tag tryWithClassTag(ascription(tpt1, isWildcard = true), pt) } @@ -3153,7 +3153,7 @@ class Typer extends Namer case _: RefTree | _: Literal if !isVarPattern(tree) && !(pt <:< tree.tpe) && - !(tree.tpe <:< pt)(ctx.addMode(Mode.GADTflexible)) => + !ctx.addMode(Mode.GadtConstraintInference).typeComparer.constrainPatternType(tree.tpe, pt) => val cmp = untpd.Apply( untpd.Select(untpd.TypedSplice(tree), nme.EQ), diff --git a/tests/neg/gadt-alias-injectivity.scala b/tests/neg/gadt-alias-injectivity.scala new file mode 100644 index 000000000000..34203a45f4f8 --- /dev/null +++ b/tests/neg/gadt-alias-injectivity.scala @@ -0,0 +1,48 @@ +object Test { + enum EQ[A, B] { + case Refl[T]() extends EQ[T, T] + } + import EQ._ + + object A { + type Foo[+X] = (X, X) + def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match { + case Refl() => x + } + } + + object B { + type Foo[X] = (X, X) + def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match { + case Refl() => x + } + } + + object C { + type Foo[+X] = Int | (X, X) + def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match { + case Refl() => x + } + } + + object D { + type Foo[+X] = (Int, Int) + def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match { + case Refl() => x // error + } + } + + trait E { + type Foo[+X] <: Int | (X, X) + def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match { + case Refl() => x // error + } + } + + trait F { + type Foo[X] >: Int | (X, X) + def foo[X, Y](x: X, eq: EQ[Foo[X], Foo[Y]]): Y = eq match { + case Refl() => x // error + } + } +} diff --git a/tests/neg/gadt-uninjectivity.scala b/tests/neg/gadt-uninjectivity.scala index f1d0fc59000a..30ebac32b735 100644 --- a/tests/neg/gadt-uninjectivity.scala +++ b/tests/neg/gadt-uninjectivity.scala @@ -4,7 +4,7 @@ object uninjectivity { def absurd1[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match { case Refl() => - x // should be an error + x // error } def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fi: F[Int], fs: F[String]): G[Int] = eq match { diff --git a/tests/neg/nontrivial-intersection-gadt.scala b/tests/neg/nontrivial-intersection-gadt.scala new file mode 100644 index 000000000000..c8d5aa9975cb --- /dev/null +++ b/tests/neg/nontrivial-intersection-gadt.scala @@ -0,0 +1,22 @@ +object Test { + trait Expr[+T] + trait IntExpr extends Expr[Int] + class Const[+T] extends Expr[T] + final class Fin + + def foo1[T](x: Unit | Const[T]): T = x match { + case _: IntExpr => 0 // error + } + + def bar1[T](x: Const[T]): T = x match { + case _: (Unit | IntExpr) => 0 // error + } + + def foo2[T](x: Fin | Const[T]): T = x match { + case _: IntExpr => 0 // error + } + + def bar2[T](x: Const[T]): T = x match { + case _: (Fin | IntExpr) => 0 // error + } +} diff --git a/tests/neg/overconstrained-abstract-type-gadt.scala b/tests/neg/overconstrained-abstract-type-gadt.scala new file mode 100644 index 000000000000..1d8b08f243d9 --- /dev/null +++ b/tests/neg/overconstrained-abstract-type-gadt.scala @@ -0,0 +1,14 @@ +trait Test { + type A + + enum Foo[X, Y] { + case StrStr() extends Foo[String, String] + case IntInt() extends Foo[Int, Int] + } + + def foo[T, U](f: Foo[A, T] | Foo[String, U]): Unit = + f match { case Foo.StrStr() => + val t: T = "" // error + val u: U = "" // error + } +} diff --git a/tests/neg/overconstrained-type-variables-gadt.scala b/tests/neg/overconstrained-type-variables-gadt.scala new file mode 100644 index 000000000000..b8670f28e76b --- /dev/null +++ b/tests/neg/overconstrained-type-variables-gadt.scala @@ -0,0 +1,27 @@ +object Test { + trait T1[A] { def a: A } + trait T2[B] { def b: B } + + def foo[X, Y](v: T1[X] | T2[Y]): X = v match { + case t1: T1[t] => + // consider: foo[Int, String](new T1[String] with T2[String] { ... }) + t1.a // error + } + + class T1Int extends T1[Int] { def a = 0 } + def bar[X, Y](v: T1[X] | T2[Y]): X = v match { + case t1: T1Int => + // similar reasoning to above applies + t1.a // error + } + + class T1IntT2String extends T1[Int] with T2[String] { + def a = 0 + def b = "" + } + def baz[X](v: T1[X] | T2[X]): Unit = v match { + case _: T1IntT2String => + val x1: X = 0 // error + val x2: X = "" // error + } +} diff --git a/tests/neg/structural-gadt.scala b/tests/neg/structural-gadt.scala new file mode 100644 index 000000000000..9a14881b5804 --- /dev/null +++ b/tests/neg/structural-gadt.scala @@ -0,0 +1,56 @@ +// This file is part of tests for inferring GADT constraints from type members, +// which needed to be reverted because of soundness issues. +// +// Lines with "// limitation" are the ones that we could soundly allow. +object Test { + + trait Expr { type T } + trait IntLit extends Expr { type T <: Int } + trait IntExpr extends Expr { type T = Int } + + def foo[A](e: Expr { type T = A }) = e match { + case _: IntLit => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: Expr { type T <: Int } => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + + case _: Expr { type T = Int } => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + } + + def bar[A](e: Expr { type T <: A }) = e match { + case _: IntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: Expr { type T <: Int } => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: Expr { type T = Int } => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } + + trait IndirectExprOfIntList extends Expr { + type T = U + type U <: List[Int] + } + def baz[A](e: Expr { type T <: List[A] }) = e match { + case _: IndirectExprOfIntList => + val a: A = 0 // error + val i: Int = ??? : A // error + } +} diff --git a/tests/neg/structural-recursive-both1-gadt.scala b/tests/neg/structural-recursive-both1-gadt.scala new file mode 100644 index 000000000000..97df59a92bb5 --- /dev/null +++ b/tests/neg/structural-recursive-both1-gadt.scala @@ -0,0 +1,93 @@ +// This file is part of tests for inferring GADT constraints from type members, +// which needed to be reverted because of soundness issues. +// +// Lines with "// limitation" are the ones that we could soundly allow. +object Test { + + trait Expr { type T } + trait IntLit extends Expr { type T <: Int } + trait IntExpr extends Expr { type T = Int } + + type ExprSub[+A] = Expr { type T <: A } + type ExprExact[A] = Expr { type T = A } + + trait IndirectIntLit extends Expr { type S <: Int; type T = S } + trait IndirectIntExpr extends Expr { type S = Int; type T = S } + + type IndirectExprSub[+A] = Expr { type S <: A; type T = S } + type IndirectExprSub2[A] = Expr { type S = A; type T <: S } + type IndirectExprExact[A] = Expr { type S = A; type T = S } + + trait AltIndirectIntLit extends Expr { type U <: Int; type T = U } + trait AltIndirectIntExpr extends Expr { type U = Int; type T = U } + + type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U } + type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U } + type AltIndirectExprExact[A] = Expr { type U = A; type T = U } + + def foo[A](e: IndirectExprExact[A]) = e match { + case _: AltIndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: AltIndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: AltIndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: AltIndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + + case _: AltIndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + } + + def bar[A](e: IndirectExprSub[A]) = e match { + case _: AltIndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: AltIndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: AltIndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: AltIndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: AltIndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } + + def baz[A](e: IndirectExprSub2[A]) = e match { + case _: AltIndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: AltIndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: AltIndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: AltIndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: AltIndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } +} diff --git a/tests/neg/structural-recursive-both2-gadt.scala b/tests/neg/structural-recursive-both2-gadt.scala new file mode 100644 index 000000000000..b58e05f3ed43 --- /dev/null +++ b/tests/neg/structural-recursive-both2-gadt.scala @@ -0,0 +1,93 @@ +// This file is part of tests for inferring GADT constraints from type members, +// which needed to be reverted because of soundness issues. +// +// Lines with "// limitation" are the ones that we could soundly allow. +object Test { + + trait Expr { type T } + trait IntLit extends Expr { type T <: Int } + trait IntExpr extends Expr { type T = Int } + + type ExprSub[+A] = Expr { type T <: A } + type ExprExact[A] = Expr { type T = A } + + trait IndirectIntLit extends Expr { type S <: Int; type T = S } + trait IndirectIntExpr extends Expr { type S = Int; type T = S } + + type IndirectExprSub[+A] = Expr { type S <: A; type T = S } + type IndirectExprSub2[A] = Expr { type S = A; type T <: S } + type IndirectExprExact[A] = Expr { type S = A; type T = S } + + trait AltIndirectIntLit extends Expr { type U <: Int; type T = U } + trait AltIndirectIntExpr extends Expr { type U = Int; type T = U } + + type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U } + type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U } + type AltIndirectExprExact[A] = Expr { type U = A; type T = U } + + def foo[A](e: AltIndirectExprExact[A]) = e match { + case _: IndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + + case _: IndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + } + + def bar[A](e: AltIndirectExprSub[A]) = e match { + case _: IndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: IndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } + + def baz[A](e: AltIndirectExprSub2[A]) = e match { + case _: IndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: IndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } +} diff --git a/tests/neg/structural-recursive-pattern-gadt.scala b/tests/neg/structural-recursive-pattern-gadt.scala new file mode 100644 index 000000000000..ea7394b5b66b --- /dev/null +++ b/tests/neg/structural-recursive-pattern-gadt.scala @@ -0,0 +1,71 @@ +// This file is part of tests for inferring GADT constraints from type members, +// which needed to be reverted because of soundness issues. +// +// Lines with "// limitation" are the ones that we could soundly allow. +object Test { + + trait Expr { type T } + trait IntLit extends Expr { type T <: Int } + trait IntExpr extends Expr { type T = Int } + + type ExprSub[+A] = Expr { type T <: A } + type ExprExact[A] = Expr { type T = A } + + trait IndirectIntLit extends Expr { type S <: Int; type T = S } + trait IndirectIntExpr extends Expr { type S = Int; type T = S } + + type IndirectExprSub[+A] = Expr { type S <: A; type T = S } + type IndirectExprSub2[A] = Expr { type S = A; type T <: S } + type IndirectExprExact[A] = Expr { type S = A; type T = S } + + trait AltIndirectIntLit extends Expr { type U <: Int; type T = U } + trait AltIndirectIntExpr extends Expr { type U = Int; type T = U } + + type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U } + type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U } + type AltIndirectExprExact[A] = Expr { type U = A; type T = U } + + def foo[A](e: ExprExact[A]) = e match { + case _: IndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + + case _: IndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + } + + def bar[A](e: ExprSub[A]) = e match { + case _: IndirectIntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectExprSub2[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IndirectIntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: IndirectExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } +} diff --git a/tests/neg/structural-recursive-scrutinee-gadt.scala b/tests/neg/structural-recursive-scrutinee-gadt.scala new file mode 100644 index 000000000000..cd4e2376f49a --- /dev/null +++ b/tests/neg/structural-recursive-scrutinee-gadt.scala @@ -0,0 +1,81 @@ +// This file is part of tests for inferring GADT constraints from type members, +// which needed to be reverted because of soundness issues. +// +// Lines with "// limitation" are the ones that we could soundly allow. +object Test { + + trait Expr { type T } + trait IntLit extends Expr { type T <: Int } + trait IntExpr extends Expr { type T = Int } + + type ExprSub[+A] = Expr { type T <: A } + type ExprExact[A] = Expr { type T = A } + + trait IndirectIntLit extends Expr { type S <: Int; type T = S } + trait IndirectIntExpr extends Expr { type S = Int; type T = S } + + type IndirectExprSub[+A] = Expr { type S <: A; type T = S } + type IndirectExprSub2[A] = Expr { type S = A; type T <: S } + type IndirectExprExact[A] = Expr { type S = A; type T = S } + + trait AltIndirectIntLit extends Expr { type U <: Int; type T = U } + trait AltIndirectIntExpr extends Expr { type U = Int; type T = U } + + type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U } + type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U } + type AltIndirectExprExact[A] = Expr { type U = A; type T = U } + + def foo[A](e: IndirectExprExact[A]) = e match { + case _: IntLit => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: ExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // limitation // error + + case _: IntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + + case _: ExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // limitation // error + } + + def bar[A](e: IndirectExprSub[A]) = e match { + case _: IntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: ExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: ExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } + + def baz[A](e: IndirectExprSub2[A]) = e match { + case _: IntLit => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: ExprSub[Int] => + val a: A = 0 // error + val i: Int = ??? : A // error + + case _: IntExpr => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + + case _: ExprExact[Int] => + val a: A = 0 // limitation // error + val i: Int = ??? : A // error + } +} diff --git a/tests/neg/unsound-covariant-gadt.scala b/tests/neg/unsound-covariant-gadt.scala new file mode 100644 index 000000000000..e8dcb14a5eee --- /dev/null +++ b/tests/neg/unsound-covariant-gadt.scala @@ -0,0 +1,10 @@ +object Test { + sealed trait Expr[+T] + case class IntVal[+T <: Int]() extends Expr[T] + case object ActualInt extends Expr[Int] + def eval[T](e: Expr[T]): T = e match { + case IntVal() => 0 // error + case ActualInt => 0 + } +} + diff --git a/tests/neg/unsound-union-gadt.scala b/tests/neg/unsound-union-gadt.scala new file mode 100644 index 000000000000..9412f1581e1a --- /dev/null +++ b/tests/neg/unsound-union-gadt.scala @@ -0,0 +1,13 @@ +object Test { + enum Expr[+T] { + case StrLit() extends Expr[String] + case IntLit() extends Expr[Int] + } + import Expr._ + + def foo[T](e: Expr[T]) = e match { + case _: (StrLit | IntLit) => + val str: T = "" // error + val int: T = 42 // error + } +} diff --git a/tests/neg/unsound-union-object-gadt.scala b/tests/neg/unsound-union-object-gadt.scala new file mode 100644 index 000000000000..81b55e7dc493 --- /dev/null +++ b/tests/neg/unsound-union-object-gadt.scala @@ -0,0 +1,20 @@ +object Test { + enum Foo[X] { + case Str extends Foo[String] + case Int extends Foo[Int] + } + + trait Test { + type A + + def foo[T](f: Foo[A] | Foo[T]): T = + f match { case Foo.Str => + "" // error + } + + def bar[T](f: Unit | Foo[T]): T = + f match { case Foo.Str => + "" + } + } +} diff --git a/tests/patmat/3469.scala b/tests/patmat/3469.scala deleted file mode 100644 index 8abad0252d11..000000000000 --- a/tests/patmat/3469.scala +++ /dev/null @@ -1,9 +0,0 @@ -object O { - sealed trait Trait[+A] { type T } - case class CaseClass[+A](a: A) extends Trait[A] { type T = Nothing } - - def id[TT, A](v: Trait[A] { type T = TT }): Trait[A] { type T = TT } = - v match { - case CaseClass(a) => CaseClass(a) - } -} \ No newline at end of file diff --git a/tests/pos/gadt-EQK.scala b/tests/pos/gadt-EQK.scala index b713de2d833b..0c1fbfe03f81 100644 --- a/tests/pos/gadt-EQK.scala +++ b/tests/pos/gadt-EQK.scala @@ -18,16 +18,4 @@ object EQK { fa : G[Int] } } - - def m2[F[_], G[_], A](fa: F[A], a: A, eq: EQ[F[A], G[Int]], eqk: EQK[F, G]): Int = - eqk match { - case ReflK() => eq match { - case Refl() => - val r1: F[Int] = fa - val r2: G[A] = fa - val r3: F[Int] = r2 - a - } - } - } diff --git a/tests/pos/nontrivial-intersection-gadt.scala b/tests/pos/nontrivial-intersection-gadt.scala new file mode 100644 index 000000000000..92862080f9ce --- /dev/null +++ b/tests/pos/nontrivial-intersection-gadt.scala @@ -0,0 +1,22 @@ +object Test { + trait Expr[T] + trait IntExpr extends Expr[Int] + class Const[T] extends Expr[T] + final class Fin + + def foo1[T](x: Unit | Const[T]): T = x match { + case _: IntExpr => 0 + } + + def bar1[T](x: Const[T]): T = x match { + case _: (Unit | IntExpr) => 0 + } + + def foo2[T](x: Fin | Const[T]): T = x match { + case _: IntExpr => 0 + } + + def bar2[T](x: Const[T]): T = x match { + case _: (Fin | IntExpr) => 0 + } +} diff --git a/tests/pos/precise-pattern-type.scala b/tests/pos/precise-pattern-type.scala index 856672fafbf2..e8c64f019313 100644 --- a/tests/pos/precise-pattern-type.scala +++ b/tests/pos/precise-pattern-type.scala @@ -13,4 +13,20 @@ object `precise-pattern-type` { case Select(q) => q.tpe.isType } + + trait O { + type ThisTree <: Tree[Type] + val tree: ThisTree + def test = tree match { + case Select(q) => q.tpe.isType + case tree1: Select[t] => (tree1 : Select[Type]).qual.tpe.isType + } + } + + trait OO { + type ThisTree[T >: Null] <: Tree[T] + def foo(t: ThisTree[Type]) = t match { + case Select(q) => q.tpe.isType + } + } } diff --git a/tests/pos/pseudo-thistype-constraints.scala b/tests/pos/pseudo-thistype-constraints.scala new file mode 100644 index 000000000000..8bdb123847b2 --- /dev/null +++ b/tests/pos/pseudo-thistype-constraints.scala @@ -0,0 +1,12 @@ +object Test { + enum Expr[+T] { + case BoolLit(b: Boolean) extends Expr[Boolean] + def eval: T = { + def go[TT](self: this.type & Expr[TT]): TT = self match { + case BoolLit(b) => b + } + + go(this) + } + } +} diff --git a/tests/run/gadt-injectivity-unsoundness.scala b/tests/run/gadt-injectivity-unsoundness.scala deleted file mode 100644 index 192a82afb539..000000000000 --- a/tests/run/gadt-injectivity-unsoundness.scala +++ /dev/null @@ -1,19 +0,0 @@ -object Test { - sealed trait EQ[A, B] - final case class Refl[T]() extends EQ[T, T] - - def absurd[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match { - case Refl() => x - } - - var ex: Exception = _ - try { - type Unsoundness[X] = Int - val s: String = absurd[Unsoundness, Int, String](Refl(), 0) - } catch { - case e: ClassCastException => ex = e - } - - def main(args: Array[String]) = - assert(ex != null) -}