Hello, consider the following monad (which is a slight adaptation of the one used in "Typing Haskell in Haskell") as given: data Error a = Error String | Ok a data TI a = TI (Subst -> Int -> Error (Subst, Int, a)) instance Monad TI where return x = TI (\s n -> Ok (s,n,x)) TI f >>= g = TI (\s n -> case f s n of Ok (s',m,x) -> let TI gx = g x in gx s' m Error s->Error s) fail s = TI (\_ _->Error s) Now I would like to verify the monad laws. It is really easy to show that return is both a left- and a right-unit. But I got stuck with associativity: m@(TI mf) >>= (\a->f a >>= h) = = TI (\s n -> case mf s n of Ok (s',m,x) -> let TI gx = (\a->f a >>= h) x in gx s' m Error s->Error s) = ... = ((TI mf) >>= f) >>= h Is there someone outside who is willing to tell what fills the gap? A hint may be sufficient already. Or is there a tool, which finds such derivations? I have read the tutorial "All about Monads", but there only is mentioned, that there is an obligation for the programmer to prove these laws. It would be helpful as well, to provide an example! I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in ...". But the "a" may occur in "h"? Thank you. Steffen