@uncheckedVariance soundness

Here is the documentation for @uncheckedVariance:

An annotation for type arguments for which one wants to suppress variance checking.

This seems rather lacking. What about soundness? In which cases can @uncheckedVariance lead to unsound compiler behavior? In which cases is it safe to use? Without documentation, there are even concrete use cases for which it is not easy to find out whether using @uncheckedVariance is safe.

I couldn’t find anything in the spec about this either.

It’s plain unsafe, like @unchecked in pattern matching. It’s all basically asInstanceOf.

1 Like

I understand it’s unsafe in general. But

  1. asInstanceOf is properly documented:

Cast the receiver object to be of type T0.
Note that the success of a cast at runtime is modulo Scala’s erasure semantics. Therefore the expression 1.asInstanceOf[String] will throw a ClassCastException at runtime, while the expression List(1).asInstanceOf[List[String]] will not. In the latter example, because the type argument is erased as part of compilation it is not possible to check whether the contents of the list are of the requested type.

  1. The cases when asInstanceOf actually lead to unsoundness in code are relatively straightforward.

In contrast, @uncheckedVariance, while “plain unsafe”, is basically undocumented, as well as being more subtle than asInstanceOf.

Finally, there are valid use cases for both (unfortunately), otherwise they would not be included. But with the current state of documentation, finding out whether a use-case is valid for @uncheckedVariance is sometimes based on guesswork as to how it interacts with type checking.

A language and its features really only go as far as they can be trusted. And that trust is established via documentation of some sort (otherwise, who knows how it could change in the future?). Currently, @uncheckedVariance is more dangerous and painful to use than it has to be, due to a lack of documentation, even for potentially legitimate uses.

3 Likes

The spec defines variance checking and the object-private exception.

The doc for IterableOps has a “variance note”. There may be more info in the source than is represented in the public API.

I just deleted a random annotation and it still compiled, so that was an unsatisfying experiment.

Below is an answer by an LLM assistant about when it’s safe to use @uncheckedVariance:

Only when you can prove something the compiler can’t: that the variance violation is never exercised at runtime.

Concretely, it’s safe when all of these hold:

  • The annotated type parameter is used only in positions that are logically variance-safe for the actual concrete instances you allow.
  • No code can ever observe a value at the wrong type (no casts, pattern matches, or method calls that would rely on the forbidden direction).
  • The abstraction boundary is tight: subclasses, overrides, and future extensions cannot introduce unsound uses.

Typical safe cases:

  • Phantom types (the value doesn’t actually contain the type).
  • Private/internal fields where construction is fully controlled.
  • GADT-like encodings where invariants are enforced by constructors.

If any external or future code could break the invariant, it’s not safe.

I think this summarizes typical beliefs about when @uncheckedVariance is safe to use. But is that actually correct? Can I trust this?

1 Like

Perhaps Scala has found its mascot.

@som-snytt how though? How can I put out this “fire”, other than trying to raise attention here? I’d love any suggestion.

Here is the issue as I see it. Scala has only a handful of primitives that can introduce unsoundness. It seems to me that these primitives should be some of the best documented. @uncheckedVariance is one of these primitives, but is mostly unspeced.

It’s not just about making it easier to learn and use the language, but more fundamentally about clearly specifying the behavior of such primitives, as well as their interactions with the rest of the language (like subtyping in this case).

Currently, I feel like we are in “undefined behavior” territory, à la C.

2 Likes

Because we probably are.

Use case of all of these annotations is “Either there is a bug in compiler or I got into type system limitation where there is a guarantee I know of but cannot express. Trust me on this, if there will be a runtime error, it’s on me”.

On JVM an undefined behavior usually is “just” an unaddressable exception (you can catch it, but then what? There might be no way to reasonably address it). Not the same league like C, but still. And these annotations, if you failed to implement yourself the guarantees that you just opted out of using, will result in some error. What error, when, will it even be visible instead of some silent failure? Who knows!

There is no list of when to use them, because if you don’t know JVM well enough to guess what would happen, you should probably not use it. And of you do, then you probably only use it as last resort, followed by a lot of unit tests to make sure that they’re is some “manual” checking that would avoid the error in the runtime after the type erasure kicked in.

