Add variants of compiletime.erasedValue

Author: odersky

compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

@@ -462,15 +462,13 @@ extension (sym: Symbol)
 
   /** Does this symbol allow results carrying the universal capability?
    *  Currently this is true only for function type applies (since their
-   *  results are unboxed) and `erasedValue` since this function is magic in
-   *  that is allows to conjure global capabilies from nothing (aside: can we find a
-   *  more controlled way to achieve this?).
+   *  results are unboxed) and `caps.{$internal,unsafe}.erasedValue` since
+   *  these function are magic in that they allow to conjure global capabilies from nothing.
    *  But it could be generalized to other functions that so that they can take capability
    *  classes as arguments.
    */
   def allowsRootCapture(using Context): Boolean =
-    sym == defn.Compiletime_erasedValue
-    || defn.isFunctionClass(sym.maybeOwner)
+    defn.capsErasedValueMethods.contains(sym) || defn.isFunctionClass(sym.maybeOwner)
 
   /** When applying `sym`, would the result type be unboxed?
    *  This is the case if the result type contains a top-level reference to an enclosing

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -576,7 +576,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  @param  args the type arguments
      */
     def disallowCapInTypeArgs(fn: Tree, sym: Symbol, args: List[Tree])(using Context): Unit =
-      def isExempt = sym.isTypeTestOrCast || sym == defn.Compiletime_erasedValue
+      def isExempt = sym.isTypeTestOrCast || defn.capsErasedValueMethods.contains(sym)
       if !isExempt then
         val paramNames = atPhase(thisPhase.prev):
           fn.tpe.widenDealias match

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -1004,9 +1004,11 @@ class Definitions {
     @tu lazy val Caps_Capability: ClassSymbol = requiredClass("scala.caps.Capability")
     @tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet")
     @tu lazy val CapsInternalModule: Symbol = requiredModule("scala.caps.internal")
+    @tu lazy val Caps_erasedValue: Symbol = CapsInternalModule.requiredMethod("erasedValue")
     @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
     @tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
     @tu lazy val Caps_unsafeAssumeSeparate: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumeSeparate")
+    @tu lazy val Caps_unsafeErasedValue: Symbol = CapsUnsafeModule.requiredMethod("unsafeErasedValue")
     @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
     @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains")
     @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl")
@@ -1559,7 +1561,7 @@ class Definitions {
     Set(StringClass, NothingClass, NullClass) ++ ScalaValueClasses()
 
   @tu lazy val capsErasedValueMethods =
-    Set[Symbol]()
+    Set(Caps_erasedValue, Caps_unsafeErasedValue)
   @tu lazy val erasedValueMethods =
     capsErasedValueMethods + Compiletime_erasedValue
 

compiler/src/dotty/tools/dotc/typer/Synthesizer.scala

@@ -231,7 +231,7 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
     case PreciseConstrained(tp, true) =>
       if tp.isSingletonBounded(frozen = false) then
         withNoErrors:
-          ref(defn.Compiletime_erasedValue).appliedToType(formal).withSpan(span)
+          ref(defn.Caps_erasedValue).appliedToType(formal).withSpan(span)
       else
         withErrors(i"$tp is not a singleton")
     case _ =>
@@ -240,7 +240,7 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
   val synthesizedPrecise: SpecialHandler = (formal, span) => formal match
     case PreciseConstrained(tp, false) =>
       withNoErrors:
-        ref(defn.Compiletime_erasedValue).appliedToType(formal).withSpan(span)
+        ref(defn.Caps_erasedValue).appliedToType(formal).withSpan(span)
     case _ =>
       EmptyTreeNoError
 

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -2384,7 +2384,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
       untpd.ValDef(
           CanThrowEvidenceName.fresh(),
           untpd.TypeTree(defn.CanThrowClass.typeRef.appliedTo(tp)),
-          untpd.ref(defn.Compiletime_erasedValue))
+          untpd.ref(defn.Caps_erasedValue))
         .withFlags(Given | Final | Erased)
         .withSpan(expr.span)
     val caughtExceptions =

library/src/scala/caps/package.scala

@@ -110,6 +110,13 @@ object internal:
    */
   final class inferredDepFun extends annotation.StaticAnnotation
 
+  /** An erasedValue issued internally by the compiler. Unlike the
+   *  user-accessible compiletime.erasedValue, this version is assumed
+   *  to be a pure expression, hence capability safe. The compiler generates this
+   *  version only where it is known that a value can be generated.
+   */
+  def erasedValue[T]: T = ???
+
 end internal
 
 @experimental
@@ -135,4 +142,11 @@ object unsafe:
    */
   def unsafeAssumeSeparate(op: Any): op.type = op
 
+  /** An unsafe variant of erasedValue that can be used as an escape hatch. Unlike the
+   *  user-accessible compiletime.erasedValue, this version is assumed
+   *  to be a pure expression, hence capability safe. But there is no proof
+   *  of realizability, hence it is unsafe.
+   */
+  def unsafeErasedValue[T]: T = ???
+
 end unsafe