Improved treatment of mixed programs

Author: eernstg

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

@@ -362,9 +362,9 @@ available, but it is simply not using them.*
 
 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 removed.
+variance modifiers in type parameter declarations are ignored.
 
-*[TODO: This is a source of unsoundness; we probably cannot require that
-every type argument passed to a contravariant type parameter in legacy code
-must be a top type. Can we generate all the required dynamic checks to
-maintain soundness?]*
+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.