The Invisible Engine: Why Your Type System is Smarter Than You Think

Programming languages are, at their core, contracts between human intent and machine execution. We write code to express logic, but that logic lives in a fragile world of bits and bytes, where a single misstep—a null where an Integer was promised, a function applied to a list instead of a number—can bring the entire digital edifice crashing down. For decades, developers have sought guardians against this chaos. We have linters, static analyzers, and the ever-present specter of unit tests. But the most elegant, most deeply integrated guardian is the type system.

If you have ever written a line of Haskell, Rust, OCaml, TypeScript (with strict: true), or even Swift, you have experienced the quiet miracle of type inference. You did not tell the compiler that let x = 5 is an integer. You didn’t annotate the function map with its full, terrifying type signature. Yet, the compiler knew. It saw your code, traced the data flow, and deduced the types with a precision that feels almost magical. This magic has a name: Hindley-Milner (HM) type inference.

Today, we are going to pull back the curtain. We are not going to just use a language with this feature; we are going to build one. We will deconstruct the computational engine that powers this magic, focusing on its two most critical, most fascinating gears: Unification and the Occurs Check.

This isn’t merely an academic exercise. Understanding how to build a type checker is a superpower. It teaches you to think about code not as a sequence of instructions, but as a system of equations. It transforms the compiler from a mysterious black box into a logical machine whose every error message is a solvable puzzle. Whether you are designing a domain-specific language (DSL) for a niche industry, debugging a perplexing type error in a large codebase, or simply satisfying your curiosity about how programming languages work, the knowledge you gain here will fundamentally change how you write code.

So grab your favorite editor. We are about to implement a type checker for a tiny functional language. By the end of this journey, you will have a working inference engine that can handle variables, lambda abstractions, function application, and even the crown jewel of HM: let-polymorphism. And along the way, we will demystify every algorithm and every check, including the subtle but crucial occurs check that prevents the type system from collapsing into infinite recursion.

The Language We’ll Type-Check

Before we dive into the inference machinery, we need a language to work with. Let’s define a minimal but expressive typed lambda calculus. Our language will support:

• Integer literals (42, -1, 0)
• Variables (x, y, f)
• Lambda abstractions (fun x -> e)
• Function application (e1 e2)
• Local definitions (let x = e1 in e2)

We’ll call this language MiniML. It’s a pure functional core, which means we don’t have side effects, mutation, or loops. That’s fine—type inference for an impure language requires a bit more care (the infamous “value restriction”), but we’ll touch on that later.

In ML-like syntax, the abstract syntax tree (AST) can be represented as:

type expr =
  | Int of int
  | Var of string
  | Lam of string * expr
  | App of expr * expr
  | Let of string * expr * expr

For example, the lambda term (fun x -> x + 1) 5 is parsed as:

App (Lam ("x", App (App (Var "+", Var "x"), Int 1)), Int 5)

We’ll assume + is a predefined function of type int -> int -> int. Our type checker will treat it as a built-in constant with that type. Similarly, we could add other primitives like *, -, if-then-else, but for clarity, we’ll keep the core minimal.

Our goal is to write a function infer : expr -> type_scheme that, given an expression, returns its type scheme (allowing polymorphism). Along the way, we’ll need to manage a type environment (context) that maps variable names to type schemes.

Types and Type Schemes

A type system is built on a grammar of types. For our language, we need:

• Base types: int (and maybe bool, but we’ll keep it simple).
• Type variables: 'a, 'b, 'c, etc. These represent unknown types that can be instantiated or unified.
• Function types: t1 -> t2.

In a richer language we would also have product types (tuples), sum types (variants), etc., but functions alone are surprisingly powerful.

We can model types in OCaml as:

type typ =
  | TInt                          (* integer base type *)
  | TVar of type_var              (* type variable *)
  | TFun of typ * typ             (* function type *)

and type_var = { id: int; mutable binding: typ option }

