In the paper Practical type inference for arbitrary-rank types, the covariance and contravariance rules are essential when dealing with function types. Covariance applies to the return types of functions, while contravariance applies to the argument types.
In (∀b. [b] → [b]) → Bool < (∀a. a → a) → Bool, the types are compared in a contravariant manner for the input types, which means the more general type must be on the right side. Here, the type a → a is more general than [b] → [b], making the inequality hold. However, in the case of [b] → Int < a → Int, the argument types are compared contravariantly. For contravariance to hold, the left-hand side argument must be more specific than the right-hand side. Since a can be any type and [b] is a specific type (a list of b), the inequality holds but it should not, for example you can not type annotate length function with a -> Int.
In my opinion, the correct relationship would be a → Int < [b] → Int, and this happens by matching a with [b].
I've been reading some papers on type inference, particularly around co- and contravariant rules for functions. I understand where the contravariant rule comes from, but I don't understand why it doesn't work for examples like [b] → Int < a → Int.
Could someone explain why the contravariant rule doesn't apply here, or if I'm misunderstanding something fundamental?
([b] -> Int) < (a -> Int)from? You are saying it is wrong but it is not clear where the claim that it is right comes from. $\endgroup$