Warn on erased definitions with ???

[nicolasstucki]

Compiler version

3.0.0-RC1

Minimized example

erased given CanThrow[Ex1] = ???

Expectation

It should emit a warning suggesting the code

import scala.compiletime.erasedValue

erased given CanThrow[Ex1] = erasedValue

[nicolasstucki]

See #11736

[odersky]

I think we have a real and deep question here: How do we tame the unsoundness related to using erased undefined values? They are harmless in matchtypes but dangerous for capabilties. But morally erasedValue and ??? are the same, so warning just for one and not the other falls short.

[nicolasstucki]

??? and erasedValue are not the same, erasedValue cannot be used in all the places where ??? can be used. It also forces the users to write explicitly their intention which will make them think twice about what they are creating.

[nicolasstucki]

Looking at the code, it seems that it might be beneficial to only allow erasedValue.

[japgolly]

The only problem with that is that erasedValue needs an import. Can we move erasedValue to scala/Predef?

[nicolasstucki]

I have been considering something even more drastic. In this system the RHSs of definitions have no meaning at all, we only put some body as a placeholder. It also does not seem to be important if the definition is abstract or not. My suggestion would be to just not have an implementation. Make all of them look like abstract method. We would just need to define the signature which is all we care about.

erased given CanThrow[Ex1]

Furthermore with the erased classes idea we could just write

given CanThrow[Ex1]

[japgolly]

@nicolasstucki There seems to already be precedent for this:

https://dotty.epfl.ch/docs/reference/other-new-features/type-test.html#example

   given typeTestOfZero: TypeTest[Nat, Zero]
   given typeTestOfSucc: TypeTest[Nat, Succ]

[japgolly]

...by "this" I mean declaring a given without specifying a body. I'm assuming that the TypeTest examples could also be written in anonymous form:

   given TypeTest[Nat, Zero]
   given TypeTest[Nat, Succ]

[nicolasstucki]

In that case TypeTest is not erased nor the definition is erased, therefore it is an abstract given that must be implemented by one of the subclasses. The names are of no consequence for this idea.

[odersky]

I have been considering something even more drastic. In this system the RHSs of definitions have no meaning at all, we only put some body as a placeholder. It also does not seem to be important if the definition is abstract or not. My suggestion would be to just not have an implementation. Make all of them look like abstract method. We would just need to define the signature which is all we care about.

Maybe. But I fear that would introduce too many corner cases. Sometimes class bodies are important, for instance because we want to do typelevel computations with the parameters or members of a class.

[nicolasstucki]

In which cases the bodies might be important? I haven't seen any type-level computation using erased that requires the body. The only type-level computations that I can see that require the body are transparent inline definitions, which may be erased.

In case it was not clear, internally we would just generate the dummy ??? implementation and do the same as we do right now.

[japgolly]

it is an abstract given that must be implemented by one of the subclasses

Oh sorry I misread, I thought the compiler was implicitly providing bodies.

Maybe this would be better then:

given CanThrow[Ex1] = erased

// translates to
// erased given CanThrow[Ex1] = scala.compiletime.erasedValue

[nicolasstucki]

The issue with that approach is that erased is a soft modifier. This would require changing it to a proper keyword or having some more complex syntactical rules.