I am trying to make comparisons with Coq just to learn more about functional programming and proof assistants (and their relationships and difference).

The simplest example is the polymorphic identity function. In Coq it is easy to pass types as actual arguments and show them explicitly in function e.g.

```
Check fun {T: Type} (x:T) => x.
```

output

```
fun (T : Type) (x : T) => x
: forall T : Type, T -> T
```

or

```
Definition id (T:Type) (x:T) := x.
Check id.
```

output:

```
id
: forall T : Type, T -> T
```

and I can call it with

```
Compute id nat 1.
```

output

```
= 1
: nat
```

Notice that I passed `nat`

as an argument. Can this be done in Ocaml or does type inference the only way to determine the values of type variables like `'a`

? (my guess is that one cannot pass them since I’ve never seen them and I read somewhere that the type system of OCaml is decidable so my guess is that there is no need…)