Crucially, type variables are mutable references to an optional resolved type. This is the classic approach used in algorithm W: we treat type variables as cells that can be filled in gradually during unification. The binding field starts as None and becomes Some resolved_typ when the type variable is unified with something concrete.

A type scheme generalizes a type by quantifying over some type variables. For example, the identity function fun x -> x has type 'a -> 'a. That’s a scheme: forall 'a. 'a -> 'a. We represent a scheme as:

type scheme = Forall of int list * typ

where the integer list are the IDs of the type variables that are universally quantified. However, since our unification uses mutable variables, quantification is more subtle—we’ll handle it by creating fresh type variables and then generalizing those that are not free in the environment.

For simplicity, during inference we’ll avoid explicit forall and instead work with an environment that maps variable names to syntactic type schemes. The environment will have a special tag indicating whether a variable is polymorphic (from a let) or monomorphic (from a lambda parameter).

The Algorithm: A Bird’s-Eye View

The Hindley-Milner inference algorithm, typically called Algorithm W (due to Damas and Milner’s 1982 paper), proceeds in two phases:

1. Constraint generation: Walk the AST and, for each subexpression, produce a type variable that represents its result type, and a set of equality constraints between types that must hold for the expression to be well-typed. For example, in an application e1 e2, we generate a constraint that the type of e1 must be T -> T_result where T is the type of e2.

2. Unification: Solve the constraints by a process called unification. Unification finds a substitution—a mapping from type variables to types—that makes all constraints hold. The substitution is then applied to all inferred types.

In practice, Algorithm W combines these phases: it generates constraints and solves them on the fly, returning a substitution and the inferred type. We’ll present a slightly modernized version that is easier to implement in a functional language with mutable references: the algorithm by Pierce, called Algorithm J (or “naive” algorithm) that uses mutable type variables and unification as an effect.

We’ll walk through each inference rule with examples.

Inference for Basic Expressions

Integer Literals

Rule: Int n has type int.

No constraints needed. We return the type TInt.

Variables

Rule: A variable x gets its type from the environment. The environment contains a typ (which may be a monomorphic type or a type scheme). For a monomorphic variable (e.g., a lambda parameter), we simply look up the type. For a polymorphic variable from a let binding, we need to instantiate it: replace all universally quantified type variables with fresh type variables (this is what makes ML polymorphic functions work).

We’ll implement a helper: instantiate : scheme -> typ that replaces each quantified variable ID with a fresh TVar { id="i6c519a6" binding = None }.

Lambda Abstractions

Rule: For fun x -> e, we create a fresh type variable a for the parameter (unless an explicit annotation is given, but we don’t have those yet). Then we extend the environment with x : a (monomorphic) and infer the type of e, getting body_typ. The overall type is a -> body_typ.

The substitution produced from inferring the body is applied to both a and body_typ. This is straightforward.

Function Application

Rule: For e1 e2, we infer the type of e1 (call it t1) and of e2 (call it t2). Then we create a fresh type variable result for the result. We unify t1 with TFun(t2, result). This unification may fill in some type variables. The final type is result.

This is where the core of the inference happens. Unification is the engine.

Let Expressions

Rule: For let x = e1 in e2, we infer the type of e1 (call it t1). Then we generalize over all type variables that are free in t1 but not free in the current environment. This produces a type scheme forall ... t1. Then we instantiate that scheme to get a fresh monomorphic type for x, extend the environment, and infer e2. The overall type is the type of e2.

This is the key to parametric polymorphism. Without let-polymorphism, lambda-bound variables would be monomorphic, severely limiting expressiveness (e.g., you couldn’t use the identity function twice with different types inside the same lambda).

Now let’s implement each of these rules concretely.

A Practical Implementation of Algorithm W

We’ll implement the inference in OCaml, using mutable type variables. First, we need a global counter for fresh type variable IDs:

let fresh_counter = ref 0

let fresh_var () =
  let id = !fresh_counter in
  incr fresh_counter;
  TVar { id; binding = None }

