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 #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 #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.

[Blaisorblade]

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.

👍 💯 to this.

From the work on DOT it seems unlikely that bad bounds can be detected a priori. [...]

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.

Wait—why can one not detect that x.M has incompatible kinds (with member L taking one or two arguments) after declaring x: C with D? All the given crashes arise from actually inconsistent bounds. "We can't detect bad bounds" a priori means something different. For instance, if you declare instead test(x: C), later you can call test with argument y: C with D; but all uses of x.M in the source will keep having a single kind.* So I contend (without proof) this can't crash the compiler. I'd love to see a counterexample. (I mentioned similar ideas earlier in #2771 and haven't seen counterexamples yet).

However, my contention only allows (at best) patching known examples, so I agree this is unsatisfying.

*As long as you don't actually substitute x by y. But since DOT formalisms don't reduce open terms and y can't be instantiated with a value, nothing suggests that substitution should work.

[Blaisorblade]

Regarding coercions in ASTs: I don't think stuck terms/types would be a problem—as long as long as you have the theory needed to simplify safely enough expressions. Since producing this theory is nontrivial research, I agree with @sstucki that coercions can't be used yet.

Also, using coercions here seems out of "balance". In contrast, GHC uses coercions to handle GADTs, even though they sometimes interfere with optimizations—while Scalac (and I assume Dotty) don't. Coercions might be needed as input for some type-preserving transformations; but even otherwise, having to produce evidence that GADT coercions are safe makes GHC more robust—in other words, that's technology to increase robustness. Right now, Scalac tries to handle trickier GADTs with weaker PL technology—so it's not surprising this is hard to get right.

IMHO, implementing coercions to handle GADTs would matter more to user experience than using them for higher-kinded types. But even there, research (and volunteers for it) is needed :-)

[odersky]

So I contend (without proof) this can't crash the compiler. I'd love to see a counterexample. (I mentioned similar ideas earlier in #2771 and haven't seen counterexamples yet).

I believe the counter example would involve a type A & B where A and B are abstract without any higher-kinded type members. Then in subclasses refine A and B separately with the abstract type members L at different kinds. I think that would be sufficient to get an ill-kinded type somewhere without it being written down explicitly.

[sstucki]

I believe the counter example would involve a type A & B where A and B are abstract without any higher-kinded type members.

Exactly. Here's an example:

trait A { type L; type U; type T }
trait B extends A { type T >: L }
trait C extends A { type T <: U }

trait Cast[X <: B, Y <: C] {
  def cast(x: X & Y)(z: x.L):x.U = (z: x.T)
}

trait Lower     extends B { type L = Int }
trait GoodUpper extends C { type U = Int }
trait BadUpper  extends C { type U = Int => Int }

object GoodCast extends Cast[Lower, GoodUpper]
object BadCast  extends Cast[Lower, BadUpper]

The GoodCast and BadCast objects illustrate that there's nothing wrong with the trait Cast a priori, even though the cast method uses inconsistent bounds. Checking for inconsistencies at the point of abstraction (here cast) will necessarily exclude some useful cases.

scalac rejects the program with the error

error: stable identifier required, but x found.
Note that value x is not stable because its type, X with Y, is volatile.

[sjrd]

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).

Scala.js, like Scala/JVM, introduces the necessary casts during erasure. After that, inlining never introduces more casts. Scala.js simplifies unnecessary casts of the form a.asInstanceOf[B] once it knows (typically after inlining) that a.type <:< B.

I'm not sure whether this is actually relevant to the present discussion, though.

[sstucki]

Scala.js simplifies unnecessary casts of the form a.asInstanceOf[B] once it knows (typically after inlining) that a.type <:< B.

That makes sense, provided that a.type <:< B is always "safe", i.e. that it doesn't rely on possibly absurd assumptions. That may well be the case post erasure.

If it's not the case, then there are some other subtleties here, like (t.asInstanceOf[S]).asInstanceOf[T] might simplify to t or not depending on whether the outer or inner cast are eliminated first.

I'm not sure whether this is actually relevant to the present discussion, though.

I think it is.

[sjrd]

Yes, after erasure (or, at the very least, once at the IR/bytecode level), subtyping relationships that hold at compile/link time are guarantee to still be valid at run-time. It is not the case before erasure.

[Blaisorblade]

I think that would be sufficient to get an ill-kinded type somewhere without it being written down explicitly.

I'm not trying to prevent ill-kinded types. They won't crash Dotty. Code using them will. But I might have realized why I misunderstand what you meant by "detecting a priori".

Does Dotty expect that reducing open types is kind-sound? Sure, that doesn't work, so I agree one should just detect when reducing types produces actual dynamic kind errors. But yeah, I see why that's probably your "nightmare scenario". To distinguish Dotty bugs from exploits of actually inconsistent boundaries, I think one can tune where errors are detected.

Normally, you just need to detect violations of a sort of "canonical forms lemma" for type reductions—for instance, having a binary type constructor when a unary one is expected, like more or less here. This is where HK-types might be relevant: without HK-types all kinds are subkinds of *, and Dotty doesn't need additional kind-safety.

When debugging the compiler or type errors, you probably want to detect (and reject) actual inconsistency—not like cast in @sstucki's example.

But I'll confess I'm not sure yet where the original example should be rejected: at the earliest, x.M#L (or rather y.L where y: x.M) is actually ill-kinded, so x.M and x might be rejected as having (indirectly) actually ill-kinded members. You can detect this more or less lazily, if it is necessary for performance to be lazy. You can analyze types upon dynamic kind errors. But that can generate some puzzlers. For instance, if you add the call to baz(new B { type L[F[_],X] = F[X] })(1), and Dotty then investigates the resulting runtime kind error, this might reveal that in fact C with D was inconsistent. EDIT: would that be acceptable?

[sstucki]

I think this should be re-opened because the problem persists (checked with dotty 3.0.0-M2).

There's an error in one of the regression tests committed by @nicolasstucki that makes it fail, but it's just a syntax error (the syntax of type lambdas has changed form [X] => T to [X] =>> T). If the syntax error is fixed, the test causes the compiler to crash again. See e.g. https://github.com/lampepfl/dotty/blob/0f0d25cd5a1c8fee8af16bbce047b7d8938ba69f/tests/neg/i2887b.scala#L1-L2

Here's the fixed version of tests/neg/i2887b.scala

trait A { type S[X[_] <: [_] =>> Any, Y[_]] <: [_] =>> Any; type I[_] } // error // error
trait B { type S[X[_],Y[_]]; type I[_] <: [_] =>> Any } // error
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 // error
    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) // error // error
  }
}

[no-identd]

…well, I wish I remembered/could recall why I started tracking this issue/what made me Stert tracking it, I know it was (and probably still is? Is say damn my memory, but already seems pretty damned.) important, but I apparently didn't and/or can't, but I'm glad to see it fixed. Thanks @odersky !