Skip to content

Commit a260a54

Browse files
committed
Fix provablyDisjoint handling of HK types
If refineUsingParent/instantiateToSubType is passed a HK to2 then it's not possible to instantiate a class to that type (at the moment and perhaps ever). So it's important we guard against that. This came up while trying to see if Mark[?] and Foo[Int] (from pos/i19031.ci-reg1.scala) are provably disjoint - which they should be reported not to be. Because they're not applied types of the same type constructor we end up trying to prove that HK type Mark is disjoint from HK type Foo. Because we don't know how to instantiate Foo's subclasses (e.g Bar2) such that it's a subtype of higher-kinded type "Mark", we end up discarding all of Foo's subclasses, which implies that Foo & Mark is uninhabited, thus they are provably disjoint - which is incorrect. We originally didn't encounter this because we eagerly decomposed in Space intersection, while now we've dispatched it to provablyDisjoint.
1 parent 24b70e5 commit a260a54

File tree

2 files changed

+16
-4
lines changed

2 files changed

+16
-4
lines changed

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2841,8 +2841,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28412841
case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
28422842
val cls1 = tp1.classSymbol
28432843
val cls2 = tp2.classSymbol
2844-
def isDecomposable(tp: Symbol): Boolean =
2845-
tp.is(Sealed) && !tp.hasAnonymousChild
2844+
def isDecomposable(sym: Symbol, tp: Type): Boolean =
2845+
tp.hasSimpleKind && sym.is(Sealed) && !sym.hasAnonymousChild
28462846
def decompose(sym: Symbol, tp: Type): List[Type] =
28472847
sym.children.map(x => refineUsingParent(tp, x)).filter(_.exists)
28482848
if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1))
@@ -2857,13 +2857,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28572857
// subtype, so they must be unrelated by single inheritance
28582858
// of classes.
28592859
true
2860-
else if (isDecomposable(cls1))
2860+
else if (isDecomposable(cls1, tp1))
28612861
// At this point, !cls1.derivesFrom(cls2): we know that direct
28622862
// instantiations of `cls1` (terms of the form `new cls1`) are not
28632863
// of type `tp2`. Therefore, we can safely decompose `cls1` using
28642864
// `.children`, even if `cls1` is non abstract.
28652865
decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2))
2866-
else if (isDecomposable(cls2))
2866+
else if (isDecomposable(cls2, tp2))
28672867
decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1))
28682868
else
28692869
false

tests/pos/i19031.ci-reg1.scala

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
//> using options -Werror
2+
3+
sealed trait Mark[T]
4+
5+
trait Foo[T]
6+
class Bar1[T] extends Foo[T]
7+
class Bar2[T] extends Foo[T] with Mark[T]
8+
9+
class Test:
10+
def t1(foo: Foo[Int]): Unit = foo match
11+
case _: Mark[t] =>
12+
case _ =>

0 commit comments

Comments
 (0)