Considering trying to succinctly write the covariant/contravariant subtyping inference rules, as an in-place reference for someone reading this without internet?  I know one can infer the relationships from the examples you provide in the doc below; i'm just wondering if there's some pithy four or five line summary we could put here.

e.g. something like: `for all types A, B`,
 * `A subtype-of B ==> tuple (A, Covariant<A>) subtype-of (B, Covariant<B>)`
 * `A subtype-of B ==> tuple (A, Contravariant<B>) subtype-of (B, Contravariant<A>)`

(I made the consequents tuples to try to stress the role of these types as markers; maybe a flawed idea...)