Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve handling of AndTypes on the LHS of subtype comparisons #18235

Merged
merged 6 commits into from
Jul 19, 2023
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 34 additions & 11 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -478,7 +478,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
tp2.isRef(AnyClass, skipRefined = false)
|| !tp1.evaluating && recur(tp1.ref, tp2)
case AndType(tp11, tp12) =>
if (tp11.stripTypeVar eq tp12.stripTypeVar) recur(tp11, tp2)
if tp11.stripTypeVar eq tp12.stripTypeVar then recur(tp11, tp2)
else thirdTry
case tp1 @ OrType(tp11, tp12) =>
compareAtoms(tp1, tp2) match
Expand Down Expand Up @@ -898,21 +898,43 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling

canWidenAbstract && acc(true, tp)

def tryBaseType(cls2: Symbol) = {
val base = nonExprBaseType(tp1, cls2).boxedIfTypeParam(tp1.typeSymbol)
def tryBaseType(cls2: Symbol) =

def computeBase(tp1: Type): Type = tp1.widenDealias match
case tp @ AndType(tp11, tp12) =>
// We have to treat AndTypes specially, since the normal treatment
// of `(T1 & T2).baseType(C)` combines the base types of T1 and T2 via glb
// which drops any types that don't exist. That forgets possible solutions.
// For instance, in i18266.scala, we get to a subgoal `R & Row[Int] <: Row[String]`
// where R is an uninstantiated type variable. The base type computation
// of the LHS drops the non-existing base type of R and results in
// `Row[Int]`, which leads to a subtype failure since `Row[Int] <: Row[String]`
// does not hold. The new strategy is to declare that the base type computation
// failed since R does not have a base type, and to proceed to fourthTry instead,
// where we try both sides of an AndType individually.
val b1 = computeBase(tp11)
val b2 = computeBase(tp12)
if b1.exists && b2.exists then tp.derivedAndType(b1, b2) else NoType
case _ =>
nonExprBaseType(tp1, cls2).boxedIfTypeParam(tp1.typeSymbol)

val base = computeBase(tp1)
if base.exists && (base ne tp1)
&& (!caseLambda.exists
|| widenAbstractOKFor(tp2)
|| tp1.widen.underlyingClassRef(refinementOK = true).exists)
then
isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow)
&& recordGadtUsageIf { MatchType.thatReducesUsingGadt(tp1) }
|| base.isInstanceOf[OrType] && fourthTry
// if base is a disjunction, this might have come from a tp1 type that
|| base.isInstanceOf[AndOrType] && fourthTry
// If base is a disjunction, this might have come from a tp1 type that
// expands to a match type. In this case, we should try to reduce the type
// and compare the redux. This is done in fourthTry
// If base is a conjunction, it could be that one of the original
// branches of the AndType tp1 conforms to tp2, but its base type does
// not. So we need to also fall back to fourthTry. Test case is i18226a.scala.
else fourthTry
}
end tryBaseType

def fourthTry: Boolean = tp1 match {
case tp1: TypeRef =>
Expand Down Expand Up @@ -989,7 +1011,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
}
}
compareHKLambda
case AndType(tp11, tp12) =>
case tp1 @ AndType(tp11, tp12) =>
val tp2a = tp2.dealiasKeepRefiningAnnots
if (tp2a ne tp2) // Follow the alias; this might avoid truncating the search space in the either below
return recur(tp1, tp2a)
Expand All @@ -1009,8 +1031,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
return recur(AndType(tp11, tp121), tp2) && recur(AndType(tp11, tp122), tp2)
case _ =>
}
val tp1norm = simplifyAndTypeWithFallback(tp11, tp12, tp1)
if (tp1 ne tp1norm) recur(tp1norm, tp2)
val tp1norm = trySimplify(tp1)
if tp1 ne tp1norm then recur(tp1norm, tp2)
else either(recur(tp11, tp2), recur(tp12, tp2))
case tp1: MatchType =>
def compareMatch = tp2 match {
Expand Down Expand Up @@ -2506,8 +2528,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
final def andType(tp1: Type, tp2: Type, isErased: Boolean = ctx.erasedTypes): Type =
andTypeGen(tp1, tp2, AndType.balanced(_, _), isErased = isErased)

final def simplifyAndTypeWithFallback(tp1: Type, tp2: Type, fallback: Type): Type =
andTypeGen(tp1, tp2, (_, _) => fallback)
/** Try to simplify AndType, or return the type itself if no simplifiying opportunities exist. */
private def trySimplify(tp: AndType): Type =
andTypeGen(tp.tp1, tp.tp2, (_, _) => tp)

/** Form a normalized conjunction of two types.
* Note: For certain types, `|` is distributed inside the type. This holds for
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/allow-deep-subtypes/i5877.scala
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ object Main {
assert(implicitly[thatSelf.type <:< that.This] != null)
}
val that: HasThisType[_] = Foo() // null.asInstanceOf
testSelf(that) // error
testSelf(that) // error: recursion limit exceeded
}


Expand All @@ -36,7 +36,7 @@ object Main {
}
val that: HasThisType[_] = Foo() // null.asInstanceOf
// this line of code makes Dotty compiler infinite recursion (stopped only by overflow) - comment it to make it compilable again
testSelf(that) // error
testSelf(that) // error: recursion limit exceeded
}

// ---- ---- ---- ----
Expand Down
7 changes: 7 additions & 0 deletions tests/pos/i12077.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
trait Wrapper[K]
trait Has0[T]

def test[R](v: Wrapper[Has0[String] with R]):R = ???

val zz:Wrapper[Has0[String] with Has0[Int]] = ???
val _ = test(zz)
11 changes: 11 additions & 0 deletions tests/pos/i18226.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
trait F[-R]

trait Row[A]

def eliminateInt[R](f: F[R & Row[Int]]): F[R] = new F[R] {}

val x = new F[Row[Int] & Row[String]] {}

val _ = eliminateInt[Row[String]](x) // compiles OK when given explicit type
val y = eliminateInt(x) // was error
val _: F[Row[String]] = y
19 changes: 19 additions & 0 deletions tests/pos/i18226a.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
class Has[A]
trait Foo

class TestAspect[+LowerR, -UpperR]

class Spec[-R] {
def foo[R1 <: R](aspect: TestAspect[R1, R1]): Unit = {}
}

class SuiteBuilder[R <: Has[_]] {
def toSpec(
spec: Spec[R & Has[Foo]],
aspect: TestAspect[
R & Has[Foo],
R & Has[Foo]
]
) =
spec.foo(aspect)
}