scala / scala3

The Scala 3 compiler, also known as Dotty.
https://dotty.epfl.ch
Apache License 2.0
5.79k stars 1.04k forks source link

[cc] inline polymorphic function failed to instantiate its type parameter to capturing type #16978

Open yawen-guan opened 1 year ago

yawen-guan commented 1 year ago

Compiler version

3.3.0-RC2

Minimized code

def foo[T](x: T): T = x
inline def inlineFoo[T](x: T): T = x

case class A() {}
case class B(a: {*} A) {}
val a: {*} A = new A()
foo(new B(a)) // passed
inlineFoo(new B(a)) // failed
val b0 = new B(a) 
inlineFoo(b0) // failed
val b1: {a} B = new B(a)
inlineFoo(b1) // passed

Output

-- [E007] Type Mismatch Error: ...
16 |    inlineFoo(new B(a))
   |              ^^^^^^^^
   |              Found:    {a} B{val a²: (a : {*} A)}
   |              Required: B
   |
   |              where:    a  is a value in method main
   |                        a² is a value in class B
   |
   | longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: ...
18 |    inlineFoo(b0)
   |    ^^^^^^^^^^^^^
   |    Found:    (b0 : {a} B{val a²: {a} A})
   |    Required: B
   |
   |    where:    a  is a value in method main
   |              a² is a value in class B
   |----------------------------------------------------------------------------
   |Inline stack trace
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |This location contains code that was inlined from Main.scala:7
 7 |inline def inlineFoo[T](x: T): T = x
   |                                   ^
    ----------------------------------------------------------------------------
   |
   | longer explanation available when compiling with `-explain`
2 errors found

Expectation

I expect this code to pass.

scala-center-bot commented 1 year ago

This issue was picked for the Issue Spree No. 27 of 07 March 2023 which takes place in a week from now. @SethTisue, @natsukagami, @yawen-guan will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.

SethTisue commented 1 year ago

Curious how this ticket got selected? Looks challenging. Note that I have zero experience with capture checking. I have some experience with typer, but not a ton. Is there any capture checking experience in this group...?

mbovel commented 1 year ago

Guess from Martin: during the captureChecking phase, InferredTypedTree and TypeTree are treated differently. Maybe B gets wrapped inside a TypeTree instead of a InferredTypedTree, which would explain it doesn't get the excepted capture set. Tips for debugging:

mbovel commented 1 year ago

Curious how this ticket got selected? Looks challenging.

Indeed, it is a challenging one! Someone suggested it for the spree and I thought it might be appropriate for your group because you all have some experience hacking on the compiler already. It could be a nice opportunity to learn more about capture checking and inlining. Additionally, @nicolasstucki (inlining ninja) and @Linyxus (capture checking boss) might join as well (or add some comments here 🙂) to guide you on fixing this issue.

That said, if you see that its is really not feasible, it's of course always possible to switch to another issue.

nicolasstucki commented 1 year ago

Minimization

import scala.language.experimental.captureChecking

def foo[T](x: T): T = x
/*transparent*/ inline def inlineFoo[T](inline x: T): T = x

class A() {}
class B(a: {*} A) {}

def test(a: {*} A) =
  val b1 = foo(new B(a)) // passed
  val b2 = inlineFoo(new B(a)) // failed

after inlining

 def test(a: {*} A): Unit =
      {
        val b1: B = foo[B](new B(a))
        val b2: B = new B(a):B
        ()
      }

The issue could be related to the :B ascription added on non-transparent inline methods.

nicolasstucki commented 1 year ago

Minimization

import scala.language.experimental.captureChecking
class A() {}
class B(a: {*} A) {}
def test(a: {*} A) = new B(a): B
7 |def test(a: {*} A) = new B(a): B
  |                     ^^^^^^^^
  |                     Found:    {a} B{val a²: (a : {*} A)}
  |                     Required: B
  |
  |                     where:    a  is a parameter in method test
  |                               a² is a value in class B
SethTisue commented 1 year ago

ah, hell, I can't attend this spree after all. sorry about that :-/

natsukagami commented 1 year ago

The problem is exactly due to TypeTrees from inlining not being marked as inferred, causing CC to not infer its capture sets after that.

We followed @mbovel's comment and traced the TypeTrees down to https://github.com/lampepfl/dotty/blob/833a41e8a37091074c89fb8c53fdef7306af66a5/compiler/src/dotty/tools/dotc/inlines/Inliner.scala#L231 (for the parameter binding), and https://github.com/lampepfl/dotty/blob/833a41e8a37091074c89fb8c53fdef7306af66a5/compiler/src/dotty/tools/dotc/inlines/Inliner.scala#L590 for the type ascriptions.

However this seems hard to fix, since we need to preserve inferred-ness of the Types coming from the proxies and that seems hard to keep track of (since inferred seems to be exclusive to TypeTrees and not Types).

natsukagami commented 1 year ago

Minimization

import scala.language.experimental.captureChecking
class A() {}
class B(a: {*} A) {}
def test(a: {*} A) = new B(a): B
7 |def test(a: {*} A) = new B(a): B
  |                     ^^^^^^^^
  |                     Found:    {a} B{val a²: (a : {*} A)}
  |                     Required: B
  |
  |                     where:    a  is a parameter in method test
  |                               a² is a value in class B

Per @Linyxus, this is not wrong, since we have an explicit type ascription with pure B here, which forces the values to have an empty capture set rather than an inferred set.

natsukagami commented 1 year ago

I found a testcase where forcing inferred = true is wrong:

import scala.language.experimental.captureChecking

transparent inline def inlineFoo[T >: B](x: {*} A): {x} T = (new B(x)) : T

class A() {}
class B(a: {*} A) {}

def test(a: {*} A) =
  val b2 = inlineFoo[B](a)

This should not pass capture checking, but does. Note that we should expect b2's type to be B (and not {a} B) here, since we are asserting (new B(x)) : T in the inline def, which should be expanded to non-inferred B. However the forced inferrence makes the ascription (new B(x)) : {a} B anyway.

This is not unsound, just unexpected that b2's type is not B as we should guess.