Type inference should be more careful when unifying wildcards to avoid unsoundness

[smarter]

class Foo[T](var elem: T)

object Test {
  def setFirstInPair[T](pair: (Foo[T], Foo[T])) = {
    pair._1.elem = pair._2.elem
  }

  def setFirstInList[T](list: List[Foo[T]]) = {
    list(0).elem = list(1).elem
  }

  def test1(): Unit = {
    val fooInt = new Foo(1)
    val fooString = new Foo("")
    val pair: (Foo[_], Foo[_]) = (fooInt, fooString)
    setFirstInPair(pair) // Should be an error, like in Scala 2
    println(fooInt.elem + 1) // ClassCastException in Dotty
  }

  def test2(): Unit = {
    val fooInt = new Foo(1)
    val fooString = new Foo("")
    val list: List[Foo[_]] = List(fooInt, fooString)
    setFirstInList(list) // Should be an error, like in Scala 2
    println(fooInt.elem + 1) // ClassCastException in Dotty
  }

  def main(args: Array[String]): Unit = {
    test1()
    test2()
  }
}

The Scala 2 errors are:

try/sound.scala:16: error: no type parameters for method setFirstInPair: (pair: (Foo[T], Foo[T]))Unit exist so that it can be applied to arguments ((Foo[_], Foo[_]))
 --- because ---
argument expression's type is not compatible with formal parameter type;
 found   : (Foo[_], Foo[_])
 required: (Foo[?T], Foo[?T])
    setFirstInPair(pair) // Should be an error, like in Scala 2
    ^
try/sound.scala:16: error: type mismatch;
 found   : (Foo[_], Foo[_])
 required: (Foo[T], Foo[T])
    setFirstInPair(pair) // Should be an error, like in Scala 2
                   ^
try/sound.scala:24: error: no type parameters for method setFirstInList: (list: List[Foo[T]])Unit exist so that it can be applied to arguments (List[Foo[_]])
 --- because ---
argument expression's type is not compatible with formal parameter type;
 found   : List[Foo[_]]
 required: List[Foo[?T]]
    setFirstInList(list) // Should be an error, like in Scala 2
    ^
try/sound.scala:24: error: type mismatch;
 found   : List[Foo[_]]
 required: List[Foo[T]]
    setFirstInList(list) // Should be an error, like in Scala 2
                   ^

Note that the following compiles fine in Scala 2, so it's not just applying a blanket ban on unifying with wildcards:

  def foo[T](foo: Foo[T]) = {}
  val x: Foo[_] = new Foo(1)
  foo(x)

I'm actually not sure how to reason about the difference in Dotty since we don't have a concept of existential types, /cc @Blaisorblade ?

[smarter]

Turns out we don't even need wildcards to have a problem:

abstract class Foo {
  type A
  var elem: A
}

object Test {
  def setFirstInList[T](list: List[Foo { type A = T }]) = {
    list(0).elem = list(1).elem
  }

  def main(args: Array[String]): Unit = {
    val fooInt = new Foo { type A = Int; var elem = 1 }
    val fooString = new Foo { type A = String; var elem = "" }
    val list: List[Foo] = List(fooInt, fooString)
    setFirstInList(list) // Should be an error, like in Scala 2
    println(fooInt.elem + 1) // ClassCastException in Dotty
  }
}

Scala 2 says:

try/sound2.scala:15: error: type mismatch;
 found   : List[Foo]
 required: List[Foo{type A = this.A}]
    setFirstInList(list) // Should be an error, like in Scala 2
                   ^

Whereas Dotty happily infers:

