Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Inferred types must uniformly encounter the same restrictions as declared types #6944

Open
scabug opened this issue Jan 8, 2013 · 5 comments
Open
Milestone

Comments

@scabug
Copy link

@scabug scabug commented Jan 8, 2013

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
Copy link
Author

@scabug scabug commented Jan 8, 2013

@scabug
Copy link
Author

@scabug scabug commented Jan 8, 2013

@paulp said:
Definitely see also #5585.

@scabug
Copy link
Author

@scabug scabug commented Apr 19, 2013

@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
Copy link
Author

@scabug scabug commented Jun 11, 2013

@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
Copy link
Author

@scabug scabug commented Jun 11, 2013

@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 }
                                                                             ^
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
2 participants
You can’t perform that action at this time.