Typer: Instability & Inconsistent Conformance Check Report

[ftucky]

Edited to reflect code minimization findings, absent from the original submission.

Compiler version

3.2.0, 3.2.2, 3.3.0-RC2

Minimized code

object Foo:
  def bar(x:YOf[K]):Unit = ???
  bar(???)

trait K:
  type C
  sealed trait X:
    type CType <: YOf[C]
    def foo : K#Y =
      val x : CType = ???
      x

  sealed trait Y extends X

type YOf[+T] = K#Y { type M <: T }

https://scastie.scala-lang.org/8oKKJzCeRMK0Coc7uaGKCw

Output

Scala compiler reports failed type conformance check (`...but the comparison trace ended with false).
However, the trace itself ends with true.

13 |      x
   |      ^
   |      Found:    (x : X.this.CType)
   |      Required: a.K#Y
   |----------------------------------------------------------------------------
   | Explanation (enabled by `-explain`)
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |
   | Tree: x
   | I tried to show that
   |   (x : X.this.CType)
   | conforms to
   |   a.K#Y
   | but the comparison trace ended with `false`:
   |
   |   ==> (x : X.this.CType)  <:  a.K#Y
   |     ==> X.this.CType  <:  a.K#Y (left is approximated)
   |       ==> a.YOf[K.this.C]  <:  a.K#Y (left is approximated)
   |         ==> a.K#Y{M <: K.this.C}  <:  a.K#Y (left is approximated)
   |           ==> a.K#Y  <:  a.K#Y (left is approximated)
   |           <== a.K#Y  <:  a.K#Y (left is approximated) = true
   |         <== a.K#Y{M <: K.this.C}  <:  a.K#Y (left is approximated) = true
   |       <== a.YOf[K.this.C]  <:  a.K#Y (left is approximated) = true
   |     <== X.this.CType  <:  a.K#Y (left is approximated) = true
   |   <== (x : X.this.CType)  <:  a.K#Y = true
   |
   | The tests were made under the empty constraint
    ----------------------------------------------------------------------------

Expectation

Either

• the conformance check to pass, or
• the trace to end with = false

Observations

• Failure depends on the positions of object Foo and trait K. https://scastie.scala-lang.org/UqVDSBaURW22P6Qsnw4ZgQ compiles correctly.
• When object Foo is not present in the file, the file compiles correctly by itself.
• However, when object Foo is present in another file, failure becomes dependent on the relative order of both files compilation, with a race condition.
• Under sbt the race creates a memory effect: if a former compilation run left a valid tasty for trait K, issue disappears as well. ( sometimes until sbt clean, sometimes not )

Any clue about what could cause the inconsistency in the report ?

[smarter]

Could you check if you can reproduce this issue with the latest nightly (in your sbt build, set scalaVersion := "3.3.1-RC1-bin-20230218-7c9c72a-NIGHTLY")? It contains a fix for a recently reported non-deterministic bug (#16884).

[ftucky]

@smarter: Unfortunately no. Symptom remains unchanged with 3.3.1-RC1-bin-20230218-7c9c72a-NIGHTLY.

[smarter]

Thanks for checking. I assume the project contains multiple file, is the problem still reproducible in sbt if you delete the other files from this project?

[ftucky]

Here is the minimization I get to :
Sorry, original codebase is private, code is obfuscated.

file a.scala:

import b.*

object Foo:
	def bar(x : YOf[K]):Unit = ???
	bar(???)

file b.scala:

package b

trait K:
  type C
		
  sealed trait X:
    type CType <: YOf[C]
    def foo : K#Y = 
      val x : CType = ???
      x

  sealed trait Y extends X 

type YOf     [+T] = K#Y {type M <: T}

When compiled separately (b.scala then a.scala) everything is fine.

The bug appears using sbt. When sbt starts with a.scala, the compilation of b.scala fails with

[error] 11 |      x
[error]    |      ^
[error]    |      Found:    (x : X.this.CType)
[error]    |      Required: com.arteris.forj.ir.K#Y
[error]    |----------------------------------------------------------------------------
[error]    | Explanation (enabled by `-explain`)
[error]    |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[error]    |
[error]    | Tree: x
[error]    | I tried to show that
[error]    |   (x : X.this.CType)
[error]    | conforms to
[error]    |   com.arteris.forj.ir.K#Y
[error]    | but the comparison trace ended with `false`:
[error]    |
[error]    |   ==> (x : X.this.CType)  <:  com.arteris.forj.ir.K#Y
[error]    |     ==> X.this.CType  <:  com.arteris.forj.ir.K#Y (left is approximated)
[error]    |       ==> com.arteris.forj.ir.YOf[K.this.C]  <:  com.arteris.forj.ir.K#Y (left is approximated)
[error]    |         ==> com.arteris.forj.ir.K#Y{type M <: K.this.C}  <:  com.arteris.forj.ir.K#Y (left is approximated)
[error]    |           ==> com.arteris.forj.ir.K#Y  <:  com.arteris.forj.ir.K#Y (left is approximated)
[error]    |           <== com.arteris.forj.ir.K#Y  <:  com.arteris.forj.ir.K#Y (left is approximated) = true
[error]    |         <== com.arteris.forj.ir.K#Y{type M <: K.this.C}  <:  com.arteris.forj.ir.K#Y (left is approximated) = true
[error]    |       <== com.arteris.forj.ir.YOf[K.this.C]  <:  com.arteris.forj.ir.K#Y (left is approximated) = true
[error]    |     <== X.this.CType  <:  com.arteris.forj.ir.K#Y (left is approximated) = true
[error]    |   <== (x : X.this.CType)  <:  com.arteris.forj.ir.K#Y = true
[error]    |
[error]    | The tests were made under the empty constraint
[error]     ----------------------------------------------------------------------------

Observations:

• Renaming a.scala to c.scala makes sbt start with b.scala... and the issue disappears. Really looks like a race condition.
• Replacing YOf[K] by K#Y in a.scala, makes the issue disappear (in the compilation of b.scala ?!)
• The race creates a memory effect. Once b.scala has been compiled normally once, re-introducing the offensive flavor of a.scala does not re-create the issue, ... until sbt clean.

[ftucky]

Actually when a.scala and b.scala are merged in a single file, in the right order, issue appears in a single scalac run, independently from sbt. I edited the orginal post to reflect the minimized code, and scastie pointers.

[smarter]

Thanks! I was able to minimize it slightly more:

object Foo:
	def bar(x : YOf[Any]): Unit = ???
	bar(???)

trait K:
  trait X:
    type CType <: YOf[Any]
    def foo : K#X = 
      val x : CType = ???
      x

type YOf[T] = K#X {type M}

It seems to be a caching issue: while computing the right-hand side of YOf, we temporarily set YOf[T] >: Nothing <: Any to handle cycles. We have logic to ensure this is sound, but it looks like in this particular situation we end up incorrectly caching the temporary bounds as the super-type of YOf[Any]. The trace ends up returning true because by the time it gets run, this particular cache happens to have been invalidated (I'll have to investigate this too since it sounds like the cache shouldn't need to be invalidated if it weren't set incorrectly, but I'll focus on the correctness issue first :)).

[smarter]

I have a PR up at #16989, meanwhile I think the only workaround is to move definitions around to change the order in which they're processed by the compiler as you already discovered. Note that the list of files passed to the compiler by sbt is sorted, so changing filenames is a reliable to change the order in which files are processed.

[ftucky]

Thank you for all. I already walked away from the scheme: too twisted !
It was clear though that something fishy was happening: no reason to waste a minimized failing code.