HK type aliasing bug

[sir-wabbit]

object App {
  def main(args: Array[String]): Unit = {
    trait ModuleSig {
      type F[_]
      type Type = F

      def subst[F[_[_]]](fa: F[List]): F[Type]
    }
    val Module: ModuleSig = new ModuleSig {
      type F[A] = List[A]

      def subst[F[_[_]]](fa: F[List]): F[Type] = fa
    }
  }
}

doesn't compile, but if you change

type F[A] = List[A]

to

type F = List

it does...

[odersky]

I'd argue the program should be rejected. F[Type] is a self-application is you follow aliases and as such kind-incorrect.

[liufengyun]

@odersky I think there's some missing dealias somewhere, there's no self-application as the two F in F[F] are different: one from the method type parameter, one from a type member.

[smarter]

It works if you do:

object App {
  def main(args: Array[String]): Unit = {
    trait ModuleSig {
      type F[_]
      type Type = F

      def subst[F[_[_]]](fa: F[[X] => List[X]]): F[Type]
    }
    val Module: ModuleSig = new ModuleSig {
      type F[A] = List[A]

      def subst[F[_[_]]](fa: F[[X] => List[X]]): F[Type] = fa
    }
  }
}

This is the same kind of bug as #2989, (I have a potential fix for #2989 at https://github.com/dotty-staging/dotty/commits/fix-eta-expansion-new but it doesn't seem to handle this case. I really wish we could find a more principled way to write hk subtyping checks).

[odersky]

doesn't compile, but if you change

type F[A] = List[A]

to

type F = List

it does...

Turns out, if you change it to

type F[+A] = List[A]

is compiles, too. So the question is, is [A] => List[A] a subtype of [+A] => List[A]? By our normal reasoning about variances, it should not be. The reason it works with type F = List is that this definition expands to

type F[+A] = List[A]

not

type F[A] = List[A]