Conformance of type projections in SLS 3.5.2 violates expectations, conflicts with intersection types and isn't supported

[Blaisorblade]

Just noticed a likely bug in the SLS 3.5.2 on conformance, possibly relevant to #7278 — it says that

A type projection T#t conforms to U#t if T conforms to U.

and that looks incorrect.

That's only correct for nested classes in an inheritance relation (scala/scala3#4361 (comment)), as when you emulate virtual classes in Scala; but it's wrong for nested classes in general, and it appears incorrect even for abstract types.
Take T <: U and T#t <: U#t, then we can have U#t >: S <: U1 and T#t = U1, which leads us to the false conclusion that U1 <: U#t.

What is true is that T#t's bounds must be at least as restrictive than U#t's, or, borrowing @sstucki's terminology, T#t must have a interval kind that is a (non-strict) subkind of U#t's kind. That seems analogue to the rule for term-level members, after you shift one level up everything: the type of term member T.method must be a (non-strict) subtype of U.method's type.

Proposed replacement

Quoting myself in scala/scala3#4583 (comment):

Proposed new clauses:

SLS 3.5.1:

A type projection T#t is equivalent to U#t if T is equivalent to U.

SLS 3.5.2:

A type projection T#t conforms to U#t if T is equivalent to U. [not if T conforms to U].

[Blaisorblade]

BTW, that SLS clause appears to be implemented rather closely by Scalac in
https://github.com/scala/scala/blob/4e120ce7863758ac863bb42d2295b3040459f28e/src/reflect/scala/reflect/internal/tpe/TypeComparers.scala#L444-L449 — though the use sym2.isAbstractType and sym2.isClass shows this rule is not used for inner classes.

[eparejatobes]

Take T <: U and T#t <: U#t, then we can have U#t >: S <: U1 and T#t = U1, which leads us to the false conclusion that U1 <: U#t.

where's the problem there?

[Blaisorblade]

All that's true is that U#t <: U1, not that U1 <: U#t — U#t should be abstract.

[milessabin]

Here's an example where conformance would be wrong. Fortunately scalac doesn't follow the spec here,

scala> object Foo { type T = Int } ; object Bar { type T = String }
defined object Foo
defined object Bar

scala> type FB = Foo.type with Bar.type
defined type alias FB

scala> def frob(ft: Foo.type#T): FB#T = ft
<console>:13: error: type mismatch;
 found   : Foo.T
    (which expands to)  Int
 required: String
       def frob(ft: Foo.type#T): FB#T = ft

Foo.type conforms to FB, so if we follow SLS 3.5.2 as it is now it ought to follow that Foo.type#T conforms to FB#T.

[eparejatobes]

@eparejatobes's question is trickier than I first thought — took me a while to convince myself, but it appears this might not lead to type unsoundness, but only to turning abstract type projections U#t into concrete types equal to their upper bound.

Exactly, and incidentally this is how I think they should behave :)

[eparejatobes]

@milessabin

Here's an example where conformance would be wrong. (...)
Foo.type conforms to FB

why? it obviously shouldn't; plus in that case FB#t should be Int with String.

[Blaisorblade]

@milessabin that's true and it is an issue, but since FB is uninhabited, that's a bad bounds problem. A correct Scala compiler would have to reject FB#T, and Dotty does:

scala> def frob(bt: Bar.type#T): FB#T = bt
1 |def frob(bt: Bar.type#T): FB#T = bt
  |                          ^
  |FB is not a legal path
  |since it has a member T with possibly conflicting bounds Int | String <: ... <: Int & String

So I'd like to focus on "issues with this SLS rule for type projections that we'll keep allowing in Dotty".

(Reposting with fixes)
@eparejatobes's question is trickier than I first thought — took me a while to convince myself, but it appears this might not lead to type unsoundness, but only to turning abstract type projections U#t into concrete types equal to their upper bound.

In the OP I've replaced "unsound" with "incorrect" to clarify (though I didn't mean to talk about type unsoundness).

FWIW, that clause also appears problematic for another reason: it's false for any implementation that does eager dealiasing of type projections. Below it implies B#T <: A#T, but B#T = Any and Any <: A#T doesn't hold. I agree that taking the consequences of that paragraph would force A#T = Any but a.T <: Any for any a: A, but I'm not convinced that's desirable. (EDIT: fixed, I had written Int for Any before).

scala> class A { type T }
defined class A

scala> class B extends A { type T = Any }
defined class B

scala> def downcast(x: Any): A#T = x
<console>:12: error: type mismatch;
 found   : x.type (with underlying type Any)
 required: A#T
       def downcast(x: Any): A#T = x
                                   ^

scala> def downcast(x: Any): A#T = (x: B#T): A#T
<console>:13: error: type mismatch;
 found   : Any
 required: A#T
       def downcast(x: Any): A#T = (x: B#T): A#T
                                     ^

[milessabin]

So I'd like to focus on "issues with this SLS rule for type projections that we'll keep allowing in Dotty".

Fair enough, but then I think this discussion belongs on the Dotty issue. I don't see this being fixed in scalac any time soon.

[Blaisorblade]

Foo.type conforms to FB

why? it obviously shouldn't;

Uh right, it's only FB <: Foo.type not the other way around.

plus in that case FB#t should be Int with String.

That's indeed the Dotty semantics of with, but it's not so in Scalac (which I'm sure has its share of issues).

@milessabin can your example be made to work then?

Fair enough, but then I think this discussion belongs on the Dotty issue. I don't see this being fixed in scalac any time soon.

Ignoring the issues with your example, that might be true. Tho the only Scala spec currently lives here and I'm uneasy with hosting a diverging spec in Dotty.
In any case, the SLS rule in question seems to not work well in Scalac either.

[eparejatobes]

@Blaisorblade

FWIW, that clause also appears problematic for another reason: it's false for any implementation that does eager dealiasing of type projections. (...)

I don't quite see what Int is doing there. In your snippet, the main issue I see is with letting classes have undefined types; nobody would think this is a good idea for values, yet scala allows it for types (??). I see "turning abstract type projections U#t into concrete types equal to their upper bound" only as a patch for this.

[milessabin]

Uh right, it's only FB <: Foo.type not the other way around.

Whoops, yes, back to front. But it's still an issue the right way around,

scala> object Foo { type T = Int } ; object Bar { type T = String }
defined object Foo
defined object Bar

scala> type FB = Foo.type with Bar.type
defined type alias FB

scala> def frob(fbt: FB#T): Foo.type#T = fbt
<console>:13: error: type mismatch;
 found   : String
 required: Foo.T
    (which expands to)  Int
       def frob(fbt: FB#T): Foo.type#T = fbt
                                         ^

[eparejatobes]

Whoops, yes, back to front. But it's still an issue the right way around, (...)

your frob there should compile; a different matter altogether is being able to come up with a value of type FB#T, which should be Int with String (I know, this is not the case in scala 2.x etc). Note that 3.5.2 would actually imply that the projection on an intersection would be equivalent to the intersection of the projections.

[Blaisorblade]

I don't quite see what Int is doing there.

Oh, fixed, I meant Any (or whatever B.T is set to).

In your snippet, the main issue I see is with letting classes have undefined types; nobody would think this is a good idea for values, yet scala allows it for types (??). I see "turning abstract type projections U#t into concrete types equal to their upper bound" only as a patch for this.

First, I can make A's abstract (edited the snippet for it, thanks GitHub for edit histories), but your idea would set that to its upper bound as well, unnecessarily.

But thanks for explaining your reasoning. I used to think that too, but this is actually by design and I agree — Scalac was changed to allow it. Undefined type members are supposed to behave as existentials, and they'll be the only way to have existentials in Scala 3.
I'm not sure they're fundamental in concrete values and there are a couple of open questions there in the theory, but I'm planning to address those theoretical questions anyway.

[milessabin]

a different matter altogether is being able to come up with a value of type FB#T, which should be Int with String (I know, this is not the case in scala 2.x etc)

I think we're talking at cross purposes here. I agree with you wrt Dotty, but given the semantics of with in Scala, clause 3.5.2 is clearly wrong wrt Scala.

[Blaisorblade]

Note that 3.5.2 would actually imply that the projection on an intersection would be equivalent to the intersection of the projections.

That's true, and that's indeed one reason 3.5.2 can't be true for Scala 2.

[eparejatobes]

I think we're talking at cross purposes here. I agree with you wrt Dotty, but given the semantics of with in Scala, clause 3.5.2 is clearly wrong wrt Scala.

I see it the other way round: first, what's wrong at any rate is the implementation; otherwise, let's just definitely throw away the spec for good. But also, why is 3.5.2 wrong and not the semantics of with?

[milessabin]

Let's at least agree that 3.5.2 conflicts with the semantics of with in Scala, and that @Blaisorblade's proposed amendment eliminates that conflict.

Whether or not that's that right thing to do in Dotty is a different question altogether.

[Blaisorblade]

Yes, I'll have to figure this out for Dotty, and confirm the intended semantics of type projections.

[Blaisorblade]

Looking at the problematic example in light of lampepfl/dotty-feature-requests#14 (comment), I'd now blame with and not projections. Expanding FB#T to String is wrong.

(EDITED): I'd suggest closing this issue, or focusing it on @milessabin valid complaints on intersections.

[SethTisue]

The discussion here is long and difficult to follow. If someone thinks the intersections aspect deserves its own ticket, I invite y'all to open one that concisely focuses on that alone.