Superfluous asInstanceOf breaking singleton types

[Ang9876]

Compiler version

Scala compiler version 3.0.0-M3

Minimized code

This code is inspired by tests/pos/i4345.scala.

import scala.annotation.tailrec
class Context {
  type Tree
}

final def loop3[C <: Context](): Unit =
  @tailrec
  def loop4[A <: C](c: A): c.Tree = loop4(c)

Output

-- [E007] Type Mismatch Error: test.scala:19:41 --------------------------------
19 |  def loop4[A <: C](c: A): c.Tree = loop4(c)
   |                                    ^^^^^^^^
   |                              Found:    ?1.Tree
   |                              Required: c.Tree
   |
   |                              where:    ?1 is an unknown value of type A
1 error found

Result after typer

result of test.scala after typer:
package <empty> {
  import scala.annotation.tailrec
  class Context() extends Object() {
    type Tree >: Nothing <: Any
  }
  final lazy module val test$package: test$package$ = new test$package$()
  final module class test$package$() extends Object() {
    this: test$package.type =>
    final def loop3[C >: Nothing <: Context](): Unit =
      {
        @annotation.tailrec() def loop4[A >: Nothing <: C](c: A): c.Tree =
          loop4[A](c.$asInstanceOf$[A])
        ()
      }
  }
}

Expectation

This code should be compiled but not. c is converted to c.$asInstanceOf$[A] in method adapt when the compiler testSubType (c:A) and A. testSubType returns OKwithGADTused, but GADT usage in thirdTryNamed is unnecessary.

https://github.com/lampepfl/dotty/blob/a3b7ed601061e3a309fa23f09a740b7759c61bf6/compiler/src/dotty/tools/dotc/typer/Typer.scala#L3418

[smarter]

testSubType returns OKwithGADTused, but GADTusage in thirdTryNamed is unnecessary.

Indeed, if I comment out the usage of compareGADT in thirdTryNamed the problem goes away, because we end up in fourhTry running isSubType(hi1, tp2, approx.addLow) which succeeds without looking at GADT bounds. Could we move the compareGADT in thirdTryNamed to fourthTry instead, thereby keeping more of the GADT logic in one place and making sure it's only used as a fallback (so we don't set GADTused = true when we don't have to) ? I have no idea because I haven't looked at this code in a long time, so I'll defer to @abgruszecki :).

[abgruszecki]

@Ang9876 thanks for opening the issue! Could you also upload the traces that you've shown me to Github Gist or something similar? They will be very useful for solving the issue.

@smarter I already took a look at this code in more detail (thanks to @Ang9876's traces). IIRC, it indeed looked like what needed to be changed was the place in which we looked up GADT constraints, because we looked at them before looking at the "normal" bounds (where normal == not refined by GADTs).

[LPTK]

It seems wrong that GADT lookup would break singleton types in any case. So am I guessing correctly that pushing the problem into fourthTry will not definitively solve the bug?

I've also had Found: ?1.Tree; Required: c.Tree-style errors in the past, though I haven't minimized them, but I suspect they had the same source. And it was likely in genuine GADT code.

[abgruszecki]

The problem is that when we conclude that a subtype check succeeded by looking up GADT constraints, we add a type ascription to, I guess, satisfy the JVM. In this particular case, we look up GADTs too early, and using GADTs we conclude something we could've concluded w/o using them. So it seems to me that checking GADTs "later" should be considered a "definitive" solution.

[LPTK]

@abgruszecki But what happens when the GADT reasoning is needed, and the singleton type is also needed? For instance, imagine if we were calling some method foo requiring a (c: B) where we know by GADTs that A <:< B, but we still don't want to widen the argument to that call to B through asInstanceOf, as foo may still depend on using c in a path.

[abgruszecki]

Ah, right, it's this case you're talking about. I think what could work is to instead cast to singleton type, and then in the backend emit a JVM cast to the type we originally applied to .asInstanceOf. We should keep that issue in mind when fixing this.

[Ang9876]

These are the traces for two similar test cases. I am not sure whether they are useful now.
I am not very clear why a cast is needed and how JVM works for this case.
error.txt
succeed.txt