Deal with expansion lost caused by intersection

[samuelgruetter]

From Section 4.2 of the FOOL'12 DOT paper:

object test {

  trait T1 {
    type A <: B
    type B
  }

  trait T2 {
    type A
    type B <: A
  }

  val x: T1 & T2 = ???
  val y: x.A = 42

}

This example sends dotty into an infinite loop. In Scala 2, this cannot happen because there's no symmetric type intersection.

[samuelgruetter]

This example is also interesting from a theoretical point of view because it shows that narrowing only holds if we allow subsumption (imprecise typing): If we narrow from Γ = {x: T1} to Γ = {x: T1 & T2}, x.A loses its expansion, unless we can apply subsumption to consider that x is of type T1.

And guess what I'd need in the DOT soundness proof: Narrowing for precise typing ;-)

[smarter]

Not sure about the theoretical side, but this is now disallowed in Dotty:

error: cyclic reference involving class Any
   val y: x.A = 42
            ^