Type constructor V parameterized with a type A including a member type T does not resolve T when parameterized with a concrete subtype of A

[noresttherein]

reproduction steps

    trait Assembler {
        type T
    }

    class AssemblerFunct[X] extends Assembler {
        type T = X
    }

    type AssemblerT[X] = Assembler { type T = X }

    class Values[A <: AssemblerT[_]] {
        def get: A#T = ???
        def value[N](a: AssemblerT[N]): N = component(a).get
        def component[N](a: AssemblerT[N]): Values[a.type] = new Values[a.type]
    }

problem

Error:(20, 52) type mismatch;
 found   : this.T
    (which expands to)  _$1
 required: N
        def value[N](a: AssemblerT[N]): N = component(a).get

expectation

Typer should(?) resolve A#T forSome { type A = a.type } to a.type#T => a.T => N.

[joroKr21]

That might be a bug but A <: AssemblerT[_] makes no sense in this example - you can just use A <: Assembler. In case you need a workaround.

[noresttherein]

Assembler { type T = t } forSome { type T = t } very much isn't the same as Assembler. This is a very stripped down example for the described issue, but there are many constructs which compile with one of the above and not the other and vice versa. My guess (at least intention behind experimenting with many variants of the above) is that the former is a subtype of Assembler which has a definition of T (so A#T forSome { type A <: AssemblerT[_] } =:= a.T for any a :A. I may be totally wrong, because expermenting with constructs like these yield a lot of compiler errors despite looking to my untrained eye like they should be allowed.

[SethTisue]

in Dotty,

12 |        def get: A#T = ???
   |                 ^
   |                 A is not a legal path
   |                 since it is not a concrete type

since projections on abstract types aren't allowed anymore

[noresttherein]

As I said, I may be completely wrong because I don't know the exact algorithm the typer uses to unify abstract type terms with type parameters of the argument, particularly when a type is 'fixed' as some abstact type _$1 and not unified further as in the example.

My understanding was that as a :AssemblerT[N] and a.type =:= N, then as seen from Values[a.type], A =:= a.type and, after parameter substitution, A#T =:= a.type#T =:= N.

It may entirely be that once again I was foiled by my poor understanding of path dependent types and a.type(in type Values[a.type]is a different type thana.type(in method component)`. If so, I apologize for taking your time, but I found this example so confusing I assumed it was a not intentional side effect at best. Of course, it is not your job to educate programmers on Scala :)

[joroKr21]

I'm not sure TBH. What you're saying makes sense, but we have to check the details (I haven't yet). Just wanted to say that abstract type members are semantically equivalent to existential types and in fact dotty is removing existential types without losing much expressivity because we can still use abstract type members.

Is there anything in your original code that prevents you from just using abstract type members as a workaround?

[joroKr21]

since projections on abstract types aren't allowed anymore

Ah right then there is also the issue that this is all unsound 😄

[noresttherein]

If by refactoring to abstract type members you mean only Values[A <: Assembler], then I alread did it because of this issue. I tried to go with the above because I wanted to somehow eliminate casts A#T.asInstanceOf[a.T] without mandating A <: Singleton.

What got me somewhat worried though is the mention that projections on all abstract types aren't allowed in Dotty (ergo, at some point, in scala). If I understand correctly then, I won't be able to use A#T even inside Values[A <: Assembler]? It would hit me very hard in ways I can't see workarounds for right of the bat. I would gladly elaborate, but this probably isn't the best place for it.

That bane would become a boon however if I were able to express 'A <: Assembler where the member type T has a concrete definition' (which indirectly inspired the posting of this issue). If I could put bounds enforcing a1.T =:= a2.T for all a1, a2 :A, where A is a type parameter, it would actually clean a lot of code in most of my projects which currently rely on 'safe' casting.

[SethTisue]

@joroKr21 noticed this looks like a duplicate of #2346