You might want to try writing out a test instance in full and re-checking the second law.
Ok, while the part upto Applicative is correct and unambiguous: data Pair a = Pair a a instance Functor Pair where fmap f (Pair a b) = Pair (f a) (f b) instance Applicative Pair where pure a = Pair a a Pair fa fb <*> Pair a b = Pair (fa a) (fb b) there are at least two implementations of Monad (assuming return=pure, also GHC 7.10 allows omitting return and implements it exactly like that): -- implementation (a) instance Monad Pair where Pair a _ >>= k = k a -- implementation (b) instance Monad Pair where Pair _ b >>= k = k b ... neither of which can satisfy the laws. There are more: -- implementation (c) instance Monad Pair where Pair a b >>= k = Pair a' b' where Pair a' _ = k a Pair _ b' = k b -- implementation (d) instance Monad Pair where Pair a b >>= k = Pair a' b' where Pair _ b' = k a Pair a' _ = k b and, well: instance Monad Pair where Pair a b >>= _ = Pair a b Did I miss anything? Now, trying to get the second law to work: a) m >>= return = m Pair a b >>= (\a -> Pair a a) = Pair a b Pair a a = Pair a b contradiction. b) m >>= return = m Pair a b >>= (\a -> Pair a a) = Pair a b Pair b b = Pair a b contradiction. c) m >>= return = m Pair a b >>= (\a -> Pair a a) = Pair a b Pair a b = Pair a b no contradiction this time, I'll write the other laws after I'm done with the second for the other instances. d) m >>= return = m Pair a b >>= (\a -> Pair a a) = Pair a b Pair b a = Pair a b contradiction. e) m >>= return = m trivially correct. Testing the first law for (c) and (e) that passed the second law: c) return a >>= k = k a Pair a a >>= k a = k a --- Pair a' b' = k a where Pair a' _ = k a Pair _ b' = k a --- no contradiction again. e) return a >>= k = k a return a = k a contradiction. Okay, then testing the third law for (c): m >>= (\x -> k x >>= h) = (m >>= k) >>= h Pair a b >>= (\x -> k x >>= h) = (Pair a b >>= k) >>= h (*) Let's again unpack the application of >>= in some pseud-haskell: Pair a1 _ = (\x -> k x >>= h) a = k a >>= h (**) Pair _ b1 = (\x -> k x >>= h) b = k b >> =h Pair a2 _ = k a (***) Pair _ b2 = k b plugging it into (*): Pair a1 b1 = Pair a2 b2 >>= h Unpacking >>= again: Pair a3 _ = h a2 (****) Pair _ b3 = h b2 Pair a1 b1 = Pair a3 b3 Now, testing if a1 = a3, lets bring in (**), (***), and (****): Pair a1 _ = k a >>= h Pair a2 _ = k a Pair a3 _ = h a2 Form the first and the second equations (also using the one for b2 earlier, but it's going to be dropped anyway sooner or later) we get: Pair a1 _ = Pair a2 b2 >>= h Unpacking >>= : Pair a4 _ = h a2 Pair _ b4 = h b2 But from the third equation we know that (Pair a3 _ = h a2) so: Pair a1 _ = Pair a3 _ This does seem to work, I have no idea why. I'm pretty sure there I've made a mistake somewhere. Perhaps I shouldn't do equational reasoning after just getting up, or just use Agda :-/ Best regards, Marcin Mrotek