Level checking failing with path dependent types

[nicolasstucki]

Minimization:

import scala.quoted.*
trait C:
  type T
  def foo: T
inline def makro(inline x: C): x.T = ${ impl[x.type]('x) }
def impl[CC <: C](xp: Expr[CC])(using Quotes): Expr[CC#T] = '{ $xp.foo }

-- Error: Test.scala:5:45 ------------------------------------------------------
5 |inline def makro(inline x: C): x.T = ${ impl[x.type]('x) }
  |                                             ^
  |                           access to parameter x from wrong staging level:
  |                            - the definition is at level 0,
  |                            - but the access is at level -1.
-- Error: Test.scala:5:53 ------------------------------------------------------
5 |inline def makro(inline x: C): x.T = ${ impl[x.type]('x) }
  |                                                     ^
  |                           access to parameter x from wrong staging level:
  |                            - the definition is at level 0,
  |                            - but the access is at level -1.

(only the first error shows if the [x.type] argument left to inference)

Originally posted by @lrytz in https://github.com/sirthias/parboiled2/issues/274#issuecomment-904926294

[lrytz]

In Scala 2, Expr has a value field for that purpose

https://www.scala-lang.org/api/2.13.6/scala-reflect/scala/reflect/api/Exprs$Expr.html#value:T

https://docs.google.com/document/d/1O879Iz-567FzVb8kw6N5OBpei9dnbW0ZaT7-XNSa6Cs/edit?hl=en_US#heading=h.jwrr3vbdoy3q

[nicolasstucki]

In Scala 2, Expr has a value field for that purpose

That would be a good addition, but the current code should compile.

[nicolasstucki]

Note that inline x cannot be used for x.T as x is not a stable path.

5 |inline def makro(inline x: C): x.T = ${ impl[x.type]('x) }
  |                               ^
  |     (x : C) is not a valid type prefix, since it is not an immutable path

The variant

import scala.quoted.*
trait C:
  type T
  def foo: T
inline def makro(x: C): x.T = ${ impl[x.type]('x) }
def impl[CC <: C](xp: Expr[CC])(using Quotes): Expr[CC#T] = '{ $xp.foo }

fails with

6 |def impl[CC <: C](xp: Expr[CC])(using Quotes): Expr[CC#T] = '{ $xp.foo }
  |                                                    ^^
  |                                           CC is not a legal path
  |                                           since it is not a concrete type

which also seems to be the correct failure.

[nicolasstucki]

The pattern can be encoded as

import scala.quoted.*
trait C:
  type T
  def foo: T
inline def makro(x: C): x.T = ${ impl[x.T]('x) }
def impl[U: Type](xp: Expr[C { def foo: U }])(using Quotes): Expr[U] =
  '{ $xp.foo }