Existential type does not conform to itself

[scabug]

trait Iterable[+S]
trait Box[U]

trait A {
 type T <: Iterable[S] forSome { type S <: Box[U]; type U }
}

trait B extends A {
 type T <: Iterable[S] forSome { type S <: Box[U]; type U }
}

Compilation with 2.8.0.r18050-b20090618020144 gives:

a.scala:9: error: overriding type T in trait A with bounds >: Nothing <: Iterable[_ <: Box[U]];
 type T has incompatible type
 type T <: Iterable[S] forSome { type S <: Box[U]; type U }

But according to SLS, 3.5.1 Type Equivalence:
Two existential types (�3.2.10) are equivalent if they have the same number of quantifiers, and, after renaming one list of type quantifiers by another, the quantified types as well as lower and upper bounds of corresponding quantifiers are equivalent.

So, every existential type must be equivalent to (and conform to) itself.

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-2071?orig=1
Reporter: Vladimir Reshetnikov (nikov)

[scabug]

@odersky said:
We still have to evaluate whether we will permit existentials
with cross type dependencies. My current reaction would be no.
Ticket stays open until a decision is made.

[scabug]

@paulp said:
Here is an example with fewer elements. Note that if C[T] is instead C[-T], this compiles.

class C[T]
class A {
  def f: C[S1] forSome { type S1 <: C[S2]; type S2 } = ???
  var x = f
  //  ./a.scala:4: error: type mismatch;
  // found   : C[S1(in method x_=)] where type S1(in method x_=) <: C[S2]
  // required: C[S1(in variable x)] forSome { type S1(in variable x) <: C[S2]; type S2 }
  //  var x = f
  //      ^
}

[scabug]

@adriaanm said:
I also ran into this while working on #6493.

This does not typecheck:

class Test {
  val c: x forSome { type x <: {type X <: C}; type C } = ???
}

I traced it to failing to solve the type vars in withTypeVars when multiple type vars must be related. There's a kind of backstop in existentialTransform that chases these bounds transitively, which kind of works but creates other problems. I'd like to get rid of the backstop and fix subtyping of existentials instead.

[SethTisue]

"fixed" in Scala 3 in the sense that forSome isn't supported at all

(unless someone comes forward with a forSome-less reproduction, anyway)