Skip to content

Inappropriate Widening of Invariant Type #11941

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

Open
adamgfraser opened this issue Apr 15, 2020 · 14 comments
Open

Inappropriate Widening of Invariant Type #11941

adamgfraser opened this issue Apr 15, 2020 · 14 comments
Labels
Milestone

Comments

@adamgfraser
Copy link

adamgfraser commented Apr 15, 2020

reproduction steps

import scala.reflect.ClassTag

trait X
trait Y
trait Z

trait Invariant[A]

trait Arrow[-A, +B] {
  def >>>[C](that: Arrow[B, C]): Arrow[A, C] =
    new Arrow[A, C] {}
}

def identity[A]: Arrow[A, A] = new Arrow[A, A] {}

def succeed[A]: Arrow[Any, A] = new Arrow[Any, A] {}


def f[A: ClassTag]: Arrow[Invariant[A with Y], Invariant[A with Z]] = {
  println("ClassTag in f is " + implicitly[ClassTag[A]])
  identity[Invariant[A with Y]] >>> g
  
}

def g[A: ClassTag]: Arrow[Invariant[A with Y], Invariant[A with Z]] = {
  println("ClassTag in g is " + implicitly[ClassTag[A]])
  succeed[Invariant[A with Z]]
}

val result Arrow[Invariant[X with Y], Invariant[X with Z]] = f[X]

problem

// ClassTag in f is X
// ClassTag in g is Object

expectation

I don't understand how the type of the ClassTag in g is Object. We're explicitly providing the type to f of X. So then the type of identity should be Arrow[X with Y, X with Y]. The type of the In parameter to g should have to be the same as the type of the Out from identity, which should get us X with Y and lead to the A type in g being inferred as X. But instead it is Object. I would have expected the type of both tags to be X or for this not to have compiled at all.

Copying @jdegoes.

@adamgfraser
Copy link
Author

Note that this appears to work correctly in Dotty. See here.

@lrytz
Copy link
Member

lrytz commented Apr 15, 2020

scala> implicitly[A with B <:< Object with A with B]
res0: A with B <:< A with B = generalized constraint

scala> implicitly[Object with A with B <:< A with B]
res1: A with B <:< A with B = generalized constraint

I guess the compiler expands the compound type at some point. Compiling the example with -Vprint:typer

    def f[A](implicit evidence$1: scala.reflect.ClassTag[A]): Arrow[Invariant[A with Y],Invariant[A with Z]] = {
      scala.Predef.println("ClassTag in f is ".+(scala.Predef.implicitly[scala.reflect.ClassTag[A]](evidence$1)));
      Test.this.identity[Invariant[A with Y]].>>>[Invariant[Object with A with Z]](Test.this.g[Object with A]((ClassTag.apply[Object with A](classOf[java.lang.Object]): scala.reflect.ClassTag[Object with A])))
    };

@lrytz lrytz added this to the Backlog milestone Apr 15, 2020
@joroKr21
Copy link
Member

joroKr21 commented Apr 15, 2020

This is just the normal LUB:

scala> trait X; trait Y
defined trait X
defined trait Y

scala> :t def foo[A](b: Boolean) = if (b) Option.empty[A with X] else Option.empty[A with Y]
[A](b: Boolean)Option[Object with A]

scala> :t def bar[A <: AnyRef](b: Boolean) = if (b) Option.empty[A with X] else Option.empty[A with Y]
[A <: AnyRef](b: Boolean)Option[A]

Since we can't assume that A <: Object for unbound type variable.
I guess it works in Dotty because it has proper support for intersection types.
So that A with X does not imply A with X <:< Object.
The workaround is to add <: AnyRef bound.

Actually not sure how it works in Dotty. Is there special handling?
A with X <:< Object because X <:< Object and Y <:< Object.
So then Object is a common supertype of both.

@adamgfraser
Copy link
Author

I think the problem here is that this is the parameter of an invariant type. Invariant[X with Y with Object] is a completely unrelated type to Invariant[X with Y]. So if the output type of identity is X with Y it isn't sound to widen the input type of G to X with Y with Object because now we're essentially allowing function composition of unrelated types.

@smarter
Copy link
Member

smarter commented Apr 15, 2020

Invariant[X with Y with Object] is a completely unrelated type to Invariant[X with Y]

I don't see why. Traits by default extend AnyRef, which is just a type alias of Object, since X and Y are trait, X with Y with Object is the same type as X with Y.

@joroKr21
Copy link
Member

joroKr21 commented Apr 15, 2020

Yes, that's right A with X with Object is the same as A with X because X <:< Object.
But A with Object is not the same as A since A could be anything.
So A with Object (or AnyRef) is the most specific solution for the type parameter of g.
Now I'm really intrigued, how does it work in Dotty?
Heuristics to not always infer the most specific type?

@joroKr21
Copy link
Member

It might be more illuminating to try what happens if we have:

trait Base
trait X extends Base
trait Y extends Base

@joroKr21
Copy link
Member

Oh I keep forgetting that in the Dotty the LUB is just the union type.

@joroKr21
Copy link
Member

ClassTag is very capricious

scala> classTag[X & Y | X & Z]
val res0: scala.reflect.ClassTag[X & Y | X & Z] = X

scala> classTag[Y & X | Z & X]
val res2: scala.reflect.ClassTag[Y & X | Z & X] = Object

@smarter
Copy link
Member

smarter commented Apr 15, 2020

ClassTag[X] gives you the class of the erasure of type X, and the erasure of an intersection/union type is not commutative: scala/scala3#5139 (and we most probably cannot fix this without compromising further the two-way binary interop between scala 2 and dotty). Type inference can mean you get intersections/unions in different orders and therefore different classtags.
In conclusion, ClassTag is evil and shouldn't be used for anything (as I've argued at length before) :).

@smarter
Copy link
Member

smarter commented Apr 15, 2020

(Actually afaik only intersection/compound types have non-commutative erasure, unions are fine I think)

@dwijnand
Copy link
Member

Seeing as implicit ClassTag synthesis isn't user-land code, maybe it should require a user's intervention when given an intersection type? At worst, a lint.

@neko-kai
Copy link

@adamgfraser izumi Tag contains a cls: Class[_] field, unlike native ClassTag it takes the class of the LUB of intersections, instead of the first element, maybe that would work better in your case?

@adamgfraser
Copy link
Author

@neko-kai Good idea! Let me look at that.

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

No branches or pull requests

7 participants