普通のMLと同様に、MinCamlでは変数や関数の型を書かなくても自動で推論してくれます。これを型推論といい、多相関数や高階関数のあるプログラムでは非常に便利です。
MinCamlの型推論の本体は関数Typing.gです。この関数は、型環境（変数の名前から、その型への写像）envと、式eとを受け取り、eの型を推論して返します。また、式の中に出てくる変数の型が合っているかどうかも調べます。もし未定義の型変数があったら、適切な型を代入します。このような代入により型を合わせる関数がTyping.unifyです。
たとえば、足し算e1 +
e2（Syntax.tに合わせて書くとAdd(e1,
e2) ）だったら、まずg env e1により部分式e1の型を推論し、その型がintであることをunifyにより確かめます。部分式e2についても同様です。そして、式全体の型としてintを返します。
少しややこしい例としては、関数適用e e1
... enがあります。eが関数で、e1からenまでが引数です。この場合は、関数の型はg
env e、引数の型はg
env e1, ..., g env enのように推論できますが、返値の型がわかりません。そこで、未定義の新しい型変数tを作り、g
env eが「g
env e1, ..., g env en を受け取ってtを返す」関数型と等しくなるようにunifyを呼んでいます。そして、式全体の型としてtを返します。
letやlet recのように新しい変数が導入されるところでは、型環境envが拡張されます。逆に変数xが出てきたら、型環境envを引いて型を得ます。ただし、型環境に含まれていない変数が出てきたら、プログラムの外から与えられる外部変数とみなし、未定義の新しい型変数を与え、外部変数のための特別な環境extenvに追加します。これは普通のMLでは実現されてない、MinCamlに特有の機能です。これにより、宣言しなくても外部変数を使用することができます。
関数Typing.unifyは、与えられた二つの型が等しいかどうかを中まで調べていき、一方が未定義の型変数Type.var(ref
None)だったら、他方と等しくなるように代入を行います。ただし一方の型変数が、他方の型の中に現れていないかどうかチェックします（occur checkと呼ばれます）。もし現れていると、代入結果の型にサイクルができてしまうからです。たとえば、もし（occur
checkをしないで）型変数αと関数型int→αをunifyしてしまうと、α
= int→αなので、int→int→int→...という無限長の型になってしまいます！ このようなことを防止するために（ちょっとややこしいですが）occur
checkは必要なのです。
型推論が終了したら（エラーでも正常終了でも）、結果をわかりやすくするために、すべての型変数をその中身でおきかえます（Typing.deref_typ）。もしまだ未定義の型変数があったら、型が決まらないということなので、勝手にintとしてしまいます。これもMinCamlに特有の仕様です。