type aliases leak underlying opaque types through separate compilation

[soronpo]

Match types defined in the scope of an opaque definition leak the underlying opaque type if used in separate compilation module.
Note: could be related to #12944

Compiler version

v3.0.2-RC2

Minimized code

See minimized branch at: https://github.com/soronpo/dottybug/tree/match_type_opaque_leak

main/scala/core/Foo.scala

package core

opaque type Foo <: Int = Int
type LeakFoo[M] = M match
  case _ => Foo

main/scala/LeakFoo.scala

type LeakFoo[M] = core.LeakFoo[M]

val works = summon[LeakFoo[Any] =:= core.Foo]

test/scala/Foo.scala

val shouldFail: LeakFoo[Any] = 1
val shouldWork = summon[LeakFoo[Any] =:= core.Foo]

Output

[error] -- Error: IdeaProjects\dottybug\src\test\scala\Foo.scala:2:50 --
[error] 2 |val shouldWork = summon[LeakFoo[Any] =:= core.Foo]
[error]   |                                                  ^
[error]   |                      Cannot prove that core.Foo$package.Foo =:= core.Foo.
[error] one error found

Expectation

shouldFail should generate a type-mismatch error
shouldWork should compile fine.

[prolativ]

It looks like the type alias is quite important, which is not emphasised in the description. Everything seems to behave as expected if we use core.LeakFoo[M] instead of just LeakFoo[M] in the test

[soronpo]

OK, it looks like match types have nothing to do with this, and any type referencing (aliasing) within the opaque source code is exposed to leaks via separate compilation.

Minimized code

See minimized branch at: https://github.com/soronpo/dottybug/tree/opaque_loss

main/scala/core/Foo.scala

package core

opaque type Foo[T] <: Int = Int
type LeakFoo[T] = Foo[T]

main/scala/LeakFoo.scala

import scala.util.NotGiven
type LeakFoo[T] = core.LeakFoo[T]
val ok = summon[NotGiven[LeakFoo[1] =:= LeakFoo[2]]]

test/scala/Foo.scala

import scala.util.NotGiven
val notok = summon[NotGiven[LeakFoo[1] =:= LeakFoo[2]]]

Output

[error] 2 |val notok = summon[NotGiven[LeakFoo[1] =:= LeakFoo[2]]]
[error]   |                                                       ^
[error]   |no implicit argument of type util.NotGiven[core.Foo$package.Foo[(1 : Int)] =:=
[error]   |  core.Foo$package.Foo[(2 : Int)]
[error]   |] was found for parameter x of method summon in object Predef
[error] one error found

[odersky]

The problem is that the opaque type is defined toplevel in a package rather than a class or object. I have looked into it in depth now, but I have not yet found a way to make this work. There might be too many assumptions about packages that prevent us from mapping opaque type members to their bounds. So a possible outcome might be add a restriction that opaque types cannot be toplevel.

[smarter]

We define IArray as a top-level opaque type so it won't be easy to walk that back.

[soronpo]

I just checked and indeed if I place the opaque in an object and export it to top-level or alias it into top-level the problem goes away.
How does that relate to the separate compilation?
Can't the implementation somehow simulate all top-level opaques to be in an anonymous object that is exported?:

//at top-level
opaque type Foo = Int

Will change into

export `$opaqueFoo`.Foo
object `$opaqueFoo`:
  opaque type Foo = Int

This is an ugly hack, but maybe the easiest way to solve the problem.

[dwijnand]

@odersky Do you know what's different in the model between the separate and the joint compilation scenarios?

[odersky]

I could track it down to a difference in the way package objects were inserted when typechecking source and unpickling. The unpickling version was faulty.