[skew]

That's actually the only place ML^F ever requires type annotations - when you want to take a polymorphic function as argument and use it at different types. MLF is basically as strong as inference for polymorphic types gets, so it's not surprising annotations might be needed here too. (intersection types handle the example nicely, but I don't know of any languages using them).

If you want to faithfully translate the idea that 5 and "Test" are different values that can be passed into the same places but told apart by tests if you want, you might translate the second line to something like f (\x -> x) (Left 5) (Right "Test"), which does pass.