Permalink
Browse files

[nomaster] SI-8146 Fix non-deterministic <:< for deeply nested types

Backported from master. This is a squashed commmit comprising:

SI-8146 Pending test, diagnosis for bug in decidability of <:<

(cherry picked from commit 8beeef3)

SI-8146 Test cases for typechecking decidability

Taken from "On Decidability of Nominal Subtyping with Variance"
(Pierce, Kennedy), which was implemented in 152563b.

Part of the implementation (SubTypePair) will be changed in the
following commit to fix the non-deterministic errors typechecking
heavily nested types involving aliases or annotations.

(cherry picked from commit 2e28cf7)

SI-8146 Fix non-deterministic <:< for deeply nested types

In the interests of keeping subtyping decidable [1], 152563b
added some bookkeeping to `isSubType` to detect cycles.

However, this was based on a hash set containing instances of
`SubTypePair`, and that class had inconsistencies between its
`hashCode` (in terms of `Type#hashCode`) and `equals`
(in terms of `=:=`).

This inconsistency can be seen in:

    scala> trait C { def apply: (Int @unchecked) }
    defined trait C

    scala> val intUnchecked = typeOf[C].decls.head.info.finalResultType
    intUnchecked: $r.intp.global.Type = Int @unchecked

    scala> val p1 = new SubTypePair(intUnchecked, intUnchecked)
    p1: $r.intp.global.SubTypePair = Int @unchecked <:<? Int @unchecked

    scala> val p2 = new SubTypePair(intUnchecked.withoutAnnotations, intUnchecked.withoutAnnotations)
    p2: $r.intp.global.SubTypePair = Int <:<? Int

    scala> p1 == p2
    res0: Boolean = true

    scala> p1.hashCode == p2.hashCode
    res1: Boolean = false

This commit switches to using `Type#==`, by way of the standard
case class equality.

The risk here is that you could find a subtyping computation that
progresses in such a manner that we don't detect the cycle. It would
need to produce an infinite stream of representations for types that
were `=:=` but not `==`. If that happened, we'd fail to terminate,
rather than judging the relationship as `false`.

[1] http://research.microsoft.com/pubs/64041/fool2007.pdf

(cherry picked from commit a09e143)

Conflicts:
	src/reflect/scala/reflect/internal/tpe/TypeComparers.scala
	src/reflect/scala/reflect/runtime/JavaUniverseForce.scala
  • Loading branch information...
