If there is one piece of advice about type inference I think everyone should hear it's absolutely this

Be very explicit about the difference between type variables, unification variables and skolems

Type variables are always bound by foralls and represent variables that can be instantiated to any possible concrete type. For example, forall a. a -> a can be instantiated to Int -> Int, String -> String or Bool -> Bool

Unification variables are placeholders that stand for as of yet unknown concrete types. These usually originate from usages of polymorphic types (where type variables are instantiated with fresh(!!!) unification variables at every use site, since every use site instantiates the type variable to a possibly different concrete type, but which one that is might not be known yet), but they are more generally useful in places where a type is needed that might not be fully known yet (e.g. unannotated lambda parameters or recursive let bindings)

Skolems on the other hand are type constants that are only equal to themselves. These are needed when checking against polymorphic types. The idea is that a function with type forall a. a -> a cannot make any assumptions about the type of its parameter, which is ensured by checking it against the type #a -> #a (where #a is a fresh skolem).

These three are often confused since they could all reasonably be called “type variables”, but doing so will only bring you pain. They are distinct concepts and should really be treated as such.

Unfortunately GHC is not great at this. In error messages, unification variables are usually displayed with a trailing number (a0), although something like a1 can either be a unification variable or a skolem if just a would be ambiguous. The only way to tell which one it is is by looking for 'a1' is a rigid type variable bound by... (you know, in the section of the error that noone actually reads because it’s massive and almost never useful)