I guess it won’t help a lot but I remember that I had to use it once to trick the compiler choosing implicits. The problem was roughly that the implicit was for a trait which had a type parameter which had to be invariant. The implicit was based on this type parameter and since it had to work in a covariant way I used this annotation. Back then I could reason that this is sound as it was a closed world scenario and I knew there won’t be ever any subclasses which accidentally could have been chosen instead. I guess I could have worked around this problem in a more complex way but using this annotation kept it simple.

As said in the beginning, probably doesn’t help a lot besides that when you use it, you need to reason yourself. the compiler will shoot you in the foot as demanded if your reasoning is wrong.

Indeed, we definitely are in undefined behavior territory, exactly like C. But, you’ll say, Scala can’t make demons fly out of your nose, so it can’t be “true” UB!

The thing is, C cannot, in fact, do that either. Not because the C language standard prevents it, but because the OS won’t let your process do that! UB is only ever up to the security/capability boundaries of the underlying platform.

Likewise, the Scala language standard doesn’t preclude nasal demons in case of wrong casts. Anything can happen as far as Scala is concerned. But “anything” is bounded by the security boundaries of the JVM/JS/Wasm/Native platform, depending on what you target.

2 Likes

In retrospect, that was not the right point. Sorry about that. Let me try again.

Undefined behavior is one thing; undefined undefined behavior is another. It’s one thing to have clearly labeled escape hatches with limited scope that are rigorously documented, like Rust does. It’s another thing altogether to have escape hatches that are not even documented as such, and whose behavior is unspecified.

Anyways, since we are currently in the latter situation, can someone tell me whether it is always fine to use @uncheckedVariance on phantom type parameters? Perhaps we can build a body of precedent for Scala in a similar way to case law.

If you have a type parameter, annotate it with `@uncheckedVariance`, Scala would belive you that it’s co-/contravariant, even when under the hood it’s used in something marked as invariant.

If it’s an actual phantom type parameter, then it’s not used anywhere in the runtime, so there will be no runtime error related to casting. But it should not cause an error that needs suppression with @uncheckedVariance.

But if this is used as e.g. implicit evidence, that some code uses to decide whether it can perform asInstanceOfthen it might cause an issue in seemingly unrelated part of code.

So whether or not a phantom type parameter can be safely casted when is entirely context dependent. With no annotation compiler would do that analysis with some possible false negatives. You can use annotation to mark something as false negative, but bo general advice can be made other than “it’s safe if you prove it is, and keep proving that anew after each change to that code”.

1 Like

How? How can I prove something is safe, or behaves a certain way, without having a reference for its behavior? The best I can do is run the code and observe the result. But that only provides me with a proof for that exact code. It doesn’t generalize.

That is my whole point. There is currently no way to do provide general proofs. Even if the context is known. I can come up with a proof according to the beliefs I have about how Scala behaves. But what if Scala actually behaves differently?

Sure, if I try out enough stuff, I will eventually feel confident enough in my model for a limited fragment of the semantics, without any guarantee that it won’t change in the future. But that is not what we want from a language. The whole point of a language is its semantics (in the general sense). That is why language documentation is important.

If you understand variance well, you know everything you need to know to tell the compiler you know better than it does.

If you don’t, it’s not safe to use the annotation even if it gives you a mini-tutorial.

The challenge is simply to understand variance and if the compiler complains about variance to think very carefully about whether it is a false concern given constraints you can’t express to the compiler (or which it can’t understand). You don’t need a “reference for its behavior” beyond understanding how the JVM handles casting. @uncheckedVariance a special case of asInstanceOf where you only are allowed to effectively perform the cast if the only error is that the variance doesn’t match. If the variance corresponds, eventually, to some type, and that type ends up wrong, then when you try to use it you’ll get a ClassCastException or the like, most likely.

One case it comes up (see this StackOverflow question, for instance) is where you’re trying to abstract over mutable-collection-like and immutable-collection-like classes.

But there is no shortcut or cheat. To assess the correctness of variance checking, one must variance deeply enough. If you do, you already know when the compiler is getting it wrong, and if you don’t, you’d better trust the compiler that what you’re trying to do is likely to be unsound.

An annotation that says, “I understand variance better than the compiler–trust me” isn’t the right place to put a tutorial on how variance works, and as to what can go wrong, there isn’t that much to say other than “depending on details, pretty much anything that can go wrong when the actual type doesn’t match the expected type”.

