forSome scope introduction conflates distinct types

[scabug]

The following should not compile; outerd cannot prove that there exists one E that unifies the left.S and right.S, but introduces one anyway. We use that to throw a ClassCastException.

package forsomescope

trait Magic {
  type S
  def init: S
  def step(s: S): String
}

case class Pair[A](left: A, right: A)

object Main extends App {
  type Aux[A] = Magic {type S = A}

  // These method types are equivalent in meaning; they both mean the
  // left and right of the pair have the same 'S'.
  def a[A](p: Pair[Aux[A]]): String = b(p)
  def b(p: Pair[Aux[E]] forSome {type E}): String = a(p)

  // I can't call this one from outerd,
  def outertp[A](p: Pair[Aux[A]]) =
    p.right.step(p.left.init)

  // but I can call this one.
  def outere(p: Pair[Aux[E]] forSome {type E}) =
    outertp(p)

  // This one means the left and the right may have *different* S.  I
  // shouldn't be able to call outere with p.
  def outerd(p: Pair[Magic]) =
    outere(p)

  def boom =
    outerd(Pair(new Magic {
                  type S = String
                  def init = "hi"
                  def step(s: S) = s.reverse
                },
                new Magic {
                  type S = Int
                  def init = 42
                  def step(s: S) = (s - 3).toString
                }))

  boom
}

(scastie here) throws

java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
	at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:101)
	at forsomescope.Main$$anon$2.step(test.scala:42)
	at forsomescope.Main$.outertp(test.scala:25)
	at forsomescope.Main$.outere(test.scala:29)
	at forsomescope.Main$.outerd(test.scala:34)
	at forsomescope.Main$.boom(test.scala:37)
	at forsomescope.Main$.delayedEndpoint$forsomescope$Main$1(test.scala:48)

On the other hand, if outerd directly calls the morally equivalent outertp (scastie here), we correctly get an error:

/tmp/rendererWlqSMa9Oi9/src/main/scala/test.scala:28: type mismatch;
 found   : forsomescope.Pair[forsomescope.Magic]
 required: forsomescope.Pair[forsomescope.Main.Aux[this.S]]
    (which expands to)  forsomescope.Pair[forsomescope.Magic{type S = this.S}]
Note: forsomescope.Magic >: forsomescope.Main.Aux[this.S], but class Pair is invariant in type A.
You may wish to define A as -A instead. (SLS 4.5)
    outertp(p)
            ^

Although, a better error would be more like when you do

import java.util.{ List => JList }
 
def doit[A](xs: JList[JList[A]]) = 42
 
def brokeit(xs: JList[JList[_]]) = doit(xs)

Which appropriately fails to compile (scastie here):

/tmp/rendererWlqSMa9Oi9/src/main/scala/test.scala:11: no type parameters for method doit: (xs: java.util.List[java.util.List[A]])Int exist so that it can be applied to arguments (java.util.List[java.util.List[_]])
 --- because ---
argument expression's type is not compatible with formal parameter type;
 found   : java.util.List[java.util.List[_]]
 required: java.util.List[java.util.List[?A]]
Note: java.util.List[_] >: java.util.List[?A], but Java-defined trait List is invariant in type E.
You may wish to investigate a wildcard type such as `_ >: java.util.List[?A]`. (SLS 3.2.10)
  def brokeit(xs: JList[JList[_]]) = doit(xs)
                                     ^

Original discovery context here.

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-9410?orig=1
Reporter: Stephen Compall (s11001001)
Affected Versions: 2.10.5, 2.11.7, 2.12.0-M2