Incorrect type error after inlining

[eejbyfeldt]

Compiler version

3.7.4, 3.8.1-RC1-bin-20251119-df117fc-NIGHTLY

Minimized code

object test {
  class A
  class B extends A

  inline def f[T](inline v: Any): T = inline v match {
    case x: T => x
  }

  inline def b: B = new B() 
  f[A](b: A)
}

Output

[error] ./inline_bug.scala:10:8
[error] Found:    test.A
[error] Required: test.B
[error]   f[A](b: A)
[error]        ^^^^

Expectation

Compiles without failure.

[eejbyfeldt]

Based on #24432 the correct behavior should maybe be failure with a better error message.

[hamzaremmal]

Before we dive into this issue, we need to specify what the ascription does here, can the inliner go through it or not.
Say we have:

object test {
  class A
  class B extends A

  inline def f[T](inline v: Any): Any = inline v match {
     case x: B => x
     case x: A => x
  }

  inline def b: B = new B() 
}

This f[A](b) should clearly reduce to the path for B but should f[A](b: A) reduce to the path for A or should the ascription be invisible and reduce to the path for B? If it is the former then what is the point of the ascription and how can I force the reduction to A?

/cc @mbovel

[mbovel]

Compiles without failure.

I would expect that too.

---

The example can be further simplifier by removing the type parameter T:

object test {
  class A
  class B extends A

  inline def f(inline v: Any): A = (inline v match {
    case x: A => x
  })

  inline def b: B = new B()
  f(b: A)
}

Here is the stack trace:

> scalac -Ydebug-error test.scala
[info] running (fork) dotty.tools.dotc.Main -d /localhome/bovel/scala3/out/default-last-scalac-out.jar -classpath /localhome/bovel/scala3/library/target/scala-library-nonbootstrapped/scala-library-3.8.1-RC1-bin-SNAPSHOT-nonbootstrapped.jar -Ydebug-error test.scala
-- [E007] Type Mismatch Error: test.scala:10:4 ---------------------------------
10 |  f(b: A)
   |    ^^^^
   |    Found:    test.A
   |    Required: test.B
   |
   | longer explanation available when compiling with `-explain`
java.lang.Exception: Stack trace
        at java.base/java.lang.Thread.dumpStack(Thread.java:1389)
        at dotty.tools.dotc.report$.error(report.scala:73)
        at dotty.tools.dotc.typer.ErrorReporting$.errorType(ErrorReporting.scala:32)
        at dotty.tools.dotc.typer.ErrorReporting$.errorTree(ErrorReporting.scala:23)
        at dotty.tools.dotc.typer.ErrorReporting$.errorTree(ErrorReporting.scala:26)
        at dotty.tools.dotc.typer.ErrorReporting$Errors.typeMismatch(ErrorReporting.scala:193)
        at dotty.tools.dotc.typer.Typer.recover$1(Typer.scala:4947)
        at dotty.tools.dotc.typer.Typer.adaptToSubType$1(Typer.scala:4973)
        at dotty.tools.dotc.typer.Typer.adaptNoArgsOther$1(Typer.scala:4769)
        at dotty.tools.dotc.typer.Typer.adaptNoArgs$1(Typer.scala:4849)
        at dotty.tools.dotc.typer.Typer.adapt1(Typer.scala:5113)
        at dotty.tools.dotc.typer.Typer.adapt(Typer.scala:4322)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3942)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3947)
        at dotty.tools.dotc.typer.ReTyper.typedInlined(ReTyper.scala:100)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:3784)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3855)
        at dotty.tools.dotc.inlines.Inliner$InlineTyper.typedUnadapted(Inliner.scala:1063)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3942)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3947)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:4058)
        at dotty.tools.dotc.typer.Typer.typedValDef(Typer.scala:3047)
        at dotty.tools.dotc.inlines.Inliner$InlineTyper.typedValDef(Inliner.scala:935)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:3740)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3854)
        at dotty.tools.dotc.inlines.Inliner$InlineTyper.typedUnadapted(Inliner.scala:1063)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3942)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3947)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3969)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:4015)
        at dotty.tools.dotc.typer.Typer.typedBlockStats(Typer.scala:1534)
        at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:1538)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:3769)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3855)
        at dotty.tools.dotc.inlines.Inliner$InlineTyper.typedUnadapted(Inliner.scala:1063)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3942)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3947)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:4058)
        at dotty.tools.dotc.inlines.Inliner$InlineTyper.reduceInlineMatchExpr$1(Inliner.scala:1033)
        at dotty.tools.dotc.inlines.Inliner$InlineTyper.typedMatchFinish(Inliner.scala:1047)
        at dotty.tools.dotc.typer.Typer.typedMatch(Typer.scala:2209)
        at dotty.tools.dotc.inlines.Inliner$InlineTyper.typedMatch(Inliner.scala:970)

