What deeper lore am I not seeing here?
The "deeper lore" you are looking for is: - Type variables that look unbound are actually implicitly bound with a universal quantifier: - "Maybe a" is actually "forall a. Maybe a"; - "Either a b" is actually "forall a. forall b. Either a b", that is, "forall a. (forall b. Either a b)"; - "Either a (Either b c)" is actually "forall a. forall b. forall c. Either a (Either b c)"; - "a" is actually "forall a. a"; - "f a" is actually "forall f. forall a. f a". - alpha-equivalence: You can rename the bound variables of an expression without changing its meaning, as long as you don't change the bindings. - Example of changing the bindings: "forall x. forall y. x" (x is bound by the first/outer quantifier) is not alpha-equivalent to "forall y. forall x. x" (x is bound by the second/inner quantifier). Examples of alpha-equivalence (here "≡" reads "is alpha-equivalent to"): forall a. forall b. Either a b ≡ forall x. forall y. Either x y ≡ forall b. forall a. Either b a forall a. Either Bool a ≡ forall b. Either Bool b