Type inference issue involve type alias and higher-kinded type

[TimWSpence]

As discussed in https://gitter.im/lampepfl/dotty?at=6033a71be634904e60b71e22

Compiler version

3.0.0-RC1

Minimized code

trait Functor[F[_]] {
  def map[A, B](fa: F[A]): F[B]
}

object data {

  opaque type OptionT[F[_], A] = F[Option[A]]

  extension [F[_], A](value: OptionT[F, A]) {

    def fold[B](default: => B)(f: A => B)(using F: Functor[F]): F[B] =
      F.map(value)(_.fold(default)(f))

    def cata[B](default: => B, f: A => B)(using x: Functor[F]): F[B] =
      fold(default)(f)(using x)
  }

}

Output

Compiler error
[error] -- [E050] Type Error: /Users/tim/dev/cheetahs/core/src/main/scala/io/github/timwspence/cheetahs/data.scala:30:11
[error] 30 |      F.map(value)(_.fold(default)(f))
[error]    |      ^^^^^^^^^^^^
[error]    |      method map in trait Functor does not take more parameters
[error] -- [E007] Type Mismatch Error: /Users/tim/dev/cheetahs/core/src/main/scala/io/github/timwspence/cheetahs/data.scala:33:29
[error] 33 |      fold(default)(f)(using x)
[error]    |                             ^
[error]    |Found:    (x : io.github.timwspence.cheetahs.Functor[F])
[error]    |Required: io.github.timwspence.cheetahs.Functor[F²]
[error]    |
[error]    |where:    F  is a type in method cata with bounds <: [_$3] =>> Any
[error]    |          F² is a type variable with constraint >: [X0] =>> io.github.timwspence.cheetahs.data.OptionT[F, X0] | F[X0] and <: [_$3] =>> Any

[smarter]

The problem isn't specific to extension methods or opaque types, it can be reproduced when writing:

import cats._

object data {

  type OptionT[F[_], A] = F[Option[A]]

  def fold[F[_], A, B](value: OptionT[F, A])(default: => B)(f: A => B)(using F: Functor[F]): F[B] =
    F.map(value)(_.fold(default)(f))

  def cata[F[_], A, B](value: OptionT[F, A])(default: => B, f: A => B)(using F: Functor[F]): F[B] =
    fold(value)(default)(f)(using F)
}

But inference works fine when dealiasing manually:

import cats._

object data {

  def fold[F[_], A, B](value: F[Option[A]])(default: => B)(f: A => B)(using F: Functor[F]): F[B] =
    F.map(value)(_.fold(default)(f))

  def cata[F[_], A, B](value: F[Option[A]])(default: => B, f: A => B)(using F: Functor[F]): F[B] =
    fold(value)(default)(f)(using F)
}

[smarter]

Minimized without the cats dependency:

trait Functor[F[_]]

object data {

  type OptionT[F[_], A] = F[Option[A]]

  def fold[F[_], A, B](value: OptionT[F, A])(f: Functor[F]): F[B] = ???

  def cata[F[_], A, B](value: OptionT[F, A])(f: Functor[F]): F[B] =
    fold(value)(f) // error
}

This compiles with Scala 2.

[anatoliykmetyuk]

I did some investigations on this issue. Minimized a bit to:

type X[F[_]]
type G[F[_], A] = F[String]

def g[M[_]](value: G[M, Int], f: X[M]): Unit = ???

def h[L[_]](value: G[L, Int], f: X[L]): Unit =
  g(value, f) // error

Apparently the typing of value in g(value, f) goes wrong. Here's how the compiler reasons:

G[L, Int] <:< G[M, Int]
G[L, Int] <:< M[String]
[A] =>> G[L, A] <:< M  // wrong, turned Int into a hole

First, the compiler dealiases the second G. Then, we try to carry out the G[L, Int] <:< M[String] check.

https://github.com/lampepfl/dotty/blob/00cf0b7878edd783c0ce552be183c4e3cd2c9735/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L938-L965

The compareAppliedTypeParamRef method above does not do the right thing here. Apparently it ends up trying to compare type constructors M and G, sees that G has more type parameters than M and tries to equalise the type parameters amount. It does so simply by making extra type arguments into holes:

https://github.com/lampepfl/dotty/blob/00cf0b7878edd783c0ce552be183c4e3cd2c9735/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L950

So that the comparison is done now between:

[A] =>> G[L, A] <:< M