Note that if we remove the inline modifier for the v parameter, then the example compiles:

object test {
  class A
  class B extends A

  inline def f(v: Any): A = (inline v match {
    case x: A => x
  })

  inline def b: B = new B()
  f(b: A)
}

[mbovel]

This f[A](b) should clearly reduce to the path for B but should f[A](b: A) reduce to the path for A or should the ascription be invisible and reduce to the path for B?

Matches have a runtime semantic (unlike overload resolution for example). At runtime, we would always take thecase x: B if v is an instance of B. I think what we do at compile-time should be a correct approximation of the runtime behavior. Therefore in your example, like for match types, we should reduce to case x: B if v.type <:< B. And we should reduce to case x: A if and only if v.type <:< A and v.type is provably disjoint from B.

[hamzaremmal]

This f[A](b) should clearly reduce to the path for B but should f[A](b: A) reduce to the path for A or should the ascription be invisible and reduce to the path for B?

Matches have a runtime semantic (unlike overload resolution for example). At runtime, we would always take thecase x: B if v is an instance of B. I think what we do at compile-time should be a correct approximation of the runtime behavior. Therefore in your example, like for match types, we should reduce to case x: B if v.type <:< B. And we should reduce to case x: A if and only if v.type <:< A and v.type is provably disjoint from B.

Both semantics are possible, I just say we need to make it clear which one we are choosing and what are the limitations of it.

[hamzaremmal]

@mbovel, during the LAMP meeting, the consensus was towards having f[A](b: A) reduce to the case x: A, not case x: B. Nevertheless, I agree about being close to runtime semantics but at the same time this might not be how we use compile time constructs. This is still an open question.

[hamzaremmal]

Based on #24432 the correct behavior should maybe be failure with a better error message.

Not really, it should pass. It fails now because when we inline we generate wrong code.

[som-snytt]

I didn't want to pollute the conversation, but my comment was:

It's too bad the semantics of inlining paper is behind a paywall.

Where v is not inlined (and the code compiles):

    {
      val v$proxy1: test.A = new test.B():test.B:test.A
      {
        val $scrutinee1: (v$proxy1 : test.A) = v$proxy1
        val x: test.A = $scrutinee1
        x:test.A
      }:test.A
    }

but inlined:

    {
      val $scrutinee1: test.B = new test.B():test.B:test.A
      val x: test.B = $scrutinee1
      x:test.B
    }:test.A

In what sense is that semantics-preserving? Even if it were to downcast for the failing assignment, x should still be A. If the type arg were not specified, it would be free to infer B, but in fact it infers Nothing.

With the caveat that I'm not fully awake at the moment, inlining v can only provide a more specific type, so the match shouldn't suddenly fail.

[hamzaremmal]

In what sense is that semantics-preserving?

If adding the ascription were to affect the reduction then it isn't semantics-preserving.

so the match shouldn't suddenly fail.

No there is no reason for it to fail, the generated code is wrong. The question here would be should we strip the ascription or should $scrutinee1 be typed as A. Here, a decision has to be taken.