Next, the unification function. Unification takes two types and attempts to make them equal by updating the mutable bindings of type variables. It returns () on success and raises an exception on failure.

exception UnificationError of string

let rec unify t1 t2 =
  match (t1, t2) with
  | TInt, TInt -> ()
  | TVar v1, TVar v2 when v1.id = v2.id -> ()
  | TVar v, t | t, TVar v ->
      begin match v.binding with
      | Some t' -> unify t' t
      | None ->
          if occurs_check v t then
            raise (UnificationError "occurs check failed")
          else
            v.binding := Some t
      end
  | TFun (a1, r1), TFun (a2, r2) ->
      unify a1 a2;
      unify r1 r2
  | _ -> raise (UnificationError (Printf.sprintf "cannot unify %s with %s" (show_typ t1) (show_typ t2)))

Note the occurs_check before binding a variable to a type. That’s crucial: we must ensure we don’t produce an infinite type like 'a = 'a -> 'a. We’ll implement it:

let occurs_check var typ =
  let rec occurs = function
    | TVar v -> if v.id = var.id then true
                else match v.binding with Some t -> occurs t | None -> false
    | TFun (a, r) -> occurs a || occurs r
    | TInt -> false
  in
  occurs typ

Now we can write the main infer function. It takes an environment (env : (string, scheme) Hashtbl.t or a list; we’ll use a list of bindings for simplicity) and an expression, and returns a type.

But we must handle the environment carefully. We’ll define a type for environment entries that can be either monomorphic or polymorphic:

type env_entry =
  | Mono of typ              (* a monomorphic type (e.g., lambda param) *)
  | Poly of string list * typ  (* quantified var IDs and body type *)

However, to keep the implementation clean, we’ll use the standard approach: represent the environment as a list of (string, scheme) pairs where scheme is either a simple type (monomorphic) or a scheme with quantified variables. We’ll use a single type scheme that can represent both:

type scheme =
  | Mono of typ
  | Poly of int list * typ

But that’s messy for generalization. A cleaner method is to use the prune function: after inferring an expression, we collect all free type variables in the resulting type and in the environment, and generalize those that are free in the result but not in the environment. To do that, we need to “flatten” any mutable bindings first. The standard technique is to create a substitution that replaces all type variables with fresh ones after resolving bindings, but that’s overkill for a tutorial. Instead, we can use the occurs-free set approach: we collect all type variable IDs that appear in the type (after following bindings) and subtract those appearing in the environment. Then we create a Poly with those IDs.

But implementing generalization with mutable variables is tricky because we must “freeze” the type. In many textbook implementations, they use immutable variables and explicit substitutions. For this blog, we’ll adopt a simpler, executable approach: we will not implement full let-polymorphism in the first pass; instead, we’ll implement monomorphic inference first, then extend it.

Let’s first implement a monomorphic type checker (lambda calculus without let). That will give us unification practice. Then we’ll add let and polymorphism.

Monomorphic Type Inference

We’ll define a type context as a list of (string, typ) pairs (no schemes yet). The inference function will be:

let rec infer env = function
  | Int _ -> TInt
  | Var x ->
      (try List.assoc x env
       with Not_found -> raise (InferError ("unbound variable " ^ x)))
  | Lam (x, e) ->
      let a = fresh_var () in
      let body_typ = infer ((x, a) :: env) e in
      TFun (a, body_typ)
  | App (e1, e2) ->
      let t1 = infer env e1 in
      let t2 = infer env e2 in
      let result = fresh_var () in
      unify t1 (TFun (t2, result));
      result
  | Let _ -> failwith "let not implemented yet"

Notice that in the lambda case, we don’t unify a with anything—it remains a free variable until the function is applied. If the lambda is used polymorphically, we’d need to instantiate, but here we treat the lambda body’s type as fixed: any application will unify the parameter type. This is fine for a monomorphic language.

Let’s test with a simple expression:

