Type variables versus unification variables

I've always gotten the sense that GHC is a little bit fast-and-loose about this, especially as polymorphic types can be inferred, whereby unification variables become type variables due to an implicit quantifier.

I am not sure exactly what I want different, especially implementation wise, but this just makes me feel like GHC is gaslighting me by virtue of me being unable to describe what the alternative looks like!

@xplat one remarked the same thing, after which a wave of relief and validation swept over me. Maybe he can describe the problem and potential solutions more eloquently.