Skip to content

Commit

Permalink
Fix provablyDisjoint handling of HK types
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
dwijnand committed Dec 7, 2023
1 parent e167c64 commit 3e37592
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 4 deletions.
8 changes: 4 additions & 4 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2841,8 +2841,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
val cls1 = tp1.classSymbol
val cls2 = tp2.classSymbol
def isDecomposable(tp: Symbol): Boolean =
tp.is(Sealed) && !tp.hasAnonymousChild
def isDecomposable(sym: Symbol, tp: Type): Boolean =
tp.hasSimpleKind && sym.is(Sealed) && !sym.hasAnonymousChild
def decompose(sym: Symbol, tp: Type): List[Type] =
sym.children.map(x => refineUsingParent(tp, x)).filter(_.exists)
if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1))
Expand All @@ -2857,13 +2857,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
// subtype, so they must be unrelated by single inheritance
// of classes.
true
else if (isDecomposable(cls1))
else if (isDecomposable(cls1, tp1))
// At this point, !cls1.derivesFrom(cls2): we know that direct
// instantiations of `cls1` (terms of the form `new cls1`) are not
// of type `tp2`. Therefore, we can safely decompose `cls1` using
// `.children`, even if `cls1` is non abstract.
decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2))
else if (isDecomposable(cls2))
else if (isDecomposable(cls2, tp2))
decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1))
else
false
Expand Down
12 changes: 12 additions & 0 deletions tests/pos/i19031.ci-reg1.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
//> using options -Werror

sealed trait Mark[T]

trait Foo[T]
class Bar1[T] extends Foo[T]
class Bar2[T] extends Foo[T] with Mark[T]

class Test:
def t1(foo: Foo[Int]): Unit = foo match
case _: Mark[t] =>
case _ =>

0 comments on commit 3e37592

Please sign in to comment.