Follow substitutions, structural decomposition, conflicts, and the occurs check.
By the end: explain each unification step and recognize when a partial substitution is not a solution.
To unify a with Int, bind a to Int and substitute that binding wherever a occurs in the remaining problem. To unify two function types, equate their inputs and equate their outputs. Constructor names and arities must agree before component equations can solve the whole problem.
The problem (a -> b) = (Int -> Bool) decomposes into a = Int and b = Bool. A chain a = b, b = Int resolves both names to Int. Our display follows substitutions to their resolved form rather than showing a misleading unresolved chain.
A substitution is a consistent replacement of type variables by type trees. It is different from assigning a runtime value to a program variable. In the paper notation used here, a := Int means replace the type unknown a with Int wherever that unknown occurs. The player selects already authored equations; it does not parse these written examples. A solution must make both sides of every original equation the same finite tree. Solving one equation is useful progress, but the other equations can still rule out that replacement.
Consider the paper equation Pair<a, Fn<a, b>> = Pair<Int, Fn<Int, Bool>>. Fn names the function constructor; its first child is the input type and its second child is the output type. Matching the outer Pair constructors gives a = Int and Fn<a, b> = Fn<Int, Bool>. The second equation then gives another a = Int and b = Bool. Both occurrences of a receive the same replacement. After substitution, each original side is Pair<Int, Fn<Int, Bool>>. Checking the original equation confirms more than merely seeing two names in a bindings list.
Contrast that with Pair<a, Fn<a, b>> = Pair<Int, Fn<Bool, Bool>>. The first component still requires a = Int. The function inputs now require a = Bool, so the earlier binding changes that obligation into Int = Bool. No replacement for b can repair the different input constructors. The failure concerns a shared unknown in two positions, not an inherent problem with functions inside pairs. If the second occurrence had been a different unknown c, the independent choices a = Int, c = Bool, and b = Bool would satisfy the equation.
A constructor is a named way to build a type from component types. Int and Bool have no children here. Fn and Pair each have two ordered children. Decomposition is justified because equal trees with the same constructor must have equal corresponding children. Fn<Int, Bool> and Fn<Bool, Int> do not become equal by exchanging children. Function inputs and outputs have different roles, just as the first and second fields of an ordered pair do. Neither function application nor pair construction changes this structural equality rule into a directional compatibility test.
Replacement must also reach inside types already associated with other variables. Suppose a is bound to Fn<b, b>, and a later equation binds b to Int. Resolving a now gives Fn<Int, Int>. Stopping after one lookup would leave b visible and conceal information already established by the equations. This is substitution composition: later replacements act inside the result of earlier ones. The lesson display follows these chains to their resolved types. The underlying bookkeeping can retain a link to b without changing what the fully resolved type means.
| Stage | Resolved a | Remaining equation |
|---|---|---|
| Before binding | a | a = Fn<b, b>; b = Int |
| Bind a | Fn<b, b> | b = Int |
| Bind b | Fn<Int, Int> | None |
| Original equations checked | Fn<Int, Int> = Fn<Int, Int> | Int = Int |
One way to verify a proposed solution independently is to copy each original equation, replace all occurrences consistently, and compare constructors down to their leaves. For a = b followed by b = Int, the resolved substitution makes both original equations Int = Int. Replacing only the a in the first equation would not check the second obligation at all. This method also detects an overconfident report after failure. A map containing a := Int cannot solve the conflicting pair equation if its second component still requires that very same a to be Bool.
Int = Bool is a constructor conflict in this language. No coercion or subtype search repairs it. For a = (a -> Int), binding a would require a finite type containing itself as a proper part. The occurs check rejects this equation.
First check equality: a = a adds no information and succeeds. It must not be rejected simply because a appears on both sides. Recursive type systems can deliberately represent recursive structures, but that needs different semantics and rules; bypassing this occurs check is not a safe implementation of them.
The occurs check asks whether an unknown appears inside the type proposed as its replacement. A proper part of a tree means a child, a grandchild, or any deeper descendant, rather than the complete tree itself. An equation such as a = Fn<a, Int> would make a equal to a tree that contains a as a proper part. Our types must be finite constructor trees. The issue is therefore structural, even before considering whether a program using that equation would run. This engine has no separate notation for recursive types.
To see the obstruction, temporarily suppose a finite tree A satisfies A = Fn<A, Int>. Count all constructor and variable nodes in A and call that number n. The right side contains one Fn node, all n nodes of A, and one Int node. It therefore has n + 2 nodes. Equal finite trees must have equal node counts, but n cannot equal n + 2. This argument uses counts rather than a drawing's apparent size. Repeatedly expanding a only produces a longer unfinished tree, never a finite solution.
| Proposed equality | Left node count | Right node count | Consequence |
|---|---|---|---|
| A = A | n | n | Equal without expansion |
| A = Fn<A, Int> | n | n + 2 | Impossible for finite n |
| A = Pair<Bool, A> | n | n + 2 | The same obstruction |
The identical equation a = a needs no expansion at all. Every permitted replacement already makes its two sides equal. The solver therefore checks equality before looking for forbidden self-containment. If an implementation rejected every equation in which a variable appears on both sides, it would reject this harmless case. The distinction is between equality to oneself and equality to a larger type containing oneself. Pair<a, Int> = Pair<a, Int> likewise needs no new binding. Recognizing already equal structures avoids inventing work that supplies no additional information about the unknowns.
Self-containment can become visible only after another replacement. Consider the paper equations a = b and b = Pair<a, Int>. After identifying a with b, the second obligation resolves to b = Pair<b, Int>. Looking only at the unreplaced second equation would miss the connection between its two variable names. The solver applies known substitutions before choosing an action, so its occurs check inspects the current resolved types. Reversing the order exposes the same obstruction through a different sequence. Neither ordering makes a finite tree containing itself into a valid solution.
Self application supplies an expression-level source of this pattern. In the written term fun x -> x(x), give the parameter unknown a. Both uses of x look up that same parameter binding. Applying the first x to the second requires a = Fn<a, b>, where b is a fresh result unknown. No rule says b must be Int; the occurs failure already follows from the input position containing a. The actual Self application preset uses this authored tree. It fails inference before the interface invokes its independent interpreter.
| Step | a = b first | b = Pair<a, Int> first |
|---|---|---|
| Initial binding | a := b | b := Pair<a, Int> |
| Next equation resolved | b = Pair<b, Int> | a = Pair<a, Int> |
| Occurrence tested | b occurs inside Pair<b, Int> | a occurs inside Pair<a, Int> |
| Outcome | Occurs failure | Occurs failure |
A language with explicit recursive types can describe some self-referential structures using different rules for constructing and comparing types. That does not justify deleting this engine's occurs check. Its display, substitution expansion, and equality rules assume finite trees, and blindly following a cyclic replacement would not create the missing semantics. There is also a separate practical boundary: an acyclic tree can exceed an implementation budget. An expansion-limit error says the bounded process stopped. It does not establish the same logical contradiction as the node-count argument for a = Fn<a, Int>.
Final result: Constraints solved
(a → b) = (Int → Bool)(a → b) = (Int → Bool). Same function typeStep 0 of 3. Start these constraints.
No bindings yet| Step | Action | Pending | Bindings |
|---|---|---|---|
| 0 | Start these constraints | (a → b) = (Int → Bool). Same function type | None |
| 1 | Decompose Fn into corresponding components | a = Int. Same function type; b = Bool. Same function type | None |
| 2 | Bind a to Int | b = Bool. Same function type | a := Int |
| 3 | Bind b to Bool | None | a := Int; b := Bool |
| Equation | Action |
|---|---|
| a = a | Discard as already equal |
| a = Int | Bind a |
| Fn<a,b> = Fn<Int,Bool> | Decompose components |
| a = Fn<a,Int> | Reject by occurs check |
The player above has five named scenarios rather than an equation editor. Choose Function components and compare Original constraints with Current pending equations. The original function equality stays fixed while decomposition replaces one obligation with its input and output equations. Step forward once to see a = Int and b = Bool pending. After the next binding, the remaining obligation is b = Bool. After the last binding, none remain and the final result reports success. The disappearance of an equation means the action accounted for it, not that the original requirement ceased to matter.
Now select Conflicting pair, which replaces the scenario and resets the player. Its outer Pair equality decomposes into a = Int and a = Bool. Binding a to Int changes the displayed second obligation to Int = Bool. The next action reports a constructor conflict. Importantly, that final frame can have no pending equations because the solver removed the current equation before attempting it. An empty queue therefore occurs in both a successful run and this failed run. Read the action and final result together; the pending count alone omits the outcome of the last attempted obligation.
| Evidence | Function components | Conflicting pair |
|---|---|---|
| Original requirement | Fn<a, b> = Fn<Int, Bool> | Pair<a, a> = Pair<Int, Bool> |
| Last action | Bind b to Bool | Constructor conflict: Int versus Bool |
| Pending equations | None | None |
| Bindings retained | a := Int; b := Bool | a := Int |
| Final result | Constraints solved | No solution |
The complete unification trace records the same information without requiring playback. It is especially useful for comparing a binding with the equations that existed before it. In the failed pair scenario, a := Int remains in the bindings display because it explains how the conflict arose. It is diagnostic state, meaning information about the attempted computation. It is not a usable solution for the original equation. Returning that map as a successful type result would confuse a locally valid replacement with a globally consistent answer and erase the remaining Bool requirement.
Substitution chain isolates replacement propagation without any constructor conflict. At the start, a = b does not identify either variable as an integer. After binding a to b, the remaining equation b = Int supplies that missing fact. The resolved display then reports Int for both names. Already identical isolates a different action. Its equation a = a disappears without adding a binding. These scenarios distinguish learning a concrete constructor, sharing an unknown, and discovering no new information. All three can reduce pending work, but they carry different evidence about what types remain possible.
Use Occurs check to contrast the final action with Conflicting pair. The former rejects an attempt to contain the same variable inside its own finite replacement. The latter reaches two distinct fixed constructors. Both have no solution under these rules, but their explanations identify different structural causes. Reset keeps whichever scenario is selected and returns its playback to the starting state. Selecting a different preset replaces the equations and remounts the player. Neither operation changes the equality rules, and the speed control changes teaching-step duration rather than the amount of solver work required.
| Evidence | Conflicting pair | Occurs check |
|---|---|---|
| Original equation | Pair<a, a> = Pair<Int, Bool> | a = Fn<a, Int> |
| Obstruction | Int and Bool constructors differ | Replacement contains a |
| Useful partial binding | a := Int explains the conflict | No valid binding for a |
| Conclusion | No finite unifier | No finite unifier |
For a paper variation, change the conflicting target to Pair<Int, Int>. Decomposition would still produce two equations about the same a. The first would bind a to Int, and the second would become Int = Int and require no additional binding. Compare that with Pair<a, b> = Pair<Int, Bool>, where two independent variables can take different replacements. These variations are not extra player controls. They explain why repeated occurrence itself is legal: the failure depends on incompatible demands on that occurrence. The original presets let you observe each of the necessary actions separately.
A most general unifier satisfies the equations without unnecessary specialization. Solving a = b may leave a shared unknown rather than guessing Int. More specific solutions can then instantiate that unknown. Generality refers to this constraint language, not every feature of a production language.
A failed run may have bound some variables before discovering a conflict. Those bindings are diagnostic state, not a valid solution of the original set. The complete trace stays available without animation. Playback time measures teaching steps, not algorithm performance.
Most general describes the information a solution commits to. For the equation a = b, identifying the two unknowns satisfies the requirement while leaving their common type unspecified. Choosing Int for both also satisfies it, but adds a choice the equation did not demand. A more specific solution is an instance of a general one if further consistent replacements produce it. Thus the shared unknown can later become Int, Bool, or a whole function type. Generality is about preserving these possibilities, not about printing the greatest number of constructor names in a result.
Consider the paper equation Fn<a, b> = Fn<c, Pair<c, c>>. Decomposition requires a = c and b = Pair<c, c>. Neither requirement fixes c. The remaining family has a shared c in the function input and both positions of its pair output. Choosing c := Bool gives Fn<Bool, Pair<Bool, Bool>> on both sides. Choosing c := Fn<Int, Int> also works, with that whole function type repeated in all three positions. Choosing b := Pair<Int, Bool> cannot work because one consistent replacement for c cannot produce two different component constructors.
| Replacement for c | Instance of Fn<c, Pair<c, c>> | Valid? |
|---|---|---|
| Int | Fn<Int, Pair<Int, Int>> | Yes |
| Bool | Fn<Bool, Pair<Bool, Bool>> | Yes |
| Fn<Int, Int> | Fn<Fn<Int, Int>, Pair<Fn<Int, Int>, Fn<Int, Int>>> | Yes |
| No consistent choice | Fn<Int, Pair<Int, Bool>> | No |
Variable names and binding orientation can disguise equivalent generality. A solver may represent a = b by a := b, while another uses b := a. Both preserve one shared unknown. Renaming that unknown consistently does not alter the equality relation. By contrast, replacing one occurrence but not another changes the type itself. Compare Fn<c, Pair<c, c>> with Fn<c, Pair<c, d>>. The second admits pairs whose second component has an unrelated type. A display that ignores repeated-variable identity would incorrectly treat these as the same family because their outer constructors match.
Check satisfaction and generality separately. Applying a valid substitution must satisfy every original equation. For a most general unifier, every other solution must also be obtainable by further consistent replacements. This excludes both unnecessary constructors and unnecessary equality between independent unknowns. For the paper equation Fn<a, b> = Fn<c, d>, a := c and b := d leaves input and output independent. Further setting d := c still satisfies the equation without choosing a constructor, but excludes an Int input with Bool output. The extra equality therefore loses generality. Choosing Int for both sides of a = b loses generality in a different way. These checks concern the finite equality language, not a promise about directional subtyping, overload resolution, or every other process called constraint solving.
The finite implementation also distinguishes impossibility from exhausted resources. It accepts at most 64 starting equations in a solver batch, validates starting type trees against node and depth bounds, and limits solving and replacement expansion. A larger valid equation system might stop at a budget without containing either a constructor conflict or a self-containing type. The inference engine uses incremental batches, so the batch limit is not a claim that an entire expression can generate at most 64 recorded equalities. Resource accounting and mathematical satisfiability answer different questions and need different diagnostics.
| Original equation | Proposed resolved substitution | Satisfies all equations? | Avoids needless specialization? |
|---|---|---|---|
| a = b | a := b | Yes | Yes |
| a = b | a := Int; b := Int | Yes | No |
| Pair<a, a> = Pair<Int, Bool> | a := Int | No | Not a solution |
| Fn<a, b> = Fn<c, d> | a := c; b := d | Yes | Yes |
| Fn<a, b> = Fn<c, d> | a := c; b := c; d := c | Yes | No |
The transferable method is to preserve unknown relationships until a rule supplies more information, then verify replacements against the original obligations. In a larger paper example, start with the outer constructors, compare ordered components, and carry every established replacement into later equations. If a conflict appears, identify the two demands that became incompatible rather than treating the last binding as the whole explanation. If the process succeeds with unknowns remaining, that can be the desired general answer. The next lesson uses precisely this combination to reconstruct a type from an expression instead of starting with equations already supplied.
Solve Pair<a, a> = Pair<Int, Bool>. Why is the first successful binding insufficient?
Both component equations share the same a.
| Step | Remaining obligation |
|---|---|
| Decompose | a = Int; a = Bool |
| Bind a to Int | Int = Bool |
| Conflict | No unifier |
Decompose into a = Int and a = Bool. Binding a to Int makes the second equation Int = Bool, which fails. The partial binding does not solve the original pair equality. Both occurrences must agree simultaneously.
For a = b, is a := Int and b := Int a solution? Is it the most general one?
Compare it with identifying a and b without choosing a constructor.
| Substitution | Solves equation? | Unnecessary specialization? |
|---|---|---|
| a := b | Yes | No |
| a := Int; b := Int | Yes | Yes |
| a := Bool; b := Bool | Yes | Yes |
It is a solution but is more specific than necessary. A most general solution identifies a with b and leaves the shared type unconstrained. Choosing Bool for both is also possible later. Inferring Int without evidence discards valid instances.
Selected reference passages support the definitions and algorithms below. The examples, explanations, and implementations are original. Terminology and assumptions are stated within each lesson; source review is not an independent audit of this course. Optional links are not runtime dependencies.
Selected constraint generation, unification, principal-type, and let-polymorphism passages. The lesson uses its own bounded tree-based engine, not a complete OCaml implementation.