2 Likes

Is that a promise? I’d love to believe it. But I have had this experience many times over the years now, where such claims turned out to be wrong, and there is no easy way for me to know whether it’s a bug in the compiler, or whether someone will decide it’s actually intended.

Well then, using it for phantom type parameters should never cause issues, right?

But consider that @uncheckedVariance widens the set of expressible type hierarchies. So there is a possibility of it interacting in an unexpected way with anything that works with types. Type checking, type inference, subtyping, type aliases, binaries, etc.

Can you tell, without doing any experiments, whether and how each of these might interact with hierarchies that are expressed using @uncheckedVariance? It might seem far-fetched a priori that there would be any unexpected interaction. But without documentation, any of these is a possibility.

For (an arguably contrived) example, can you tell what the compiler will output for the code below, without running it?

import scala.annotation.unchecked.uncheckedVariance

sealed trait A
sealed trait B extends A

sealed trait Foo[T >: B <: A]
type Bar[+T >: B <: A] = Foo[T @uncheckedVariance]

val a: Bar[B] = ???
val _: Bar[A] = a
val _: Foo[A] = a

It’s a definition of what it means to understand variance well, and if the compiler breaks it as a definition, it’s a compiler bug. (That is: if you have things correct and you have told it to trust you, it is a compiler bug for things to break anyway.)

The first val _ should work because you told it Bar is covariant, and A >: B so Bar[A] >: Bar[B].

I can’t predict whether the second one will work. On the one hand, Bar[A] is just Foo[A] according to the typing (with variance details suppressed). So you ought to be able to assign one Foo[A] to another. On the other hand, the A in Bar[A] isn’t necessarily a real A, it’s a _ <: A. So it might fail.

My guess is it will fail, based on it turning off variance checking when saying a Bar is a type of Foo. That’s what the type X = Y thing means. Once you have an X with its own type parameters, you’d follow the rules for its parameters first, I think. And here you have Foo, A needing an exact match but the RHS resolves to Foo, _ <: A, which is a fail.

But this isn’t a feature of the annotation itself–this has to do with how the compiler thinks about generic type parameters in typedefs vs. the underlying type. That should be documented somewhere. (If it is, I don’t know where it is, though.)

(You can’t directly apply my asInstanceOf logic here, because it’s at the type level, and type assignments are not exactly equivalent to text substitution of the RHS for the LHS. For instance, how types are searched depends on the LHS, not the RHS.)

(Addendum: whether or not this is sound depends on what else it interacts with. As it is, it’s markers, so anything is sound, even val b: Foo[B] = (new Foo[A] {}).asInstanceOf[Foo[B]]. But if the marker was invariant because it was used for something where it matters, then it might eventually lead to a runtime error.)

I think you have shifted this argument towards the abstract idea of overriding the compiler’s variance checking. In that case, yes, understanding variance is sufficient. But in practice, to “tell the compiler”, @uncheckedVariance must be used. And to understand how the latter works, it is not sufficient in all cases to understand how variance works. I think my previous example proves that point.

Agreed. That is basically my main point. This should be documented somewhere. But type aliases are not documented at all, except indirectly in the spec. Moreover, this particular behavior of type aliases is triggered by @uncheckedBehavior. And I doubt it’s possible to deduce it even from the full Scala spec.

Let’s consider a less contrived example:

import scala.annotation.unchecked.uncheckedVariance

// An arbitrarily complex type hierarchy could be used here;
// an almost trivial one is used for simplicity.
sealed trait A
sealed trait B extends A

// This defines a theoretically sound "mirroring augmentation" of the hierarchy;
// it's impossible to define in general without @uncheckedVariance.
sealed trait Pos[+T >: B <: A]
sealed trait Neg[-T >: B <: A] extends Pos[T @uncheckedVariance]

You might be able to foresee potential issues with this definition, but I don’t think it’s easy to do with confidence - even with knowledge of the spec. Once more, understanding variance is insufficient.

For the sake of this thread’s completeness, here is the issue with the definition from my previous post:

summon[Neg[A] <:< Neg[B]] // Works
summon[Neg[B] <:< Pos[B]] // Works
summon[Neg[A] <:< Pos[B]] // Doesn't

So subtyping transitivity is lost.

1 Like