Context: Dafny is a programming language with a built-in SMT solver that can encode formally-checked statements (e.g. preconditions, postconditions, assertions).
Dafny has features of most programming languages; for example, covariant/contravariant/"non-variant" (invariant) type parameters. But in order to keep said verification sound and decidable in reasonable time, these features have extra restrictions and other complexities.
This article explains that there are 2 more "variance modes", because the of "covariant" and "invariant" variances may be "cardinality-preserving" or "not cardinality-preserving".
// Most "traditional" languages have 3 variances
type Foo<
+CovariantParameter,
NonVariantParameter,
-ContravariantParameter>
// Dafny has 5
type Bar<
+CovariantCardinalityPreservingParameter,
NonVariantCardinalityPreservingParameter,
-ContravariantParameter,
*CovariantNonCardinalityPreservingParameter,
!NonVariantNonCardinalityPreservingParameter>