Skip to content

Level checking failing with path dependent types #13376

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
nicolasstucki opened this issue Aug 24, 2021 · 4 comments · Fixed by #17388
Closed

Level checking failing with path dependent types #13376

nicolasstucki opened this issue Aug 24, 2021 · 4 comments · Fixed by #17388
Assignees
Labels
area:metaprogramming:quotes Issues related to quotes and splices

Comments

@nicolasstucki
Copy link
Contributor

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 sirthias/parboiled2#274 (comment)

@lrytz
Copy link
Member

lrytz commented Aug 25, 2021

@nicolasstucki
Copy link
Contributor Author

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

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

@nicolasstucki
Copy link
Contributor Author

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
Copy link
Contributor Author

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 }

nicolasstucki added a commit to dotty-staging/dotty that referenced this issue May 2, 2023
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue May 2, 2023
smarter added a commit that referenced this issue May 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:metaprogramming:quotes Issues related to quotes and splices
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants