substitution broken for dependent types

[scabug]

In the following example (I'm afraid I haven't been able to significantly reduce it further), the equivalence of si.Out and si.instance.Out has been lost at the call sites of direct and indirect.

Notice that in direct the type si.Out is known in the second parameter block at the call site, and so the expression typechecks. However in indirect the type si.instance.Out is unknown or, at least, is sufficiently opaque to prevent the second expression from typechecking.

si.Out is defined in terms of the implicitly summoned i, so if si.Out =:= i.Out is available at the call sites of direct and indirect then intuitively it seems that si.instance.Out =:= i.Out (where si.instance: i.type) should be available too.

package si

import scala.language.{ higherKinds, implicitConversions }

trait Foo[T] { type Out }

object Foo {
  implicit def mkFoo1: Foo[Boolean] { type Out = Int } =
    new Foo[Boolean] { type Out = Int }
}

trait SI[TC[_]] {
  type T
  val instance: TC[T]
  type Out
}

object SI {
  implicit def conv[TC[_] <: { type Out }, T0](t: T0)
    (implicit i: TC[T0]): SI[TC] { type T = T0 ; type Out = i.Out } =
      new SI[TC] {
        type T = T0
        val instance: i.type = i
        type Out = i.Out
      }
}

object Test {
  def direct(si: SI[Foo])(v: si.Out) = v

  val v1: Int = direct(true)(23)    // OK

  def indirect(si: SI[Foo])(v: si.instance.Out) = v

  val v2: Int = indirect(true)(23)  // Fails
  // test.scala:35: error: type mismatch;
  //  found   : Int(23)
  //  required: si.instance.Out
  //   val i: Int = indirect(true)(23)
  //                               ^
}

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-7753?orig=1
Reporter: @milessabin
Affected Versions: 2.10.2, 2.11.0-M4
Other Milestones: 2.11.0-RC1
See #8177, #3873

[scabug]

@paulp said:
I think you are looking at #6161. There are a billion examples of it.

[scabug]

@paulp said:
Here it is with no use of implicits. It's pretty well killing my project.

trait CC[A]
trait HasElem[Repr] { type A }
object ccInt extends HasElem[CC[Int]] { type A = Int }

object Test {
  final class View[Repr, AIn](repr: Repr, val tc: HasElem[Repr] { type A = AIn }) {
    // For a time it's completely convinced AIn and tc.A are the same type.
    def equivalence1[B](implicit ev: B =:= AIn) = true
    def equivalence2[B](implicit ev: B =:= tc.A) = true
    def evidences = List(equivalence1[tc.A], equivalence1[AIn], equivalence2[tc.A], equivalence2[AIn]) // 4 out of 4

    // Foreshadow.
    def f1(p: AIn): AIn = p
    def f2(p: tc.A): tc.A = p
  }

  def xs: CC[Int] = ???
  val view = new View[CC[Int], Int](xs, ccInt)

  // No longer equivalent, transitivity lost.
  def g0 = List(view.equivalence1[Int], view.equivalence2[Int])
  // b.scala:33: error: Cannot prove that Int =:= Test.view.tc.A.
  //   def g0 = List(view.equivalence1[Int], view.equivalence2[Int])
  //                                                          ^

  def g1 = view f1 5  // compiles
  def g2 = view f2 5  // fails
  // b.scala:31: error: type mismatch;
  //  found   : Int(5)
  //  required: Test.view.tc.A
  //     (which expands to)  AIn
  //   def g2 = view f2 5  // fails
  //                    ^
}

[scabug]

@paulp said:
See also #8177.

[scabug]

@retronym said:
I believe this provides a better look at Miles' reported problem:

import scala.language.{ higherKinds, implicitConversions }
 
trait Foo { type Out }
 
trait SI {
  val instance: Foo
  type Out
}

object Test {
  def test {
    def indirect(si: SI)(v: si.instance.Out) = v
   
    val foo: Foo { type Out = Int } = ???
    def conv(i: Foo): SI { type Out = i.Out; val instance: i.type } = ???
    
    val converted = conv(foo)

    val v1: Int = indirect(converted)(23)  // Okay (after refining the return type `instance` in the return type of `conv`)
    /*
    indirect(converted){(v: converted.instance.Out)converted.instance.Out}(
      23{Int(23)}
    ){converted.instance.Out};
    */

    val v2: Int = indirect(conv(foo))(23)  // Fails.
    /*
    indirect(
        conv(foo){si.SI{type Out = foo.Out; val instance: si.Test.<refinement>.type}}
    ){(v: si.instance.Out)si.instance.Out}(
      23{<error>}
    ){<error>};
    */

  }
}

First of all, I needed to refine instance in the return type of conv. Without that, I don't believe that one could expect this example to work.

However, after doing that, we can still see a difference between the case when the first argument to indirect is a stable value vs when it is a method call to conv. I've annotated the computed types in those expressions above.

actuals = SI{type Out = foo.Out; val instance: Test.<refinement>.type}
params =  value si
actuals.head.isStable = false

The unstable type of the argument is intentionally not substituted for si. This behaviour is a fix for a soundness hole, #3873.

My conclusion is that this isn't a bug. I'm going to mark it as such, but feel free to reopen if you think I've got it wrong.

I'll move Paul's test case over to #8177. It is a bug in as-seen-from.

[scabug]

@retronym said:
Adriaan: perhaps you could check my reasoning here.

[scabug]

@adriaanm said:
Thanks for the clear exposition, Jason. I agree with your analysis.

[scabug]

