Improve MonadFail docs - isn't 'fail s' always a left zero?

[tomjaguarpaw]

The MonadFail docs say that fail s must be a "left zero", i.e.

fail s >>= f  =  fail s

But given that fail s :: forall a. m a is there any way that it couldn't be a left zero?

[kindaro]

How do you even begin to prove this?

1. fail s cannot contain any values of an arbitrary type a.
2. Therefore, f can never be invoked by >>=.
3. Since f cannot be invoked, >>= must behave the same way for any f.
4. Take f be pure — by a law of monad >>= pure ≡ id. Therefore, by №3 >>= f ≡ id for any f.
5. id (fail s) ≡ fail s. ∎

— Maybe like this.

But this all on the assumption that everything is defined. Is this an admissible assumption? Otherwise, we can consider situations where >>= invokes f with undefined — then f can either crash (≢ fail s) or return an arbitrary value (≢ fail s).

[tomjaguarpaw]

Apparently you can prove it by parametricity. See https://www.reddit.com/r/haskell/comments/u5k4gv/is_it_possible_for_fail_s_not_to_be_a_left_zero/.