Unification check in deriving is incorrect

[sugakandrey]

Compiler version

3.0.1

Minimized code

trait TC[F[_, _[_]]]
object TC {
  def derived[F[_, _[_]]]: TC[F] = ???
}

case class Foo[A](a: A) derives TC

Output

Missing type parameter for _ in subpart Foo[_] of inferred type ([_, _[_$3]] =>> Foo[_])

Expectation

Foo cannot be unified with the type argument of TC as kinds of A and _[_] are different.
Note, that if we change TC to TC[_[_], _], we will now get Foo cannot be unified with the type argument of TC, even though it should compile. Perhaps https://github.com/lampepfl/dotty/blob/b7d2a122555a6aa44cc7590852a80f12512c535e/compiler/src/dotty/tools/dotc/typer/Deriving.scala#L163 was meant to use takeRight instead of take?

[Kordyjan]

I'm not sure I understand what you mean.

Note, that if we change TC to TC[[], _], we will now get Foo cannot be unified with the type argument of TC, even though it should compile.

This part is especially is not clear to me. Could you provide a sample that should compile with some explanation? I'm still convinced that in the case you described compilation should fail.

[sugakandrey]

@Kordyjan

Of course compilation should fail, only for a correct reason. Currently, it wrongly passes preliminary checks for the same-kindness of overlapping type parameters, generates a member with a nonsensical type TC[[x, y[_] =>> Foo[y]] and only then fails to typecheck it.

https://github.com/lampepfl/dotty/blob/b7d2a122555a6aa44cc7590852a80f12512c535e/compiler/src/dotty/tools/dotc/typer/Deriving.scala#L111-L133

trait TC[F[_[_], _]]
object TC {
  def derived[F[_[_], _]]: TC[F] = ???
}

case class Foo[A](a: A) derives TC

This example fails to compile, even though it should, because kinds of A and _ are both Type. In this cases generated derived$TC member would have return type TC[[x[_], y] =>> Foo[y]].

[Kordyjan]

Oh, I see it now! Thanks for the explanation. Both of these behaviors are indeed the result of an underlying bug.