Typings.txt

   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.



Nothing :< (A forSome { type A >: String <: Any })


Mappings:
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 <: Any >: String

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 }



<=================================================>



Let's try another:

Int :< (M forSome { type M <: String >: Nothing })

Mappings:
T -> Int
U -> M
X1 -> M
L1 -> Nothing
H1 -> String

We need:

Int <: V1
Nothing <: V1
V1 <: String

Which simplify to:
Int <: V1
V1 <: String

V1 <: String >: Int

Alas! These are inconsistent! No subtype of String is a supertype of Int! We can say nothing, Lebowski,
nothing.



<=================================================>



Now, let's do a more complicated one:

(Nothing, List[String]) <: ((A, B) forSome { type A >: String <: AnyRef; type B >: Null <: List[A] })

Mappings:
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]

Which simplify to:
String <: V1
V1 <: AnyRef
String <: V1

Which simplify to:
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] })



<=================================================>



Now, let's try Paul's example:
String :< X forSome { type X <: String }

More fully, this is:
String :< X forSome { type X >: Nothing <: String }

Mappings:
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
// Hey! These are the constraints I referred to in my original post on the thread!

Which simplify to:
V1 >: String <: String

So, we can say:
T <: U forSome { type X1 >: L1 <: H1 }
which means:
String :< X forSome { type X >: Nothing <: String }