Overlapping monadic typeclass assumptions

Stream: lean4

[Eric Wieser]

It looks to me like most of https://loogle.lean-lang.org/?q=Monad+%3Fm+%E2%86%92+Alternative+%3Fm+%E2%86%92+_ are bad, as by assuming Monad and Alternative they assume two separate pure operators. Should these be corrected to use docs#AlternativeMonad (which would need upstreaming)?

[Eric Wieser]

(cc @Devon Tuma in reference to #lean4 > Functor.map instance with `Alternative` @ 💬 )

[Robin Arnez]

I think this shouldn't be a problem since when there is an AlternativeMonad instance, then the pure operations (or more specifically, the Applicative instance) will coincide and if not then you may still use it for programming but maybe just won't prove many things about them

[Eric Wieser]

Are you saying that things are fine as is, or just that the problem is mostly benign?

[Robin Arnez]

Probably fine yeah it seems to me that a change would likely only make the instances less general albeit more correct. If you have a concrete example of something breaking I'd be willing to change my mind though