Skip to content

Path dependent types don't play well with macros and typeclasses #7048

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
anatoliykmetyuk opened this issue Aug 15, 2019 · 14 comments
Closed
Assignees

Comments

@anatoliykmetyuk
Copy link
Contributor

Consider the following:

import scala.quoted._


trait IsExpr[T] {
  type Underlying
  def toExpr(x: T): Expr[Underlying]
}

// object IsExpr { type Aux[T, U] = IsExpr[T] { type Underlying = U } }

// given [U] as IsExpr.Aux[Expr[U], U] = new IsExpr[Expr[U]] {
given [U] as IsExpr[Expr[U]] = new IsExpr[Expr[U]] {
  type Underlying = U
  def toExpr(x: Expr[U]): Expr[U] = x
}

def f(x: Any): String = x.toString

def g[T](x: T) given (e: IsExpr[T], tu: Type[e.Underlying]): given QuoteContext => Expr[String] = {
  val underlying: Expr[e.Underlying] = e.toExpr(x)
  '{f($underlying)}
}

// def g[T, U](x: T) given (e: IsExpr.Aux[T, U], tu: Type[U]): given QuoteContext => Expr[String] = {
//   val underlying: Expr[U] = e.toExpr(x)
//   '{f($underlying)}
// }

inline def mcr: Any = ${mcrImpl}
def mcrImpl given QuoteContext: Expr[Any] = {
  val x = '{1}
  g(x)
}

Will output:

-- Error: ../pg/Lib.scala:21:6 -------------------------------------------------
21 |  '{f($underlying)}
   |      ^^^^^^^^^^^
   |      access to value e from wrong staging level:
   |       - the definition is at level 0,
   |       - but the access is at level 1.

Sort of makes sense, since e is indeed defined at level 0. However, two facts make me think something can be done here. First, only the path-dependent type is accessed there (presumably, since the compiler needs to know the type of underlying), and we have it with the Type argument. Second, the following trick works:

import scala.quoted._


trait IsExpr[T] {
  type Underlying
  def toExpr(x: T): Expr[Underlying]
}

object IsExpr { type Aux[T, U] = IsExpr[T] { type Underlying = U } }

given [U] as IsExpr.Aux[Expr[U], U] = new IsExpr[Expr[U]] {
// given [U] as IsExpr[Expr[U]] = new IsExpr[Expr[U]] {
  type Underlying = U
  def toExpr(x: Expr[U]): Expr[U] = x
}

def f(x: Any): String = x.toString

// def g[T](x: T) given (e: IsExpr[T], tu: Type[e.Underlying]): given QuoteContext => Expr[String] = {
//   val underlying: Expr[e.Underlying] = e.toExpr(x)
//   '{f($underlying)}
// }

def g[T, U](x: T) given (e: IsExpr.Aux[T, U], tu: Type[U]): given QuoteContext => Expr[String] = {
  val underlying: Expr[U] = e.toExpr(x)
  '{f($underlying)}
}

inline def mcr: Any = ${mcrImpl}
def mcrImpl given QuoteContext: Expr[Any] = {
  val x = '{1}
  g(x)
}

Aux trick comes from Shapeless 2 and was used to bypass the limitations of Scala 2, where it was impossible to refer to a path-dependent type of a sibling argument from the same argument list.

@nicolasstucki
Copy link
Contributor

The error is correct. You cannot refer to a path in another stage (e.i. a term prefix in another stage).

As far as I understand the Aux pattern is a workaround for Scala2 limitations that we do not have anymore. @milessabin is that correct? Or am I missing some use cases?

@milessabin
Copy link
Contributor

There are still situations where using an aux type as an abbreviation for a complex refinement makes sense.

For the most part the non-sugar uses of aux types can be replaced by intra-parameter list path dependencies.

I'm not confident enough to be able to say that that exhausts all the possible uses for aux types though.

@anatoliykmetyuk
Copy link
Contributor Author

@nicolasstucki do you think it is possible to capture the type somehow (similarly to the aux pattern) in a type variable under the hood, and then substitute in place of the prefix based reference? Essentially making the compiler do the aux pattern for the user?

