Yes, we have to walk a fine line here. The fact that do notation desugars to function calls in a complete deterministic way is nevertheless not easy to explain

Yes, we have to walk a fine line here. The fact that do notation desugars to function calls in a complete deterministic way is nevertheless not easy to explain to learners. It's a judgement call but overall its benefits outweigh the drawbacks--IMO.