Infinite type comparison when narrowing GADT bounds

[Linyxus]

Compiler version

3.0.0

Minimized code

object test {
  def foo[A, B](m: B) = {
    m match {
      case _: A =>
        m match {
          case _: B =>  // crash with -Yno-deep-subtypes
        }
    }
  }
}

Output

exception occurred while compiling examples/same-skolem.scala
Exception in thread "main" java.lang.AssertionError: assertion failed while compiling examples/same-skolem.scala
java.lang.AssertionError: assertion failed
	at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:11)
	at dotty.tools.dotc.core.TypeComparer.monitoredIsSubType$1(TypeComparer.scala:224)
	at dotty.tools.dotc.core.TypeComparer.recur(TypeComparer.scala:1288)
	at dotty.tools.dotc.core.TypeComparer.isSubType(TypeComparer.scala:186)
	at dotty.tools.dotc.core.TypeComparer.isSubType(TypeComparer.scala:196)
	at dotty.tools.dotc.core.TypeComparer.isSub(TypeComparer.scala:198)
        // many lines
	at dotty.tools.dotc.Driver.process(Driver.scala:178)
	at dotty.tools.dotc.Driver.main(Driver.scala:208)
	at dotty.tools.dotc.Main.main(Main.scala)
[error] Nonzero exit code returned from runner: 1
[error] (scala3-compiler / Compile / runMain) Nonzero exit code returned from runner: 1
[error] Total time: 4 s, completed May 14, 2021, 5:53:21 PM

Expectation

Should compile without crashing.

Cause

After the first pattern matching, the GADT bounds will become

B >: (?1 : A)

The (?1 : A) here is the SkolemType we created for pattern type in constrainSimplePatternType.

When typing the second pattern matching, the GADT bounds will become

B >: (?1 : A) | (?2 : B)

and in ConstraintHandling#addOneBound we will ask isSubType (?1 : A) | (?2 : B) <:< Any? to check the narrowed bounds. Note that when we are running the subtyping check, the GADT bounds of B have already been been updated to (?1 : A) | (?2 : B). Related trace on the infinite loop:

==> isSubType (?1 : A) | (?2 : B) <:< Any?
  ==> isSubType B <:< A?  // trying to simplify the OrType
  // ...
  <== isSubType B <:< A = false
  ==> isSubType A <:< B?
    ==> isSubType A <:< (?1 : A) | (?2 : B)?  // GADT bounds of B is used here
      ==> isSubType B <:< A?  // trying to simplify the OrType, again
      // ...
      <== isSubType B <:< A = false
      ==> isSubType A <:< B?
        ==> isSubType A <:< (?1 : A) | (?2 : B)?  // GADT bounds of B is used again
        // more lines ... infinite loop!

@abgruszecki

[abgruszecki]

We shouldn't even attempt to record any constraint here, there's no useful information ATM to extract. This is yet another problem that would be best fixed by avoiding the Skolem hack in PatternTypeConstrainer.

[Linyxus]

If it is not clear how to get rid of the Skolem hack at this point, would it be okay to workaround this issue by checking whether the bound is a Skolem with its underlying type same as the narrowed type parameter?

def isAliasSkolem: Boolean = bound match {
  case SkolemType(tp) if tp == tr => true
  case _ => false
}

if isAliasSkolem then false
else ...

[abgruszecki]

The Skolem hack is that in PatternTypeConstrainer, we wrap one of the types into a Skolem and substitute type arguments in the other type to trigger a specific codepath in TypeComparer. This is sort-of morally justified by what a Skolem type is, but it has led to a bunch of subtle issues and at this point we really should just inline the codepath instead.