Skip to content

Unsoundness with the variance of type lambda bounded type variables #9061

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

Closed
neko-kai opened this issue May 27, 2020 · 7 comments
Closed

Unsoundness with the variance of type lambda bounded type variables #9061

neko-kai opened this issue May 27, 2020 · 7 comments

Comments

@neko-kai
Copy link
Contributor

Minimized code

case class Contra[-A](f: A => Int)

case class Covarify[+F <: ([A] =>> Any), +A](fa: F[A])

@main def main = {
  val x = Covarify[Contra, Int](Contra[Int](_ + 5))
  val y: Covarify[Contra, Any] = x
  println(y.fa.f("abc"))
}

https://scastie.scala-lang.org/ZfaseMB6QnyGTFsihR9FUQ

Output

java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
	at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:99)
	at dotty.runtime.function.JFunction1$mcII$sp.apply(JFunction1$mcII$sp.java:12)
	at main$package$.main(main.scala:8)
	at main.main(main.scala:5)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at sbt.Run.invokeMain(Run.scala:115)
	at sbt.Run.execute$1(Run.scala:79)
	at sbt.Run.$anonfun$runWithLoader$4(Run.scala:92)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
	at sbt.util.InterfaceUtil$$anon$1.get(InterfaceUtil.scala:10)
	at sbt.TrapExit$App.run(TrapExit.scala:257)
	at java.lang.Thread.run(Thread.java:748)

Expectation

Either case class Covarify[+F <: ([A] =>> Any), +A](fa: F[A]) or Covarify[Contra, Int] should be rejected. Rejecting the former might require reintroducing type lambda variance, to be able to express the desired kind F[+_] as the bound _ <: ([+A] =>> Any).

@smarter
Copy link
Member

smarter commented May 27, 2020

Rejecting the former might require reintroducing type lambda variance, to be able to express the desired kind F[+_] as the bound _ <: ([+A] =>> Any).

I think we intentionally chose to not support this as one can always write F[+A] instead.

@Odomontois
Copy link

Odomontois commented May 27, 2020

I think we intentionally chose to not support this as one can always write F[+A] instead.

@smarter
What would they do if the code is kind-polymorphic and they have to supply type for the K <: AnyKind parameter?

@smarter
Copy link
Member

smarter commented May 27, 2020

We added AnyKind in the language because there's some situations where it's useful, but we make no guarantee that it is always usable as one would hope (we can always try to improve that after 3.0 if needed), however if I understand your question correctly, using AnyKind is not a problem here:

class Foo { type X <: AnyKind }
class Bar extends Foo { type X[+A] <: String }

@Odomontois
Copy link

@smarter

case class Covarify[+F[_], +A](fa: F[A])
case class PolyK[K <: AnyKind, C[f[_ <: K], a <: K],  F[_ <: K] , A <: K](c: C[F, A])
PolyK[ ??? , Covarify, List, Int](Covarify(List(1)))

@smarter
Copy link
Member

smarter commented May 27, 2020

Not sure what's going on here, but you have PolyK[..., A <: K] and below PolyK[..., Int], so K would have to be Any?

@neko-kai
Copy link
Contributor Author

@Odomontois The issue in that snippet seems to be not with AnyKind, but with variance on f, the following works:

case class Covarify[+F[+_], +A](fa: F[A])

case class PolyK[K <: AnyKind, C[f[+_ <: K], a <: K],  F[+_ <: K] , A <: K](c: C[F, A])

case class MonoK[C[f[+_], a], F[+_], A](c: C[F, A])

@main def main = {
  MonoK[Covarify, List, Int](Covarify(List(1)))
  
  PolyK[Any, Covarify, List, Int](Covarify(List(1)))
}

smarter added a commit that referenced this issue May 30, 2020
Fix #9061: Treat `type F <: [X] => G` like `type F[X] <: G`.
smarter added a commit that referenced this issue May 30, 2020
Revert "Fix #9061: Treat `type F <: [X] => G` like `type F[X] <: G`."
smarter pushed a commit to dotty-staging/dotty that referenced this issue May 30, 2020
smarter added a commit to dotty-staging/dotty that referenced this issue May 30, 2020
smarter pushed a commit to dotty-staging/dotty that referenced this issue May 30, 2020
@smarter
Copy link
Member

smarter commented May 30, 2020

(reopening because the fix had to be reverted, see #9086)

@smarter smarter reopened this May 30, 2020
odersky added a commit to dotty-staging/dotty that referenced this issue Jun 1, 2020
It did not work for curried type lambdas.
odersky added a commit that referenced this issue Jun 1, 2020
Fix variance fixing code in the fix of #9061
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants