Merge pull request #3534 from clhodapp/test/literate_existentials

Add an extremely well-commented test

2 files changed, 228 insertions, 0 deletions

diff --git a/test/files/neg/literate_existentials.check b/test/files/neg/literate_existentials.check
new file mode 100644
index 0000000000..c98f976f79
--- /dev/null
+++ b/test/files/neg/literate_existentials.check
@@ -0,0 +1,4 @@
+literate_existentials.scala:189: error: Cannot prove that Int <:< M forSome { type M <: String }.
+  implicitly[Int <:< (M forSome { type M >: Nothing <: String })] // fails
+            ^
+one error found
diff --git a/test/files/neg/literate_existentials.scala b/test/files/neg/literate_existentials.scala
new file mode 100644
index 0000000000..8580347bf9
--- /dev/null
+++ b/test/files/neg/literate_existentials.scala
@@ -0,0 +1,224 @@
+
+object LiterateExistentials {
+
+//  Let's play with Scala's type system a bit.
+//
+//  From adriaanm, we have the following substitution rule, which allows us to
+//  determine whether a type is a subtype of an existential in Scala:
+//
+//
+//  T <: subst(U)    for all i: subst(Li) <: Vi /\ Vi <: subst(Hi)
+//  --------------------------------------------------------------
+//  T <: U forSome {type X1 :> L1 <: H1; ...; type Xn :> Ln <: Hn}
+//
+//  where subst(T) = T.subst(Xi, Vi) // Vi fresh type variables
+//
+//  T is a subtype of some existential if all constraints of the existential hold
+//  after substituting Vi for the existentially quantified type variables Xi,
+//  and T is a subtype of the underlying type U with the same substitution applied.
+//
+//
+//  Since we are not a formal substitution system, we will actually be using
+//  this rule 'backward' in order to determine whether it allows us to
+//  truthfully make claims; In each example, we will start with the proposition
+//  that a type is a subtype of an existential. Then, we will fit the
+//  proposition into the form on the bottom rule by creating a set of bindings
+//  which allow one to be transformed into the other. Next, we will express the
+//  top of the substitution rule in terms of a series of constraints. We will
+//  simplify those constraints until simple inspection can determine whether
+//  they are consistent. From this, we can conclude whether the type system /
+//  environment admit the top of the substitution rule (and thus, the bottom). If
+//  they do, we can say that the proposition is true.
+
+
+// In each case, we will also probe the compiler to see whether _it_ thinks that
+// the proposition holds, using an uncommented implicitly[_ <:< _] line.
+
+
+
+
+//  Proposition: Nothing :< (A forSome { type A >: String <: Any })
+//
+//
+//  Bindings:
+//  T  :=  Nothing
+//  U  := A
+//  X1 := A
+//  L1 := String
+//  H1 := Any
+//
+//  We need:
+//
+//  Nothing <: V1 // (U, which is "A", which V1 substituted for all instances of A)
+//  String <: V1
+//  V1 <: Any
+//
+//  Which simplify to:
+//  V1 >: String <: Any 
+//
+//  That's not inconsistent, so we can say that:
+//  T <: U forSome { type X1 >: L1 <: H1 }
+//  which means (under our mappings):
+//  Nothing <: A forSome { type A >: String <: Any }
+
+// Now to ask the compiler:
+  
+  implicitly[Nothing <:< (A forSome { type A >: String <: Any })]
+
+
+//  Let's try another:
+//
+//  Proposition: Int :< (M forSome { type M >: String <: Any })
+//
+//  Bindings:
+//  T := Int
+//  U := M
+//  X1 := M
+//  L1 := String
+//  H1 := Any
+//
+//  We need:
+//
+//  Int <: V1
+//  String <: V1
+//  V1 <: Any
+//
+//  Which simplify to:
+//
+//  V1 >: lub(Int, String) <: Any 
+//
+//  V1 >: Any <: Any 
+//
+//  We have demonstrated consistency! We can say that:
+//    T :< (U forSome { type U >: L1 <: H1 })
+//  Under our bindings, this is:
+//    Int :< (M forSome { type M >: String <: Any })
+  
+  implicitly[Int <:< (M forSome { type M >: String <: Any })]
+
+
+
+//  Now, let's do a more complicated one:
+//
+//  Proposition: (Nothing, List[String]) <: ((A, B) forSome { type A >: String <: AnyRef; type B >: Null <: List[A] })
+//
+//  Bindings:
+//  T  := (Nothing, List[String])
+//  U  := (A, B)
+//  X1 := A
+//  X2 := B
+//  L1 := String
+//  H1 := AnyRef
+//  L2 := Null
+//  H2 := List[A]
+//
+//  We need:
+//
+//  (Nothing, List[String]) <: (V1, V2)
+//  String <: V1
+//  V1 <: AnyRef
+//  Null <: V2
+//  V2 <: List[V1]
+//
+//  Of course, we can split the first line to make:
+//
+//  Nothing <: V1
+//  List[String]) <: V2
+//  String <: V1
+//  V1 <: AnyRef
+//  Null <: V2
+//  V2 <: List[V1]
+//
+//  Which reorder to:
+//
+//  Nothing <: V1
+//  String <: V1
+//  V1 <: AnyRef
+//  List[String]) <: V2
+//  Null <: V2
+//  V2 <: List[V1]
+//
+//  Which simplify to:
+//
+//  String <: V1
+//  V1 <: AnyRef
+//  List[String]) <: V2
+//  V2 <: List[V1]
+//
+//  String <: V1
+//  V1 <: AnyRef
+//  String <: V1
+//
+//  V1 >: String <: AnyRef
+//
+//  Consistency demonstrated! We can say that:
+//  T <: U forSome {type X1 :> L1 <: H1; type X2 :> L2 <: H2}
+//  meaning:
+//  (Nothing, List[String]) <: ((A, B) forSome { type A >: String <: AnyRef; type B >: Null <: List[A] })
+
+  implicitly[
+    (Nothing, List[String]) <:< ((A, B) forSome { type A >: String <: AnyRef; type B >: Null <: List[A] })
+   ]
+
+
+
+//  Now let's try one that isn't true:
+//
+//  Proposition: Int :< (M forSome { type M >: Nothing <: String })
+//
+//  Bindings:
+//  T  := Int
+//  U  := M
+//  X1 := M
+//  L1 := Nothing
+//  H1 := String
+//
+//  We need:
+//
+//  Int <: V1
+//  Nothing <: V1
+//  V1 <: String
+//
+//  V1 >: Int <: String 
+//
+//  Alas! These are inconsistent! There is no supertype of Int that is a
+//  subtype of String! Our substitution rule does not allow us to claim that our
+//  proposition is true.
+//
+
+  implicitly[Int <:< (M forSome { type M >: Nothing <: String })] // fails
+// The preceeding line causes the compiler to generate an error message.
+
+
+
+//  Let's look at one final example, courtesy of paulp.
+//  Proposition: String :< X forSome { type X >: Nothing <: String }
+//
+//  Bindings:
+//  T  := String
+//  U  := X
+//  X1 := X
+//  L1 := Nothing
+//  H1 := String
+//
+//  We need:
+//
+//  String <: V1
+//  Nothing <: V1
+//  V1 <: String
+//
+//  Which simplify to:
+//
+//  String <: V1
+//  V1 <: String
+//
+//  V1 >: String <: String
+//
+//  So, we can say:
+//  T <: U forSome { type X1 >: L1 <: H1 }
+//  which means:
+//  String :< X forSome { type X >: Nothing <: String }
+
+  implicitly[String <:< (X forSome { type X >: Nothing <: String })]
+
+}