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

Unsound type projection #3481

Closed
scabug opened this issue May 26, 2010 · 15 comments
Closed

Unsound type projection #3481

scabug opened this issue May 26, 2010 · 15 comments
Assignees
Milestone

Comments

@scabug
Copy link

scabug commented May 26, 2010

The following code works fine in latest nightly:

Welcome to Scala version 2.8.0.r22036-b20100526020129 (Java HotSpot(TM) Client VM, Java 1.6.0_18).
Type in expressions to have them evaluated.
Type :help for more information.

scala> trait A[T] { type B = T }
defined trait A

scala> def f[T <: A[_]](a : T#B) = 1
f: [T <: A[_]](a: Any)Int

scala> f[A[Int]]("hello")
res0: Int = 1

Instead of succeeding, it should give a type error on the last line.

@scabug
Copy link
Author

scabug commented May 26, 2010

Imported From: https://issues.scala-lang.org/browse/SI-3481?orig=1
Reporter: @jesnor

@scabug
Copy link
Author

scabug commented May 26, 2010

@harrah said:
It isn't unsound. You haven't made it do anything wrong at runtime.

Note that the argument type of f is Any, so you can't do anything on 'a' that is unsafe.

@scabug
Copy link
Author

scabug commented May 26, 2010

@jesnor said:
Well, the problem is the inferred type of f. Consider this example:

scala> trait A { type T; def m(t : T) = t.toString }
defined trait A

scala> class B[T2] extends A { type T = T2 }
defined class B

scala> def f[T <: B[_]](a : T#T, b : T) = b.m(a)
f: [T <: B[_]](a: Any,b: T)java.lang.String

scala> f("Hello", new B[Int])
res0: java.lang.String = Hello

Which obviously is unsound (calling (new B[Int]).m with a String).

Note that changing f to:

def f[T <: A](a : T#T, b : T) = b.m(a)

gives a compiler error. So the problem is obviously related to existential types.
{code}

@scabug
Copy link
Author

scabug commented May 26, 2010

@jesnor said:
Even simpler example:

scala> class B[T] { type T2 = T; def m(t : T2) = t.toString }
defined class B

scala> val b : B[_] = new B[Int]
b: B[_] = B@110d68a

scala> b.m("Hello")
res7: java.lang.String = Hello

@scabug
Copy link
Author

scabug commented May 26, 2010

@harrah said:
An example with a runtime exception:

scala> class B[T] { type T2 = T; def m(t : T2) = t.toString }
defined class B

scala> class C extends B[Int] { override def m(t: Int) = t + 2 }
defined class C

scala> val b : B[_] = new C                                     
b: B[_] = C@488d12e4

scala> b.m("Hello")                                             
java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
        at scala.runtime.BoxesRunTime.unboxToInt(Unknown Source)
        at C.m(<console>:6)
        at .<init>(<console>:9)

@scabug
Copy link
Author

scabug commented May 27, 2010

@adriaanm said:
here's my test case with initial diagnosis:

abstract class B[T] {
  type T2 = T
  def m(t : T2): Any
}

object Test {
  val b : B[_] = error("")
  b.m("Hello") // should not typecheck, but b.T2 normalizes to Any!! 
  // thus, String <: b.T2 (because thirdTryRef in isSubtype normalizes)
  // T as seen from Test.b is Any... should we have skolemized before getting here, or is asSeenFrom broken!? (oh my!)
}

@scabug
Copy link
Author

scabug commented May 27, 2010

@SethTisue said:
is this a regression in 2.8, or does 2.7 have the same issue(s)?

@scabug
Copy link
Author

scabug commented May 27, 2010

@adriaanm said:
so, since b: B[_$$1], b.T2 becomes _$$1, which is then replaced by its upper bound, Any, by existentialAbstraction(List(type _$$1), _$$1)
the last step seems undesirable in this case, but I don't understand enough of this to fix it

Martin, I'd be happy to implement a fix if you point me in the right direction

(BTW, it's not a regression, it type checks in 2.7.3.final)

@scabug
Copy link
Author

scabug commented Dec 1, 2010

@paulp said:
See also #4048.

@scabug
Copy link
Author

scabug commented Dec 1, 2011

@soc said (edited on Dec 1, 2011 7:58:42 PM UTC):
Every example above is now rejected by the compiler:

Welcome to Scala version 2.10.0.r26093-b20111130020250 (OpenJDK 64-Bit Server VM, Java 1.7.0_147-icedtea).

First example:

<console>:10: error: type mismatch;
 found   : String("hello")
 required: _$1 where type +_$1
              f[A[Int]]("hello")
                        ^

Second example:

<console>:10: error: type mismatch;
 found   : String("Hello")
 required: b.T2
    (which expands to)  _$1
              b.m("Hello")
                  ^

Is this fixed?

@scabug
Copy link
Author

scabug commented Dec 1, 2011

@paulp said:
Ahahaha, I think we should listen more closely when adriaan says "or is asSeenFrom broken!? (oh my!)" (way back in May of 2010.) Indeed asSeenFrom was broken and the relevant commit, which made these examples start correctly failing, is b7b81ca286.

@scabug
Copy link
Author

scabug commented Dec 1, 2011

@soc said:
So should I close this now?

@scabug
Copy link
Author

scabug commented Dec 1, 2011

@paulp said:
Still needs a test case. You can send me a pull request (it's a whole new ballgame over there now that we're on git.)

@scabug
Copy link
Author

scabug commented Dec 2, 2011

@soc said:
Here you go: scala/scala#10

@scabug
Copy link
Author

scabug commented Dec 2, 2011

@soc said:
Tests in scala/scala@6ecca6d

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants