Singleton bound and type projections don't play nice with each other

[Blaisorblade]

If a value member tasty has abstract type T and T is marked as being a singleton type (that is, currently, T <: Singleton), I’d expect tasty.type = T, because both types are singleton that contain tasty. This currently fails in Scalac and Dotty.

A minimized example:

scala> trait A { type T; val prod: T; val cons: T => Int = _ => 0 }; trait Foo { type U <: Singleton with A; val tasty: U }
defined trait A
defined trait Foo

scala> val v: A = new A { type T = Int; val prod: T = 1}; val u: Foo = new Foo { type U = v.type; val tasty: U = v }
v: A = $anon$1@5faeeb56
u: Foo = $anon$2@5396eeb1

scala> u.tasty.cons(u.tasty.prod: u.U#T)
<console>:13: error: type mismatch;
 found   : u.U#T
 required: u.tasty.T
       u.tasty.cons(u.tasty.prod: u.U#T)
                                ^

/cc @milessabin

Background

I ran into this while prototyping a heavily path-dependent API in Dotty (an early version of Tasty reflection), in relation to https://github.com/lampepfl/dotty/pull/4577/files/b315dbfa9f2d206cc26da75779388fca98faaabd#r191016341; the workaround involved turning defs into vals, which I suspect is acceptable here but potentially annoying when trying to save memory.

Alternatives

For the example above, enabling the definition of idempotent methods might be more general, if we ever get there.

Soundness

Not formally investigated, since nobody yet added to DOT either singleton types, type projections or singleton type variables.

[milessabin]

If you leave off the type annotation it's fine,

scala> u.tasty.cons(u.tasty.prod)
res1: Int = 0

TBQH, I have never fully understood either the intended semantics of type projections, or their realization in scalac's implementation, so I can't say I'm particularly surprised that they produce odd results.

Given that Dotty has dropped type projections, what is the corresponding failing case there?

[Blaisorblade]

If you leave off the type annotation it's fine,

Sure, but I should have clarified that's not the real usecase, just a minimized academic one. In my real example, I have u.U#T in some code and u.tasty.T in some other.

TBQH, I have never fully understood either the intended semantics of type projections, or their realization in scalac's implementation, so I can't say I'm particularly surprised that they produce odd results.

I can't speak to the implementation.
EDIT: And I don't think they can make sense together with override type. override type doesn't let you override concrete types, at least now, so all is good there.

Given that Dotty has dropped type projections, what is the corresponding failing case there?

It's literally the same, see scala/scala3#4583 (the only link was in the other direction). Dotty didn't quite drop type projections, just restricted them severely, with the intention of only allowing projections on types inhabited by non-null values (hence, having good bounds), which is approximated by "realizability" — see https://github.com/lampepfl/dotty/pull/4036/files#diff-cefd0dd90ffd752aa3b756438872098fL71 for the latest version (not yet merged) of the definition of realizability. But they don't appear in current formal DOT proofs, which is unsatisfactory (I hope we'll get there in ongoing extensions, but it's far from a trivial matter).