Unsoundness bug in pattern matcher when pattern reveals existentials

[scabug]

Scala seems to refine all existential type variables to Any when pattern matching, which is unsound and can result in runtime errors. Here's an example data type:

/* The 'coinductive' view of streams, represented as their unfold. */
trait Stream[+A]
case class Unfold[S,+A](s: S, f: S => Option[(A,S)]) extends Stream[A]

object Stream {
  def fromList[A](a: List[A]): Stream[A] = 
    Unfold(a, (l:List[A]) => l.headOption.map((_,l.tail)))
}

Now take a look at an example usage which breaks. If I have a Stream[Int], and I match and obtain an Unfold(s, f), the type of (s,f) should be (S, S => Option[(A,S)]) forSome { type S }. But Scala just promotes everything to Any:

scala> Stream.fromList(List(1,2,3,4))
res0: Stream[Int] = Unfold(List(1, 2, 3, 4),<function1>)

scala> res0 match { case Unfold(s, f) => s }
res1: Any = List(1, 2, 3, 4)

Notice that the type of s is Any. Likewise, the type of f is also wrong, it accepts an Any:

scala> res0 match { case Unfold(s, f) => f }
res2: Any => Option[(Int, Any)] = <function1>

Since f expects Any, we can give it a String and get a runtime error:

scala> res0 match { case Unfold(s, f) => f("a string!") }
java.lang.ClassCastException: java.lang.String cannot be cast to scala.collection.immutable.List

I am using Scala 2.10.0-RC2, which, I understand has the new virtual pattern matcher turned on by default (I tried passing -Yvirtpatmat to the compiler but the option was not recognized.)

I find that this situation comes up a lot when writing libraries in Scala. It is extremely common to have a data type describing computations of some sort, and a separate interpreter which pattern matches to evaluate these computations for some semantics. The data type will frequently have existential type variables like this, and this bug means that the interpreter of the DSL is not typechecked!

Incidentally, the expression 'blah match { case Unfold(s,f) => f }' should trigger a type error due to an escaping skolem (rigid) type variable. Here's Haskell by comparison:

data Stream a where
  Unfold :: s -> (s -> Maybe (a, s)) -> Stream a 

fn (Unfold s f) = f

This yields:

    Couldn't match type `t' with `s -> Maybe (t1, s)'
      `t' is a rigid type variable bound by
          the inferred type of fn :: Stream t1 -> t at Test.hs:23:1
    In the expression: f
    In an equation for `fn': fn (Unfold s f) = f

[scabug]

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

[scabug]

@retronym said:
The same types are also inferred under -Xoldpatmat and Scala 2.9.1.

[scabug]

@adriaanm said (edited on Nov 17, 2012 10:17:34 PM UTC):

trait Super[+A]
// `Hidden` must occur in both variance positions (covariant/contravariant) for the sneakiness to work
// this way type inference will infer Any for `Hidden` and `A` in the pattern below
case class Concrete[Hidden, +A](havoc: Hidden => Hidden) extends Super[A]

object Test extends App {
  (Concrete((x: Int) => x): Super[Any]) match {
    case Concrete(f) => f("not what you'd expect")
  }
}

[scabug]

@adriaanm said:
WIP: adriaanm/scala@scala:2.10.x...ticket-6680

[scabug]

@pchiusano said:
Awesome. Really looking forward to seeing this fix!

[scabug]

@adriaanm said:
Sorry, won't be able to fix this in time for 2.10.1 / either 2.10.2-RC1 or 2.11.0-M2

[scabug]

@paulp said:
When fix arrives, please verify the example in #7090 as well.

[scabug]

@adriaanm said:
Unassigning and rescheduling to M6 as previous deadline was missed.

[scabug]

@paulp said:
I just ran into this in a shockingly easy to reach way. I wonder if people realize we have holes this size in the type system.

case class Cell[A](var x: A)
object Test {
  def f(x: Any) = x match { case y @ Cell(_) => y } // Inferred type is Cell[Any]
  def g(x: Any) = x match { case y: Cell[_] => y }  // This one infers Cell[_] as the other one should

  def main(args: Array[String]): Unit = {
    val x = new Cell(1)
    val y = f(x)
    y.x = "abc"
    println(x.x + 1)
  }
}
/***

% scala Test
java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
  at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:105)
  at Test$.main(a.scala:12)
  at Test.main(a.scala)

***/

[scabug]

@paulp said:
Also, in case the dimensions of this aren't yet apparent, adriaan your example makes it appear more of a corner case than it is. You don't need a hidden type parameter. All you need is a scrutinee with type Any.

case class Concrete[A](havoc: A => A)
object Test extends App {
  (Concrete((x: Int) => x): Any) match { case Concrete(f) => f("not what you'd expect") }
}

[scabug]

Stephen Compall (s11001001) said:
And, in conveniently tweetable form:

trait AO[A];case class AOA[A,B](f:A=>B,e:A=>A)extends AO[B]
def unsfeCoerce[A,B]=(AOA[B,B](a=>a,a=>a):AO[B])match{case AOA(id,_)=>id:(A=>B)}

[scabug]

@paulp said:
I like how it becomes "unsfeCoerce" rather than shortening to "unsafe", that's a let's say "creative" route to 140.

[scabug]

@paulp said:
In the interests of more room for commentary in tweets, here's a self-contained classcastexception in a line.

case class C[A](f:A=>A);def f(x:Any)=x match { case C(f)=>f("") };f(C[Int](x=>x))

[scabug]

@retronym said:
A proposed fix for this was commited by Paul in scala/scala@5708e9d, which is part of v2.11.0-M6 and higher.

This is only enabled under -Xstrict-inference as the unsoundness is widely exploited. I'll leave this ticket open to track that. But I'd be interested in Paul C. and Stephen's experiences with that flag.

[scabug]

Stephen Compall (s11001001) said:
That does seem much better; thanks very much for pointing it out. I hope to be able to use it as a standard part of my 2.11.x compilation options.

I've found #7990 and #7991 in some initial experiments, though. I tried to build scalaz-seven core head against M7 with that option, and I believe #7991 would fix almost all of the resulting errors, if not all.

I also imagine Paul C would prefer #7990 just be an error right out.

[scabug]

Stephen Compall (s11001001) said:
Oh, per #7991, it might not be so widely exploited as it seemed.

[scabug]

@adriaanm said:
Let's refine this further under a flag post 2.11.0

[scabug]

@retronym said:
I've proposed a partial reversion of the change as we found it caused regressions, even outside of -Xstrict-inference: scala/scala#3514

In the process I've spotted implementation issues with -Xs-i. We'll get it in better shape post 2.11.0.

[scabug]

@paulp said:
-Xstrict-inference was intended only as a coarse hacky start, but it kind of coincided with my departure. I expect it is overflowing with implementation issues.

[scabug]

Stephen Compall (s11001001) said:
Dotty-fied.