Skip to content

Commit

Permalink
Be more specific about higher-kinded types in provablyDisjoint.
Browse files Browse the repository at this point in the history
Previously the disjointnessBoundary of HKTypeLambda's was
implicitly their `resultType`, through the use of
`superTypeNormalized`. This was fine as long as both sides of
`provablyDisjoint` ended up being HKTypeLambda's at the same time,
but this may not always be the case (notably with any-kinded types).

It is safer to consider type lambdas as boundaries themselves, and
explicitly recurse on the result types when arities match.

This change surfaced a weird case in `TypeTestsCasts`, which called
`provablyDisjoint` with ill-kinded types. We now explicitly apply
what I suspect are partially-erased types to wildcards to recover
appropriate kinds.
  • Loading branch information
sjrd committed Aug 29, 2023
1 parent 4086ada commit f876971
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 2 deletions.
14 changes: 13 additions & 1 deletion compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2813,6 +2813,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
tp.symbol match
case cls: ClassSymbol =>
if cls == defn.SingletonClass then defn.AnyType
else if cls.typeParams.nonEmpty then EtaExpansion(tp)
else tp
case sym =>
if !ctx.erasedTypes && sym == defn.FromJavaObjectSymbol then defn.AnyType
Expand All @@ -2833,6 +2834,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
tp
case tp: ConstantType =>
tp
case tp: HKTypeLambda =>
tp
case tp: TypeProxy =>
disjointnessBoundary(tp.superTypeNormalized)
case tp: WildcardType =>
Expand All @@ -2858,6 +2861,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
case (tp1: AndType, tp2) =>
provablyDisjoint(tp1.tp1, tp2, pending) || provablyDisjoint(tp1.tp2, tp2, pending)

// Cases involving type lambdas
case (tp1: HKTypeLambda, tp2: HKTypeLambda) =>
tp1.paramNames.sizeCompare(tp2.paramNames) != 0
|| provablyDisjoint(tp1.resultType, tp2.resultType, pending)
case (tp1: HKTypeLambda, tp2) =>
!tp2.isDirectRef(defn.AnyKindClass)
case (tp1, tp2: HKTypeLambda) =>
!tp1.isDirectRef(defn.AnyKindClass)

/* 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
Expand Down Expand Up @@ -2918,7 +2930,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
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.
* This does not happen with match types, but happens when coming from the Space engine.
* In that case, we cannot prove disjointness based on type arguments.
*/
false
Expand Down
6 changes: 5 additions & 1 deletion compiler/src/dotty/tools/dotc/transform/TypeTestsCasts.scala
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,11 @@ object TypeTestsCasts {

case x =>
// always false test warnings are emitted elsewhere
TypeComparer.provablyDisjoint(x, tpe.derivedAppliedType(tycon, targs.map(_ => WildcardType)))
// provablyDisjoint wants fully applied types as input; because we're in the middle of erasure, we sometimes get raw types here
val xApplied =
val tparams = x.typeParams
if tparams.isEmpty then x else x.appliedTo(tparams.map(_ => WildcardType))
TypeComparer.provablyDisjoint(xApplied, tpe.derivedAppliedType(tycon, targs.map(_ => WildcardType)))
|| typeArgsTrivial(X, tpe)
||| i"its type arguments can't be determined from $X"
}
Expand Down

0 comments on commit f876971

Please sign in to comment.