(* fun x -> x  *)
infer [] (Lam ("x", Var "x"))

This returns TFun(TVar {id="i66d27b4" binding=None}, TVar {id="i66d27b4" binding=None}) which looks like 'a -> 'a. That’s correct, but note that the two TVar share the same ID, so they are the same variable. Indeed, the inference correctly deduces that the parameter type and the return type are identical.

Now test application:

(* (fun x -> x) 42 *)
infer [] (App (Lam ("x", Var "x"), Int 42))

The lambda gives 'a -> 'a. The integer gives int. Unifying 'a -> 'a with int -> result unifies 'a with int and then 'a with result, so result = int. Final type: int. Perfect.

What about a mismatched application:

(* (fun x -> x) (fun y -> y) *)
infer [] (App (Lam ("x", Var "x"), Lam ("y", Var "y")))

The lambda body of the inner lambda is its own parameter; the inner lambda type is 'b -> 'b. The outer lambda unifies 'a with 'b -> 'b, so result is 'b -> 'b. Final type: 'b -> 'b. Works.

Now try something that should fail:

(* (fun x -> x) (fun y -> y) (fun z -> z)  *)
infer [] (App (App (Lam ("x", Var "x"), Lam ("y", Var "y")), Lam ("z", Var "z")))

The first application gives 'b -> 'b. The second application unifies 'b -> 'b with 'c -> result where 'c is the type of the third lambda ('d -> 'd). This unification will require 'b to equal 'd -> 'd, so 'b becomes 'd -> 'd. Then result = 'b = 'd -> 'd. So the final type is 'd -> 'd. That’s legal: the expression is the identity function applied to an identity function and then to another identity function. It’s well-typed.

But what about (fun x -> x x)? That’s self-application. In our monomorphic system:

(* fun x -> x x *)
infer [] (Lam ("x", App (Var "x", Var "x")))

Let’s step through:

• Lambda: fresh var 'a for x, infer body.
• Body: App(Var "x", Var "x"). Infer Var "x" gives 'a. Then second Var "x" also gives 'a. So we unify 'a with TFun('a, result). That is, 'a = 'a -> result.

This is exactly the case where the occurs check must fire. Indeed, the body type will attempt to unify 'a with a type containing 'a. Our unification function will call occurs_check and raise an error. So the expression fun x -> x x is rejected, as it should be in a simply typed lambda calculus (without recursive types). In ML, such an expression is not typeable because it would require a type 'a = 'a -> 'b, which is an infinite type. Hindley-Milner’s type system disallows this, preventing the Y combinator and thus ensuring strong normalization for the simply typed part.

That’s the occurs check doing its job. But wait: in real ML, you can write let rec f x = f x to achieve recursion, but that’s a special fixpoint combinator allowed via let rec (which introduces a recursive type). Our core language without let rec is non-recursive.

Now let’s add let to support polymorphism.

Adding Let-Polymorphism

The real power of HM inference comes from let expressions. Without let, lambda-bound variables are monomorphic, meaning you cannot write:

let id = fun x -> x in (id 5, id true)

Because the first use of id would unify its parameter type with int, and the second would try to unify with bool, causing a unification error. But ML allows this because let introduces a polymorphic scheme.

Generalization

When we infer the type of e1 in let x = e1 in e2, we need to generalize over all type variables that are not free in the current environment. But because our type variables are mutable, we must be careful: we need to “prune” the type by following all mutable bindings until we reach either a TInt or a TVar with no binding. Then we collect the IDs of all free variables in that pruned type. Then we create a scheme with those IDs. When we later look up x in the body, we instantiate the scheme by creating fresh type variables for every quantified ID.

This process requires us to traverse the type graph, which is possible. But to keep the implementation simple, we can adopt an alternative approach: use the let-generalization algorithm that works by first computing the set of free type variables in the inferred type, then the set of free type variables in the environment, and generalizing the difference. However, computing free variables of a mutable type requires following bindings.

