[kragen]

Thank you for explaining!

To clarify, when I wrote α, I always and only meant a bound variable under a quantifier, because I didn't know about this metavariable thing at all. I was writing α → α because that's how tuareg-font-lock-symbols renders 'a -> 'a, which does include the implicit quantifier.

It's no wonder I was never able to understand HM since I didn't know about this dual nature of variables. This will probably help me a lot next time I try to understand it! I do think I understand unification, though I've only implemented it once.

I really appreciate you being willing to engage on HN, despite the unpleasant aggressiveness and character assassination that runs rampant here.