Constraint solving of higher-kinded type variables is too coarse

[joroKr21]

Straight out of scala/bug#10753 (comment)

trait Bar[F[_]]
trait Foo[A]
trait Qux[A] extends Foo[A]
object Qux {
  implicit def string: Qux[String] = ???
  implicit def bar: Bar[Qux] = ???
}

case class Problem[A](a: A)
object Problem {
  import Qux._
  implicit def deriv[A, F[_]](implicit B: Bar[F], F: F[A]): F[Problem[A]] = ???
  implicitly[Foo[Problem[String]]]
}

I don't know if this is the intended behaviour in Dotty, but I'm reporting it just in case. It looks like F is instantiated to Foo in Dotty but not in Scala, which is what scala/bug#10753 is all about. The code above is a counterexample (maybe it can be minimized further).

[smarter]

Here's a minimized example:

trait Higher[F[_]]
trait Super[A]
trait Sub[A] extends Super[A]

object Test {
  implicit def higherSub: Higher[Sub] = ???
  implicit def deriv[F[_]](implicit bla: Higher[F]): F[String] = ???

  val x: Super[String] = deriv
}

To typecheck this we need to solve:

   ?F[String] <: Super[String]

At this point we instantiate ?F := Super, meaning that higherSub is no longer a valid solution. We do this because ?F <: Super wouldn't be a precise enough constraint, for example Wrong defined as trait Wrong[A <: Int] extends Super[A] would satisfy this constraint, but Wrong[String] wouldn't typecheck. scalac does not have this issue because it does not constrain ?F before doing the implicit search, this means that if we add an implicit def higherList: Higher[List] = ???, scalac will complain with an ambiguous implicit error even though there is no ambiguity.

To solve this properly we would need a way to constrain the kind of ?F without constraining ?F itself (we want ?F to have kind * -> * which is different from (* <: Int) -> *, the kind of Wrong), this is likely to be hard to do given how complex constraint solving already is, and the fact that we never explicitly represent kinds in the compiler currently.

[smarter]

Thinking about it more, I wonder if we could constrain the kind of ?F using just type constraints. If we introduce a fresh type variable ?F_1 and set the constraints:

?F =: [X] => ?F_1[X]
?F_1 <: Foo

Then ?F_1 = Wrong wouldn't be a valid solution.

[smarter]

Actually, no need for a fresh type variable, we can just set:

?F >: [X] => Nothing <: [X] => Foo[X]

[Blaisorblade]

We do this because ?F <: Super wouldn't be a precise enough constraint, for example Wrong defined as trait Wrong[A <: Int] extends Super[A] would satisfy this constrain

There seems to be some confusion. I think we have Super = [X] => Super[X], right?
Then, I think we have Wrong[A] <: Super[A] but not Wrong <: Super because of the variance. Otherwise, ?F <: [X] => Foo[X] would be equivalent to ?F := Foo.

I already suspected you can have Wrong[A] <: Super[A] but not Wrong <: Super earlier in #3856 (comment).

[smarter]

Hmm right, then you can scratch everything I said above :).

[Blaisorblade]

If my interpretation works, then maybe we could set ?F <: Super, and then fix any code that gets confused about this if possible, no?

[smarter]

Yes.

[smarter]

I've played a bit with this, but this will be annoying to get working properly until we get rid of the poly-kinded Nothing, because currently we can end up instantiating type variables with a wrong kind if we're not careful, see https://github.com/dotty-staging/dotty/commits/fix/hk-constraint

[Blaisorblade]

Wait, if Nothing is poly-kinded then ?F := Nothing is well-kinded, no? (And Martin wants to add AnyKind). OTOH, Nothing isn't poly-kinded enough.

[smarter]

Yes, but the problem is that we start with for example: ?F >: Nothing <: [X <: Int] => Any, then we do:

?F[A] <:< List[A]
  ?F <:< List

At this point we should not instantiate anything and return false because the kind of?F is not a subkind of the kind of List, but since the lower-bound of ?F is a valid solution, we end up setting ?F := Nothing.