setFirstInList[Foo#A](list)

[smarter]

For some weird reason, this compiles:

trait Bar {
  type A
}

object Test {
  def test1: Unit = {
    val b1: List[Bar] = List(new Bar {})
    val b2: List[Bar { type A = Bar#A }] = b1 // error in Scala 2, compiles with Dotty
  }
}

But this doesn't:

  def test2: Unit = {
    val b1: Bar = new Bar {}
    val b2: Bar { type A = Bar#A } = b1 // error as expected: Found: Bar, Required: Bar { type A = Bar#A }
  }

[abgruszecki]

Note for posterity: in the original example, the parameter to setFirstInPair that gets inferred is Foo[_]#T, which is somewhat suspicious.

[smarter]

Here's the subtyping log with the List example that incorrectly returns true:

[log frontend] ==> isSubType List[Bar](b1) <:< List[Bar{A = Bar#A}] ?
[log frontend]   ==> isSubType List[Bar] <:< List[Bar{A = Bar#A}] LoApprox?
[log frontend]     ==> isSubType scala.collection.immutable.type(scala.collection.immutable) <:< scala.collection.immutable.type(scala.collection.immutable) ?
[log frontend]     <== isSubType scala.collection.immutable.type(scala.collection.immutable) <:< scala.collection.immutable.type(scala.collection.immutable)  = true
[log frontend]     ==> isSubType Bar <:< Bar{A = Bar#A} ?
[log frontend]       ==> isSubType Bar <:< Bar ?
[log frontend]       <== isSubType Bar <:< Bar  = true
[log frontend]       ==> hasMatchingMember(Bar . A :?  = Bar#A), mbr: ?
[log frontend]         ==> isSubType  <:<  = Bar#A ?
[log frontend]           ==> isSubType Bar#A <:< Nothing ?
[log frontend]             ==> isSubType Any <:< Nothing LoApprox?
[log frontend]             <== isSubType Any <:< Nothing LoApprox = false
[log frontend]           <== isSubType Bar#A <:< Nothing  = false
[log frontend]         <== isSubType  <:<  = Bar#A  = false
[log frontend]         ==> isSubType Bar#A <:< Bar#A ?
[log frontend]         <== isSubType Bar#A <:< Bar#A  = true
[log frontend]         ==> isSubType Bar#A <:< Bar#A ?
[log frontend]         <== isSubType Bar#A <:< Bar#A  = true
[log frontend]       <== hasMatchingMember(Bar . A :?  = Bar#A), mbr:  = true
[log frontend]     <== isSubType Bar <:< Bar{A = Bar#A}  = true
[log frontend]   <== isSubType List[Bar] <:< List[Bar{A = Bar#A}] LoApprox = true
[log frontend] <== isSubType List[Bar](b1) <:< List[Bar{A = Bar#A}]  = true

And the one that correctly returns false:

[log frontend] ==> isSubType Bar(b1) <:< Bar{A = Bar#A} ?
[log frontend]   ==> isSubType Bar(b1) <:< Bar ?
[log frontend]     ==> isSubType Bar <:< Bar LoApprox?
[log frontend]     <== isSubType Bar <:< Bar LoApprox = true
[log frontend]   <== isSubType Bar(b1) <:< Bar  = true
[log frontend]   ==> hasMatchingMember(Bar(b1) . A :?  = Bar#A), mbr: ?
[log frontend]     ==> isSubType  <:<  = Bar#A ?
[log frontend]       ==> isSubType Bar#A <:< Nothing ?
[log frontend]         ==> isSubType Any <:< Nothing LoApprox?
[log frontend]         <== isSubType Any <:< Nothing LoApprox = false
[log frontend]       <== isSubType Bar#A <:< Nothing  = false
[log frontend]     <== isSubType  <:<  = Bar#A  = false
[log frontend]     ==> isSubType Bar#A <:< b1.A ?
[log frontend]       ==> isSubType Bar <:< Bar(b1) ?
[log frontend]       <== isSubType Bar <:< Bar(b1)  = false
[log frontend]       ==> isSubType Any <:< b1.A LoApprox?
[log frontend]       <== isSubType Any <:< b1.A LoApprox = false
[log frontend]     <== isSubType Bar#A <:< b1.A  = false
[log frontend]   <== hasMatchingMember(Bar(b1) . A :?  = Bar#A), mbr:  = false
[log frontend] <== isSubType Bar(b1) <:< Bar{A = Bar#A}  = false

[smarter]

matchAbstractTypeMember in hasMatchingMember is looking very suspicious: https://github.com/lampepfl/dotty/blob/6bc505236a3b93a8c5a5d41f8d2f78aa94835695/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1135-L1158

[odersky]

Indeed. If we fix it then all the examples with type members get the expected errors. But the first example with wildcards still compiles. On the other hand, if we turn capturing off this one also gets the expected errors. Here's the capturing code (it's part of isSubArgs):

      def compareCaptured(arg1: Type, arg2: Type): Boolean = arg1 match {
        case arg1: TypeBounds =>
          val captured = TypeRef(tp1, tparam.asInstanceOf[TypeSymbol])
          isSubArg(captured, arg2)
        case _ =>
          false
      }

[smarter]

Reopening since part of the problem (the original example) still remains.