What type annations can I use to allow different calls to a function to assume different polymoprhic types

This question is connected to another question I asked here.

But this question is a bit more focused on this simple piece of code that I wrote in trying to understand the different type annotations like (type a): versus : type a..

let f = fun id x -> 
    let i = id 4 in
    let f = id 4.0 in
       (Int.to_float i) +. f;;

This code doesn't type check. I understand that is because the checker 'infers' id : int -> ... from let i = id 4 but that conflicts with inferring id : float -> ... on next line.

Intuitively though I would expect the above code to be 'fine' if we can somehow tell the type system that the function id is of type a -> a and this type is allowed to vary between call sites. (i.e. we can pick a different 'a on every call to id).

I gather that annotations like type a. and (type a) : are there precisely to let me tell that to the type checker somehow.

Here's one of the things I tried. I annotated the 'binding occurrence' of id to use type a. to try and make it 'explicitly polymorphic'. But the syntax won't let me actually use type a. ... there as a type annotation.

let f = fun (id : type a.a -> a) x -> begin 
               (* ^^^^ syntax error: type expected *) 
         let i = id 4 in
         let f = id 4.0 in
         (Int.to_float i) +. f
end;;

A bit confusing/ironic that error. It points at the word 'type' and says that what is expected there is type. I gather the error means it expects 'a type' rather than the keyword type. However I thought (mistakenly I guess) that type a. ... would actually considered as a valid 'type'.

So, finally the question is there some way to annotate my piece of code and make it type check? Or is it not possible?

Solution

The underlying problem here is that this requires higher-rank polymorphism, which OCaml does not support implicitly. The workaround is to make it explicit by wrapping the function in a record or object, which allows for universal quantification on a field or method level.

type f = { f: 'a. 'a -> 'a }

let f = fun id ->
   let i = id.f 4 in
   let f = id.f 4.0 in
   float_of_int i +. f

See the section on Polymorphism and its limitations in the OCaml manual for a more detailed explanation.