First, as stated by @lukstafi , your use case can be covered by an explicit universal quantification:

```
type ('a, 'b) conv =
| Int_to_float : (int, float) conv
| Int_to_string : (int, string) conv
| Float_to_int : (float, int) conv
let int_conv: type a. int -> (int, a) conv -> a = fun i conv ->
match conv with
| Int_to_float -> float_of_int i
| Int_to_string -> string_of_int i
| _ -> .
```

Here I am using `type a. ... `

since we need both the universal quantification and the locally abstract type. I generally recommend to use this variant in all cases.

Polymorphic record fields are needed for higher-rank polymorphic functions: functions that takes other functions as argument and use those functions on multiple types.

For instance, if I try to write a function that convert a integer to both `float`

and `int`

using a `conv`

function taken in argument

```
let apply_twice conv n =
Format.printf "%f=%s" (conv n Int_to_float) (conv n Int_to_string)
```

I end up with a compiler error:

```
Error: This expression has type (int, string) conv
but an expression was expected of type (int, float) conv
Type string is not compatible with type float
```

because in the body of `apply_twice`

, the function `conv`

is supposed to be monomorphic.

Polymorphic record fields are a solution to *this* conundrum:

```
type 'a polyconv = { conv: 'b. 'a -> ('a,'b) conv -> 'b }
let apply_twice {conv} n =
Format.printf "%f=%s" (conv n Int_to_float) (conv n Int_to_string)
```

(The polymorphism and its limitation section of manual has more information)

The issue however is that type inference for higher-rank polymorphism is undecidable in general. To alleviate this issue, OCaml limit the use of explicit universal type quantification to either let bindings, record fields and object methods. Those limitations are sufficient to make type inference decidable once again. But this means that it is not possible to allow a type abbreviation to contain explicit universal quantification, like

```
type t = 'a. 'a -> 'a
```

and generally it is simpler to have only one way (or two if counting object methods and record fields separately) to box polymorphic type expressions.

Note that for constructors, it is possible to have an explicit universal quantification too. However, in this case the quantification describes the behavior of the constructor. Typically, in

```
type printable = Printable: 'elt. ('elt -> string) * 'elt -> printable
```

the type `'a. ('a -> string) * 'a -> printable`

means that for any type 'a, I can construct a `printable`

value by putting both a printing function of type `'a -> string`

and a value inside the constructor `Printable`

. However, this is the dual situation compared to the record type: I am declaring how to construct a value of type `printable`

from a value of type `'a . ('a -> string) * 'a`

rather than defining the content after deconstructing the value.

Consequently, when I peak inside `Printable (print,x)`

, I don’t get an universally quantified type, but its dual: an existential quantification. In other words, I know that there is some type `'a`

, such that the type of `print`

is `'a -> int`

, and the type of `x`

is `'a`

. Thus I can write:

```
let to_string (Printable(print,x)) = print x
let int n = Printable(string_of_int, n)
let string s = Printable(Fun.id, s)
let l = List.map to_string [int 0; string "hi"]
```

but I don’t know anything else about this type `'a`

. In particular, I cannot write

```
let print_int (Printable(print,_)) = print 0
```

because as stated by the compiler

Error: This expression has type int but an expression was expected of type

$Printable_'elt

I have no idea if the type `int`

is compatible with the type expected by the printer stored inside the constructor `Printable`

.