Function's case_return_of_ clashes with RawMonad's return

[gallais]

It is very unfortunate that as soon as you write open RawMonad m to be able to write
some monadic code, you get a parse error on case_return_of_.

I suggest changing the definition of RawIMonad to a RawIApplicative + _>>=_ and
to explicitly deprecate return in favour of pure.

[JacquesCarette]

return to pure makes perfect sense. Deduplification of definitions is often a good thing, so the other half of this seems like a good idea as well. But it could reduce usability in non-trivial ways... [nest record structures are a pain. Creating them in a modular way is nice, but the flattening them before offering them to users is a much nicer interface.]

[gallais]

flattening them before offering them to users is a much nicer interface

In the standard library we systematically open the module associated to a nested
record which means that all of its fields are brought in scope whenever someone
opens the enclosing module.

For instance IsPartialOrder opens IsPreorder.

Is that not sufficient?

[JacquesCarette]

Almost. For access, it is. For creation, AFAIK, you still have to use the nested structure. Or, at least, that's what ctrl-R always gives me.

[gallais]

Ah I see. I suppose we could also think about having smart constructors taking a
pure and a bind and generating the whole RawIMonad record given that the rest
can be derived automatically.

[MatthewDaggitt]

Ah I see. I suppose we could also think about having smart constructors taking a
pure and a bind and generating the whole RawIMonad record given that the rest
can be derived automatically.

That sounds reasonable. Now to come up with a good name...

[MatthewDaggitt]

In #2157 this was fixed by renaming case_return_of to case_returning_of.