Type alias causes problems for implicit search

[travisbrown]

minimized code

trait TC[F[_]]

object TC {
  def check[F[_], A](x: F[A])(implicit F: TC[F]): Unit = ()
}

case class Foo[+E, +A](value: A)

object Foo {
  type WithList[+E, +A] = Foo[List[E], A]

  implicit def instance[E]: TC[[x] =>> Foo[E, x]] =
    new TC[[x] =>> Foo[E, x]] {}
}

val x1: Foo[List[String], Int] = Foo(1)
val x2: Foo.WithList[String, Int] = Foo(1)

TC.check(x1)
TC.check(x2)

Compilation output

20 |TC.check(x2)
   |            ^
   |no implicit argument of type TC[([+A] => Foo.WithList[String, A])] was found for parameter F of method check in object TC.
   |I found:
   |
   |    Foo.instance[Nothing]
   |
   |But method instance in object Foo does not match type TC[([+A] => Foo.WithList[String, A])].

expectation

This is a minimization from the Cats tests, and the Scala 2 equivalent (using either kind-projector or ({ type L[x] = ... })#L for the type lambda) has no problems with this code.

Note that removing the variance annotation on the A in WithList resolves the issue for Dotty, but this isn't an option for Cats.

[smarter]

If we change the result type of instance to take a type lambda with a covariant type parameter (implicit def instance[E]: TC[[+x] =>> Foo[E, x]]), then TC.check(x2) works ... but TC.check(x1) doesn't work anymore. The problem is that we instantiate F to some type lambda with a specific variance before doing the implicit search, but if we guess wrong we won't find the typeclass instance.
More precisely, constraint solving ends up with:

?F >: [+A] => Foo.WithList[String, A] <: [A] => Any

If we leave ?F like this we risk ambiguous errors in implicit search, so currently we instantiate it:

?F := [+A] => Foo.WithList[String, A]

but maybe we could be less strict and leave the variance to be resolved by implicit search:

?F >: [+A] => Foo.WithList[String, A] <: [A] => Foo.WithList[String, A]

Hopefully that strikes a good balance between making implicit search too wide (and therefore finding multiple candidates) vs making it too narrow (and therefore not finding anything).