Why this weakly polymorphic type?

Question

module type M = sig
  type ('k, 'v) t
  val foo : 'k -> ('k, 'v) t
end

module M : M = struct
  type ('k, 'v) t = ('k * 'v) list
  let foo k = []
end

In this little example, why would M.foo 123 have a weakly polymorphic type, (int, '_a) M.t)?

Answer 1

This is the value restriction, I believe. M.foo 123 is not a value, it's a function application. So it can't have fully polymorphic type.

You can actually fix this by declaring 'v to be covariant in your module type. I never personally tried this before, but it does seem to work:

# module type M = sig
  type ('k, +'v) t
  val foo: 'k -> ('k, 'v) t
  end;;
module type M = sig type ('k, +'v) t val foo : 'k -> ('k, 'v) t end
# module M: M = struct
  type ('k, 'v) t = ('k * 'v) list
  let foo k = []
  end;;
module M : M
# M.foo 123;;
- : (int, 'a) M.t = <abstr>

I believe this works because of the "relaxed value restriction".

I learned about this use of the variance annotation from @gasche here: When does the relaxed value restriction kick in in OCaml?