Allow references to erased values in types

[mbovel]

This PR allows references to erased values from within types. This should be safe as types are also erased.

Motivation

@asunluer found that the following code (tests/run/erased-inline-product.scala) fails to compile:

import scala.compiletime.{erasedValue, summonInline, error}

inline def sizeTuple[T <: Tuple](): Long =
  inline erasedValue[T] match
    case _: EmptyTuple => 0
    case _: (h *: t)   => size[h] + sizeTuple[t]()

inline def sizeProduct[T <: Product](m: scala.deriving.Mirror.ProductOf[T]): Long =
  sizeTuple[m.MirroredElemTypes]()

inline def size[T]: Long =
  inline erasedValue[T] match
    case _: Char    => 2
    case _: Int     => 4
    case _: Long    => 8
    case _: Double  => 8
    case p: Product => sizeProduct(summonInline[scala.deriving.Mirror.ProductOf[p.type]])
    case _          => error(s"unsupported type")

@main def Test =
  println(size[(Int, Long)])

This currently fails with:

$ scala tests/run/erased-inline-product.scala
Compiling project (Scala 3.7.3, JVM (17))
[error] ./tests/run/erased-inline-product.scala:21:11
[error] value p is unusable in method Test because it refers to an erased expression
[error] in the selector of an inline match that reduces to
[error] 
[error] {
[error]   erased val $scrutinee1: (Int, Long) =
[error]     scala.compiletime.erasedValue[(Int, Long)]
[error]   erased val p: (Int, Long) = $scrutinee1
[error]   {
[error]     sizeProduct[(p : (Int, Long))](
[error]       scala.compiletime.summonInline[scala.deriving.Mirror.ProductOf[p.type]])
[error]   }
[error] }
[error]   println(size[(Int, Long)])

which is unfortunate, because this looks like a useful pattern. I don’t know of a better way to decompose a Product in an inline function, and references to erased values from within types should be safe.

As a workaround, we tried introducing a type variable using p & Product, which is demonstrated in tests/run/erased-inline-product-2.scala. That version already works without any compiler changes, but it feels more fragile and less readable.

We could probably also use match types, but we would prefer to stay at the term level if possible.

[mbovel]

🤖 ChatGPT review

[sjrd]

For a path-dependent type to be sound, we need evidence that the value in the path can be created. That is not the case for erased values, I think.

[mbovel]

For a path-dependent type to be sound, we need evidence that the value in the path can be created. That is not the case for erased values, I think.

Ah. Could we maybe use CheckRealizable.realizability (as used in checkRealizable) to only allow erased values in paths if there type is known to be inhabited?

[mbovel]

Another simpler workaround; removing the <: Product bound for the type parameter T in sizeProduct works in that case:

import scala.compiletime.{erasedValue, summonInline, error}

inline def sizeTuple[T <: Tuple](): Long =
  inline erasedValue[T] match
    case _: EmptyTuple => 0
    case _: (h *: t)   => size[h] + sizeTuple[t]()

inline def sizeProduct[T](m: scala.deriving.Mirror.ProductOf[T]): Long =
  sizeTuple[m.MirroredElemTypes]()

inline def size[T]: Long =
  inline erasedValue[T] match
    case _: Char    => 2
    case _: Int     => 4
    case _: Long    => 8
    case _: Double  => 8
    case _: Product => sizeProduct[T](summonInline[scala.deriving.Mirror.ProductOf[T]])
    case _          => error(s"unsupported type")

@main def Test =
  assert(size[(Int, Long)] == 12)

[mbovel]

@odersky mentioned that erased values should always be checked for realizability.

But currently the following compile:

import scala.compiletime.erasedValue

inline def f() =
  inline erasedValue[String & Int] match
    case _: String => "String"

@main def Test = println(f())

Isn't that a problem?

[odersky]

No, there's a special exception for inline matches. If you use erasedValue elsewhere you'll get an error

  erased val x = compiletime.erasedValue[Int & String]

-- [E217] Type Error: ../../new/test.scala:6:40 --------------------------------
6 |  erased val x = compiletime.erasedValue[Int & String]
  |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |          right-hand-side of an erased value fails to be a pure expression
  |
  | longer explanation available when compiling with `-explain`
1 error found

[mbovel]

Okay, but that's still a problem inside inline matches, in its current state this PR would allow:

import scala.compiletime.erasedValue

class Box[T]

trait T:
  type L

class A extends T:
  type L <: Int

class B extends T:
  type L >: String

inline def f() =
  inline erasedValue[A & B] match
    case x: (A & B) =>
      val y: String = "String"
      val z: x.L = y
      z: Int

@main def Test =
  println(f().abs)

So we need an additional inhabitance check, don't we?

[mbovel]

I tried to only allow references to erased values if their types are realizable. This allows to accept the motivating example from this PR, but to still reject the bad bounds example above.

However, it would accept:

import scala.compiletime.erasedValue

class Box[T]

inline def f() =
  inline erasedValue[String & Int] match
    case x: (String & Int) =>
      val y =  Box[x.type]
      y

@main def Test =
  println(f())

because apparently String & Int is realizable? 🤔

[odersky]

Yes, as long as intersections don't have any type members we don't care.