Pre SIP: Replace non-sensical @unchecked annotations

The Problem

There are ongoing efforts to tighten up pattern matching to make refutable patterns static errors. For instance, consider:

  def xs: List[Any] = ???
  val y :: ys = xs

This compiled without warning in 3.0, became a warning in 3.2, and we’d like to make it an error in one of the next 3.x versions. As an escape hatch we recommend to use @unchecked:

-- Warning: ../../new/test.scala:6:16 ------------------------------------------
6 |  val y :: ys = xs
  |                ^^
  |pattern's type ::[Any] is more specialized than the right hand side expression's type List[Any]
  |
  |If the narrowing is intentional, this can be communicated by adding `: @unchecked` after the expression,
  |which may result in a MatchError at runtime.

Similarly for non-exhaustive matches, where we also recommend to put @unchecked on the scrutinee.

But @unchecked has several problems. First, it is ergonomically bad. For instance to fix the exhaustivity warning in

  xs match
    case y :: ys => ...

we’d have to write

  (xs: @unchecked) match
    case y :: ys => ...

Having to wrap the @unchecked in parentheses feels clunky and unnatural.

Second, and more importantly, the word unchecked is a misnomer. After all, the pattern is checked, but it is done at runtime. This is particularly bad since there is another usage of @unchecked which means the exact opposite:

  xs match
    case _: List[Int @unchecked] => 

Here, @unchecked means not checked at runtime: The compiler trusts the user that this a List[int]; it might insert casts to Int but not at the place where the pattern is matched.

The Proposal

I propose to fix both problems by deprecating @unchecked in the usage where it means “checked at runtime” and replacing it with a new magic method on Any, named checkedCast, or something similar.

So the previous examples would become:

  def xs: List[Any] = ???
  val y :: ys = xs.checkedCast

  xs.checkedCast match
    case y :: ys => ...

The Spec

The rules for checkedCast would be similar to the current @unchecked annotation on selectors. checkedCast could be a synthetic method on Any defined like this:

  def checkedCast: this.type = this

Then when it comes to exhaustivity or refutability checking, a scrutinee ending with .checkedCast would silence all warnings or errors. Furthermore, .checkedCast calls would be removed after
the pattern matching translation.

A Possible Refinement

One tricky aspect of val definitions is this:

  val x: Any = ???
  val (y: Int) = x: @unchecked // works
  val y: Int = x: @unchecked   // gives a type error: found: `Any`, expected: `Int`

Line 2 is syntactically a pattern match, where we allow refutable patterns, so the code typechecks.
By contrast line 3 is a val definition, where we do not allow this. I believe with checkedCast we don’t need such hair splitting anymore. So we could allow both of the following two definitions:

  val (y: Int) = x.checkedCast
  val y: Int   = x.checkedCast

The general rule would be that checkedCast can also heal type errors. In an expression
e.checkedCast, if the type of e does not conform to the expected type XT, translate the expression to

e.checkedCast match
  case $x: XT => $x

and proceed as before.

Why not use asInstanceOf instead?

asInstanceOf is a low-level cast which might not necessarily check missing cases. Furthermore, one cannot in general simply leave out the type argument of an asInstanceOf. if you write x.asInstanceOf without a type argument this will often work, but sometimes the missing type argument will be inferred to Nothing in which case you get a runtime error since x cannot be cast to Nothing. This is typically if the expected type of the asInstanceOf is underdefined. By contrast, an underdefined expected type would lead to a warning or error in the match expansion of checkedCast.

Why not use a new method based on TypeTest instead?

Essentially, simplicity. One method is easier to remember than two. And they do morally the same thing. Also, it might be hard to encode the precise meaning of “case x: XT is a pattern match that does not produce errors or warnings” into a testable type.

Alternative names

We could also consider other names instead of checkedCast. Maybe simply checked, or narrowed?

4 Likes

I believe that asMatchable (from compiletime package) already serves this purpose in a way - i.e it recovers the ability to match on a value typed as Any, therefore allowing us to use Array extractor on an IArray - a nominally unrelated type.

perhaps we can expand its meaning to mean “silence warnings for refutable pattern”, and even “generate conformance assertion”

2 Likes

Naming is hard, except for this one.

  def xs: List[Any] = ???
  val y :: ys = xs.!!!

Nothing says, “Danger, Will Robinson!!!”, like the !!! operator. Probably it’s already highlighted in the IDE.

I’m pleased that after all these years, this name finally found its ideal referent.

As a footnote on naming, I think we users of the language just employ the idioms as we pick them up, and do not give the name itself much thought, once we understand how it works (or does not work).

Not sure about !!!. What do others think???

One other aspect this proposal does not address is if we have a non-exhaustive pattern matching closure. In that case, the best thing we can do is something like

xs.map:
  _.checkedCast match
     case P1 => ...
     case P2 => ...