Which succeeds and creates a lower bound constraint on L. Curiously, if we flip the parameter order in G, the error goes away:

type X[F[_]]
type G[A, F[_]] = F[String]

def g[M[_]](value: G[Int, M], f: X[M]): Unit = ???

def h[L[_]](value: G[Int, L], f: X[L]): Unit =
  g(value, f)

This is because the hole is now created where it should be: in place of M and L, not in place of Int, and [F] =>> G[Int, F] <:< M wouldn't be true.

I believe the error could be avoided in several ways. First, we could make sure the holes are inferred in an intelligent way rather than simply turning extra arguments into the holes. Second, we may want to try to dealias G[L, Int] sooner, e.g.

G[L, Int] <:< G[M, Int]
G[L, Int] <:< M[String]
L[String] <:< M[String]

Maybe canInstantiate can be the right place for doing this dealias:

https://github.com/lampepfl/dotty/blob/00cf0b7878edd783c0ce552be183c4e3cd2c9735/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1095-L1114

Because it happens after the G[M, Int] is dealiased and that's where tp1 starts to be treated as applied type.

I'm not sure which way is the best fix.

[smarter]

First, we could make sure the holes are inferred in an intelligent way rather than simply turning extra arguments into the holes.

Higher-order unification is an extremely hard problem in general (cf https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification), the current solution was chosen because it does "the right thing" in many situations and it's easy enough to understand what it does to adapt code to work with it, so any attempt at changing it is likely to break more code than it fixes, see the infamous scala/bug#2712.

Second, we may want to try to dealias G[L, Int] sooner

I haven't looked at the details here but in general dealiasing too early can break inference since people sometimes intentionally use aliases to change what gets inferred: https://github.com/lampepfl/dotty/blob/f8bd01c6219942b33bccd098b8bf5412ec22c264/compiler/src/dotty/tools/dotc/core/TypeApplications.scala#L324-L327

See also the discussion in #10221

[joroKr21]

Maybe a stupid question but why are we dealiasing instead of unifying G[L, Int] and G[M, Int] directly?

[smarter]

First, the compiler dealiases the second G.

Before we dealias, we should be compared the applied types as written, it looks like this is done but failing, looking around this seems to fix it:

diff --git compiler/src/dotty/tools/dotc/core/TypeComparer.scala compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 23cd8b25d25..46c3be62047 100644
--- compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -973,7 +973,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       /** True if `tp1` and `tp2` have compatible type constructors and their
        *  corresponding arguments are subtypes relative to their variance (see `isSubArgs`).
        */
-      def isMatchingApply(tp1: Type): Boolean = tp1 match {
+      def isMatchingApply(tp1: Type): Boolean = tp1.widen match {
         case tp1 @ AppliedType(tycon1, args1) =>
           // We intentionally do not automatically dealias `tycon1` or `tycon2` here.
           // `TypeApplications#appliedTo` already takes care of dealiasing type

now running the tests to see if this break anything, but this looks promising :)

[smarter]

Unfortunately this change breaks one patmat test, when I run scalac -Ycheck-all-patmat tests/patmat/i6197d.scala on master I get:

-- [E029] Pattern Match Exhaustivity Warning: tests/patmat/i6197d.scala:5:28 ----------------------------------------------------------------------------------------------------------------------------------------------------------------
5 |def bar(x: Array[String]) = x match {
  |                            ^
  |                            match may not be exhaustive.
  |
  |                            It would fail on pattern case: _: Array[String]

But this warning disappears after applying the diff in my previous comment, digging a bit it seems that in Typer we generate a symbol for _ in Array[_ <: Int] which initially has bounds _ >: Nothing <: Int as expected, but then gets its info changed in:
https://github.com/lampepfl/dotty/blob/ecceb15084fb15e40dce13ca70c25f516cd07a65/compiler/src/dotty/tools/dotc/typer/Typer.scala#L1570-L1571
Where it turns out that ctx.gadt.fullBounds(sym) returns >: String <: String, I haven't investigated further to see how this is related to the widening change. @abgruszecki, could you help diagnose what's going on here?

[abgruszecki]

I think I know what causes the problem. It seems that we continue mishandling ConstraintHandling in GadtConstraint, and that before the change you propose could work, we'd need #11988 first.

Reg. our previous discussion - the bit of code you quote does seem to be (at least somewhat) necessary. It seems that some checks in the compiler don't look up GADT constraints (match types, for instance) and if we remove that bit of code, we can't compile stdlib anymore.