Boxy types: inference for higher-rank types and impredicativity