Inference means working out a type nobody wrote down, so you need a way to stand for an unknown type. Today you add the type variable and a supply of fresh ones - the placeholder the whole inference engine reasons about.
Represent a type variable, generate fresh ones, and compare and print them.
Every rule so far read a type off something already known: a literal, an annotation, an environment entry. Inference is the opposite move - you meet an expression whose type nobody stated, and you have to discover it. The tool that makes this possible is the type variable: a stand-in, “some type I do not know yet”, that you can carry around and later pin down. A lambda with no annotation gets a fresh variable for its parameter; unification then fills it in from how the parameter is used.
The only requirements today are that each variable is distinct and that you can
tell two apart, so a variable is just a unique id. A small fresh supply hands out
a new one each time, and Equal treats two variables as the same exactly when their
ids match. Printing them as letters - a, b, c - is a nicety that pays off at
the end, when the checker shows a polymorphic type like a -> a back to the reader.
This placeholder is the single idea the entire inference core is built on.
// a type variable stands for an unknown type, tagged by a unique id.type TVar struct{ Id int }var counter intfunc fresh() TVar { t := TVar{counter}; counter++; return t }// Equal: two variables match iff same Id.// String: print id 0 as "a", 1 as "b", ... (rune 'a'+Id).