@clhodapp said (edited on Feb 6, 2014 10:48:48 AM UTC):
Jason, I disagree with your analysis here. The reason for the soundness hole in #3873 is not that new A as argument for parameter a is unstable, but rather that it's not the same prefix as val a. Let's try replacing new A in the #3873 code fragment with a stable reference (and fixing it a little bit so we don't have bare methods and vals):

class A { 
  class B
  def b: B = new B 
}

class B {
  def f(a: A)(b: a.B): a.B = b

  val a = new A
  f(a)(a.b)
  f({ val fresh = new A; fresh: fresh.type })(a.b) // doesn't compile
}

You would find that the code still wouldn't compile, since a-the-val.type#B does not conform to a-the-argument.type#B (which is actually fresh.type#b). This is not analogous to what's going on over here in #7753 (at least in your example). The first way to test this is to make a similar substitution:

import scala.language.{ higherKinds, implicitConversions }
 
trait Foo { type Out }
 
trait SI {
  val instance: Foo
  type Out
}

object Test {
  def test {
    def indirect(si: SI)(v: si.instance.Out) = v
   
    val foo: Foo { type Out = Int } = ???
    def conv(i: Foo): SI { type Out = i.Out; val instance: i.type } = ???
    
    val converted = conv(foo)

    val v1: Int = indirect(converted)(23)

    val v2: Int = indirect({ val fresh = conv(foo); fresh: fresh.type })(23)  // Works now

  }
}

You will find that the code compiles now. But then, of course it does: this basically comes to the same thing as what you already had above with val converted! Anyway, I do think that there is enough constraint here to make the call soundly, and that you should reconsider your position. Oh, and something else you should try: turn v2 into indirect(conv(foo))_ and you'll find that you get an Int => Int. hmmmm... Inconsistency in Scalac? That could never happen! Anyway, feel free to refute my analysis, as I could easily be missing some other factor that leads to unsoundness here.

While I'm at it, though, I'm extremely unconfident that the "stability lambdas" above ({val fresh = \_; fresh: fresh.type}) should work (I actually only kept them in so I could make this point). They seem to be letting part of the type (namely its stability) escape into an outer lexical scope, which definitely seems iffy. What do you think?

[scabug]

@retronym said:
Thanks for looking into this, Chris.

I tend to agree that the restrictions placed by #3873 didn't get to the essence of the unsoundness.

I also agree that the "stability lambda" (nicely coined!) is pretty dubious.

cat sandbox/test.scala
object Test {
  {val x = ""; x: x.type}: Singleton
}

ticket/8237 ~/code/scala qbin/scalac -Xprint:typer -Xprint-types sandbox/test.scala
sandbox/test.scala:2: warning: a pure expression does nothing in statement position; you may be omitting necessary parentheses
  {val x = ""; x: x.type}: Singleton
                         ^
[[syntax trees at end of                     typer]] // test.scala
package <empty>{<empty>.type} {
  object Test extends scala.AnyRef {
    def <init>(): Test.type = {
      Test.super{Test.type}.<init>{()Object}(){Object};
      (){Unit}
    }{Unit};
    ({
      val x: String = ""{String("")};
      (x{x.type}: x.type){x.type}
    }{x.type}: Singleton){Singleton}
  }
}

one warning found

As you point out, this has an ill-scoped reference to x in the type of the block. Maybe it should be x.type forSome { val x: String }.

Here's an analagous situation where block typing widens to a structural type to avoid leaking a locally scoped type:

scala> {class A { def foo = 0 }; new A }
res1: AnyRef{def foo: Int} = A$1@23905e3

With regards to eta-expansion, that's no surprise as you currently can't express dependently typed functions in scala.

[scabug]

@paulp said:
"They seem to be letting part of the type (namely its stability) escape into an outer lexical scope, which definitely seems iffy."

Why is that a problem? The "lexical" in "lexical scope" tells you what scopes are about: names. When properties of the value which can be expressed in the type without reference to its name are visible outside of the defining scope, that is the type system doing its job. That's what a type system is for.

[scabug]

@paulp said:
retronym: regarding the ill-scoped x in that output, I'm having trouble making sense of it. Is it the type of the expression which is carrying an explicit type ascription, before the type ascription has been applied? In which case you're really seeing an implementation artifact.

I say that because the types look right when I do good old -Xprint:typer for both these cases. Looking at the positions where Singleton is shown for f, I see no way x could possibly be escaping. And in g it is given the correct existential type.

object Test {
  def f = { val x = ""; x: x.type }: Singleton
  def g = { val x = "" ; identity[x.type] _ }
}
// def f: Singleton = ({
//   val x: String = "";
//   (x: x.type)
// }: Singleton);
// def g: x.type => x.type forSome { val x: String } = {
//   val x: String = "";
//   {
//     ((x: x.type) => scala.this.Predef.identity[x.type](x))
//   }
// }

[scabug]

@paulp said:
Okay, I can see the block is carrying the type x.type, which in principle is incorrect. But whenever the type of the block appears other than when printing internal data structures, either the x has been existentialized or it has been widened to String. I think it is pure implementation consideration.

[scabug]

@retronym said:
Here's one solution: create a refinement from the (unstable) type argument, and the singleton type over the parameter:

scala/scala#3486

That seems to get this ticket and #8223 to workingville without compromising safety in #3873.

[scabug]

@paulp said:
Aha, missing parens. Very exciting!

[scabug]

@clhodapp said:
To continue the escaping stability side-discussion, I will say that what you've said here and on #8223, I'm convinced not only that the stability can safely escape the scope, but that it would be a problem if it didn't. Obviously, the current implementation is still slightly "wrong", but at this time it doesn't seem all that pressing to fix it.