Dotty: Unsoundness due to type projections (no null or lazy vals necessary) (not in strict mode)

[alexknvl]

EDIT: simpler example in the comments below

object App {
  abstract class Boo[E <: Nothing { type R }] {
    val r: E
    type R = r.type#R
  }

  trait Leibniz[+U, A <: U, B <: U] {
    def subst[F[_ <: U]](fa : F[A]): F[B]
  }
  def refl[A]: Leibniz[A, A, A] = new Leibniz[A, A, A] {
    def subst[F[_ <: A]](fa : F[A]): F[A] = fa
  }

  val p = refl[Nothing] : Leibniz[Nothing {type R}, Nothing { type R = Int }, Nothing { type R = String }]

  def main(args : Array[String]): Unit = {
    // BOOM
    val s : String = p.subst[[x <: Nothing { type R }] => Boo[x]#R](10)
  }

}

Exception in thread "main" java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
    at App$.main(App.scala:18)
    at App.main(App.scala)

[smarter]

I assume this is just because Nothing is both a supertype and a subtype of a refined Nothing? If so the most sensible thing to do would be to disallow refining Nothing. Unless you can reproduce the issue without using them?

[alexknvl]

Refinements of Nothing are bad, but I can do it entirely without refining Nothing :smile_cat:

object App {
  def coerce[U, V](u: U): V = {
    trait X { type R >: U }
    trait Y { type R = V }

    abstract class Boo[E <: Any { type R }] {
      val r: E
      type R = r.type#R
    }

    class T[X <: Any { type R }](val value: Boo[X]#R)

    val a = new T[Y & X](u)
    a.value
  }

  def main(args : Array[String]): Unit = {
    // BOOM
    val s : String = coerce[Int, String](10)
  }
}

[smarter]

Nice. I don't see an easy way out of this, looks like it'll require even more drastic limitations on type projections.

[Blaisorblade]

@alexknvl Cool example!

Nitpick: r.type#R is r.R. But we can't simplify much further. Dotty rejects this:

object App {
  def coerce[U, V](u: U): V = {
    trait X { type R >: U }
    trait Y { type R = V }

    abstract class Boo[E <: Any { type R }] {
      val r: E
      type R = E#R
    }

    class T[X <: Any { type R }](val value: Boo[X]#R)

    val a = new T[Y & X](u)
    a.value
  }

  def main(args : Array[String]): Unit = {
    // BOOM
    val s : String = coerce[Int, String](10)
  }
}

but accepts this:

object App2 {
  def coerce[U, V](u: U): V = {
    trait X { type R >: U }
    trait Y { type R = V }

    abstract class Boo[E <: Any { type R }] {
      val r: E
      type R = r.R
    }

    class T[X <: Any { type R }](val value: Boo[X]#R)

    val a = new T[Y & X](u)
    a.value
  }

  def main(args : Array[String]): Unit = {
    // BOOM
    val s : String = coerce[Int, String](10)
  }
}

The basic problem is that, on the one hand, we assume that r's type is realizable, because it will be in any instance of Boo, but on the other hand, _projections_ out of Boo can give to r unrealizable types.

@alexknvl Here, it might seem easy to "inline" Boo and notice the problem, but I suspect such strategies can't work.
Maybe one way to show that would be to insert some indirection that could be hard to analyze, to show no such strategy can work. But I'm too tired to try... we can do that on demand, given some fix idea.

[alexknvl]

I simplified it a bit more:

object App {
  def coerce[U, V](u: U): V = {
    trait X { type R >: U }
    trait Y { type R = V }

    abstract class Boo {
      val r: Y & X
      type R = r.R
    }
    // OR
    // final class Boo(val r: Y & X) {
    //  type R = r.R
    // }

    (u : Boo#R)
  }

  def main(args : Array[String]): Unit = {
    // BOOM
    val s : String = coerce[Int, String](10)
  }
}

[alexknvl]

Adapted https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/ to this technique:

object App {
  trait Term {
    type ap[x <: Term] <: Term
    type eval <: Term
  }

  class !#[T <: Term](val t: T) {
    type ap[x <: Term] = t.ap[x]
    type eval = t.eval
  }

  // The S combinator
  trait S extends Term {
    type ap[x <: Term] = S1[x]
    type eval = S
  }
  trait S1[x <: Term] extends Term {
    type ap[y <: Term] = S2[x, y]
    type eval = S1[x]
  }
  trait S2[x <: Term, y <: Term] extends Term {
    type ap[z <: Term] = S3[x, y, z]
    type eval = S2[x, y]
  }
  trait S3[x <: Term, y <: Term, z <: Term] extends Term {
    type ap[v <: Term] = !#[eval]#ap[v]
    type eval = !#[!#[!#[x]#ap[z]]#ap[!#[y]#ap[z]]]#eval
  }