@anatoliykmetyuk
Copy link
Contributor Author

anatoliykmetyuk commented Aug 16, 2019

I think we should really try to teach the compiler this trick. This limitation seems to have a chain reaction.

E.g. to implement Liftable derivation, I need zip on tuples with precise types. However, if I do it the easy way, with path-dependent types, I won't be able to use this operation in macros. Good that I control the implementation of the operation and can build it with macros in mind: #7057.

However, if I'm the user of the standard library, not its developer, I won't be able to use an op implemented with path-dependent types in my macros.

If Shapeless 2 was written in Scala 3 with path-dependent types instead of the Aux pattern, using it from macros would present serious difficulties. You would need to constantly make sure the values returned by Shapeless 2 operations do not end up in Exprs.

@nicolasstucki
Copy link
Contributor

Aren't those the patterns that become trivial with white box inline?

@anatoliykmetyuk
Copy link
Contributor Author

I am not sure I understand what you mean here

@anatoliykmetyuk
Copy link
Contributor Author

Can you show an example?

@nicolasstucki
Copy link
Contributor

#7057 (comment)

@anatoliykmetyuk
Copy link
Contributor Author

anatoliykmetyuk commented Aug 20, 2019

That one is not related to this issue. The example in question is very specific to our use case of compiler development and is not supposed to be used by the end users.

The point of type safety is to ensure the correctness of the program. As library developers, we can sacrifice internal type safety for user-friendly API and marginal performance gains. By making this decision, we consciously complicate lives for ourselves for the better end-user experience.

However, that's not how you should write Scala – or any other language with a good-enough type system and a compiler that verifies programs using that type system. We should not do that either – the current tuple API implementation is suboptimal. We should have both type safety, performance and a user-friendly API. The reason why we can't have them all right now is that the match types and GADT constraints are not powerful enough and that the tail operation on tuples has linear complexity. The answer is to work on lifting the above constraints, not to justify the type-unsafe style by them.

@milessabin
Copy link
Contributor

@anatoliykmetyuk see #7078 ... I think you might be running into the same issue.

@anatoliykmetyuk
Copy link
Contributor Author

@milessabin I do not think it is the same. The minimized example of this issue does not involve given or implicit definitions at all:

import scala.quoted._

trait IsExpr[T] {
  type Underlying
  def toExpr(x: T): Expr[Underlying]
}

def f(x: Any): String = x.toString

def g[T](x: T) given (e: IsExpr[T], tu: Type[e.Underlying]): given QuoteContext => Expr[String] = {
  val underlying: Expr[e.Underlying] = e.toExpr(x)
  '{f($underlying)}
}

Out:

-- Error: ../pg/Macros03.scala:12:6 --------------------------------------------
12 |  '{f($underlying)}
   |      ^^^^^^^^^^^
   |      access to value e from wrong staging level:
   |       - the definition is at level 0,
   |       - but the access is at level 1.
one error found

We don't care where e comes from, we only care that it is accessed from the wrong staging level.

The only place where #7078 comes into play in this example is the following:

import scala.quoted._

trait IsExpr[T] {
  type Underlying
  def toExpr(x: T): Expr[Underlying]
}

object IsExpr { type Aux[T, U] = IsExpr[T] { type Underlying = U } }

given [U] as IsExpr[Expr[U]] = new IsExpr[Expr[U]] {
  type Underlying = U
  def toExpr(x: Expr[U]): Expr[U] = x
}

def g[T, U](x: T) given (e: IsExpr.Aux[T, U], tu: Type[U]): given QuoteContext => Expr[String] = ???

inline def mcr: Any = ${mcrImpl}
def mcrImpl given QuoteContext: Expr[Any] = {
  val x = '{1}
  g(x)
}

Out:

-- Error: ../pg/Macros01.scala:20:6 --------------------------------------------
20 |  g(x)
   |      ^
   |no implicit argument of type IsExpr.Aux[quoted.Expr[Int], U] was found for parameter e of method g.
   |I found:
   |
   |    Macros01$package.IsExpr_Expr_given[Nothing]
   |
   |But method IsExpr_Expr_given does not match type IsExpr.Aux[quoted.Expr[Int], U].

To fix this, replace the given which defines IsExpr as follows:

inline implicit def isExprGen[U] <: IsExpr[Expr[U]] = new IsExpr[Expr[U]] {
  type Underlying = U
  def toExpr(x: Expr[U]): Expr[U] = x
}

Or, as follows:

given [U] as IsExpr.Aux[Expr[U], U] = new IsExpr[Expr[U]] {
  type Underlying = U
  def toExpr(x: Expr[U]): Expr[U] = x
}

@LPTK
Copy link
Contributor

LPTK commented Aug 23, 2019

Why is there a level restriction on the paths of path-dependent types? The paths are erased anyways, so as long as there is the appropriate type evidence in scope to construct the term, it shouldn't matter.

And the obligatory "it works in Squid!":

scala> trait IsCode[T] { type U; def toCode(x: T): OpenCode[U] }
defined trait IsCode

scala> def g[T,U0:CodeType](x:T)(e: IsCode[T]{type U=U0}): OpenCode[String] = code"identity(${e.toCode(x)}).toString"
g2: [T, U0](x: T)(e: IsCode[T]{type U = U0})(implicit evidence$1: squid.IR.Predef.CodeType[U0])squid.IR.Predef.OpenCode[String]

scala> g(42)(new IsCode[Int]{type U = Double; def toCode(x:Int)=Const(x.toDouble)})
res9: squid.IR.Predef.OpenCode[String] = code"scala.Predef.identity[scala.Double](42.0).toString()"

@LPTK
Copy link
Contributor

LPTK commented Aug 23, 2019

BTW, this is much more than "making the Aux pattern work".
In our Squid use cases, there are many places where we build advanced staging representations that use type members and path-dependent types rooted in staging-time instances to manipulate terms in a type-safe way.

nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Aug 28, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Aug 28, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Aug 28, 2019
odersky added a commit that referenced this issue Aug 30, 2019
Fix #7048: Heal phase inconsistent path dependent types
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 3, 2019
@nicolasstucki nicolasstucki reopened this Oct 4, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 7, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 8, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 8, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 8, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 8, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 8, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 10, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 11, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 11, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Oct 11, 2019
odersky added a commit that referenced this issue Oct 26, 2019
Fix #7048: PCP heal path dependent types
@LPTK
Copy link
Contributor

LPTK commented Dec 20, 2019

@nicolasstucki @odersky following today's discussion, can we reopen this?

The following code should work, but it currently crashes the compiler or fails with a level inconsistency error:

import scala.quoted.{given, _}

abstract class Test {
  type T
  
  val T: Type[T]
  def getT: Type[T] = T // need this to avoid getting `null`
  given Type[T] = getT
  
  def foo(given QuoteContext): Expr[Any] = {
    
    val r = '{Option.empty[T]} // crash
    
    // val t: Test = this
    // import t.{given}
    // println(summon[Type[t.T]].show)
    // val r = '{Option.empty[t.T]} // access to value t from wrong staging level
    // val r = '{Option.empty[${t.T}]} // works
    
    // val r = '{Option.empty[${T}]} // works
    // val r = '{Option.empty[List[${T}]]} // works
    // val r = '{summon[Type[${T}]]} // access to Test.this from wrong staging level
    // val r = '{summon[${T} <:< Any]} // crash
    
    // val s = '{Option.empty[${T}]}
    // val r = '{identity($s)} // works
    // val r = '{identity(${s: Expr[Option[T]]})} // crash
    
    r
  }
}

@main def main = ()

https://scastie.scala-lang.org/A6Z8BGb9Rj6cu2DJYOPQGA

Note that the level error on '{summon[Type[${T}]]} is expected, but the one on '{Option.empty[t.T]} is a bug.

@nicolasstucki nicolasstucki reopened this Dec 20, 2019
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Jan 27, 2020
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Jan 27, 2020
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Jan 27, 2020
nicolasstucki added a commit to dotty-staging/dotty that referenced this issue Jan 27, 2020
nicolasstucki added a commit that referenced this issue Jan 28, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants