Inline error when exploiting transparency of opaque type within an object

[sjrd]

Compiler version

482dfeb

Minimized code

object O:
  opaque type T = Int
  inline def x: Int = P.id(2)

object P:
  def id(x: O.T): O.T = x

object Test {
  def main(args: Array[String]): Unit = println(foo())

  def foo(): Int = O.x
}

Output

-- [E007] Type Mismatch Error: tests/run/hello.scala:11:21 ---------------------
11 |  def foo(): Int = O.x
   |                   ^^^
   |                   Found:    (2 : Int)
   |                   Required: O.T
   |----------------------------------------------------------------------------
   |Inline stack trace
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |This location contains code that was inlined from hello.scala:3
 3 |  inline def x: Int = P.id(2)
   |                           ^
    ----------------------------------------------------------------------------
   |
   | longer explanation available when compiling with `-explain`
1 error found

Note that error happens during inlining. The code originally typechecks.

Expectation

Either there should be a compile error at the definition of O.x, or inlining O.x should succeed.

Analysis

The definition of O.x can be seen as a bit dubious, since it needs Int =:= O.T. Normally, the alias of an opaque type alias is only visible when accessed through a this prefix (Int =:= this.T is true). The documentation for opaque type aliases has a specific rule for this case: within the definition of O, we accept that O.T can see the alias. This is supposed to be fine, since we know that O eq this. I am not sure how the compiler even allows that in the first place, though.

Once inlined, however, the O.T escapes the scope of O. And that causes an issue. Normally, opaque aliases are seen after inlining because (IIUC what @odersky told me) the val $this receives a more specific type which contains the aliases of opaque types in a refinement. That's fine for this.T references, which become $this.T, but it does not help for those out-of-band references O.T. Once outside the definition of O, they break.

TBH I don't see how inlining can fix this in the general case. Simple cases might be patched up with some casts, but it doesn't work for general subtyping relationships.

This makes me question the validity of the special rule in the first place. 😕

[dwijnand]

I don't think we should negotiate with exploiters! 😉

Either there should be a compile error at the definition of O.x,

I disagree. There's nothing illegal about the definition. Indeed using it within O, for whatever reason, works as intended.

Now, I won't disagree with you that the error message could explain more (and I didn't look at what -explain adds).

Otherwise we'd have to disallow O.x unless it's private[this] - after we've correctly identified that O.x uses O.this knowledge.

[sjrd]

Maybe I wasn't very clear on what I suggest being disallowed. The following alternative definition of O.x works in all situations:

-inline def x: Int = P.id(2)
+inline def x: Int = P.id(2: O.T): this.T

In that alternative, we introduce type ascriptions as intermediate "evidences". They help in the same way that (x: T): B helps where T >: A <: B, i.e., they tell the type checker how to recover the lost transitivity.

The current rule is weird because it artificially creates the transitivity O.T =:= this.T =:= Int gives O.T =:= Int, but only within a certain scope. AFAICT, this is the only case of scope-dependent subtyping in the system (GADTs are close, but they're transient and converted to casts in TASTy). It is similar to saying that we should in fact receive A <: B within a scope where type T >: A <: B is defined, although that is not something we do.

[SethTisue]

def id(x: O.T): O.T can be split into def get: O.T and def put(x: O.T): Unit and it's put that's problematic, not get. (Though we don't want to break get, of course...)