Potential kind-checking bugs for curried type functions

[Blaisorblade]

Some pre-kind-checking code never made sense to me — and talking with @smarter and @sstucki, @smarter just pointed out that it's restricted to non-curried type functions. Since at least @milessabin is interested in making this right, I'm making a note.

Miles, please feel free to close if not actionable — tho one could document these caveats in comments. EDIT: If you want, I can do it.

1. AppliedType.superType assumes that applications of type functions have "kind" *, hence they're subtypes of Any:

    override def superType(implicit ctx: Context): Type = {
      if (ctx.period != validSuper) {
        cachedSuper = tycon match {
          case tycon: HKTypeLambda => defn.AnyType

2. TypeApplications.hkResult assumes that classes only have one type parameter list

    case self: AppliedType =>
      if (self.tycon.typeSymbol.isClass) NoType else self.superType.hkResult

3. A non-quite-bug but a trap: if C is a parameterized class, then AppliedType.superType on C[A] returns C; however, for some callers this is the correct thing. Inside <:<, instead, this is not correct, except that <:< seems to avoid relying on superType in this case.

          case tycon: TypeRef if tycon.symbol.isClass => tycon

[milessabin]

Thanks! I'll take a look and at least document these observations.

[odersky]

Thanks for digging into it Paolo. That's very useful.

   override def superType(implicit ctx: Context): Type = {
      if (ctx.period != validSuper) {
        cachedSuper = tycon match {
          case tycon: HKTypeLambda => defn.AnyType

I believe If we hit that case, we have already strayed off the happy path. The type constructor of an AppliedType is a HKTypeLambda only if the application is irreducible (which will be flagged as an error). An example is ([X] => (X, X)))[_]. Irreducible applications are equivalent to existential types. They are flagged as errors at some later point, but they can still arise in some situations.

[smarter]

The type constructor of an AppliedType is a HKTypeLambda only if the application is irreducible (which will be flagged as an error).

I'm not sure that's true since we don't reduce type lambda applications when doing so would change the number of type parameters of the type, since that can affect type inference: https://github.com/lampepfl/dotty/blob/c99e7718b205f59a427c033734f0c2726f633645/compiler/src/dotty/tools/dotc/core/TypeApplications.scala#L368-L371

[odersky]

I'm not sure that's true since we don't reduce type lambda applications when doing so would change the number of type parameters of the type, since that can affect type inference:

But in these cases the constructor is a TypeParam or TypeRef with an info that is a HKTypeLambda, not a HKTypeLambda itself, right?

[Blaisorblade]

I believe if we hit that case, we have already strayed off the happy path.

Oh! Indeed, testCompilation pos keeps working if I add assert(false) there, while a couple of neg tests crash indeed — (details below). Thanks for clarifying! Still worth documenting maybe.

But in these cases the constructor is a TypeParam or TypeRef with an info that is a HKTypeLambda, not a HKTypeLambda itself, right?

Data below

sbt:dotty> testCompilation pos
[... compile...]
[info] Test dotty.tools.dotc.CompilationTests.negAll started
[=======================================] completed (3/3, 0 failed, 3s)
[info] Test dotty.tools.dotc.CompilationTests.runAll started
[=======================================] completed (1/1, 0 failed, 1s)
[info] Test dotty.tools.dotc.CompilationTests.pickling started
[=======================================] completed (1739/1739, 0 failed, 68s)
[info] Test dotty.tools.dotc.CompilationTests.pos started
[=======================================] completed (1872/1872, 0 failed, 113s)
[info] Test dotty.tools.dotc.CompilationTests.tastyBootstrap started
No files matched "pos" in test
No files matched "pos" in test
No files matched "pos" in test
No files matched "pos" in test
[info] Test dotty.tools.dotc.CompilationTests.posTwice started
[=======================================] completed (109/109, 0 failed, 17s)
[info] Test dotty.tools.dotc.CompilationTests.fuzzyAll started
No files matched "pos" in test
[info] Test dotty.tools.dotc.CompilationTests.genericJavaSignatures started
No files matched "pos" in test

diff --git compiler/src/dotty/tools/dotc/core/Types.scala compiler/src/dotty/tools/dotc/core/Types.scala
index 7521fb646..ef1302185 100644
--- compiler/src/dotty/tools/dotc/core/Types.scala
+++ compiler/src/dotty/tools/dotc/core/Types.scala
@@ -3512,7 +3512,10 @@ object Types {
     override def superType(implicit ctx: Context): Type = {
       if (ctx.period != validSuper) {
         cachedSuper = tycon match {
-          case tycon: HKTypeLambda => defn.AnyType
+          case tycon: HKTypeLambda =>
+            println(s"tycon is ${tycon.show} this is ${this.show}")
+            assert(false)
+            defn.AnyType
           case tycon: TypeRef if tycon.symbol.isClass => tycon
           case tycon: TypeProxy => tycon.superType.applyIfParameterized(args)
           case _ => defn.AnyType

Failures I've seen (i4368a.scala is local-only):

    tests/neg/i4368a.scala failed
    tests/neg/i6063.scala failed
    tests/fuzzy/AE-854cfacb52282336bde0799f1ddbb5bbef974b59.scala failed
    tests/fuzzy/AE-ac9906c65ae7b715ce547b314cfb5b55a5bd899e.scala failed
[...]
tycon is i0.I1 this is i0.I1[<error unspecified error>]8/689, 0 failed, 14s)
tycon is test.I0.i2 this is test.I0.i2[<error unspecified error>]
tycon is I0.i2 this is I0.i2[<error unspecified error>]/173, 0 failed, 4s)
tycon is i0.i1 this is i0.i1[<error unspecified error>]5/173, 0 failed, 8s)