Skip to content

Commit cb8888c

Browse files
committed
infer: Compare variances in tvar instantiate check
1 parent 11ef0de commit cb8888c

File tree

2 files changed

+31
-6
lines changed

2 files changed

+31
-6
lines changed

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -409,15 +409,17 @@ object Inferencing {
409409
Stats.record("maximizeType")
410410
val vs = variances(tp)
411411
val patternBindings = new mutable.ListBuffer[(Symbol, TypeParamRef)]
412-
val gadtBounds = ctx.gadt.symbols.map(ctx.gadt.bounds(_).nn)
412+
val gadtVariances = ctx.gadt.symbols.map(sym => variances(ctx.gadt.bounds(sym).nn))
413413
vs foreachBinding { (tvar, v) =>
414414
if !tvar.isInstantiated then
415415
// if the tvar is covariant/contravariant (v == 1/-1, respectively) in the input type tp
416-
// then check the tvar doesn't occur in the opposite GADT bound (lower/upper) within any of the GADT bounds
417-
// if it doesn't occur then it's safe to instantiate the tvar
418-
// Eg neg/i14983 the C in Node[+C] is in the GADT lower bound X >: List[C] so maximising to Node[Any] is unsound
419-
// Eg pos/precise-pattern-type the T in Tree[-T] is in no GADT upper bound so can maximise to Tree[Type]
420-
val safeToInstantiate = v != 0 && gadtBounds.forall(tb => !tvar.occursIn(if v == 1 then tb.lo else tb.hi))
416+
// then it is safe to instantiate if it has the same variance within the GADT bounds.
417+
// Eg neg/i14983 the C in Node[+C] differs in variance to the GADT bound X >: List[C] so maximising to Node[Any] is unsound
418+
// Eg pos/precise-pattern-type the T in Tree[-T] is in no GADT bound so can maximise to Tree[Type]
419+
val safeToInstantiate = v != 0 && gadtVariances.forall { vmap =>
420+
val v2 = vmap(tvar)
421+
v2 == null || v2 == v
422+
}
421423
if safeToInstantiate then tvar.instantiate(fromBelow = v == -1)
422424
else {
423425
val bounds = TypeComparer.fullBounds(tvar.origin)

tests/neg/i14983.co-contra.scala

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
case class Showing[-C](show: C => String)
2+
3+
sealed trait Tree[+A]
4+
final case class Leaf[+B](b: B) extends Tree[B]
5+
final case class Node[-C](l: Showing[C]) extends Tree[Showing[C]]
6+
7+
object Test:
8+
def meth[X](tree: Tree[X]): X = tree match
9+
case Leaf(v) => v
10+
case Node(x) =>
11+
// tree: Tree[X] vs Node[C] aka Tree[Showing[C]]
12+
// PTC: X >: Showing[C]
13+
// max: Node[C] to Node[Nothing], instantiating C := Nothing, which makes X >: Showing[Nothing]
14+
// adapt: Showing[String] <: X = OKwithGADTUsed; insert GADT cast asInstanceOf[X]
15+
Showing[String](_ + " boom!") // error: Found: Showing[String] Required: X where: X is a type in method meth with bounds >: Showing[C$1]
16+
// after fix:
17+
// max: Node[C] => Node[C$1], instantiating C := C$1, a new symbol, so X >: Showing[C$1]
18+
// adapt: Showing[String] <: X = Fail, because String !<: C$1
19+
20+
def main(args: Array[String]): Unit =
21+
val tree = Node(Showing[Int](_.toString))
22+
val res = meth(tree)
23+
println(res.show(42)) // was: ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String

0 commit comments

Comments
 (0)