`pass` does nothing in instances of `MonadWriter` for `stateT` and `eitherT`

[bamarsha]

pass can be used to suppress the output of a writer computation by mapping the output to the empty list:

Example writer_pass_applies_function_to_log :
  let m : writer (@Monoid_list_app nat) unit :=
    pass (bind (tell (cons 1 nil)) (fun _ =>
          ret (tt, fun _ => nil)))
  in
  nil = PPair.psnd (runWriter m).
Proof. reflexivity. Qed.

But pass does nothing when it's used with a stateT or eitherT that contains a writer. The output from the tell [1] persists through the call to pass:

Example stateT_writer_pass_applies_function_to_log :
  let m : stateT nat (writer (@Monoid_list_app nat)) unit :=
    pass (bind (tell (cons 1 nil)) (fun _ =>
          ret (tt, fun _ => nil)))
  in
  nil = PPair.psnd (runWriter (runStateT m 0)).
Proof. simpl. (* nil = 1 :: nil *) Abort.

Example eitherT_writer_pass_applies_function_to_log :
  let m : eitherT nat (writer (@Monoid_list_app nat)) unit :=
    pass (bind (tell (cons 1 nil)) (fun _ =>
          ret (tt, fun _ => nil)))
  in
  nil = PPair.psnd (runWriter (unEitherT m)).
Proof. simpl. (* nil = 1 :: nil *) Abort.