Description
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.