What the machine annotates and what the programmer wants to read are two very different things, for we often condense some long, confusing type signatures into things we can talk about - for example, a lens.
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
If we want to compose several of these, for example, with our regular function composition operator, then we check the resulting type - it's not what you really want to see.
fun l1 l2 = l1 . l2
:t fun
The signature given is less than helpful - if you manage to parse it you'll probably have forgot what you were tying to do next. When all we really wanted was a signature like
Lens' b y -> Lens' a b -> Lens' a y
Making the machine pick the "right" representation is probably a futile task - there could be any number of ambiguous representations of the same type, but the only meaningful one is the one the original programmer intended.