I like that it is a method as the syntax with a dot is less cluttered than the annotation syntax @ (or it could be a soft keyword before match as in e checkedCast match

I think checkedCast is a bit too cryptic and perhaps we can find something closer to explaining the intent. Perhaps unsafe as it shows that it might blow at runtime?

e.unsafe match
  case ...

or as a soft keyword

e unsafe match
  case ...

other names I considered: runtime, runtimeType, dynamic, dynamicType, nowarn, …
I’d like it to be single, short word that is without camelCase. (I think !!! is very cryptic and it is not easy to say, looks like a shout out)

The good thing with a soft keyword compared to a magic method is that it wont clutter Any. On the other hand a magic method is discoverable using tab in repl and in IDE.

6 Likes

So far, I like unsafe best of the proposed names. I worry that a feature that can “heal type errors” will be abused (I deal with students who already abuse instanceof/asInstanceOf); it needs a scary name (though maybe not as scary as !!!).

3 Likes

Not always, consider:

val xs: List[Any] = Nil
val ys = (xs: @unchecked) match
  case xs: List[Int] => xs

The @unchecked here is enough to suppress all warnings without adding another @unchecked on Int.

Yes, that makes it even worse!

:jack_o_lantern:

Worth noting that -Yunsafe was recently deemed a bit cryptic and threatening.

Since Scala is supposed to be a scalable language, we ought to scale unchecked with -language:unsafe, which would apply type healing to all values. (All healing remedies come with fine print explaining why they are also unsafe.)

Scala should scale from type-unsafe scripting, through semi-typed unit testing, to typesafe code for PRs, modulo explicit usage of unsafe aka the pumpkin operator. Instead of type- or test-driven development, students can learn type-lax development: in TDD, you write a test that fails; in TLD, you remove unsafe until you get a type error.

1 Like

In Akka typed actorRef there are narrow and unsafeUpcast methods.

And in Kotlin the unsafe cast is as, and a safer one is as?

narrow should be seen as an artefact of the way Akka is implemented in Scala 2.13 (and earlier).

The note on the concrete implementation of narrow in Behavior.scala states:

  /**
   * Narrow the type of this Behavior, which is always a safe operation. This
   * method is necessary to implement the contravariant nature of Behavior
   * (which cannot be expressed directly due to type inference problems).
   */
  final def narrow[U <: T]: Behavior[U] = this.asInstanceOf[Behavior[U]]

Ideally (correct me if I’m wrong), Behavior[T] should have been declared as contravariant in its type parameter T, but that wasn’t possible do to limitations in type inference in the Scala 2 compiler.

If people are against adding a method then we have to consider the consequences of a new keyword, e.g. for the val definition with pattern:

val try y :: ys = xs

I use try here, as the semantics are quite clear - try the pattern or throw, but suppose it could be dyn or check. However this now requires inventing a separate syntax for ignoring exhaustivity for a standard pattern match.

If we moved the keyword to instead be a modifier for the expression, this would be problematic. It might be nice in the simple case, e.g. val y :: ys = dyn xs, but with the current syntax precedence rules then we would require more parens everywhere.

e.g. this looks hideous

(dyn xs) match
  case y :: ys => ...

I think adding a keyword to modify match would be problematic, today we can do

e.match
  case ...

so e.unsafe match ... would then be ambiguous.

ok, thanks. But having a magic method called unsafe on Any is ok?

1 Like

Perhaps a bit scary but less cryptic in my view compared to checkedCast etc. I’d like something that relates to the actual runtime check that, while silencing warnings, might blow up at runtime…

If we’re going to add syntax, how about case val y :: ys = xs?

1 Like

We need a solution that works for both refutable patterns in vals and non-exhaustive patterns in matches. So any tweaks of vals alone are not enough.

The method call notation does not look right to me, if we’re defining its semantics that way. The problem is that it won’t behave as a method at all. It will have a different meaning depending on it’s syntactic position. For example:

x.checkedCast match { ... }

won’t be the same as

{ val y: x.type = x; y.checkedCast } match { ... }

or

val y: x.type = x.checkedCast
y match { ... }

It would make sense as a method call if it were defined in user-space as something like:

extension (x: S)
  def checkedCast[T](using test: TypeTest[S, T]): x.type & T =
    test.unapply(x).getOrElse(throw MatchError(x))

In that case, it would naturally work for the val x: Int = someAny.checkedCast, since type inference would infer T = Int.

It would not directly work for a match scrutinee (including for pattern val), but perhaps that’s where type inference would be nudged to do what’s expected for that particular method. Of course that falls into @odersky’s earlier comment:

which maybe kills this idea. At least, it restricts it to cases where matching the top-level unapply’s type parameter is enough to guarantee matching the whole pattern. For example

val Left(x) = someEither.uncheckedCast // ok with inference providing [Left]

Regardless, using the method notation for something that does not behave at all like a method seems problematic.


We should also evaluate the actual benefit of having this at all. Deliberately telling the compiler to ignore exhaustivity in order to turn write what amounts to an assertion is not something we do every day. It’s certainly not something we would encourage Scala users to do on a regular basis. The compiler is full of these things because its ADTs have very complex invariants involving external data structures and even state (at what phase we are). A typical application or even library codebase hopefully have ADTs whose invariants are self-contained. In those situations, that kind of checked cast would be a code smell more often than not.

As one data point: Lichess’ server contains 150k+ lines of Scala 3.3.1 code, and not a single @unchecked!

6 Likes

I believe the relative rarity of @unchecked is because we currently do only a very superficial job of refutability and exhaustiveness checking. So there is usually a way around this without using @unchecked. But as we tighten the screws, this will become much more of a problem.

Also Lichess is just one example. As a counterpoint I already count 334 uses of @unchecked in the dotty compiler, and I would argue that this is not due to sloppy coding,

I disagree that methods cannot be magic. asInstanceOf, isInstanceOf, eq and ne are all magic in the sense that they cannot be expressed as user code.

1 Like

eq, ne and even asInstanceOf, like Int.+ and virtually all other primitives, are only magic in their implementation. We cannot implement them in user space. But their signature, and they behavior at call site, is completely consistent with how regular methods behave.

isInstanceOf is slightly different, in that the shape of its type parameter is checked and taken into account by the compiler. But IMO that’s only because we did not have TypeTest as a primitive to begin with. If we had, we could have perfectly well defined the signature of isInstanceOf as:

def isInstanceOf[T](using test: TypeTest[this.type, T]): Boolean =
  test.unapply(this).isDefined

So I don’t think any of these is a strong enough precedent for what checkedCast would introduce in terms of magic.

5 Likes