Clarified treatment of mixed programs

Author: eernstg

accepted/future-releases/variance/feature-specification.md

@@ -364,7 +364,10 @@ When a legacy library _L_ imports a library _L2_ with sound variance, the
 declarations imported from _L2_ are _legacy erased_. This means that all
 variance modifiers in type parameter declarations are ignored.
 
-In a mixed program (where both legacy libraries and libraries with sound
-variance exist), a dynamic type check is performed on the actual arguments
-for each instance method parameter whose declared type contains a
-contravariant type variable.
+*To maintain a sound heap in a mixed program execution (that is, when both
+legacy libraries and libraries with sound variance exist), it is then
+necessary to perform some type checks at run time.  In particular, a
+dynamic type check is performed on method calls: The actual argument for
+each instance method parameter whose declared type contains a contravariant
+type variable. Moreover, a caller-side check is performed on each
+expression whose static type contains a contravariant type variable.*