Let’s write a helper prune : typ -> typ that returns a “canonical” type where all mutable bindings have been followed to their deepest resolved type (or to a variable with no binding). For example, if a variable 'a is bound to int, then prune (TVar 'a') returns TInt. If 'a is bound to 'b and 'b is bound to int, prune returns int. If there’s a cycle? That would have been caught by occurs check. So prune is safe.

let rec prune = function
  | TVar v ->
      begin match v.binding with
      | None -> TVar v
      | Some t -> let p = prune t in v.binding <- Some p; p
      end
  | t -> t

We also need a function free_vars : typ -> int list that returns the IDs of all type variables (after pruning). Because prune follows bindings, any remaining TVar in the result is a variable with no binding.

let rec free_vars = function
  | TVar v -> [v.id]
  | TFun (a, r) -> free_vars a @ free_vars r
  | TInt -> []

Now, to generalize a type t relative to an environment env, we compute free_vars t and free_vars_env env (union of free vars of all types in env). Then the quantified IDs are set_diff (free_vars t) (free_vars_env env). The scheme becomes Poly (quantified_ids, t). But note: the type t may still contain mutable bindings inside? We should prune before computing free vars.

But here’s a subtlety: the environment may contain types that themselves have mutable bindings. We need to prune those too. Also, the environment’s types are already “resolved” as much as possible from inference. So we should prune the whole environment’s types before computing free vars.

Let’s define:

let free_vars_env env =
  List.fold_left (fun acc (_, scheme) ->
    let typ = match scheme with Mono t | Poly(_, t) -> t in
    let pruned = prune typ in
    let fv = free_vars pruned in
    List.fold_left (fun set id -> if List.mem id set then set else id :: set) acc fv
  ) [] env

Now we can implement the infer function with let-polymorphism:

let rec infer env = function
  | Int _ -> TInt
  | Var x ->
      (try
        match List.assoc x env with
        | Mono t -> t
        | Poly (ids, t) -> instantiate ids t
       with Not_found -> raise (InferError ("unbound variable " ^ x)))
  | Lam (x, e) ->
      let a = fresh_var () in
      let body_typ = infer ((x, Mono a) :: env) e in
      TFun (a, body_typ)
  | App (e1, e2) ->
      let t1 = infer env e1 in
      let t2 = infer env e2 in
      let result = fresh_var () in
      unify t1 (TFun (t2, result));
      result
  | Let (x, e1, e2) ->
      let t1 = infer env e1 in
      let pruned_t1 = prune t1 in
      let fv_t1 = free_vars pruned_t1 in
      let fv_env = free_vars_env env in
      let quantified = List.filter (fun id -> not (List.mem id fv_env)) fv_t1 in
      let scheme = Poly (quantified, pruned_t1) in
      infer ((x, scheme) :: env) e2

We need instantiate:

let instantiate ids t =
  let mapping = Hashtbl.create 10 in
  List.iter (fun id -> Hashtbl.add mapping id (fresh_var ())) ids;
  let rec inst = function
    | TVar v ->
        (try Hashtbl.find mapping v.id with Not_found -> TVar v)
    | TFun (a, r) -> TFun (inst a, inst r)
    | TInt -> TInt
  in
  inst t

