Inconsistent handling of match types on dependent types when overriding

[m8nmueller]

Compiler version

3.4.2

Minimized code

trait P:
  type Q

type Qaux[QQ] = P { type Q = QQ }
type QP[P] = P match
  case Qaux[q] => q

trait PString extends P:
  type Q = String

trait User[X <: P]:
  def get(x: X): QP[x.type]
  def use(f: (x: X) => QP[x.type] => String): String

class StringUser extends User[PString]:
  def get(x: PString): QP[x.type] = ???
  def use(f: (x: PString) => QP[x.type] => String): String = ???

Output

-- Error: test.scala:16:6 ------------------------------------------------------
16 |class StringUser extends User[PString]:
   |      ^
   |class StringUser needs to be abstract, since def use(f: (x: X) => QP[x.type] => String): String in trait User is not defined 
   |(Note that
   | parameter (x: X) => QP[x.type] => String in def use(f: (x: X) => QP[x.type] => String): String in trait User does not match
   | parameter (x: PString) => String => String in def use(f: (x: PString) => String => String): String in class StringUser
   | )
1 error found

Expectation

The compiler should realize that the two function types are exactly the result of replacing the type parameter X with the type PString, as it does for the non-function type in get.

[natsukagami]

This also happens with paths instead of match types

//> using scala 3.6.0-RC1-bin-SNAPSHOT

trait P:
  type Q

trait PString extends P:
  type Q = String

trait User[X <: P]:
  def get(x: X): x.Q
  def use(f: (x: X) => x.Q => String): String

class StringUser extends User[PString]:
  def get(x: PString): x.Q = ???
  def use(f: (x: PString) => x.Q => String): String = ???

I suspect it's something to do with variance...

[natsukagami]

//> using scala 3.6.0-RC1-bin-SNAPSHOT

trait P:
  type Q

trait PString extends P:
  type Q = String

type F[X <: P] = (x: X) => x.Q => String

val u = summon[F[PString] <:< ((x: PString) => x.Q => String)]

The compiler cannot prove this

[EugeneFlesselle]

Being invariant is enough:

type Inv[X]
type F[X <: P] = (x: X) => Inv[x.Q]

val v0: F[PString] = ???
val v2: (x: PString) => Inv[x.Q] = v0 // error