Invariant opaque type refinement loss across external dependency

[soronpo]

Edit:

I managed to further minimize the example.

---

It seems that type inference behaves differently across test dependency and fails to reduce (possibly any kind of different module dependency is affected).

Compiler version

v3.0.1-RC2 (also checked on nightly 3.0.2-RC1-bin-20210624-ecbe3d2-NIGHTLY)

Minimized code

Minimized project at: https://github.com/soronpo/dottybug/tree/invariance_widen_err

Main.scala

opaque type Lie[W <: Int] = Int
object Lie:
  trait TC[-T]:
    type Out
  object TC:
    given [W <: Int]: TC[Lie[W]] with
      type Out = W

val x  = summon[Lie.TC[Lie[7]]]
val works = summon[x.Out =:= 7]

Test.scala //must be placed at scala/test

object Test:
  val x  = summon[Lie.TC[Lie[7]]]
  val fails = summon[x.Out =:= 7]

Output

[error] -- Error: C:\IdeaProjects\dottybug\src\test\scala\Test.scala:3:33
[error] 3 |  val fails = summon[x.Out =:= 7]
[error]   |                                 ^
[error]   |                 Cannot prove that Test.x.Out =:= (7 : Int).
[error] one error found

Expectation

No error. Notice the same expression works within the main module and fails within the test module.

Note

Opaque types seem to be part of the problem, since if we change Lie to a trait the error goes away.
The contravariance in Lie.TC is also crucial for the error, but it should not cause widening because Lie is invariant.

[SethTisue]

(Dale and I briefly wondered if works works because it can see inside the opaque type (being in the same scope), but moving the opaque type to an inner scope doesn't break works, so apparently separate compilation is a key ingredient here.)

[soronpo]

I updated the title to reflect this is an opaque type issue

[joroKr21]

Another issue with separate compilation of opaque types: #13001

[anatoliykmetyuk]

It would be good to narrow the original example down a bit. Also, it would be good to see if it can be expressed in terms of separate compilation – using scalac only, factoring out SBT.

[soronpo]

@anatoliykmetyuk I further minimized the example. See updated OP.
I also verified that when running the compilation manually via scala3-compiler, I still get the error.

# scala3-compiler src\main\scala\Main.scala                                                                             
# scala3-compiler src\test\scala\Test.scala                                                                             
-- Error: src\test\scala\Test.scala:3:33 -------------------------------------------------------------------------------
3 |  val fails = summon[x.Out =:= 7]                                                                                    
  |                                 ^                                                                                   
  |                                 Cannot prove that Test.x.Out =:= (7 : Int).                                         
1 error found                                                                                                           

[anatoliykmetyuk]

Looks good!