From a1067ebe8689462d5971dbacb31e33d3c55222b6 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Wed, 20 May 2020 16:15:26 +0200 Subject: [PATCH 1/2] Disallow recursive lower bounds in constraints These can lead to deep subtype errors, this also fixes #8976 but see also the next commit which fixes the underlying soundness issue. --- .../src/dotty/tools/dotc/core/ConstraintHandling.scala | 4 ++++ tests/neg/i8976.scala | 5 +++++ tests/neg/recursive-lower-constraint.scala | 7 +++++++ 3 files changed, 16 insertions(+) create mode 100644 tests/neg/i8976.scala create mode 100644 tests/neg/recursive-lower-constraint.scala diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 47414593d781..07000214c410 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -87,6 +87,10 @@ trait ConstraintHandling[AbstractContext] { protected def addOneBound(param: TypeParamRef, bound: Type, isUpper: Boolean)(using AbstractContext): Boolean = if !constraint.contains(param) then true + else if !isUpper && param.occursIn(bound) + // We don't allow recursive lower bounds when defining a type, + // so we shouldn't allow them as constraints either. + false else val oldBounds @ TypeBounds(lo, hi) = constraint.nonParamBounds(param) val equalBounds = (if isUpper then lo else hi) eq bound diff --git a/tests/neg/i8976.scala b/tests/neg/i8976.scala new file mode 100644 index 000000000000..d2b803b53205 --- /dev/null +++ b/tests/neg/i8976.scala @@ -0,0 +1,5 @@ +trait Cons[X, Y] + +def solve[X, Y](using Cons[X, Y] =:= Cons[1, Cons[2, Y]]) = () + +@main def main = solve // error diff --git a/tests/neg/recursive-lower-constraint.scala b/tests/neg/recursive-lower-constraint.scala new file mode 100644 index 000000000000..8009ab5fce6e --- /dev/null +++ b/tests/neg/recursive-lower-constraint.scala @@ -0,0 +1,7 @@ +class Foo[F <: Foo[F]] +class Bar extends Foo[Bar] + +class A { + def foo[T <: Foo[T], U >: Foo[T] <: T](x: T): T = x + foo(new Bar) // error +} From 9ac5a5bb7db17feccd584cf493f3ff52827e1336 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Wed, 20 May 2020 16:19:19 +0200 Subject: [PATCH 2/2] Fix unsound type variable instantiation with recursive bounds `approximation` used to replace recursive occurences of the type variable being instantiated by `TypeBounds.empty`, but this is not sound in general since the approximation might be outside the bounds of the type variable. We could try to do something fancy with ApproximatingTypeMap but it seems complicated (and expensive) and there's an easier solution: since last commit, only the upper bound is allowed to be recursive, so we can just instantiate the type variable to its lower bound to avoid the problem in a sound and cheap way. --- .../tools/dotc/core/ConstraintHandling.scala | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 07000214c410..1c575b1c5f68 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -242,25 +242,20 @@ trait ConstraintHandling[AbstractContext] { /** Solve constraint set for given type parameter `param`. * If `fromBelow` is true the parameter is approximated by its lower bound, - * otherwise it is approximated by its upper bound. However, any occurrences - * of the parameter in a refinement somewhere in the bound are removed. Also - * wildcard types in bounds are approximated by their upper or lower bounds. + * otherwise it is approximated by its upper bound, unless the upper bound + * contains a reference to the parameter itself (`addOneBound` ensures that + * such reference never occur in the lower bound). + * Wildcard types in bounds are approximated by their upper or lower bounds. * (Such occurrences can arise for F-bounded types). * The constraint is left unchanged. * @return the instantiating type * @pre `param` is in the constraint's domain. */ final def approximation(param: TypeParamRef, fromBelow: Boolean)(implicit actx: AbstractContext): Type = { - val avoidParam = new TypeMap { + val replaceWildcards = new TypeMap { override def stopAtStatic = true - def avoidInArg(arg: Type): Type = - if (param.occursIn(arg)) TypeBounds.empty else arg def apply(tp: Type) = mapOver { tp match { - case tp @ AppliedType(tycon, args) => - tp.derivedAppliedType(tycon, args.mapConserve(avoidInArg)) - case tp: RefinedType if param occursIn tp.refinedInfo => - tp.parent case tp: WildcardType => val bounds = tp.optBounds.orElse(TypeBounds.empty).bounds // Try to instantiate the wildcard to a type that is known to conform to it. @@ -287,9 +282,10 @@ trait ConstraintHandling[AbstractContext] { } } constraint.entry(param) match { - case _: TypeBounds => - val bound = if (fromBelow) fullLowerBound(param) else fullUpperBound(param) - val inst = avoidParam(bound) + case entry: TypeBounds => + val useLowerBound = fromBelow || param.occursIn(entry.hi) + val bound = if (useLowerBound) fullLowerBound(param) else fullUpperBound(param) + val inst = replaceWildcards(bound) typr.println(s"approx ${param.show}, from below = $fromBelow, bound = ${bound.show}, inst = ${inst.show}") inst case inst =>