Inferred types must uniformly encounter the same restrictions as declared types

[scabug]

This example is taken from my comments in #5189:

trait Covariant[+A]
val arr = Array("abc")
case class Invariant[A](xs: Array[A]) extends Covariant[A]
def f[A](v: Covariant[A]) = v match { case Invariant(xs) => xs }
f(Invariant(arr): Covariant[Any])(0) = Nil

That is a soundness hole in every version of scala. It is interesting to note however that through scala 2.9.2, you could write f in either of these ways, and it would still compile unsoundly:

def f[A](v: Covariant[A]) = v match { case Invariant(xs) => (xs: Array[A]) }
def f[A](v: Covariant[A]): Array[A] = v match { case Invariant(xs) => xs }

In scala 2.10 those versions no longer compile, BUT the unsound type could still be inferred! My certainty that this is not the only example of that motivates this separate ticket.

// scala 2.10
scala> def f[A](v: Covariant[A]): Array[A] = v match { case Invariant(xs) => xs }
<console>:10: error: type mismatch;
 found   : Array[?A1] where type ?A1 <: A (this is a GADT skolem)
 required: Array[A]
Note: ?A1 <: A, but class Array is invariant in type T.
You may wish to investigate a wildcard type such as `_ <: A`. (SLS 3.2.10)
       def f[A](v: Covariant[A]): Array[A] = v match { case Invariant(xs) => xs }
                                                                             ^
scala> def f[A](v: Covariant[A]) = v match { case Invariant(xs) => xs }
f: [A](v: Covariant[A])Array[A]

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-6944?orig=1
Reporter: @paulp
See #5585, #5189, #6925

[scabug]

@paulp said:
Definitely see also #5585.

[scabug]

@Blaisorblade said:
One does not need an invariant class to trigger this, nor arrays. Here's a reduced version, inspired to what happens in Lightweight Modular Staging:

object MinimalUnsoundness {
  trait Exp[+T]
  case class Const[+T](t: T) extends Exp[T] //Making Const invariant makes no difference.
  def interp[T](term: Exp[T]): T =
    term match {
      case Const(t) => t //This should be rejected...
    }

  //Because classes like this can be declared:
  class MyConst(t: String) extends Const[Any](t) with Exp[Boolean]
}
//At the REPL:
scala> import MinimalUnsoundness._
import MinimalUnsoundness._

scala> :type interp(new MyConst(""))
Boolean

scala> interp(new MyConst(""))
java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Boolean

In the actual code, I want to prevent declaring classes like MyConst, so that interp is actually accepted, and making Const final is often not an option, but that's another story.

A more complete example - an interpreter for embedded simply-typed lambda-calculus with subtyping:

trait Lambda {
  trait Exp[+T]
  case class Const[T](t: T) extends Exp[T]
  case class App[S, T](fun: Exp[S => T], arg: Exp[S]) extends Exp[T]
  case class Fun[S, T](body: Exp[S] => Exp[T]) extends Exp[S => T]
}

trait Interp extends Lambda {
  def interp[T](term: Exp[T]): T =
    term match {
      case Const(t) => t //Unsound!
      case App(fun, arg) =>
        interp(fun) apply interp(arg) //Unsound!
      case f: Fun[s, t] =>
        //(x: s) => interp(f.body(Const(x)))
        (((x: s) => interp(f.body(Const(x)))): (s => t)).asInstanceOf[T] //What I have to write
      //case Fun(body) =>
        //x => interp(body(Const(x)))
    }
}

object Language extends Lambda with Interp {
  //Demonstrate why all the above branches can trigger an error.
  class MyFun[T]() extends Fun[T, T](x => x) with Exp[runtime.AbstractFunction1[T, T]]
  class MyApp[T](t: T) extends App[Int, List[T]](Fun(x => Const(List(t))), Const(1)) with Exp[Nil.type]
  class MyConst(t: String) extends Const[Any](t) with Exp[Boolean]

  println(interp(new MyApp(1))) //This works thanks to heap pollution
  println("""Executing 'interp(new MyApp(1))' in the REPL won't work -
    |you'll get a ClassCastException""".stripMargin)
  println("""Same for 'interp(new MyConst(""))'""")
}

[scabug]

@Blaisorblade said:
Upon closer observation, the bug you describe is different from the one I mentioned. Moreover, the one you describe cannot be reproduced any more in 2.10.2. Now we get:

scala> def f[A](v: Covariant[A]) = v match { case Invariant(xs) => xs }
f: [A](v: Covariant[A])Array[_ <: A]

hence the soundness hole you describe does not show up:

scala> f(Invariant(arr): Covariant[Any])(0) = Nil
<console>:13: error: type mismatch;
 found   : scala.collection.immutable.Nil.type
 required: ?A1 where type ?A1
              f(Invariant(arr): Covariant[Any])(0) = Nil
                                                     ^

But the type of f is still very bad, and I can use the technique of my example:

class Bad extends Invariant[Any](Array(1, 2, 3)) with Covariant[Boolean]

scala> f(new Bad)
res3: Array[_ <: Boolean] = Array(1, 2, 3) //What???

scala> res3(0)
java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.Boolean
<BOOM>

Should I open another bug and close this one?

[scabug]

@Blaisorblade said:
Amazing. Unlike I said, using an invariant class (here, arrays, which force Invariant to be invariant) makes a difference.

Usually, to fix the bug I mentioned, the compiler should deduce not ?A1 <: A (as in your error, which I repasted below) but ?A1 >: A. But because arrays are involved, it's not clear whether the compiler can deduce a constraint between ?A1 and A. On pen and paper, I could only deduce that if the most specific solution for v is Covariant[A2], then A2 <: ?A1 and A2 <: A. You can only set A2 = ?A1, giving ?A1 <: A, if you forbid the definition of Bad, as done by one sentence in the paper on case classes and extractors, "Matching objects with patterns", ECOOP 2007, by Burak Emir, Martin Odersky and John Williams. However, forbidding that definition will break valid code that doesn't care about pattern matching.

// scala 2.10
scala> def f[A](v: Covariant[A]): Array[A] = v match { case Invariant(xs) => xs }
<console>:10: error: type mismatch;
 found   : Array[?A1] where type ?A1 <: A (this is a GADT skolem)
 required: Array[A]
Note: ?A1 <: A, but class Array is invariant in type T.
You may wish to investigate a wildcard type such as `_ <: A`. (SLS 3.2.10)
       def f[A](v: Covariant[A]): Array[A] = v match { case Invariant(xs) => xs }
                                                                             ^

[dwijnand]

Seems like this one is fixed?

Welcome to Scala 2.13.5 (OpenJDK 64-Bit Server VM, Java 1.8.0_282).
Type in expressions for evaluation. Or try :help.

scala> trait Covariant[+A]
trait Covariant

scala> val arr = Array("abc")
val arr: Array[String] = Array(abc)

scala> case class Invariant[A](xs: Array[A]) extends Covariant[A]
class Invariant

scala> def f[A](v: Covariant[A]) = v match { case Invariant(xs) => xs }
def f[A](v: Covariant[A]): Array[_ <: A]

scala> f(Invariant(arr): Covariant[Any])(0) = Nil
                                              ^
       error: type mismatch;
        found   : Nil.type
        required: ?A1 where type ?A1

[lrytz]

The minimization in #6944 (comment) still runs with a CCE