Hello, thank you for the idea of using variables directly to see what happens. This is really a simplification for the proof. At first I thought that there should be a simpler solution and I tried to modify your approach, so that it applies to >>= as well, but now I am convinced :-) I have downloaded the paper of Filinski "Representing Monads" to take a look at the definition directly. It seems to be interesting for me, but deterringly difficult as well :-( Would it be possible to write a piece of Haskell code which checks the monadic laws automatically by simulating evaluation in this way? Maybe a little theoretical section in the monad tutorial which deals with this stuff would be a help as well. Iavor, I am really happy, that this monad is working :-) Never touch a running system or try to make it more difficult as it is! These monad transformers are still a red rag to me. Nevertheless thank you. Ciao, Steffen