Widen types in ocaml

Question

I am trying to write a free monad library in ocaml, following Control.Monad.Free from haskell but I am stuck at one point, in the implementation of hoistFree.

hoistFree :: Functor g => (forall a. f a -> g a) -> Free f b -> Free g b
hoistFree _ (Pure a)  = Pure a
hoistFree f (Free as) = Free (hoistFree f <$> f as)

Here is my attempt at a translation.

let rec hoistfree : 'b.('b t -> 'b t) -> 'a m -> 'a m =
      fun f x -> match x with
       | Return x -> Return x
       | Free x   -> Free (T.map (hoistfree f) (f x));;

Unfortunately I get an error telling me I am not widening correctly the type of g.

Error: This definition has type ('b m t -> 'b m t) -> 'b m -> 'b m
       which is less general than 'a. ('a t -> 'a t) -> 'b m -> 'b m

Everything works fine if I don't insert the function type annotation, but then as the error message says, I don't get the general type for f. Where is the problem? How can I widen the type of f?

Answer 1

I'm not very familiar with Ocaml but I believe that

let rec hoistfree : 'b.('b t -> 'b t) -> 'a m -> 'a m =

is parsed as

let rec hoistfree : 'b. ( ('b t -> 'b t) -> 'a m -> 'a m ) =

instead of

let rec hoistfree : ('b. ('b t -> 'b t)) -> 'a m -> 'a m =

The former is a basic polymorphic type, the latter is a rank2-type which requires more support from the type system than Hindley-Milner.

IIRC, to achieve the latter you need to define a custom wrapper data type. For instance:

type poly = { polyf: 'a . 'a -> 'a } ;;

let foo (x: poly): int = x.polyf 4;;
let bar: poly = { polyf = fun x -> x } ;;

let _ = print_string ("hello " ^ string_of_int (foo bar));;