1 parent cbb88ac commit ff137422794a3da002bcad9b67afd3ef02fceaa1 @retronym retronym committed Jan 14, 2014
View
35 src/reflect/scala/reflect/internal/Types.scala
@@ -5230,30 +5230,15 @@ trait Types extends api.Types { self: SymbolTable =>
}
}
- class SubTypePair(val tp1: Type, val tp2: Type) {
- override def hashCode = tp1.hashCode * 41 + tp2.hashCode
- override def equals(other: Any) = other match {
- case stp: SubTypePair =>
- // suspend TypeVars in types compared by =:=,
- // since we don't want to mutate them simply to check whether a subtype test is pending
- // in addition to making subtyping "more correct" for type vars,
- // it should avoid the stackoverflow that's been plaguing us (https://groups.google.com/d/topic/scala-internals/2gHzNjtB4xA/discussion)
- // this method is only called when subtyping hits a recursion threshold (subsametypeRecursions >= LogPendingSubTypesThreshold)
- def suspend(tp: Type) =
- if (tp.isGround) null else suspendTypeVarsInType(tp)
- def revive(suspension: List[TypeVar]) =
- if (suspension ne null) suspension foreach (_.suspended = false)
-
- val suspensions = Array(tp1, stp.tp1, tp2, stp.tp2) map suspend
-
- val sameTypes = (tp1 =:= stp.tp1) && (tp2 =:= stp.tp2)
-
- suspensions foreach revive
-
- sameTypes
- case _ =>
- false
- }
+ final case class SubTypePair(tp1: Type, tp2: Type) {
+ // SI-8146 we used to implement equality here in terms of pairwise =:=.
+ // But, this was inconsistent with hashCode, which was based on the
+ // Type#hashCode, based on the structure of types, not the meaning.
+ // Now, we use `Type#{equals,hashCode}` as the (consistent) basis for
+ // detecting cycles (aka keeping subtyping decidable.)
+ //
+ // I added tests to show that we detect the cycle: neg/t8146-no-finitary*
+
override def toString = tp1+" <:<? "+tp2
}
@@ -5819,7 +5804,7 @@ trait Types extends api.Types { self: SymbolTable =>
if (subsametypeRecursions >= LogPendingSubTypesThreshold) {
val p = new SubTypePair(tp1, tp2)
if (pendingSubTypes(p))
- false
+ false // see neg/t8146-no-finitary*
else
try {
pendingSubTypes += p
View
9 test/files/neg/t8146-non-finitary-2.check
@@ -0,0 +1,9 @@
+t8146-non-finitary-2.scala:5: error: class graph is not finitary because type parameter X is expansively recursive
+trait C[X] extends N[N[C[D[X]]]]
+ ^
+t8146-non-finitary-2.scala:7: error: type mismatch;
+ found : C[Int]
+ required: N[C[Int]]
+ def foo(c: C[Int]): N[C[Int]] = c
+ ^
+two errors found
View
8 test/files/neg/t8146-non-finitary-2.scala
@@ -0,0 +1,8 @@
+// Example 3 from "On Decidability of Nominal Subtyping with Variance" (Pierce, Kennedy)
+// http://research.microsoft.com/pubs/64041/fool2007.pdf
+trait N[-Z]
+trait D[Y]
+trait C[X] extends N[N[C[D[X]]]]
+object Test {
+ def foo(c: C[Int]): N[C[Int]] = c
+}
View
9 test/files/neg/t8146-non-finitary.check
@@ -0,0 +1,9 @@
+t8146-non-finitary.scala:4: error: class graph is not finitary because type parameter A is expansively recursive
+trait C[A] extends N[N[C[C[A]]]]
+ ^
+t8146-non-finitary.scala:6: error: type mismatch;
+ found : C[Int]
+ required: N[C[Int]]
+ def foo(c: C[Int]): N[C[Int]] = c
+ ^
+two errors found
View
7 test/files/neg/t8146-non-finitary.scala
@@ -0,0 +1,7 @@
+// Example 3 from "On Decidability of Nominal Subtyping with Variance" (Pierce, Kennedy)
+// http://research.microsoft.com/pubs/64041/fool2007.pdf
+trait N[-A]
+trait C[A] extends N[N[C[C[A]]]]
+object Test {
+ def foo(c: C[Int]): N[C[Int]] = c
+}
View
9 test/files/pos/t8146a.scala
@@ -0,0 +1,9 @@
+trait M[+A]
+
+object Test {
+ type Inty = Int
+ def t1(
+ x: M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[Int @unchecked]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
+ ): M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[M[Inty @unchecked]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
+ = x
+}
View
77 test/files/pos/t8146b.scala
@@ -0,0 +1,77 @@
+// non-deterministic type errors, non-termination.
+// seems to be due to inconsistent hashing/equality in SubTypePair
+
+import scala.language.{existentials, implicitConversions}
+import scala.annotation.unchecked.uncheckedVariance
+
+trait Column[T]
+
+// Turning this into a trait reduces (eliminates?) the likelihood of type errors (but not of non-termination)
+abstract class Shape[Level <: ShapeLevel, -Mixed_, Unpacked_, Packed_]
+
+trait ShapeLevel
+trait NestedShapeLevel extends ShapeLevel
+trait FlatShapeLevel extends NestedShapeLevel
+trait ColumnsShapeLevel extends FlatShapeLevel
+
+trait ProvenShape[U]
+
+object ProvenShape {
+ implicit def proveShapeOf[T, U](v: T)(implicit sh: Shape[_ <: FlatShapeLevel, T, U, _]): ProvenShape[U] = ???
+}
+
+sealed abstract class HList {
+ type Self <: HList
+ type :: [E] = HCons[E, Self]
+ final def :: [E](elem: E): :: [E] = ???
+}
+
+final class HCons[+H, +T <: HList](val head: H, val tail: T) extends HList {
+ type Self = HCons[H @uncheckedVariance, T @uncheckedVariance]
+}
+
+final object HNil extends HList {
+ type Self = HNil.type
+}
+
+// Success is more likely when not using these aliases
+object syntax {
+ type :: [+H, +T <: HList] = HCons[H, T]
+ type HNil = HNil.type
+}
+
+class HListBench {
+
+ import syntax._
+
+ implicit def columnShape[T, Level <: ShapeLevel]: Shape[Level, Column[T], T, Column[T]] = ???
+ implicit def provenShape[T, P](implicit shape: Shape[_ <: FlatShapeLevel, T, _, P]): Shape[FlatShapeLevel, ProvenShape[T], T, P] = ???
+ final class HListShape[Level <: ShapeLevel, M <: HList, U <: HList, P <: HList](val shapes: Seq[Shape[_ <: ShapeLevel, _, _, _]]) extends Shape[Level, M, U, P]
+ implicit def hnilShape[Level <: ShapeLevel] = new HListShape[Level, HNil.type, HNil.type, HNil.type](Nil)
+ implicit def hconsShape[Level <: ShapeLevel, M1, M2 <: HList, U1, U2 <: HList, P1, P2 <: HList]
+ (implicit s1: Shape[_ <: Level, M1, U1, P1], s2: HListShape[_ <: Level, M2, U2, P2]) =
+ new HListShape[Level, M1 :: M2, U1 :: U2, P1 :: P2](s1 +: s2.shapes)
+
+ trait A[T] {
+ def * : ProvenShape[T]
+ }
+
+ trait B extends A[
+ Int :: Int :: Int :: Int :: Int ::
+ Int :: Int :: Int :: Int :: Int ::
+ Int :: Int :: Int :: Int :: Int ::
+ Int :: Int :: Int :: Int :: Int ::
+ Int :: Int :: Int :: Int :: Int ::
+ Int :: Int :: HNil ] {
+
+ def c: Column[Int]
+
+ def * = c :: c :: c :: c :: c ::
+ c :: c :: c :: c :: c ::
+ c :: c :: c :: c :: c ::
+ c :: c :: c :: c :: c ::
+ c :: c :: c :: c :: c ::
+ c :: c :: HNil
+
+ }
+}

0 comments on commit ff13742

Please sign in to comment.