Aux pattern not working for higher types

[noresttherein]

reproduction steps

using Scala 2.13.3,

    import scala.language.implicitConversions

    trait Thing[O]

    class Something[O] extends Thing[O]

    trait Project[M] {
        type Projection[O] <: Thing[O]
    }

    type Aux[X, Y[O] <: Thing[O]] = Project[X] { type Projection[O] = Y[O] }

    implicit def projectThing[T[X] <: Thing[X], O]: Project[T[O]] { type Projection[X] = T[X] } = ???

    implicit def project1[T <: Thing[_]](thing: T)(implicit projection: Project[T]): projection.Projection["xD"] = ???

    implicit def project2[T <: Thing[_], P[O] <: Thing[O]]
                         (thing: T)(implicit projection: Aux[T, P]): P["xD"] = ???

    implicit def project3[T <: Thing[_]](thing: T)(implicit projection: Project[T] { type Projection[O] <: Something[O] }): projection.Projection["xD"] = ???

    def something = new Something[Any]

    def p1 = project1(something)
    def p2 = project2(something)
    def p3 = project3(something)

    p1: Nothing //correct, Something["xD"]
    p2: Nothing //type lost: this.Projection["xD"]
    p3: Nothing //correct, Something["xD"]

problem

I would expect all three projections to result in Something["xD"]. This is of course very problematic in dependent implicits which can't use a member type of one implicit parameter as part of a type of another implicit parameter.

[SethTisue]

Is the situation improved in Dotty?

[joroKr21]

This is what I get (newlines added by me):

        p1: Nothing //correct, Something["xD"]
               ^
On line 28: error: type mismatch;
        found   : Something["xD"]
        required: Nothing

        p2: Nothing //type lost: this.Projection["xD"]
               ^
On line 29: error: type mismatch;
        found   : this.Projection["xD"]
           (which expands to)  Something["xD"]
        required: Nothing

        p3: Nothing //correct, Something["xD"]
               ^
On line 30: error: type mismatch;
        found   : Something["xD"]
        required: Nothing

It seems to be working (note the "which expands to")

[joroKr21]

This fails in the REPL (has to be two statements):

scala> import scala.language.implicitConversions
     |
     |   trait Thing[O]
     |
     |   class Something[O] extends Thing[O]
     |
     |   trait Project[M] {
     |     type Projection[O] <: Thing[O]
     |   }
     |
     |   type Aux[X, Y[O] <: Thing[O]] = Project[X] { type Projection[O] = Y[O] }
     |
     |   implicit def projectThing[T[X] <: Thing[X], O]: Project[T[O]] { type Projection[X] = T[X] } = ???
     |   implicit def project2[T <: Thing[_], P[O] <: Thing[O]]
     |     (thing: T)(implicit projection: Aux[T, P]): P["xD"] = ???
     |
     |   def something = new Something[Any]
     |   def p2 = project2(something)
import scala.language.implicitConversions
trait Thing
class Something
trait Project
type Aux
def projectThing[T[X] <: Thing[X], O]: Project[T[O]]{type Projection[X] = T[X]}
def project2[T <: Thing[_], P[O] <: Thing[O]](thing: T)(implicit projection: Aux[T,P]): P["xD"]
def something: Something[Any]
def p2: this.Projection["xD"]

scala> p2: Something["xD"]
       ^
       error: type mismatch;
        found   : this.Projection["xD"]
           (which expands to)  Something["xD"]
        required: Something["xD"]

If we paste it all at once it works. @noresttherein do you have a reproduction that fails to compile in a file (rather than the REPL)?