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.