But there’s a subtlety: the t in Poly may still contain mutable bindings inside because we pruned it before creating the scheme. However, the scheme’s type is a pruned copy; it’s still sharing the same mutable variable objects? When we pruned, we updated v.binding to point to the pruned result, but the original variable might still be bound to something. Actually, prune as defined modifies the original variable’s binding to point to the pruned result. That’s okay—it effectively “collapses” the bindings. The type returned by prune is the same structure but with bindings resolved. So the scheme stores a type that may contain TVar with binding = None (if they were never unified) or shared with others. However, when we later instantiate, we need to create fresh variables for the quantified IDs, but those IDs might not appear as top-level variables because the type might be e.g., TFun(TVar{id="i6bb06ff" TVar{id="i25bb81c">—the same variable appears multiple times. Our instantiate uses a hashtable mapping old ID to fresh variable. It replaces all occurrences of that ID with the same fresh variable. That’s correct.

But we must ensure that when we prune, we don’t lose the connection between the quantified variable and the type variable object. For example, if we have type 'a -> 'a where both occurrences are the same TVar object, the prune function returns TFun(TVar{id="ibfdf595" TVar{id="i937bcd3">. The IDs are the same. Then we compute free_vars and get [0]. Then we store in scheme Poly([0], ...). When we instantiate, we map id 0 to a fresh var, and replace both occurrences with that same fresh var, giving 'b -> 'b. Correct.

But what if the type contains a variable that is bound to another variable (like a chain)? Prune resolves it to the final variable, so we lose the chain. That’s fine.

Now let’s test the polymorphic let:

(* let id="iaf94c64" x -> x in (id 5, id true) *)
let expr =
  Let ("id",
    Lam ("x", Var "x"),
    App (App (Var "id", Int 5), App (Var "id", Bool true)))  (* but we don't have bool; we'll use int for both? Actually we need bool *)

(* Let's use a pair-like representation? No, we don't have pairs. Let's test with two numbers: (id 5, id 6) *)

Better test:

let expr =
  Let ("id",
    Lam ("x", Var "x"),
    App (Var "id", Int 5))  (* simple use *)

This should give int. Let’s mentally trace:

• Infer e1: Lam("x", Var "x"). Creates fresh 'a for x, body returns 'a. So type 'a -> 'a. Prune: still 'a -> 'a with TVar{id="icd0bae3" binding=None}. Free vars: [0]. Environment initially empty, so fv_env = []. Quantified = [0]. Scheme: Poly([0], TF(TVar{0}, TVar{0})).
• Now infer e2 with environment ("id", scheme). Variable id instantiates: create fresh var 'b for id 0. Replace both occurrences, gets 'b -> 'b. Application to Int 5 unifies 'b with int, so result int. Good.

Now test polymorphic use twice:

let expr =
  Let ("id", Lam ("x", Var "x"),
    Let ("apply", Lam ("f", Lam ("x", App (Var "f", Var "x"))),
      App (App (Var "apply", Var "id"), Int 5)))

This defines apply f x = f x, then applies it to id and 5. Should give int. The types should work.

What about the classic example: let f = fun x -> x in (f 1, f true)? Without booleans, we could simulate with two different integer types? Not possible. So we can’t test that directly. But we can test using a function that takes two different types:

(* let f = fun x -> x in let g = fun y -> (f y) in (g 1, g (fun z -> z)) *)
let expr =
  Let ("f", Lam ("x", Var "x"),
    Let ("g", Lam ("y", App (Var "f", Var "y")),
      App (App (Var "g", Int 1), Lam ("z", Var "z"))))

Let’s reason: f: 'a -> 'a. In g, f is used within g’s body; g is defined as fun y -> f y. When inferring g, we extend environment with "f" as polymorphic scheme. The body App(Var "f", Var "y") instantiates f each time? Actually, f appears once. The infer for Var "f" returns a fresh instantiated type, say 'b -> 'b. Then Var "y" returns type 'c (the fresh variable for y’s parameter). Then unification requires 'b -> 'b = 'c -> result, so 'b = 'c and result = 'b. So g gets type 'c -> 'c. That’s monomorphic: the type of g is 'c -> 'c. But wait: g is defined via a lambda, so it’s not polymorphic (lambda bindings are monomorphic). So later when we apply g to Int 1, 'c gets unified with int. Then we apply the result (which is int) to a lambda? No, the expression is (g 1, g (fun z -> z)) but we don’t have tuples; we used App (App (Var "g", Int 1), Lam ("z", Var "z")) which is actually g 1 applied to the lambda. That’s wrong. Let’s not overcomplicate.

Instead, test with a simple let-polymorphism that actually uses two different types:

(* let id="iaf94c64" x -> x in id id *)
infer [] (Let ("id", Lam ("x", Var "x"), App (Var "id", Var "id")))

This expression computes id applied to itself. In HM, id is polymorphic: forall 'a. 'a -> 'a. So id id is allowed: the outer id expects a type 'a -> 'a (since its argument is an id), and the inner id provides that. The result type is the same as the parameter type of the outer id, which is 'a -> 'a. So the whole expression type is 'a -> 'a. But note that this is the identity function again. Let’s verify with our inference:

• Infer e1: Lam("x", Var "x") => 'a -> 'a with TVar{0}. Scheme: Poly([0], ...).
• In e2, Var "id" appears twice. First occurrence instantiates to 'b -> 'b. Second occurrence also instantiates to 'c -> 'c (different fresh vars). Then application: unify 'b -> 'b with ('c -> 'c) -> result. So 'b must be 'c -> 'c, and result = 'b = 'c -> 'c. So final type is 'c -> 'c. Good: we get a fresh variable 'c, which is universally quantified? Since the overall expression is not inside a lambda, its top-level type will be generalized? Actually, our infer function returns a type, not a scheme. The user of the function can then generalize. So the output type has a free variable 'c. That’s okay.

Now, what about let id="iaf94c64" x -> x in id id id? That’s (id id) id. Should work similarly.

Our implementation seems plausible. Let’s run through the self-application again with let-polymorphism: let x = fun f -> f f in ...? That’s fun f -> f f is not polymorphic because it’s a lambda; inside the lambda, f is monomorphic, so f f fails occurs check. So the expression fun f -> f f is not typable, even though f could be instantiated? But in HM, lambda-bound variables are monomorphic, so indeed it fails. This is correct.

But what about let x = fun f -> f f in x id? The let body would try to use x as polymorphic; x’s type would be inferred as ?. Let’s see: fun f -> f f is a lambda; it fails occurs check, so the whole let expression fails. So that’s fine.

Thus, our type checker rejects all ill-typed programs and accepts all well-typed programs within the HM scope. We’ve built a working type inference engine!

The Occurs Check in Depth

Now that we have a working implementation, let’s zoom in on the occurs check. Why is it so important? Imagine we didn’t have it. Then the unification for 'a with 'a -> 'b would succeed by setting 'a.binding := Some (TFun (TVar 'a', TVar ...)), creating a cyclic structure. If we then try to print the type, we would get infinite recursion. More critically, this would allow expressions like fun x -> x x to be typed, with type 'a -> 'a where 'a is recursively defined as 'a -> 'b. This is essentially a recursive type, which breaks the normalization property and can lead to non-termination (e.g., the Y combinator would be expressible). In HM, we explicitly forbid such types to maintain soundness and termination of type checking.

The occurs check is a simple linear traversal that ensures a type variable does not appear inside the type we are about to bind it to. It does not need to be expensive; in the worst case it’s O(n) where n is the size of the type. But because types can be shared due to mutable variables, we must be careful not to double-count or miss cycles. Our implementation uses a recursive function that follows bindings. Since we always prune before unification? In our unification, we handle the case where a variable is already bound: we unify with its binding. That’s fine. The occurs check is called only when we are about to bind a variable to a type that is not itself (the TVar v, t case). We call occurs_check v t. The check traverses t, following bindings. But note: if t contains a binding to a different variable that might eventually lead back to v? That would be a cycle discovered through multiple steps, but our occurs_check only looks at the shallow representation of t (without following bindings? Actually, in the code above, occurs_check does follow bindings: when it sees TVar v2, it checks if v2.id="i8da6dd6" then true else match v2.binding with Some t -> occurs t | None -> false. That’s correct: it follows bindings to find any path to var. However, if there is a cycle of bindings (e.g., v1 bound to TFun(v2, something) and v2 bound to v1), this could lead to infinite recursion. But such cycles would have been created only if occurs check was omitted earlier. So in a well-behaved system, we never have cycles. Even if we did, our follows would eventually hit a previously visited variable? We don’t have visited tracking, so we could loop. To be safe, we could add a set of visited IDs. But in practice, as long as we only bind variables to types that have passed the occurs check, cycles cannot form. So our simple recursive version is safe.

Let’s examine an edge case: Suppose we have 'a bound to int. Then we try to unify 'a with 'b -> 'c. The unification sees TVar 'a with binding Some TInt. It calls unify TInt (TFun(TVar 'b', ...)), which fails with type mismatch. Good. No occurs check needed.

Now consider 'a bound to 'b (i.e., 'a.binding = Some (TVar 'b')). Then we unify 'a with TFun('c, 'd). The variable case expands to unify (TVar 'b') (TFun('c,'d)). Then 'b is unbound, so we do occurs check: occurs_check 'b (TFun('c,'d)). If 'c or 'd contain 'b, fails. Otherwise, we bind 'b to TFun('c,'d). That’s fine.

The occurs check ensures that the type graph remains a DAG, not a cyclic graph. This is essential for termination of the inference algorithm itself (since we may traverse types recursively during printing or further unification) and for the logical consistency of the type system.

Extensions and Limitations

Our MiniML type checker is fully functional for HM. However, real languages include many additional features that require extensions to the basic inference:

• Recursive types: let rec allows defining recursive functions. In ML, let rec f x = ... is allowed and requires the type of f to be available in its own definition. This is handled by first binding f to a fresh type variable in the environment, then inferring the body, then unifying. This may require a “fixpoint” approach but is straightforward.

• Mutual recursion: Similar to recursive types but with multiple definitions.

• Type annotations: Programmers can optionally annotate function arguments or results. These must be checked against inferred types.

• Algebraic data types (ADTs): Adding sum types, product types, and pattern matching requires extending the type grammar and unification. The occurs check still applies.

• Type classes (Haskell): This introduces constraints (e.g., Num a => a -> a). Inference becomes constraint-based, using a variant of HM called “qualified types”. Unification still works, but we also need to solve constraints.

• Higher-kinded types: Haskell’s type constructors of kind * -> * require a more sophisticated kind system. HM on its own doesn’t handle kind inference, but extensions like System Fω do.

• Dependent types: Languages like Coq and Agda blur the line between types and values, requiring full unification of terms, not just types. That’s a whole different ballgame.

Despite these extensions, the core of type inference in most functional languages still rests on the principles we’ve implemented: unification with an occurs check.

Conclusion

We’ve journeyed from a mysterious black box to a fully implemented type inference engine. We’ve seen how Hindley-Milner inference transforms expressions into equational constraints, solves them via unification, and uses the occurs check to prevent infinite types. You’ve built a tiny type checker that can handle lambda calculus with let-polymorphism.

Understanding this machinery gives you deep insight into the error messages your compiler produces. When you see “cannot unify int -> int with int”, you know exactly what the unifier is trying to do. When faced with an “occurs check” error (like in Haskell: “Occurs check: cannot construct the infinite type: a ~ a -> b”), you recognize that you’ve written an expression that would require a recursive type.

More importantly, this knowledge empowers you to design better languages and debug type errors more effectively. The next time you write let x = f y in ... and the compiler infers a type you didn’t expect, you can mentally trace the constraint generation and unification to find the source of the mismatch. The compiler is no longer a sorcerer; it’s an honest worker following a fixed set of logical rules.

I encourage you to extend this implementation. Add booleans, tuples, list types, pattern matching, or even type annotations. Implement a pretty-printer for types. Try to break the occurs check on purpose. Build a simple REPL that infers and prints types. There’s no better way to learn than to get your hands dirty with code.

And remember: every type error is a solved puzzle, waiting for you to apply the insights of unification and the never-failing vigilance of the occurs check.

Happy coding!