the protected[this] variance escape hatch is unsound

[scabug]

trait A[+X] {
  protected[this] def f(x: X): X = x
}

trait B extends A[B] {
  def kaboom = f(new B {})
}

// protected[this] disables variance checking
// of the signature of `f`.
//
// C's parent list unifies A[B] with A[C]
//
// The protected[this] loophole is widely used
// in the collections, every newBuilder method
// would fail variance checking otherwise.
class C extends B with A[C] {
  override protected[this] def f(c: C) = c
}

// java.lang.ClassCastException: B$$anon$1 cannot be cast to C
//  at C.f(<console>:15)
new C().kaboom

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-7093?orig=1
Reporter: @retronym
Affected Versions: 2.9.2, 2.10.0

[scabug]

@retronym said (edited on Feb 6, 2013 10:22:20 PM UTC):
I should note that we prevent direct inheritance from A[B] and A[C] in Typers:

scala> class C extends A[B] with A[C]
<console>:10: error: trait A is inherited twice
       class C extends A[B] with A[C]
                       ^

          if (parents exists (p => p != parent && p.tpe.typeSymbol == psym && !psym.isError))
            pending += ParentInheritedTwiceError(parent, psym)

The checks up the transitive parents come later on, in RefChecks:

scala> class C extends B with A[String]
<console>:9: error: illegal inheritance;
 class C inherits different type instances of trait A:
A[String] and A[B]
       class C extends B with A[String]
             ^

[scabug]

@Blaisorblade said:
One could argue that the problem lies in the refinement with A[C]:

class C extends B with A[C]

That's the same feature that interacts with type refinement for covariant GADTs.

[scabug]

@odersky said (edited on Sep 25, 2014 2:12:06 PM UTC):
If I apply the straightforward encoding into member types, this is what I get:

  trait A {
    type X
    protected[this] def f(x: X): X = x
  }

  trait B extends A {
    type X <: B
    def kaboom = f(new B {})
  }

This code does not typecheck - kaboom is ill typed. Interestingly, The dotc compiler does not use the straightforward encoding, but instead would type B as follows:

  trait B extends A {
    type X =+ B
    def kaboom = f(new B {})
  }

The "=+" is not available in user code, and has no foundation in DOT. It means in effect something like "covariant alias binding". With this change, the code compiles, and exhibits the same unsoundness hole.

Now, as far as I know variant aliases is the most significant deviation of dotc from DOT. It is telling that this deviation leads directly to an unsoundness hole. Why did I add variant aliases? Because, without them, the collections library could not be ingested.

So, this points to three possible ways forward, which should be investigated further.

1. Get rid of -=, +=, but keep covariant protected[this]. We will not be able to read collections as they are then. We might lose too much expressiveness that way, this remains to be checked out.

2. Get rid of protected[this]. Plaster lots of @uncheckedVariance annotations over collections to make them work. This is the least invasive change, but it casts in stone the variant alias concept and with it the difference between generics and member types.

3. Declare the rebinding differently:

  trait B extends A {
    type T = B
    def kaboom = f(new B {})
  }

This would then invalidate the definition of C. I believe this is what Paolo was proposing to also fix the GADT problem.
Again, we'd have to check what we lose in expressiveness by doing this.

[scabug]

@Blaisorblade said:
In 3, what's T? Do you mean type X = B? If so, it makes sense; I proposed to have this as an option, because sometimes allowing C and making the hierarchy less GADT-like makes sense.
I'm missing some details, but it's not clear why there's no answer with unchecked Variance and without variant aliases. Gotta look at newBuilder.

[scabug]

@odersky said (edited on Sep 25, 2014 4:33:50 PM UTC):
Yes, T should have been X. How would you express optionality?

  trait B extends A[B]   -->    trait B { type X = B }
  trait B extends A[+B]  -->    trait B { type X <: B }

maybe?

[scabug]

@odersky said:
Another option could be

  trait B extends A[_ <: B]

[scabug]

@odersky said:
In fact,

trait B extends A[_ <: B]

is legal Scala and expands to exactly what we need in dotty. So, no need for new syntax.

[scabug]

@Blaisorblade said:
I'm happy this works in Dotty (didn't check), but it doesn't seem to be valid Scala according to Scalac 2.11.2:

scala> trait B extends A[_ <: B]
<console>:20: error: illegal cyclic reference involving trait B
       trait B extends A[_ <: B]
                         ^
<console>:20: error: class type required but A[_ <: B] found
       trait B extends A[_ <: B]
                       ^

Gotta think more on other points.

[scabug]

@Blaisorblade said:

Get rid of -=, +=, but keep covariant protected[this]. We will not be able to read collections as they are then.

What's the problem with collections? The text above mentions protected[this]. Then, they also do things like defining C, all the time, for refining the arguments of *Like traits — and I guess also other code does it. The text seems assume even more — what is it? I'd expect that with the "straightforward encoding into member types", you can't actually call newBuilder (or Builder methods) without casts.

