Dotty: Regression: type inference involving higher-kinded types and upper-bounds

Created on 28 Aug 2020  路  2Comments  路  Source: lampepfl/dotty

Minimized code

// compiles fine
object Main extends App {
  trait SubtypeOf[A[_], B[_]]
  implicit def instance[F[_], G[a] >: F[a]]: SubtypeOf[F, G] = new SubtypeOf[F, G] {}

  implicitly[SubtypeOf[List, Seq]]
}

// won't compile on dotty, but compiles fine on scala 2.13.3
object Main2 extends App {
  trait SubtypeOf[A[_], B[_]]
  implicit def instance[G[_], F[a] <: G[a]]: SubtypeOf[F, G] = new SubtypeOf[F, G] {}

  implicitly[SubtypeOf[List, Seq]]
}

Output

no implicit argument of type Main.SubtypeOf[List, Seq] was found for parameter ev of method implicitly in object DottyPredef.
I found:

    Main.instance[Nothing, Nothing]

But method instance in object Main does not match type Main.SubtypeOf[List, Seq].

Expectation

Implicit resolution works in both cases.

typer scala2 bug

Most helpful comment

We don't even need implicit search to reproduce the problem:

object Test {
  trait SubtypeOf[A[_], B[_]]
  def instance[G[_], F[a] <: G[a]]: SubtypeOf[F, G] = new SubtypeOf[F, G] {}

  val x: SubtypeOf[List, Seq] = instance // error
}

All 2 comments

We don't even need implicit search to reproduce the problem:

object Test {
  trait SubtypeOf[A[_], B[_]]
  def instance[G[_], F[a] <: G[a]]: SubtypeOf[F, G] = new SubtypeOf[F, G] {}

  val x: SubtypeOf[List, Seq] = instance // error
}

It looks like our handling of constraints on higher-kinded type variable is incomplete, when we typecheck instance our constraint set looks like:

Constraint(
 uninstVars = G, F;
 constrained types = [G[_$3], F[a] <: G[a]] => SubtypeOf[F, G]
 bounds = 
     G[_$3]
     F[a] <: G[a]
 ordering = 
)

Notice that ordering is empty, compare with what we get in a method with simply-kinded type variables:

Constraint(
 uninstVars = G, F;
 constrained types = [G, F <: G] => SubtypeOf[F, G]
 bounds = 
     G
     F
 ordering = 
     F <: G
)

ordering is used to propagate constraints, the fact that we don't have it for hk types means that when we add an upper-bound constraint to G, we don't add the same constraint to F, so we might end up failing to find a valid solution to the type inference problem.

Was this page helpful?
0 / 5 - 0 ratings