Fix scala#7405: Allow types references at a lower level

To be able to have references to type tags of types defined in a higher level we need to generalize the concept of type healing. In this case we instead of needing to keep a type tag for the next stage it should be possible to refer to types for a next level. This is already the case inside of top level splices in inline methods (macros) but it should be possible to do in any code.

Author: nicolasstucki

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

@@ -215,7 +215,7 @@ class PCPCheckAndHeal(@constructorOnly ictx: Context) extends TreeMapWithStages(
           assert(ctx.inInlineMethod)
           None
         }
-        else {
+        else if (levelOf(sym).getOrElse(0) < level) {
           val reqType = defn.QuotedTypeClass.typeRef.appliedTo(tp)
           val tag = ctx.typer.inferImplicitArg(reqType, pos.span)
           tag.tpe match {
@@ -233,6 +233,8 @@ class PCPCheckAndHeal(@constructorOnly ictx: Context) extends TreeMapWithStages(
                             |
                             | The access would be accepted with an implict $reqType""")
           }
+        } else {
+          None
         }
       case _ =>
         levelError(sym, tp, pos, "")

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

@@ -44,13 +44,14 @@ class Staging extends MacroTransform {
         case PackageDef(pid, _) if tree.symbol.owner == defn.RootClass =>
           val checker = new PCPCheckAndHeal(freshStagingContext) {
             override protected def tryHeal(sym: Symbol, tp: Type, pos: SourcePosition)(implicit ctx: Context): Option[tpd.Tree] = {
+
               def symStr =
                 if (!tp.isInstanceOf[ThisType]) sym.show
                 else if (sym.is(ModuleClass)) sym.sourceModule.show
                 else i"${sym.name}.this"
 
               val errMsg = s"\nin ${ctx.owner.fullName}"
-              assert(false,
+              assert(levelOf(sym).getOrElse(0) >= level,
                 em"""access to $symStr from wrong staging level:
                     | - the definition is at level ${levelOf(sym).getOrElse(0)},
                     | - but the access is at level $level.$errMsg""")

docs/docs/reference/metaprogramming/macros.md

@@ -164,7 +164,8 @@ is legal because it is spliced, then quoted.
 ### Types and the PCP
 
 In principle, The phase consistency principle applies to types as well
-as for expressions. This might seem too restrictive. Indeed, the
+as for expressions. But it only acts on types that are used in higher levels.
+This might seem too restrictive. Indeed, the
 definition of `reflect` above is not phase correct since there is a
 quote but no splice between the parameter binding of `T` and its
 usage. But the code can be made phase correct by adding a binding

tests/pos/i7405.scala

@@ -0,0 +1,13 @@
+import scala.quoted._
+class Foo {
+  def f(given QuoteContext): Expr[Any] = {
+    '{
+      type X = Int // Level 1
+      val x: X = ???
+      ${
+        val t: Type[X] = '[X] // Level 0
+        '{ val y: $t = x }
+      }
+    }
+  }
+}

tests/pos/i7405b.scala

@@ -0,0 +1,18 @@
+import scala.quoted._
+
+class Foo {
+  def f(given QuoteContext): Expr[Any] = {
+    '{
+      trait X {
+        type Y
+        def y: Y = ???
+      }
+      val x: X = ???
+      type Z = x.Y
+      ${
+        val t: Type[Z] = '[Z]
+        '{ val y: $t = x.y }
+      }
+    }
+  }
+}