<div dir="ltr"><div dir="ltr">> What deeper lore am I not seeing here?</div><div dir="ltr"><br></div><div dir="ltr">The "deeper lore" you are looking for is:</div><div><ul><li>Type variables that look unbound are actually implicitly bound with a universal quantifier:</li><ul><li>"Maybe a" is actually "forall a. Maybe a";</li><li>"Either a b" is actually "forall a. forall b. Either a b", that is, "forall a. (forall b. Either a b)";</li><li>"Either a (Either b c)" is actually "forall a. forall b. forall c. Either a (Either b c)";</li><li>"a" is actually "forall a. a";</li><li>"f a" is actually "forall f. forall a. f a".</li></ul><li>alpha-equivalence: You can rename the bound variables of an expression without changing its meaning, as long as you don't change the bindings.</li><ul><li>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).</li></ul></ul></div><div dir="ltr"><div>Examples of alpha-equivalence (here "≡" reads "is alpha-equivalent to"):</div><div><br></div><div><font face="monospace">  forall a. forall b. Either a b</font></div><div><font face="monospace">≡ forall x. forall y. Either x y</font></div><div><font face="monospace">≡ forall b. forall a. Either b a</font></div><div><font face="monospace"><br></font></div><div><span style="font-family:monospace">  forall a. Either Bool a</span><font face="monospace"><br></font></div><div><span style="font-family:monospace">≡</span><span style="font-family:monospace"> forall b. Either Bool b</span></div></div></div>