IndexOutOfBoundsException when attempting to reduce ill-kinded types

[sstucki]

The following snippet is a variant of that causing #2771:

trait A { type L[G[F[_],_],H[F[_],_]] }
trait B { type L[F[_],_] }
trait C { type M <: A }
trait D { type M >: B }

object Test {
  def test(x: C with D): Unit = {
    def foo(a: A, b: B)(z: a.L[b.L,b.L]) = z
    def bar(y: x.M, b: B) = foo(y, b)
    def baz(b: B) = bar(b, b)
    baz(new B { type L[F[_],X] = F[X] })(1)
  }
}

The underlying issue is likely the same, though the error message is different:

exception occurred while compiling Test.scala
Exception in thread "main" java.lang.IndexOutOfBoundsException: 1
    at scala.collection.LinearSeqOptimized$class.apply(LinearSeqOptimized.scala:65)
    at scala.collection.immutable.List.apply(List.scala:84)
    at dotty.tools.dotc.core.Substituters$class.substParams(Substituters.scala:220)
    ...

The error disappears when the last line (the call to baz) is commented out. See #2771 for a more in-depth discussion.

[sstucki]

Here is another example, producing a stack overflow again (like for #2771). It uses the untyped SKI fixpoint combinator and absurd bounds to create a non-terminating term.

trait A { type S[X[_] <: [_] => Any, Y[_]] <: [_] => Any; type I[_] }
trait B { type S[X[_],Y[_]]; type I[_] <: [_] => Any }
trait C { type M <: B }
trait D { type M >: A }

object Test {
  def test(x: C with D): Unit = {
    def foo(a: A, b: B)(z: a.S[b.I,a.I][b.S[a.I,a.I]]) = z
    def bar(a: A, y: x.M) = foo(a,y)
    def baz(a: A) = bar(a, a)
    baz(new A { type S[X[_] <: [_] => Any, Y[_]] = [Z] => X[Z][Y[Z]]; type I[X] = X })(1)
  }
}

Again, the error disappears when the call to baz is commented out.

Note the use of curried type operators. One can also write an uncurried version, resulting in yet another error:

trait A { type S[X[_,_], Y[_],_]; type I[_] }
trait B { type S[X[_],Y[_]]; type I[_,_] }
trait C { type M <: B }
trait D { type M >: A }

object Test {
  def test(x: C with D): Unit = {
    def foo(a: A, b: B)(z: a.S[b.I,a.I,b.S[a.I,a.I]]) = z
    def bar(a: A, y: x.M) = foo(a,y)
    def baz(a: A) = bar(a, a)
    baz(new A { type S[X[_,_], Y[_], Z] = X[Z,Y[Z]]; type I[X] = X })(1)
  }
}

produces the error

exception occurred while compiling SKIUncurried.scala
Exception in thread "main" java.lang.AssertionError: assertion failed
    at scala.Predef$.assert(Predef.scala:156)
    at dotty.tools.dotc.core.Types$TypeAccumulator.foldArgs$1(Types.scala:3979)

Interestingly, the error does not disappear in this case when call to baz is commented out.

Note that none of these examples uses recursion (neither on the term level nor on the type level). All the trouble is caused by bad bounds.

[odersky]

This looks pretty troubling to me. What is a principled way to rule out these problems? I mean, without throwing out higher-kinded types or intersections altogether? It would be great if someone went to the bottom of this and came up with a proposal what we should do. I personally am more and more disgusted by the hidden complexities caused by higher-kinded types. If things stay as they are I see no alternative to bringing back the higher-kinded language import and declaring higher-kinded types officially unsound.

[odersky]

You might ask: Why does scalac refuse the program? It's because it does not have true intersections. In

trait C { type M <: B }
trait D { type M >: A }
C with D

the type of M is the type of M in D. This causes lots of other problems (loss of commutativity in intersections being one), but it does save us from the unsoundness problems of higher-kinded types exposed in this issue.

[sstucki]

A few comments up front:

• This is not fundamentally a problem of higher-kinded types but of bad bounds. If we could systematically prevent bad bounds then the problem would disappear, but we probably can't.
• It's not fundamentally an issue of intersection types either, they are just convenient means to introduce bad bounds. I'm sure there are others.
• Cases like the encoding of a non-terminating SKI expression don't "just happen", you have to actively engineer them. On the other hand, cases like that producing the IndexOutOfBoundException or those reported in Reducing open types is potentially unsafe #2771 might happen, so I think it's good to "fix" those by providing proper error messages.
• Because it's a problem of bad bounds, it's not strictly speaking a type soundness issue. It can never cause a run-time error, only compile-time errors. In all the test cases, the error occurs under an absurd assumption x: C with D which can never be instantiated. However, as @Blaisorblade mentioned in a comment on Reducing open types is potentially unsafe #2771, similar issues could occur at the term level when some optimization simplifies and open term. Soundness-wise, this might even be a bigger issue because it could change the semantics of a program. Of course that has nothing to do with HK types whatsoever.

Given that this is fundamentally a compile-time issue, it seems to me that the best one can do is provide better error messages. What else is there?

My pragmatic solution would be: don't try to exclude this sort of thing statically but treat it as a sort of "run-time error" for type-level computation: report a compile error when the arities of type operators and their argument lists don't match; impose a limit on the time/number of calls spent reducing types to avoid non-termination. This is not a perfect solution, but I think it will catch most real-world issues.

There might be a "cleaner" but much more complex solution which involves tracking uses of subsumption in type expressions, and not allowing type reductions unless those can be statically guaranteed to be consistent. E.g. in the SKI example, the return-type of bar is (z: a.S[x.I,a.I][x.S[a.I,a.I]])... but if we track the fact that x has type y.M rather than B by inserting explicit casts, we get (z: a.S[(x: B).I,a.I][(x: B).S[a.I,a.I]])... instead. Now one could forbid selections of the form (z: S).A to be evaluated (when normalizing types) unless the cast can be statically proven sound using some heuristics, and signal an error otherwise. Probably, some of the ideas by Cretin, Scherer and Rémy about reduction under possibly inconsistent coercion constraints could be adopted here. It's an interesting theory problem, but I'm not convinced it would actually improve the user experience.

[odersky]

I agree the problem is a combination of higher-kinded types and bad bounds. From the work on DOT it seems unlikely that bad bounds can be detected a priori. And it's not clear it can lead to type soundness problems or "just" to misbehaving compilers.

This means we are in the unenviable situation that we cannot guarantee the preconditions the bulk of our type checking operations anymore - they might all be wrong due to incompatible kinds that we cannot detect. Sure we could make our type computations more robust by dealing with all sort of illegal situations, imposing arbitrary limits on stack depth and so on. But that has an unfortunate tendency of hiding true error conditions where we want to crash because something is wrong. For a compiler writer this is a nightmare scenario.

[sstucki]

This means we are in the unenviable situation that we cannot guarantee the preconditions the bulk of our type checking operations anymore (...) For a compiler writer this is a nightmare scenario.

OK that is a very good point.

But then I'm wondering, isn't that already true to some extent for ill-typed terms? The following example type checks, but if we ever tried to evaluate the body of test it would get stuck. And the preconditions of some transformations are broken, e.g. inlining the definitions badCast, f and fBad would result in code that doesn't type check any longer. How is this sort of thing dealt with?

trait A { type L >: Int => Int }
trait B { type L <: Int => Int => Int }

object Test {
  def test(x: A with B): Unit = {
    def badCast(f: Int => Int): x.L = f

    val f    : Int => Int        = (y: Int) => y
    val fBad : Int => Int => Int = badCast(f)

    fBad(1)(1)
  }
}

[smarter]

inlining the definitions badCast, f and fBad would result in code that doesn't type check any longer.

You can inline while preserving typecheckability, you just need to introduce casts:

f.asInstanceOf[Int => Int => Int](1)(1)

[smarter]

Maybe the equivalent of runtime type-casting is compile-time kind-casting :).

[sstucki]

You can inline while preserving typecheckability, you just need to introduce casts:

Sure, but then the casts prevent your from simplifying the expression. (Side note: I wonder how Scala-JS deals with this sort of thing. AFAIK it performs quite aggressive inlining and simplifications. Maybe @sjrd can comment on this).

Maybe the equivalent of runtime type-casting is compile-time kind-casting :).

Or compile-time type-casting on paths, see my earlier comment. And as I mention there, that doesn't quite solve the problem. Just as type-casts stop you from simplifying term-level expressions, they stop you from evaluating type expressions unless you can prove that it's safe to remove them. It's that latter part that is difficult.