Infinite type comparison when narrowing GADT bounds

Linyxus commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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.

scala / scala3