Well, one can imagine a smart enough language could perform some trivial mappings to reduce the zoo of potential function types: a -> b can be trivially mapped

Well, one can imagine a smart enough language could perform some trivial mappings to reduce the zoo of potential function types: a -> b can be trivially mapped to both (a -> eventually b) and (eventually a -> eventually b).