[scabug]

@retronym said:
I take it that Martin meant that it is legal Scala syntax, rather than legal Scala 2.x code (parents must be class types, existentials aren't allowed). Under Dotty's treatment type parameters, the desired semantics seem to emerge naturally.

[scabug]

@Blaisorblade said (edited on Sep 25, 2014 11:25:06 PM UTC):
Ah, OK! It's about not changing the parser.

Still, I'm under the impression that defining C should probably be allowed by default, so this wouldn't work:

trait B extends A[B]       -->    trait B { type X = B }
trait B extends A[_ <: B]  -->    trait B { type X <: B } //or trait B { type X = _ <: B }, which seems the same

even though it's nicer

and we'd need something like this:

trait B extends A[=B]      -->    trait B { type X = B }
trait B extends A[B]       -->    trait B { type X <: B }

(Not enthusiast about the = syntax, but I am sure that picking some syntax is easier than getting soundness).

[scabug]

@Blaisorblade said:
Let's see if I understand this from the DOT point-of-view. I'll refer to "semantic subtyping": A <:s B, which simply means that at runtime any instance of A is also an instance of B. I am not sure on how to interpret variant aliases semantically. I advocate thinking in this terms to clarify the situation.

Let's analyze again this code. See the comments.

trait B extends A[B] {
  def kaboom = f(new B {})
  //Scalac seems to "believe" that X = B, in particular that B <: X, but B <:s X is false if we allow defining C. However, B <: X is only used for calling protected[this] methods: we can't refer to X explicitly. However, protected[this] isn't the root of the problem.
  //Do variant aliases force Scala to believe that B <: X, and still allow defining C? If so, they seem unsound themselves.
}

Does this understanding make sense?

[scabug]

@odersky said (edited on Sep 26, 2014 9:57:08 AM UTC):
@retronym Yes, the A[_ <: B] seems to be natural for Dotty. For current Scala, the existential interpretation gets in the way.

Problem with collections: Indeed, collections use the F-bounded pattern systematically and pervasively. E.g.

  class List[T] extends .... LinearSeqOptimized[T, List[T]]

But these recursive occurrences are covariant. So a translation to

   class List[T] extends .... LinearSeqOptimized[T, _ <: List[T]]

looks feasible (although I have not tried it).

[scabug]

@odersky said:
@Blaisorblade protected[this] is an important ingredient of the unsoundness scenario because it lets us write functions like f which have contravaraint occurrences of covariant parameters. Without it, I cannot come up with a crash scenario.

Indeed covariant aliases have the same problems as parameters when combined with protected[this]. It would be nice if we could get rid of them. And the "split encoding" idea of treating some superclass bindings as aliases and others as approximations looks the most promising so far to me.

[scabug]

@Blaisorblade said:

@paolo protected[this] is an important ingredient of the unsoundness scenario because it lets us write functions like f which have contravaraint occurrences of covariant parameters. Without it, I cannot come up with a crash scenario.

Sure, I just mean that from this POV the crash is the symptom, not the root cause.
Without covariant aliases, the whole "variance checking" business becomes a matter of "user experience"/convenience, not of soundness. Take again the encoding without covariant aliases, but without protected[this] (because it was removed in the original code):

trait A {
  type X
  def f(x: X): X = x //We can totally accept this, even if it would violate variance checking!
}
 
trait B extends A {
  type X <: B
  def callF = f(exp) //Here, exp must have type Nothing!
}

So, variance violations only translate to "useless" code, not to soundness violations. (And in fact, it's not even useless, since you can set a lower bound later).
Question: does this resemble more use-site variance than declaration-site variance? If so, do we want to keep the current checks just to keep the usability advantages of declaration-site variance? But those checks seem to restrict expressivity somewhat arbitrarily, so there's the risk of forcing people to switch to the encoding by hand.

[scabug]

@odersky said:
The translation is indeed from declaration-site variance to use-site variance. I still think declaration site variance is much better from a software engineering perspective. It provides guidance to the library designer to make the library easy to use, whereas use-site variance just dumps all the complexity at the users feet.

But having a clean translation from declaration site to use site opens up new possibilities. We could make variance violations warnings instead of errors. Or, still use @uncheckedVariance to suppress variance errors, but now we get the assurance that nothing goes wrong. @uncheckedVariance would not present a soundness risk anymore.

[szeiger]

A similar issue with a protected[this] type instead of a method, simplified from a collection strawman update that uses this design to reduce boilerplate (scala/collection-strawman#468):

trait A[+_X] {
  protected[this] type X = _X
  def f: X
}

trait B extends A[B] {
  def f: X = new B {}
}

class C extends B with A[C] {
  // should be required because the inherited f is of type B, not C
  //override def f: X = new C
}

val c1 = new C
val c2: C = c1.f

Both Scala and Dotty will happily compile this and throw a ClassCastException at runtime.