Leaking SelectionProto in GADT casts for implicit conversions

[Linyxus]

Compiler version

main branch

Minimized code

enum SUB[-A, +B]:
  case Refl[S]() extends SUB[S, S]

class Pow(self: Int):
  def **(other: Int): Int = math.pow(self, other).toInt

given fromList[T]: Conversion[List[T], Pow] = ???

given fromInt: Conversion[Int, Pow] = Pow(_)

def foo[T](t: T, ev: T SUB List[Int]) =
  ev match { case SUB.Refl() =>
    t ** 2   // error
  }

def baz[T](t: T, ev: T SUB Int) =
  ev match { case SUB.Refl() =>
    t ** 2   // works
  }

Output

-- [E008] Not Found Error: issues/selection-proto-gadt-cast.scala:13:6 -----------------------------------------------------------------------------------------------------------------------------------
13 |    t ** 2   // error
   |    ^^^^
   |    value ** is not a member of ?{ ** : ? }

Expectation

Both foo and bar should compile.

In the two functions of this example we are trying to cast t: T to Pow implicitly, where T is constrained to be a subtype of List[Int] and Int respectively. We could use the conversion fromList and fromInt based on the GADT bounds.

The reason of the error in foo is that we leak the SelectionProto type in the GADT cast for the implicit conversion instance which shadows the real type of the instance. Specifically, the typed tree of foo looks like:

def foo[T >: Nothing <: Any](t: T, ev: SUB[T, List[Int]]): <error value ** is not a member of ?{ ** : ? }> = 
  ev match 
    {
      case SUB.Refl.unapply[S$1 @ S$1]():SUB.Refl[S$1] => 
        fromList[Any].$asInstanceOf[Conversion[(t : T), ?{ ** : ? }]].apply(t).**(2)
    }

Here we look for a implicit conversion of expected type Conversion[(t : T), ?{ ** : ? }] with a SelectionProto in it, and the SelectionProto gets leaked in the GADT cast, shadowing the real type of the conversion instance.

Note that the SelectionProto also leaks in bar, the typed tree of which is:

def baz[T >: Nothing <: Any](t: T, ev: SUB[T, Int]): Int = 
  ev match 
    {
      case SUB.Refl.unapply[Int]():SUB.Refl[Int] => 
        fromInt.$asInstanceOf[(fromInt : Conversion[Int, Pow]) & Conversion[Int, Pow] & Conversion[(t : T), ?{ ** : ? }]].apply(t.$asInstanceOf[(t : T) & Int]).**(2)
    }

As seen in it, bar works because the conversion instance from Int to Pow is a stable path fromInt, causing the typer to include its identity and GADT bounds in the cast.

[ckipp01]

Note that trying this out on the latest nightly the compiler actually crashes:

     while compiling: <no file>
        during phase: <no phase>
                mode: Mode(ImplicitsEnabled)
     library version: version 2.13.10
    compiler version: version 3.3.1-RC1-bin-20230523-3923a7d-NIGHTLY-git-3923a7d
            settings: -bootclasspath /Users/ckipp/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala3-library_3/3.3.1-RC1-bin-20230523-3923a7d-NIGHTLY/scala3-library_3-3.3.1-RC1-bin-20230523-3923a7d-NIGHTLY.jar:/Users/ckipp/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.10/scala-library-2.13.10.jar -classpath /Users/ckipp/Documents/scratch-workspace/backlog-battle/.scala-build/.bloop/project_ae9d8f64de/bloop-internal-classes/main-QGi2sxNZS3a-KdJ2D2Gnhw==:/Users/ckipp/Documents/scratch-workspace/backlog-battle/.scala-build/.bloop/project_ae9d8f64de/bloop-internal-classes/main-ZiMjW-2zTHaL_2RHVqTa_g== -d /Users/ckipp/Documents/scratch-workspace/backlog-battle/.scala-build/.bloop/project_ae9d8f64de/bloop-internal-classes/main-QGi2sxNZS3a-KdJ2D2Gnhw== -java-output-version 17 -sourceroot /Users/ckipp/Documents/scratch-workspace/backlog-battle

                tree: EmptyTree
       tree position: :<unknown>
           tree type: <notype>
              symbol: val <none>
           call site: package <root> in module class <root>

  == Source file context for tree position ==


Error compiling project (Scala 3.3.1-RC1-bin-20230523-3923a7d-NIGHTLY, JVM)
Error: Unexpected error when compiling project_ae9d8f64de: 'assertion failed'
Compilation failed

[dwijnand]

If an exception is throwing while compiling no file during no phase, does it make a noise? 🤔

[SethTisue]

Note that the SelectionProto also leaks in bar

One would hope that -Ycheck would catch that, but we tried and it doesn't.

[SethTisue]

note that the problem reproduces with fromInt if you add a dummy type parameter to it (changing it from a val to a def):

enum Sub[A, B]:
  case Refl[S]() extends Sub[S, S]
class Pow:
  def meth = ???
given fromInt[Dummy]: Conversion[Int, Pow] = ???
def foo[T](t: T, ev: Sub[T, Int]) =
  ev match
    case Sub.Refl() =>
      t.meth

(Dale doubts it's interestingly more minimal that way, but perhaps it's worth noting regardless — it helped my understanding.)

[SethTisue]

If an exception is throwing while compiling no file during no phase, does it make a noise?

We began by investigating why the enriched crash report is missing so much information. Dale was able to fix it, and that fix will be its own PR, separate from the actual GADT issue.