These are important questions. I think there is a trade-off between supporting many cases and having a simple desugaring. We should find a sweet-spot where the desugaring is reasonably simple and covers most idiomatic cases.

So I guess it's possible to detect the pattern:

  do x1 <- foo1; ...; xN <- fooN; [res <-] return (f {x1..xN})

where {x1..xN} means "x1..xN" in some order"

Your third example shows that it's beneficial to also support duplicated variables.
 
and turn it into:

  do [res <-] (\x1..xN -> f {x1..xN}) <$> foo1 <*> ... <*> fooN

I think this is a reasonably simple rule and it covers most idiomatic cases.
 
Open issues would be detection of the correct "return"-like thing.  

I'm not sure how much return aliasing is worth supporting. In general it is undecidable but we could add special cases for specialized returns (like 'Just' instead of 'return') depending on how difficult it is to implement.
 
The current desugaring of do-notation is very simple because it doesn't even need to know about the monad laws.  

Could you point out which monad law your proposed desugaring requires?
 
They are used implicitly by the optimiser (e.g., "foo >>= \x -> return x" is optimised to just "foo" after inlining), but the desugarer doesn't need to know about them.

Does the inliner have RULES for monad laws or why would this work?

Sebastian