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 ?
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.