New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

IndexOutOfBoundsException when attempting to reduce ill-kinded types #2887

Open
sstucki opened this Issue Jul 18, 2017 · 17 comments

Comments

Projects
None yet
5 participants
@sstucki
Contributor

sstucki commented Jul 18, 2017

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

This comment has been minimized.

Show comment
Hide comment
@sstucki

sstucki Jul 18, 2017

Contributor

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.

Contributor

sstucki commented Jul 18, 2017

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 comment has been minimized.

Show comment
Hide comment
@odersky

odersky Jul 19, 2017

Contributor

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.

Contributor

odersky commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@odersky

odersky Jul 19, 2017

Contributor

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.

Contributor

odersky commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@sstucki

sstucki Jul 19, 2017

Contributor

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.

Contributor

sstucki commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@odersky

odersky Jul 19, 2017

Contributor

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.

Contributor

odersky commented Jul 19, 2017

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 comment has been minimized.

Show comment
Hide comment
@sstucki

sstucki Jul 19, 2017

Contributor

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)
  }
}
Contributor

sstucki commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@smarter

smarter Jul 19, 2017

Member

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

smarter commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@smarter

smarter Jul 19, 2017

Member

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

Member

smarter commented Jul 19, 2017

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

@sstucki

This comment has been minimized.

Show comment
Hide comment
@sstucki

sstucki Jul 19, 2017

Contributor

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.

Contributor

sstucki commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@Blaisorblade

Blaisorblade Jul 19, 2017

Contributor

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.

Contributor

Blaisorblade commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@Blaisorblade

Blaisorblade Jul 19, 2017

Contributor

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

Contributor

Blaisorblade commented Jul 19, 2017

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

This comment has been minimized.

Show comment
Hide comment
@odersky

odersky Jul 20, 2017

Contributor

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.

Contributor

odersky commented Jul 20, 2017

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

This comment has been minimized.

Show comment
Hide comment
@sstucki

sstucki Jul 20, 2017

Contributor

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

sstucki commented Jul 20, 2017

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

This comment has been minimized.

Show comment
Hide comment
@sjrd

sjrd Jul 20, 2017

Member

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.

Member

sjrd commented Jul 20, 2017

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

This comment has been minimized.

Show comment
Hide comment
@sstucki

sstucki Jul 20, 2017

Contributor

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.

Contributor

sstucki commented Jul 20, 2017

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

This comment has been minimized.

Show comment
Hide comment
@sjrd

sjrd Jul 20, 2017

Member

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.

Member

sjrd commented Jul 20, 2017

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

This comment has been minimized.

Show comment
Hide comment
@Blaisorblade

Blaisorblade Jul 20, 2017

Contributor

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?

Contributor

Blaisorblade commented Jul 20, 2017

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment