Skip to content

Commit f4df58d

Browse files
Factor out cov. test and use it in the inv. case
1 parent e7f6049 commit f4df58d

File tree

1 file changed

+48
-44
lines changed

1 file changed

+48
-44
lines changed

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

Lines changed: 48 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -1928,7 +1928,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
19281928
}
19291929
case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
19301930
// Unboxed xs.zip(ys).zip(zs).forall { case ((a, b), c) => f(a, b, c) }
1931-
def zip_zip_forall[A, B, C](xs: List[A], ys: List[B], zs: List[C])(f: (A, B, C) => Boolean): Boolean =
1931+
def zip_zip_forall[A, B, C](xs: List[A], ys: List[B], zs: List[C])(f: (A, B, C) => Boolean): Boolean = {
19321932
xs match {
19331933
case x :: xs => ys match {
19341934
case y :: ys => zs match {
@@ -1939,52 +1939,56 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
19391939
}
19401940
case _ => true
19411941
}
1942+
}
1943+
def covariantIntersecting(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = {
1944+
intersecting(tp1, tp2) || {
1945+
// We still need to proof that `Nothing` is not a valid
1946+
// instantiation of this type parameter. We have two ways
1947+
// to get to that conclusion:
1948+
// 1. `Nothing` does not conform to the type parameter's lb
1949+
// 2. `tycon1` has a field typed with this type parameter.
1950+
//
1951+
// Because of separate compilation, the use of 2. is
1952+
// limited to case classes.
1953+
import dotty.tools.dotc.typer.Applications.productSelectorTypes
1954+
val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType
1955+
val typeUsedAsField =
1956+
productSelectorTypes(tycon1, null).exists {
1957+
case tp: TypeRef =>
1958+
(tp.designator: Any) == tparam // Bingo!
1959+
case _ =>
1960+
false
1961+
}
1962+
lowerBoundedByNothing && !typeUsedAsField
1963+
}
1964+
}
19421965

1943-
zip_zip_forall(args1, args2, tycon1.typeParams) {
1944-
(arg1, arg2, tparam) =>
1945-
val v = tparam.paramVariance
1946-
if (v > 0)
1947-
intersecting(arg1, arg2) || {
1948-
// We still need to proof that `Nothing` is not a valid
1949-
// instantiation of this type parameter. We have two ways
1950-
// to get to that conclusion:
1951-
// 1. `Nothing` does not conform to the type parameter's lb
1952-
// 2. `tycon1` has a field typed with this type parameter.
1953-
//
1954-
// Because of separate compilation, the use of 2. is
1955-
// limited to case classes.
1956-
import dotty.tools.dotc.typer.Applications.productSelectorTypes
1957-
val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType
1958-
val typeUsedAsField =
1959-
productSelectorTypes(tycon1, null).exists {
1960-
case tp: TypeRef =>
1961-
(tp.designator: Any) == tparam // Bingo!
1962-
case _ =>
1963-
false
1964-
}
1965-
lowerBoundedByNothing && !typeUsedAsField
1966-
}
1967-
else if (v < 0)
1968-
// Contravariant case: a value where this type parameter is
1969-
// instantiated to `Any` belongs to both types.
1970-
true
1971-
else
1972-
isSameType(arg1, arg2) || {
1973-
// We can only trust a "no" from `isSameType` when both
1974-
// `arg1` and `arg2` are fully instantiated.
1975-
val fullyInstantiated = new TypeAccumulator[Boolean] {
1976-
override def apply(x: Boolean, t: Type) =
1977-
x && {
1978-
t match {
1979-
case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
1980-
case _: SkolemType | _: TypeVar | _: TypeParamRef => false
1981-
case _ => foldOver(x, t)
1982-
}
1966+
zip_zip_forall(args1, args2, tycon1.typeParams) {
1967+
(arg1, arg2, tparam) =>
1968+
val v = tparam.paramVariance
1969+
if (v > 0)
1970+
covariantIntersecting(arg1, arg2, tparam)
1971+
else if (v < 0)
1972+
// Contravariant case: a value where this type parameter is
1973+
// instantiated to `Any` belongs to both types.
1974+
true
1975+
else
1976+
covariantIntersecting(arg1, arg2, tparam) && (isSameType(arg1, arg2) || {
1977+
// We can only trust a "no" from `isSameType` when both
1978+
// `arg1` and `arg2` are fully instantiated.
1979+
val fullyInstantiated = new TypeAccumulator[Boolean] {
1980+
override def apply(x: Boolean, t: Type) =
1981+
x && {
1982+
t match {
1983+
case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
1984+
case _: SkolemType | _: TypeVar | _: TypeParamRef => false
1985+
case _ => foldOver(x, t)
19831986
}
1984-
}
1985-
!(fullyInstantiated.apply(true, arg1) &&
1986-
fullyInstantiated.apply(true, arg2))
1987+
}
19871988
}
1989+
!(fullyInstantiated.apply(true, arg1) &&
1990+
fullyInstantiated.apply(true, arg2))
1991+
})
19881992
}
19891993
case (tp1: HKLambda, tp2: HKLambda) =>
19901994
intersecting(tp1.resType, tp2.resType)

0 commit comments

Comments
 (0)