Update cross-stage safety nomenclature

Before `3.0` we experimented with the Phase Consistency Principle (PCP)
which was described in [A practical unification of multi-stage
programming and macros](https://dl.acm.org/doi/10.1145/3278122.3278139).
This principle restricted term and types to be used at the same level.

Now, and since `3.0` we use a more general version of cross-stage safety
where types can be used at any level. Lower levels get erased and higher
levels require a given `Type[T]`. The most updated reference is in
[Scalable Metaprogramming in Scala 3](https://github.com/nicolasstucki/nicolasstucki/raw/main/Scalable%20Metaprogramming%20in%20Scala%203.pdf).

We must remove the use of the term PCP to avoid confusion in the current
implementation.

Author: nicolasstucki

compiler/src/dotty/tools/dotc/inlines/PrepareInlineable.scala

@@ -18,7 +18,7 @@ import inlines.Inlines
 import NameOps._
 import Annotations._
 import transform.{AccessProxies, Splicer}
-import staging.PCPCheckAndHeal
+import staging.CrossStageSafety
 import transform.SymUtils.*
 import config.Printers.inlining
 import util.Property
@@ -294,7 +294,7 @@ object PrepareInlineable {
           if (code.symbol.flags.is(Inline))
             report.error("Macro cannot be implemented with an `inline` method", code.srcPos)
           Splicer.checkValidMacroBody(code)
-          (new PCPCheckAndHeal).transform(body) // Ignore output, only check PCP
+          (new CrossStageSafety).transform(body) // Ignore output, only check cross-stage safety
         case Block(List(stat), Literal(Constants.Constant(()))) => checkMacro(stat)
         case Block(Nil, expr) => checkMacro(expr)
         case Typed(expr, _) => checkMacro(expr)

compiler/src/dotty/tools/dotc/staging/PCPCheckAndHeal.scala renamed to compiler/src/dotty/tools/dotc/staging/CrossStageSafety.scala

@@ -17,14 +17,14 @@ import dotty.tools.dotc.util.Property
 import dotty.tools.dotc.util.Spans._
 import dotty.tools.dotc.util.SrcPos
 
-/** Checks that the Phase Consistency Principle (PCP) holds and heals types.
+/** Checks that staging level consistency holds and heals staged types .
  *
- *  Local term references are phase consistent if and only if they are used at the same level as their definition.
+ *  Local term references are level consistent if and only if they are used at the same level as their definition.
  *
  *  Local type references can be used at the level of their definition or lower. If used used at a higher level,
  *  it will be healed if possible, otherwise it is inconsistent.
  *
- *  Type healing consists in transforming a phase inconsistent type `T` into `summon[Type[T]].Underlying`.
+ *  Type healing consists in transforming a level inconsistent type `T` into `summon[Type[T]].Underlying`.
  *
  *  As references to types do not necessarily have an associated tree it is not always possible to replace the types directly.
  *  Instead we always generate a type alias for it and place it at the start of the surrounding quote. This also avoids duplication.
@@ -43,7 +43,7 @@ import dotty.tools.dotc.util.SrcPos
  *     }
  *
  */
-class PCPCheckAndHeal extends TreeMapWithStages {
+class CrossStageSafety extends TreeMapWithStages {
   import tpd._
 
   private val InAnnotation = Property.Key[Unit]()
@@ -97,7 +97,7 @@ class PCPCheckAndHeal extends TreeMapWithStages {
         super.transform(tree)
     }
 
-  /** Transform quoted trees while maintaining phase correctness */
+  /** Transform quoted trees while maintaining level correctness */
   override protected def transformQuotation(body: Tree, quote: Apply)(using Context): Tree = {
     val taggedTypes = new QuoteTypeTags(quote.span)
 

compiler/src/dotty/tools/dotc/staging/QuoteContext.scala

@@ -4,7 +4,6 @@ import dotty.tools.dotc.ast.tpd
 import dotty.tools.dotc.core.Contexts._
 import dotty.tools.dotc.ast.tpd
 import dotty.tools.dotc.util.Property
-import dotty.tools.dotc.staging.PCPCheckAndHeal
 import dotty.tools.dotc.staging.StagingLevel.*
 
 object QuoteContext {

compiler/src/dotty/tools/dotc/transform/Splicing.scala

@@ -21,7 +21,6 @@ import dotty.tools.dotc.core.Names._
 import dotty.tools.dotc.core.StdNames._
 import dotty.tools.dotc.quoted._
 import dotty.tools.dotc.config.ScalaRelease.*
-import dotty.tools.dotc.staging.PCPCheckAndHeal
 import dotty.tools.dotc.staging.QuoteContext.*
 import dotty.tools.dotc.staging.StagingLevel.*
 import dotty.tools.dotc.staging.QuoteTypeTags

compiler/src/dotty/tools/dotc/transform/Staging.scala

@@ -12,12 +12,12 @@ import dotty.tools.dotc.util.SrcPos
 import dotty.tools.dotc.transform.SymUtils._
 import dotty.tools.dotc.staging.QuoteContext.*
 import dotty.tools.dotc.staging.StagingLevel.*
-import dotty.tools.dotc.staging.PCPCheckAndHeal
+import dotty.tools.dotc.staging.CrossStageSafety
 import dotty.tools.dotc.staging.HealType
 
-/** Checks that the Phase Consistency Principle (PCP) holds and heals types.
+/** Checks that staging level consistency holds and heals types used in higher levels.
  *
- *  Type healing consists in transforming a phase inconsistent type `T` into `${ implicitly[Type[T]] }`.
+ *  See `CrossStageSafety`
  */
 class Staging extends MacroTransform {
   import tpd._
@@ -32,10 +32,10 @@ class Staging extends MacroTransform {
 
   override def checkPostCondition(tree: Tree)(using Context): Unit =
     if (ctx.phase <= splicingPhase) {
-      // Recheck that PCP holds but do not heal any inconsistent types as they should already have been heald
+      // Recheck that staging level consistency holds but do not heal any inconsistent types as they should already have been heald
       tree match {
         case PackageDef(pid, _) if tree.symbol.owner == defn.RootClass =>
-          val checker = new PCPCheckAndHeal {
+          val checker = new CrossStageSafety {
             override protected def healType(pos: SrcPos)(using Context) = new HealType(pos) {
               override protected def tryHeal(sym: Symbol, tp: TypeRef, pos: SrcPos): TypeRef = {
                 def symStr =
@@ -72,7 +72,7 @@ class Staging extends MacroTransform {
 
   protected def newTransformer(using Context): Transformer = new Transformer {
     override def transform(tree: tpd.Tree)(using Context): tpd.Tree =
-      (new PCPCheckAndHeal).transform(tree)
+      (new CrossStageSafety).transform(tree)
   }
 }
 

compiler/src/dotty/tools/dotc/transform/TreeChecker.scala

@@ -513,7 +513,7 @@ object TreeChecker {
             val inliningPhase = ctx.base.inliningPhase
             inliningPhase.exists && ctx.phase.id > inliningPhase.id
           if isAfterInlining then
-            // The staging phase destroys in PCPCheckAndHeal the property that
+            // The staging phase destroys in CrossStageSafety the property that
             // tree.expr.tpe <:< pt1. A test case where this arises is run-macros/enum-nat-macro.
             // We should follow up why this happens. If the problem is fixed, we can
             // drop the isAfterInlining special case. To reproduce the problem, just

docs/_docs/internals/overall-structure.md

@@ -104,14 +104,17 @@ phases. The current list of phases is specified in class [Compiler] as follows:
     List(new semanticdb.ExtractSemanticDB) :: // Extract info into .semanticdb files
     List(new PostTyper) ::          // Additional checks and cleanups after type checking
     List(new sjs.PrepJSInterop) ::  // Additional checks and transformations for Scala.js (Scala.js only)
-    List(new Staging) ::            // Check PCP, heal quoted types and expand macros
     List(new sbt.ExtractAPI) ::     // Sends a representation of the API of classes to sbt via callbacks
     List(new SetRootTree) ::        // Set the `rootTreeOrProvider` on class symbols
     Nil
 
   /** Phases dealing with TASTY tree pickling and unpickling */
   protected def picklerPhases: List[List[Phase]] =
     List(new Pickler) ::            // Generate TASTY info
+    List(new Inlining) ::           // Inline and execute macros
+    List(new PostInlining) ::       // Add mirror support for inlined code
+    List(new Staging) ::            // Check staging levels and heal staged types
+    List(new Splicing) ::           // Replace level 1 splices with holes
     List(new PickleQuotes) ::       // Turn quoted trees into explicit run-time data structures
     Nil
 

tests/pos-with-compiler-cc/dotc/core/StagingContext.scala

@@ -4,7 +4,7 @@ import dotty.tools.dotc.ast.tpd
 import dotty.tools.dotc.core.Contexts._
 import dotty.tools.dotc.ast.tpd
 import dotty.tools.dotc.util.Property
-import dotty.tools.dotc.transform.PCPCheckAndHeal
+import dotty.tools.dotc.transform.CrossStageSafety
 
 object StagingContext {
 
@@ -16,7 +16,7 @@ object StagingContext {
    */
   private val QuotesStack = new Property.Key[List[tpd.Tree]]
 
-  private val TaggedTypes = new Property.Key[PCPCheckAndHeal.QuoteTypeTags]
+  private val TaggedTypes = new Property.Key[CrossStageSafety.QuoteTypeTags]
 
   /** All enclosing calls that are currently inlined, from innermost to outermost. */
   def level(using Context): Int =
@@ -36,10 +36,10 @@ object StagingContext {
   def spliceContext(using Context): Context =
     ctx.fresh.setProperty(QuotationLevel, level - 1)
 
-  def contextWithQuoteTypeTags(taggedTypes: PCPCheckAndHeal.QuoteTypeTags)(using Context) =
+  def contextWithQuoteTypeTags(taggedTypes: CrossStageSafety.QuoteTypeTags)(using Context) =
     ctx.fresh.setProperty(TaggedTypes, taggedTypes)
 
-  def getQuoteTypeTags(using Context): PCPCheckAndHeal.QuoteTypeTags =
+  def getQuoteTypeTags(using Context): CrossStageSafety.QuoteTypeTags =
     ctx.property(TaggedTypes).get
 
   /** Context with a decremented quotation level and pops the Some of top of the quote context stack or None if the stack is empty.

tests/pos-with-compiler-cc/dotc/inlines/PrepareInlineable.scala

@@ -17,7 +17,7 @@ import NameKinds.{InlineAccessorName, UniqueInlineName}
 import inlines.Inlines
 import NameOps._
 import Annotations._
-import transform.{AccessProxies, PCPCheckAndHeal, Splicer}
+import transform.{AccessProxies, CrossStageSafety, Splicer}
 import transform.SymUtils.*
 import config.Printers.inlining
 import util.Property
@@ -294,7 +294,7 @@ object PrepareInlineable {
           if (code.symbol.flags.is(Inline))
             report.error("Macro cannot be implemented with an `inline` method", code.srcPos)
           Splicer.checkValidMacroBody(code)
-          new PCPCheckAndHeal(freshStagingContext).transform(body) // Ignore output, only check PCP
+          new CrossStageSafety(freshStagingContext).transform(body) // Ignore output, only check staging levels
         case Block(List(stat), Literal(Constants.Constant(()))) => checkMacro(stat)
         case Block(Nil, expr) => checkMacro(expr)
         case Typed(expr, _) => checkMacro(expr)

tests/pos-with-compiler-cc/dotc/transform/PCPCheckAndHeal.scala renamed to tests/pos-with-compiler-cc/dotc/transform/CrossStageSafety.scala

@@ -22,14 +22,14 @@ import dotty.tools.dotc.util.Property
 
 import scala.annotation.constructorOnly
 
-/** Checks that the Phase Consistency Principle (PCP) holds and heals types.
+/** Checks that staging level consistency holds and heals staged types .
  *
- *  Local term references are phase consistent if and only if they are used at the same level as their definition.
+ *  Local term references are level consistent if and only if they are used at the same level as their definition.
  *
  *  Local type references can be used at the level of their definition or lower. If used used at a higher level,
  *  it will be healed if possible, otherwise it is inconsistent.
  *
- *  Type healing consists in transforming a phase inconsistent type `T` into `summon[Type[T]].Underlying`.
+ *  Type healing consists in transforming a level inconsistent type `T` into `summon[Type[T]].Underlying`.
  *
  *  As references to types do not necessarily have an associated tree it is not always possible to replace the types directly.
  *  Instead we always generate a type alias for it and place it at the start of the surrounding quote. This also avoids duplication.
@@ -48,7 +48,7 @@ import scala.annotation.constructorOnly
  *     }
  *
  */
-class PCPCheckAndHeal(@constructorOnly ictx: DetachedContext) extends TreeMapWithStages(ictx), Checking, caps.Pure {
+class CrossStageSafety(@constructorOnly ictx: DetachedContext) extends TreeMapWithStages(ictx), Checking, caps.Pure {
   import tpd._
 
   private val InAnnotation = Property.Key[Unit]()
@@ -96,9 +96,9 @@ class PCPCheckAndHeal(@constructorOnly ictx: DetachedContext) extends TreeMapWit
         super.transform(tree)
     }
 
-  /** Transform quoted trees while maintaining phase correctness */
+  /** Transform quoted trees while maintaining level correctness */
   override protected def transformQuotation(body: Tree, quote: Apply)(using Context): Tree = {
-    val taggedTypes = new PCPCheckAndHeal.QuoteTypeTags(quote.span)
+    val taggedTypes = new CrossStageSafety.QuoteTypeTags(quote.span)
 
     if (ctx.property(InAnnotation).isDefined)
       report.error("Cannot have a quote in an annotation", quote.srcPos)
@@ -215,7 +215,7 @@ class PCPCheckAndHeal(@constructorOnly ictx: DetachedContext) extends TreeMapWit
           mapOver(tp)
   }
 
-  /** Check phase consistency of terms and heal inconsistent type references. */
+  /** Check level consistency of terms and heal inconsistent type references. */
   private def healTypeOfTerm(pos: SrcPos)(using Context) = new TypeMap {
     def apply(tp: Type): Type =
       tp match
@@ -275,7 +275,7 @@ class PCPCheckAndHeal(@constructorOnly ictx: DetachedContext) extends TreeMapWit
 
 }
 
-object PCPCheckAndHeal {
+object CrossStageSafety {
   import tpd._
 
   class QuoteTypeTags(span: Span)(using DetachedContext) extends caps.Pure {

tests/pos-with-compiler-cc/dotc/transform/Splicing.scala

@@ -191,7 +191,7 @@ class Splicing extends MacroTransform:
     private var refBindingMap = mutable.Map.empty[Symbol, (Tree, Symbol)]
     /** Reference to the `Quotes` instance of the current level 1 splice */
     private var quotes: Tree | Null = null // TODO: add to the context
-    private var healedTypes: PCPCheckAndHeal.QuoteTypeTags | Null = null // TODO: add to the context
+    private var healedTypes: CrossStageSafety.QuoteTypeTags | Null = null // TODO: add to the context
 
     def transformSplice(tree: tpd.Tree, tpe: Type, holeIdx: Int)(using Context): tpd.Tree =
       assert(level == 0)
@@ -254,7 +254,7 @@ class Splicing extends MacroTransform:
     private def transformLevel0QuoteContent(tree: Tree)(using Context): Tree =
       // transform and collect new healed types
       val old = healedTypes
-      healedTypes = new PCPCheckAndHeal.QuoteTypeTags(tree.span)
+      healedTypes = new CrossStageSafety.QuoteTypeTags(tree.span)
       val tree1 = transform(tree)
       val newHealedTypes = healedTypes.nn.getTypeTags
       healedTypes = old

tests/pos-with-compiler-cc/dotc/transform/Staging.scala

@@ -15,7 +15,7 @@ import dotty.tools.dotc.transform.TreeMapWithStages._
 
 
 
-/** Checks that the Phase Consistency Principle (PCP) holds and heals types.
+/** Checks that staging level consistency holds and heals staged types.
  *
  *  Type healing consists in transforming a phase inconsistent type `T` into `${ implicitly[Type[T]] }`.
  */
@@ -32,12 +32,12 @@ class Staging extends MacroTransform {
 
   override def checkPostCondition(tree: Tree)(using Context): Unit =
     if (ctx.phase <= splicingPhase) {
-      // Recheck that PCP holds but do not heal any inconsistent types as they should already have been heald
+      // Recheck that staging levels hold but do not heal any inconsistent types as they should already have been heald
       tree match {
         case PackageDef(pid, _) if tree.symbol.owner == defn.RootClass =>
           val stagingCtx = freshStagingContext
-          val checker = new PCPCheckAndHeal(stagingCtx) {
-            // !cc! type error is checker is defined as val checker = new PCPCheckAndHeal { ... }
+          val checker = new CrossStageSafety(stagingCtx) {
+            // !cc! type error is checker is defined as val checker = new CrossStageSafety { ... }
             override protected def tryHeal(sym: Symbol, tp: TypeRef, pos: SrcPos)(using Context): TypeRef = {
               def symStr =
                 if (sym.is(ModuleClass)) sym.sourceModule.show
@@ -72,7 +72,7 @@ class Staging extends MacroTransform {
 
   protected def newTransformer(using Context): Transformer = new Transformer {
     override def transform(tree: tpd.Tree)(using Context): tpd.Tree =
-      new PCPCheckAndHeal(ctx.detach).transform(tree)
+      new CrossStageSafety(ctx.detach).transform(tree)
   }
 }
 

tests/pos-with-compiler-cc/dotc/transform/TreeChecker.scala

@@ -458,7 +458,7 @@ class TreeChecker extends Phase with SymTransformer {
             val inliningPhase = ctx.base.inliningPhase
             inliningPhase.exists && ctx.phase.id > inliningPhase.id
           if isAfterInlining then
-            // The staging phase destroys in PCPCheckAndHeal the property that
+            // The staging phase destroys in CrossStageSafety the property that
             // tree.expr.tpe <:< pt1. A test case where this arises is run-macros/enum-nat-macro.
             // We should follow up why this happens. If the problem is fixed, we can
             // drop the isAfterInlining special case. To reproduce the problem, just