Metaprogramming + existential type fails to compile

[japgolly]

Compiler version

3.1.2

Minimized code

import scala.quoted.*

// This works no problem
object UniversalTypeParam {
  trait T[A] { def a: A }

  inline def macroDef[A](inline t: T[A]): A =
    ${ macroBody[A]('t) }

  def macroBody[A](t: Expr[T[A]])(using Quotes, Type[A]): Expr[A] = {
    import quotes.reflect.*
    '{ $t.a }
  }
}

// This morally the same as above, but doesn't compile
object ExistentialTypeParam {
  trait T { type A; def a: A }
  type TA[X] = T { type A = X }

  inline def macroDef(inline t: T): t.A =
    ${ macroBody[t.A]('t) }

  def macroBody[A](t: Expr[TA[A]])(using Quotes, Type[A]): Expr[A] = {
    import quotes.reflect.*
    '{ $t.a }
  }
}

Output

[error] 22 |    ${ macroBody[t.A]('t) }
[error]    |                      ^
[error]    |                      access to parameter t from wrong staging level:
[error]    |                       - the definition is at level 0,
[error]    |                       - but the access is at level -1.
[error] one error found

Expectation

Should compile.

[japgolly]

Workaround:

   inline def macroDef(inline t: T): t.A =
-    ${ macroBody[t.A]('t) }
+    workaround(t)
+
+  inline def workaround[A](inline t: TA[A]): A =
+    ${ macroBody[A]('t) }

[nicolasstucki]

It might be related to #13376

[nicolasstucki]

In

inline def macroDef(inline t: T): t.A =  ${ macroBody[t.A]('t) }

I notice the use of t.A. It seems strange that t.A in considered a valid path because there are no guarantees that t is a stable path once it is inlined.

[nicolasstucki]

Now it fails telling the user that inline t is not an immutable path. This is the correct failure.

-- [E083] Type Error: t/Test.scala:21:36 ---------------------------------------
21 |  inline def macroDef(inline t: T): t.A =
   |                                    ^
   |(t : ExistentialTypeParam.T) is not a valid type prefix, since it is not an immutable path
   |
   | longer explanation available when compiling with `-explain`
-- [E083] Type Error: t/Test.scala:22:17 ---------------------------------------
22 |    ${ macroBody[t.A]('t) }
   |                 ^
   |(t : ExistentialTypeParam.T) is not a valid type prefix, since it is not an immutable path
   |
   | longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: t/Test.scala:22:22 ------------------------------
22 |    ${ macroBody[t.A]('t) }
   |                      ^
   |     Found:    (t : ExistentialTypeParam.T)
   |     Required: ExistentialTypeParam.T{type A = ExistentialTypeParam.T#A}
   |
   | longer explanation available when compiling with `-explain`

This also suggests the alternative workaround, which does compile.

-  inline def macroDef(inline t: T): t.A =
+  inline def macroDef(t: T): t.A =