Abstract type convariance / contravariance

Question

I was playing with this code and I don't understand something.

type t1 = [ `A ];;
type t2 = [ t1 | `B ] ;;
type t3 = [ t2 | `C ] ;;

module type MT =
sig
  type ('a,'b) fct
  val create : ('a -> 'b) -> ('a,'b) fct
end;;

module Mt : MT =
struct
    type ('a,'b) fct = 'a -> 'b
    let create f = f
end;;

let f = (fun x -> x : t2 -> t2) ;;
let af = Mt.create (fun x -> x : t2 -> t2);;

(f :> t1 -> t3);;
(af :> (t1, t3) Mt.fct);;

Like this it doesn't work, because the compiler doesn't know if the type parameters of Mt.fct are covariant or contravarient. But if you replace the type declaration in the module signature by :

type (-'a,'+b) fct

Telling the compiler that b is covariant and a contravariant, now it works. And because I'm a tricky little annoying boy, I tried to lie to the compiler by telling him that a is also covariant !

type (+'a,'+b) fct

He's smarter than I though, and he notices that I'm lying to him.

Type declarations do not match:
         type ('a, 'b) fct = 'a -> 'b
       is not included in
         type (+'a, +'b) fct
       Their variances do not agree.

My question is : if he knows anyways the variance of the type parameters, why doesn't it just use that for my module, instead of forcing me to add those + and -. Is it again a decidability issue ?

Answer 1

The type ascription Mt : MT is opaque. Thus the compiler can't use the information about the type definition, since you could change the definition (that could be compiled separately) at any time. To see this, if you do

module type MT =
sig
  type ('a,'b) fct = 'a -> 'b
  val create : ('a -> 'b) -> ('a,'b) fct
end;;

then the code you wrote compiles fine.

Answer 2

While the compiler can perform a check as to whether your type is actually covariant or contravariant in a particular argument position, it doesn't immediately assume that this is information you'd like to expose in your abstract type. After all, once a compiler is aware of the variance of a parameter then it will be allowed to perform coercion on that parameter as needed—that may simply not be a part of your public API!