# How do Coq's bidirectionality hints (&) affect type checking?

I have used Coq's bidirectionality hints (placement of & in a call to Arguments) to some effect, mostly by trial and error. Despite familiarity with bidirectional type checking, I can't connect the explanation given in the documentation with what I actually observe. So, precisely what change does & make to the checking of an application? To start, I understand the default bidirectional typing rule for applications to be, more or less (read clockwise, with ∈ denoting type synthesis and ≤ denoting subtyping (including unification)):

f ∈ ∀ (x1 : A1) ... (xn : An), B
M1 ∈ A1'    ...    Mn ∈ An'
A1' ≤ A1    ...    An′ ≤ An
----------------------------------
f M1 ... Mn ∈ B[M1/x1, ..., Mn/xn]


Some questions I'd like to be answered as corollaries of the explanation:

1. Is Arguments foo & x y. equivalent to Arguments foo x y.?
2. Is Arguments foo x y &. equivalent to Arguments foo x y.?
3. Is Arguments foo {x} & y. equivalent to Arguments foo & {x} y.?
4. What happens for partial applications (of Curried functions)?
5. Is the Arguments f ... & ... . mechanism reasonably complete for bidirectional typing strategies you may want/expect?