Pre SIP: Replace non-sensical @unchecked annotations

@alvae and @lihaoyi have already articulated quite well many reasons why checkedCast as a method that returns : x.type does not behave like a method. I won’t repeat that here.

I just want to reply to two concrete comments:

Target typing cannot explain what is proposed here.

Until now, target typing can always be explained away as desugaring during typechecking. After typechecking (after elaboration to be precise), the behavior of a program can be fully explained without target typing. For asInstanceOf in particular, it did receive an actual type parameter, and that type parameter will not change anymore. If we move it and assign it to a separate val (for example, in a macro or compiler phase), it will keep that concrete type parameter.

With the proposed behavior of checkedCast, and if it wants to be explained in terms of target typing, this assumption is broken. Even in a macro or a compiler phase, you are not allowed to extract the call in a separate val, as it will cause compile errors that would not be there otherwise. This illustrates that the Match(Apply(_, checkedCast), ...) is magical as a pair of syntactically nested nodes.

This is not hair splitting. It has very concrete consequences that will break people’s code.

Take for example a macro for async/await. Such a macro typically needs to perform some sort of ANF transform, which does mean extracting subexpressions and putting them into vals. The macro would be well-behaved, well-tested, on every possible Tree of the metaprogramming API. And then when a user happens to use x.checkedCast match inside async { ... }, bam! they get a compile error that makes no sense.

To fix that, the macro author will have to add a specific case for Match(Apply(x, checkedCast), ...) in order not to extract that Apply. How do we expect a macro author to know that? Or to think about testing that particular combination of features? We cannot. Macros will get broken, and it won’t the macro authors’ fault; it will be our own, for designing an elaborated form of the language that is not compositional.

This can only explain the cases where a better type is enough to guarantee exhaustivity checking. But the original proposal definitely wants to be able to do things like

val Foo(Bar(x)) = any.checkedCast

or

val List(one, two) = list.checkedCast

which cannot be explained that way. So no, that does not work and we cannot move on :wink:

If we could, then my suggestion from way earlier to give a simple, user-land definition of .checkedCast would have sufficed. As a reminder, it looked like:

extension [S] (x: S) def checkedCast[T](using TypeTest[S, T]): T = x match
  case x: T => x
  case _    => throw MatchError(x)

That one would have been completely explained by target typing as we know it today. Not just the signature but even the implementation!

4 Likes