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 parameter inference #5189

Closed
scabug opened this issue Nov 15, 2011 · 12 comments
Closed

unsound type parameter inference #5189

scabug opened this issue Nov 15, 2011 · 12 comments

Comments

@scabug
Copy link

@scabug scabug commented Nov 15, 2011

I thought this was already open somewhere but I can't find it.

scala> case class Foo[T, U](f: T => U)
defined class Foo

// uh-oh, Any => Any should be Nothing => Any.
scala> def f(x: Any) = x match { case Foo(bar) => bar }
f: (x: Any)Any => Any

scala> def f(x: Any) = x match { case Foo(bar) => bar(5) }
f: (x: Any)Any

scala> f(Foo((x: String) => x))
java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
	at $anonfun$1.apply(<console>:11)
	at .f(<console>:9)
	at .<init>(<console>:11)
@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Nov 15, 2011

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Nov 15, 2011

@paulp said:
Interestingly, under -Yvirtpatmat it gives an unchecked warning (no warning with regular pattern matcher) but still infers Any => Any.

scala> def f(x: Any) = x match { case Foo(bar) => bar }
<console>:9: warning: non variable type-argument Any in type Foo[Any,Any] is unchecked since it is eliminated by erasure
       def f(x: Any) = x match { case Foo(bar) => bar }
                                      ^
f: (x: Any)Any => Any
@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Nov 18, 2011

@paulp said:
I had assigned this to the meeting, but as it didn't happen on tuesday (or I wasn't pulled in) re-assigning to martin.

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Feb 27, 2012

@adriaanm said:
see also https://gist.github.com/1925479
(and JavaConversions)

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Jun 22, 2012

@adriaanm said (edited on Jul 28, 2012 8:33:44 AM UTC):
fixed by scala/scala@29bcade

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Jul 28, 2012

@adriaanm said:
(this is the bug that causes type mismatches that refer to "GADT skolem")

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Dec 30, 2012

@paulp said:
Issues remain.

  1. As detailed in email to scala-internals, the fix was overly specific and missed numerous unsound cases.

  2. I also found that the current fix only works on explicitly declared types. For instance in t5189b.scala, if I let the return type be inferred:

def unwrap[T](x: AbsWrapperCov[T])/*: Wrapped[T]*/ = x match {
  case Wrapper/*[_ <: T ]*/(wrapped) => wrapped
}

Then it compiles - and infers Wrapped[T], unsoundly. I assume this is pt=WildcardType never coming to grips with the situation.

I believe the soundness issue requires an invariant something like: if the type of a GADT method (inferred or otherwise) uses the method's type parameters as type arguments, then either the corresponding class type parameters must be covariant, or the usages must be upper-bounded by the type parameter rather than the type parameter itself. Similar for contravariant/lower.

That doesn't address the type inference question - it has to infer Wrapped[_ <: T] rather than Wrapped[T] in the above example, and I'm not sure what that will take.

I also have serious doubts about the mitigation strategy taken with the original patch, i.e. adding a bunch of casts. Those casts look pretty unsafe, is there reason to believe otherwise?

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Jan 8, 2013

@paulp said:
Funny that I didn't immediately see the connection to #6925. (I discovered these through completely independent paths.) The funny thing is that in this one I'm pointing out that inferring Wrapped[T] is unsound and it has to infer Wrapped[_ <: T], and in #6925 we're calling the inference of Set[_ <: T] instead of Set[T] a regression. But maybe it can infer Set[T] on the invariant type? It's the covariant case for which it must only assume a bound, not a type.

My email to scala-internals was: https://groups.google.com/d/topic/scala-internals/dGQCGQ8dYNs/discussion

Here is a more direct demonstration.

scala> abstract class Covariant[+A](x: A) { def apply(): A = x }
defined class Covariant

scala> case class Invariant[A](val xs: Array[A]) extends Covariant[A](xs.head)
defined class Invariant

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

scala> f(Invariant(Array[Int](1)): Covariant[Any])
java.lang.ClassCastException: [I cannot be cast to [Ljava.lang.Object;
	at .<init>(<console>:12)
	at .<clinit>(<console>)
	at .<init>(<console>:11)
	at .<clinit>(<console>)
	at $print(<console>)
@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Jan 8, 2013

@paulp said:
And for backward compat to 2.7, here are 5 lines which incur an ArrayStoreException on any version of scala.

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
@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Jan 8, 2013

@paulp said:
See further elaboration in #6944.

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Jan 9, 2013

@adriaanm said:
ok, fixed it -- there was some deskolemization logic that was only necessary to appease the old pattern matcher
it's been moved to a less dangerous spot (/dev/null would be the most appropriate one in master)

@scabug

This comment has been minimized.

Copy link
Author

@scabug scabug commented Jan 9, 2013

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.