It can mostly be done. The OCaml programming language does exactly this - it infers co/contravariance. However, when describing a generic interface which has as

It can mostly be done. The OCaml programming language does exactly this - it infers co/contravariance. However, when describing a generic interface which has as part of it a function on types (usually called a "type constructor"), you need to say whether that type constructor is supposed to be covariant, contravariant, or invariant. For example, if I were describing a sequence interface, I would write module type SEQ = sig (* the "+" means that seq must be covariant *) type +'a seq val empty : 'a seq val singleton : 'a -> 'a seq val append : 'a seq -> 'a seq -> 'a seq val lookup : int -> 'a seq -> 'a option exception IndexOutOfBounds end;; See https://blogs.janestreet.com/a-and-a/ https://blogs.janestreet.com/a-and-a/ for a nice explanation.