No warning on uncheckable isInstanceOf call

[abgruszecki]

Minimized code

import scala.Option
object Test extends App {
  trait A[+X]
  class B[+X](val x: X) extends A[X]
  object B {
    def unapply[X](b: B[X]): Option[X] = Some(b.x)
  }

  class C[+X](x: Any) extends B[Any](x) with A[X]
  def f(a: A[Int]): Int =
    if a.isInstanceOf[B[Int]] then
      a.asInstanceOf[B[Int]].x
    else
      0
  f(new C[Int]("foo"))
}

Output

Compiles without warning, explodes at runtime.

Expectation

A warning about the .isInstanceOf test should be emitted.

Adapted from https://github.com/lampepfl/dotty/blob/master/tests/neg/i3989c.scala#L1.

/cc @liufengyun it seems that additional tweaking of how GADTs are used for checking .isInstanceOf is necessary.

[liufengyun]

@abgruszecki Nice counter-example. I'm wondering whether the compiler should check that C[X] has two different instantiations of the parent: A[Any] and A[X].

[liufengyun]

I'm wondering whether the compiler should check that C[X] has two different instantiations of the parent: A[Any] and A[X].

I think one justification for this check is the locality of reasoning. If the code only involves A and B, we need to be able to reason about their types based on the definition of just A and B. New definitions should not change the relationship between A and B. Otherwise, the rules will be difficult to understand and compromise usability.

[abgruszecki]

I think we're perfectly capable of local reasoning - we just cannot assume that if a value is of types A[Int] and B[X] for some X, then it must be of the type B[Int]. If we translate the classes to structural types like in our short paper then this becomes clear:

type structA = { type A_X }
// A[X] translated to structA & { type A_X <: X }
type structB = { type B_X; type A_X <: this.B_X }
// B[X] translates analogously to A[X]
// note that forall X, (translated B[X]) <: (translated A[X])

[liufengyun]

From the perspective of soundness, there can be many designs that make sense. However, IMHO, the design with the check is more intuitive and usable than others in practice.

[liufengyun]

we just cannot assume that if a value is of types A[Int] and B[X] for some X, then it must be of the type B[Int].

Here it depends on how we read the contract below:

trait A[+X]
class B[+X](val x: X) extends A[X]

If we think from programmer's perspective, we may think the encoding captures only part of the contract. A possible enhancement of the contract is the following:

• forall X, B[X] <: A[X]
• forall x, X, x: A[X] and x: B[?] , then x: B[X].

[abgruszecki]

If you're suggesting to forbid definitions like C then I'm not sure if it can be easily done. If we take a look at the original issue #3989, then the last time this was discussed it was concluded that the loss of expressivity from forbidding those definitions was untenable, in particular because standard library depended on being able to create such definitions.

[LPTK]

Here it depends on how we read the contract below:

trait A[+X]
class B[+X](val x: X) extends A[X]

It's easy to misread this when the types are named the same. The issue becomes more apparent if you use different names:

trait A[+X]
class B[+Y](val x: Y) extends A[Y]

Now we can see there is no reason that B's Y should be the same as A's X.

A possible solution I've always found attractive would be to bring back type class parameters, which are analogous to val class parameters in that they make the value/type public and visible from other classes.

trait A[type +X]
class B[type +X](val x: X) extends A[X]

Above, A now has a type member X which represents the "true" underlying type argument, so that for all a: A[T], we have a.X <: T. The same goes for B, so both must now denote the same type.

[dwijnand]

bring back type class parameters, which are analogous to val class parameters in that they make the value/type public and visible from other classes.

Would that give all type members the ability to declare their variance, or only type class parameters?

If we think from programmer's perspective, we may think the encoding captures only part of the contract. A possible enhancement of the contract is the following:

• forall X, B[X] <: A[X]
• forall x, X, x: A[X] and x: B[?] , then x: B[X].

I assume that today the user could (or should) be able to enforce that X doesn't get multiple instantiations by making B final or, harder, make A sealed (and reason about the known children).

Also, are those two enhancements different? I couldn't think of an example that satisfies one and not the other...

[abgruszecki]

bring back type class parameters, which are analogous to val class parameters in that they make the value/type public and visible from other classes.

Would that give all type members the ability to declare their variance, or only type class parameters?

IIRC, variance of type here affects meaning of applying the appropriate parameter, I'm not sure if variance annotation on normal type parameters makes sense.

If we think from programmer's perspective, we may think the encoding captures only part of the contract. A possible enhancement of the contract is the following:

• forall X, B[X] <: A[X]
• forall x, X, x: A[X] and x: B[?] , then x: B[X].

I assume that today the user could (or should) be able to enforce that X doesn't get multiple instantiations by making B final or, harder, make A sealed (and reason about the known children).

Also, are those two enhancements different? I couldn't think of an example that satisfies one and not the other...

You mean Fengyun's and Lionel's suggestion? Lionel is arguing for something similar to what Fengyun is suggesting, but with the ability to opt into the behaviour. There's also the matter that Lionel is proposing to make type parameters with type actual type members. So there's some differences between the two.

[LPTK]

@dwijnand

Would that give all type members the ability to declare their variance, or only type class parameters?

No. In my proposal, just like in current Scala, a variance annotation affects the variance of the type constructor, that's it. Type members have no business being variant as far as I can tell. If you disagree, would you be able to describe a reasonable semantics for variant members, as well as interesting use cases for them?

[dwijnand]

You mean Fengyun's and Lionel's suggestion?

No (and it's more of an aside) I meant between Fengyun's two "forall" examples - I thought they must intended different things but I couldn't think of a differing example.

Type members have no business being variant as far as I can tell. If you disagree, would you be able to describe a reasonable semantics for variant members, as well as interesting use cases for them?

I don't know. 😄 There was a desire to unify type parameters with type members, with type parameters desugaring to type members, but that leaves nowhere for variance to be defined, right? And then that project in Dotty was aborted and I haven't found out why. With DOT only having type member, I guess we never model variance in any of the soundness proofs? Do any of the DOT extensions add variance?

[LPTK]

Yeah you are right that at some point, IIRC, Dotty had a concept of type parameters desugaring into type members which had variance associated to them. But I think that was a conceptual mistake, or at the very least a conflation of unrelated concepts.

With DOT only having type member, I guess we never model variance in any of the soundness proofs? Do any of the DOT extensions add variance?

I think declaration-site variance of type constructors is not essential, but more of a derived concept. It can be even defined without reference to an "intrinsic" concept of type parameters. In DOT, we'd consider a definition class C[+A] to simply be defining a type C <: { type A } with type member A along with a notationC[T] which desugars to C & { type A <: T}. Notice that the type member A has no concept of variance, and that other references to C such as C & { type A = T} and even C & { type A >: T} still make sense. So for simple cases like this, declaration-site variance is just notational convenience. (It becomes more tricky when higher-kinded types and high-order subtyping is involved, though.)