Imported From: https://issues.scala-lang.org/browse/SI-4377?orig=1
Reporter: Mikhail Vorozhtsov (mikhail.vorozhtsov)

Eduardo Pareja Tobes (eparejatobes) said:
Related I guess: http://stackoverflow.com/a/40983501/614394

That looks like the correct behaviour to me. Consider this relation:

scala> implicitly[(op.Cap forSome { val op: Op }) <:< Op#Cap]
res1: op.Cap forSome { val op: Op } <:< Op#Cap = <function1>

scala> implicitly[Op#Cap <:< (op.Cap forSome { val op: Op })]
<console>:15: error: Cannot prove that Op#Cap <:< op.Cap forSome { val op: Op }.
       implicitly[Op#Cap <:< (op.Cap forSome { val op: Op })]

So we cannot say that O#Cap =:= o.Cap for some value o: O. Maybe your intuition about subtyping for structural types is failing you. Note that type T = U is effectively type T >: U <: U which makes it invariant. If you want a covariant relation you may constrain only the upper bound:

scala> def f[O <: Op] = implicitly[O <:< Op { type Cap <: O#Cap }]
f: [O <: Op]=> O <:< Op{type Cap <: O#Cap}

@joroKr21 what you wrote is of course correct, but type projections being implemented as existentials is an implementation detail, not part of spec. You cannot argue for this being correct based on it. As a matter of fact, I suspect that implementing type projections as existentials could contradict the spec.

For further context, this compiles:

def f1[O <: Op] = implicitly[O#Cap =:= (O { type Cap = O#Cap })#Cap]

Type projections are not implemented as existentials. Anyway let me show an example that will hopefully convince you why O <:< Op { type Cap = O#Cap } would be unsound. Let's first replace Op with Animal and Cap with Food to make it more intuitive and add some methods that do stuff:

  trait Animal {
    type Food
    def find(): Food = ???
    def eat(food: Food): Unit = ???
  }

  def exchangeFood[A <: Animal](x: A, y: A): Unit = {
    // This would be possible if A <:< Animal { type Food = A#Food }
    val x1 = x: Animal { type Food = A#Food }
    val y1 = y: Animal { type Food = A#Food }
    x1.eat(y1.find())
    y1.eat(x1.find())
  }

  class Grass
  class Sheep extends Animal {
    type Food = Grass
  }
  class Wolf extends Animal {
    type Food = Sheep
  }

  // Whoops we made sheep cannibals, and wolfs eat grass.
  exchangeFood(new Sheep, new Wolf)

To understand better, read up on covariance and contravariance.

It's true the spec doesn't go in much detail here, but the right model for a type projection T#L is to think of it in terms of a selection p.L where p is some unknown value of type T. The theory (DOT) only considers type selection on paths (p.L), not types (T#L). The latter is where the unsoundness lies, because it is interpreted as p.L forSome {val p: T}, where we don't know enough about the value p to exclude bad bounds. (For a very deep dive: http://lampwww.epfl.ch/~amin/dot/soundness_oopsla16.pdf -- it doesn't go into much detail on this encoding, though.)

About:

def f[C, O <: Op { type Cap = C }] {}
def g[O <: Op] = f[O#Cap, O]

Let's consider f[o#Cap, o] in the body of g. I replaced g's type parameter O by an unknown constant o to represent we're inside the body and we can't assume anything about the choice of the universally quantified parameter O coming in from outside -- this is called skolemization. Now, we need to derive o <: Op { type Cap = o#Cap }, which requires o <: Op and subtyping on the members of the refinement: Cap in o and in Op { type Cap >: o#Cap <: o#Cap } (rewriting the type alias to the corresponding abstract type member): o#Cap <: >: o#Cap <: o#Cap.

To me, this looks like a bug, potentially in member subtyping (https://github.com/scala/scala/blob/1e09de17a3473efb26db535a71f9ec8b03018ac2/src/reflect/scala/reflect/internal/Types.scala#L4260-L4303), but it's not super obvious :-) I'd have to think about it some more.

@joroKr21 sorry I didn't pay enough attention to what the issue says. What I think is reasonable to expect is that given O <: Op we should have O { type Cap = O#Cap } <:< O:

// these two compile
def f1(x: Op) = implicitly[x.type { type Cap = x.Cap } <:< x.type ]
def f2(x: Op) = implicitly[x.type <:< x.type { type Cap = x.Cap }]
// this one compiles too (of course)
def f3[O <: Op] = implicitly[O { type Cap = O#Cap } <:< O]
// this one not
// def f4[O <: Op] = implicitly[O <:< O { type Cap = O#Cap }]

I don't expect anyone to agree with me here, but I'd rather live with the unsoundness and be able to use projections, or do the same as with covariant type parameters: forbid methods with arguments in contravariant position (that's exactly what happens in the classical Animals and Food example).

@adriaanm thanks for taking a look at this.

I'm going to go with this being a (tricky) bug. It compiles when we use a weaker prefix for the type on the left in
https://github.com/scala/scala/blob/64dd408b2d6efe2d0c719feb6a3959b154127c1c/src/reflect/scala/reflect/internal/Types.scala#L4245:

-|| specializesSym(tp.narrow, member, sym.owner.thisType, sym, depth)
+|| specializesSym(tp, member, sym.owner.thisType, sym, depth)

That implies narrowing of a skolemized type is losing information. Since narrowing is "Map to a singleton type which is a subtype of this type.", it should hold that T <: U ==> T.narrow <: U. Again, this is a bit of a drive-by shooting as I'm procrastinating cutting the release, but the bug does look legit.

We all know by now that general type projection is unsound. However I don't see any bad bounds in the animal example. The problem would arise exactly from having two different instances of Op that respectively fix Op#Cap to something different. So to me narrowing looks like the right thing to do.

@adriaanm The problem isn't with T <: U ==> T.narrow <: U but with T <: F[T] ==> T.narrow <: F[T.narrow], i.e. when we have T on the RHS as well. And that is generally not true unless F is covariant in it's argument. Of course T <: F[T] ==> T.narrow <: F[T] is true, but like you said that is not what skolemization does.

@eparejatobes Living with unsoundness is not the solution IMHO, especially given the flexibility of Scala. Usually you can redesign your program to pass around an instance of Op and work with path dependant types instead of type projection (which is also future proof considering dotty). Just think about the lessons learned from Java arrays. Btw your other suggestion (prohibiting specific positions of the type) is exactly what Java does with generics - call-site variance. Scala opted for declaration site variance. There's clearly a trade-off here but we should be consistent in our choice.