Great example, it now clicks. We lifted b all the way up because it needs to be consumed by the caller, might as well lift a as well, as types with free variabl

Great example, it now clicks. We lifted b all the way up because it needs to be consumed by the caller, might as well lift a as well, as types with free variables, like b in "forall a.a -> b", are useless. Which looks a lot like let-polymorphism :)