SI-6680 unsoundness in gadt typing.

Introduces -Xstrict-inference to deal with the significant
gap between soundness and what presently compiles. I'm hopeful
that it's TOO strict, because it finds e.g. 75 errors compiling
immutable/IntMap.scala, but it might be that bad.

14 files changed, 129 insertions, 0 deletions

diff --git a/test/files/neg/gadts2-strict.check b/test/files/neg/gadts2-strict.check
new file mode 100644
index 0000000000..960b35ed2f
--- /dev/null
+++ b/test/files/neg/gadts2-strict.check
@@ -0,0 +1,6 @@
+gadts2-strict.scala:14: error: type mismatch;
+ found   : Test.MyDouble
+ required: a
+      case NumTerm(n) => c.x = MyDouble(1.0)
+                                       ^
+one error found
diff --git a/test/files/neg/gadts2-strict.flags b/test/files/neg/gadts2-strict.flags
new file mode 100644
index 0000000000..19243266d1
--- /dev/null
+++ b/test/files/neg/gadts2-strict.flags
@@ -0,0 +1 @@
+-Xstrict-inference
\ No newline at end of file
diff --git a/test/files/neg/gadts2-strict.scala b/test/files/neg/gadts2-strict.scala
new file mode 100644
index 0000000000..54978b7712
--- /dev/null
+++ b/test/files/neg/gadts2-strict.scala
@@ -0,0 +1,26 @@
+// A copy of pos/gadts2, which must fail under -Xstrict-inference.
+object Test {
+
+  abstract class Number
+  case class MyInt(n: Int) extends Number
+  case class MyDouble(d: Double) extends Number
+
+  trait Term[a]
+  case class Cell[a](var x: a) extends Term[a]
+  final case class NumTerm(val n: Number) extends Term[Number]
+
+  def f[a](t: Term[a], c: Cell[a]) {
+    t match {
+      case NumTerm(n) => c.x = MyDouble(1.0)
+    }
+  }
+
+  val x: Term[Number] = NumTerm(MyInt(5))
+
+  def main(args: Array[String]) {
+    val cell = Cell[Number](MyInt(6))
+    Console.println(cell)
+    f[Number](new NumTerm(MyInt(5)), cell)
+    Console.println(cell)
+  }
+}
diff --git a/test/files/neg/gadts2.check b/test/files/neg/gadts2.check
new file mode 100644
index 0000000000..dc21f3f52c
--- /dev/null
+++ b/test/files/neg/gadts2.check
@@ -0,0 +1,6 @@
+gadts2.scala:7: error: type mismatch;
+ found   : String("abc")
+ required: B
+  (s1: Super[Any]) match { case Sub(f) => f("abc") }
+                                            ^
+one error found
diff --git a/test/files/neg/gadts2.flags b/test/files/neg/gadts2.flags
new file mode 100644
index 0000000000..19243266d1
--- /dev/null
+++ b/test/files/neg/gadts2.flags
@@ -0,0 +1 @@
+-Xstrict-inference
\ No newline at end of file
diff --git a/test/files/neg/gadts2.scala b/test/files/neg/gadts2.scala
new file mode 100644
index 0000000000..156944b8d9
--- /dev/null
+++ b/test/files/neg/gadts2.scala
@@ -0,0 +1,12 @@
+trait Super[+A]
+case class Sub[B](f: B => B) extends Super[B]
+
+object Test extends App {
+  val s1 = Sub((x: Int) => x)
+
+  (s1: Super[Any]) match { case Sub(f) => f("abc") }
+}
+// java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
+//   at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:105)
+//   at Test$$anonfun$1.apply(a.scala:5)
+//   at Test$.delayedEndpoint$Test$1(a.scala:7)
diff --git a/test/files/neg/run-gadts-strict.check b/test/files/neg/run-gadts-strict.check
new file mode 100644
index 0000000000..b4d36c4629
--- /dev/null
+++ b/test/files/neg/run-gadts-strict.check
@@ -0,0 +1,21 @@
+run-gadts-strict.scala:12: error: type mismatch;
+ found   : n.type (with underlying type Int)
+ required: T
+    case Lit(n)        => n
+                          ^
+run-gadts-strict.scala:13: error: type mismatch;
+ found   : Int
+ required: T
+    case Succ(u)       => eval(u) + 1
+                                  ^
+run-gadts-strict.scala:14: error: type mismatch;
+ found   : Boolean
+ required: T
+    case IsZero(u)     => eval(u) == 0
+                                  ^
+run-gadts-strict.scala:15: error: type mismatch;
+ found   : T(in class If)
+ required: T(in method eval)
+    case If(c, u1, u2) => eval(if (eval(c)) u1 else u2)
+                              ^
+four errors found
diff --git a/test/files/neg/run-gadts-strict.flags b/test/files/neg/run-gadts-strict.flags
new file mode 100644
index 0000000000..19243266d1
--- /dev/null
+++ b/test/files/neg/run-gadts-strict.flags
@@ -0,0 +1 @@
+-Xstrict-inference
\ No newline at end of file
diff --git a/test/files/neg/run-gadts-strict.scala b/test/files/neg/run-gadts-strict.scala
new file mode 100644
index 0000000000..041d10d4bd
--- /dev/null
+++ b/test/files/neg/run-gadts-strict.scala
@@ -0,0 +1,18 @@
+// A copy of run/gadts.scala, which must fail under -Xstrict-inference.
+abstract class Term[T]
+case class Lit(x: Int) extends Term[Int]
+case class Succ(t: Term[Int]) extends Term[Int]
+case class IsZero(t: Term[Int]) extends Term[Boolean]
+case class If[T](c: Term[Boolean],
+                 t1: Term[T],
+                 t2: Term[T]) extends Term[T]
+
+object Test extends App {
+  def eval[T](t: Term[T]): T = t match {
+    case Lit(n)        => n
+    case Succ(u)       => eval(u) + 1
+    case IsZero(u)     => eval(u) == 0
+    case If(c, u1, u2) => eval(if (eval(c)) u1 else u2)
+  }
+  println(eval(If(IsZero(Lit(1)), Lit(41), Succ(Lit(41)))))
+}
diff --git a/test/files/neg/t6680a.check b/test/files/neg/t6680a.check
new file mode 100644
index 0000000000..03e4df10c1
--- /dev/null
+++ b/test/files/neg/t6680a.check
@@ -0,0 +1,11 @@
+t6680a.scala:10: error: type mismatch;
+ found   : String("abc")
+ required: A
+    y.x = "abc"
+          ^
+t6680a.scala:17: error: type mismatch;
+ found   : String("")
+ required: A
+  case class C[A](f:A=>A);def f(x:Any)=x match { case C(f)=>f("") };f(C[Int](x=>x))
+                                                              ^
+two errors found
diff --git a/test/files/neg/t6680a.scala b/test/files/neg/t6680a.scala
new file mode 100644
index 0000000000..93b796438f
--- /dev/null
+++ b/test/files/neg/t6680a.scala
@@ -0,0 +1,18 @@
+case class Cell[A](var x: A)
+object Test {
+  def f1(x: Any)        = x match { case y @ Cell(_) => y } // Inferred type is Cell[Any]
+  def f2(x: Cell[_])    = x match { case y @ Cell(_) => y } // Inferred type is Cell[_]
+  def f3[A](x: Cell[A]) = x match { case y @ Cell(_) => y } // Inferred type is Cell[A]
+
+  def main(args: Array[String]): Unit = {
+    val x = new Cell(1)
+    val y = f1(x)
+    y.x = "abc"
+    println(x.x + 1)
+  }
+}
+
+// The tweetable variation
+object Tweet {
+  case class C[A](f:A=>A);def f(x:Any)=x match { case C(f)=>f("") };f(C[Int](x=>x))
+}
diff --git a/test/files/neg/t6680b.flags b/test/files/neg/t6680b.flags
new file mode 100644
index 0000000000..a02d83efad
--- /dev/null
+++ b/test/files/neg/t6680b.flags
@@ -0,0 +1 @@
+-Xstrict-inference
diff --git a/test/files/neg/t6680c.check b/test/files/neg/t6680c.check
new file mode 100644
index 0000000000..7a749de1f2
--- /dev/null
+++ b/test/files/neg/t6680c.check
@@ -0,0 +1,6 @@
+t6680c.scala:15: error: type mismatch;
+ found   : String("a string!")
+ required: S
+    res match { case Unfold(s, f) => f("a string!") }
+                                       ^
+one error found
diff --git a/test/files/neg/t6680c.flags b/test/files/neg/t6680c.flags
new file mode 100644
index 0000000000..a02d83efad
--- /dev/null
+++ b/test/files/neg/t6680c.flags
@@ -0,0 +1 @@
+-Xstrict-inference