  // The K combinator
  trait K extends Term {
    type ap[x <: Term] = K1[x]
    type eval = K
  }
  trait K1[x <: Term] extends Term {
    type ap[y <: Term] = K2[x, y]
    type eval = K1[x]
  }
  trait K2[x <: Term, y <: Term] extends Term {
    type ap[z <: Term] = !#[eval]#ap[z]
    type eval = !#[x]#eval
  }

  // The I combinator
  trait I extends Term {
    type ap[x <: Term] = I1[x]
    type eval = I
  }
  trait I1[x <: Term] extends Term {
    type ap[y <: Term] = !#[eval]#ap[y]
    type eval = !#[x]#eval
  }

  trait c extends Term {
    type ap[x <: Term] = c
    type eval = c
  }
  trait d extends Term {
    type ap[x <: Term] = d
    type eval = d
  }
  trait e extends Term {
    type ap[x <: Term] = e
    type eval = e
  }

  object Equals {
    def apply[A >: B <:B , B]: Unit = ()
  }
  Equals[Int, Int]   // compiles fine


  // Ic -> c
  Equals[I#ap[c]#eval, c]

  // Kcd -> c
  Equals[K#ap[c]#ap[d]#eval, c]

  // KKcde -> d
  Equals[K#ap[K]#ap[c]#ap[d]#ap[e]#eval, d]

  // SIIIc -> Ic
  Equals[S#ap[I]#ap[I]#ap[I]#ap[c]#eval, c]

  // SKKc -> Ic
  Equals[S#ap[K]#ap[K]#ap[c]#eval, c]

  // SIIKc -> KKc
  Equals[S#ap[I]#ap[I]#ap[K]#ap[c]#eval, K#ap[K]#ap[c]#eval]

  // SIKKc -> K(KK)c
  Equals[S#ap[I]#ap[K]#ap[K]#ap[c]#eval, K#ap[K#ap[K]]#ap[c]#eval]

  // SIKIc -> KIc
  Equals[S#ap[I]#ap[K]#ap[I]#ap[c]#eval, K#ap[I]#ap[c]#eval]

  // SKIc -> Ic
  Equals[S#ap[K]#ap[I]#ap[c]#eval, c]

  // R = S(K(SI))K  (reverse)
  type R = S#ap[K#ap[S#ap[I]]]#ap[K]
  Equals[R#ap[c]#ap[d]#eval, d#ap[c]#eval]

  // b(a) = S(Ka)(SII)
  type b[a <: Term] = S#ap[K#ap[a]]#ap[S#ap[I]#ap[I]]

  trait A0 extends Term {
    type ap[x <: Term] = c
    type eval = A0
  }
  trait A1 extends Term {
    type ap[x <: Term] = !#[!#[x]#ap[A0]]#eval
    type eval = A1
  }
  trait A2 extends Term {
    type ap[x <: Term] = !#[!#[x]#ap[A1]]#eval
    type eval = A2
  }

  trait An extends Term {
    type ap[x <: Term] = !#[!#[x]#ap[An]]#eval
    type eval = An
  }

  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
  // Infinite iteration: Smashes dotc's stack
  type NNn = b[R]#ap[b[R]]#ap[An]
  Equals[NNn#eval, c]
}

[Blaisorblade]

Started talking about this with @odersky today. One insight for me: while fields of realizable prefixes are realizable, this itself is unrealizable in Boo.

[odersky]

It turns out that the example "I simplified a bit more" is rejected using -strict mode:

~/workspace/dotty/tests/neg> ldotc i4246.scala -d /classes -strict
-- Error: i4246.scala:17:9 -----------------------------------------------------
17 |    (u : Boo#R)
   |         ^
   |Boo is not a legal path
   |since it has a member value r which is not a legal path
   |since r: Y & X has a member R with possibly conflicting bounds V | U <: ... <: V

There is a comment in CheckRealizable.scala:

    if (ctx.settings.strict.value)
      // check fields only under strict mode for now.
      // Reason: An embedded field could well be nullable, which means it
      // should not be part of a path and need not be checked; but we cannot recognize
      // this situation until we have a typesystem that tracks nullability.
      ((Realizable: Realizability) /: tp.fields)(checkField)

It would be interesting to see whether the other examples are also rejected under -strict mode.

[Blaisorblade]

Modulo copy-paste errors, all examples here are indeed rejected under strict mode, except the SKI encoding which gives a StackOverflowException.
https://gist.github.com/Blaisorblade/f94e5f00015d266974aba78d459cbf50

I've started studying failures when forcing strict realizability checking — see #4284.