Question: A simple question, I hope: The `binary` package defines two types, [`Get` and `Put`](http://hackage.haskell.org/packages/archive/binary/0.5.1.0/doc/html/Data-Binary.html#g:2). The former is essentially a state monad, and the latter is essentially a writer. Both state and writer have reasonable `MonadFix` instances, so I'd expect that `Get` and `Put` also would.

`Get` does. `Put` doesn't. So, is it possible to define an appropriate `MonadFix` instance for `Put` (really for [`PutM`](http://hackage.haskell.org/packages/archive/binary/0.5.1.0/doc/html/Data-Binary-Put.html#t:PutM))?

A more general question is: how does one normally verify that a typeclass instance actually satisfies the laws of that typeclass?

Answer: 
As you can see in the source for the binary package ([Data.Binary.Put:71](http://hackage.haskell.org/packages/archive/binary/0.5.1.0/doc/html/src/Data-Binary-Put.html#line-71)), the data structure used for monadic values is strict in the builder. Since extracting the value from the monad has to force the structure in which the value is found, this will cause an infinite loop if the builder depends on the input.

```
data PairS a = PairS a !Builder
newtype PutM a = Put { unPut :: PairS a }

```

So you could write a `MonadFix` instance, but you wouldn't be able to do anything useful with it. But I don't think you could do anything useful with `MonadFix` here anyway, at least nothing that you couldn't do with plain old `fix`, since the `PutM` monad is basically `Writer Builder` (but with a specialized implementation).

**As for your second question,** it's not related to the first so you should ask it as a separate question.
Here's an answer to your second question and a follow-up to Daniel's comment. You verify laws by hand and I'll use the example of the `Functor` laws for `Maybe`:

```
-- First law
fmap id = id

-- Proof
fmap id
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just (id a)
= \x -> case x of
    Nothing -> Nothing
    Just a -> Just a
= \x -> case x of
    Nothing -> x
    Just a  -> x
= \x -> case x of
    _ -> x
= \x -> x
= id

-- Second law
fmap f . fmap g = fmap (f . g)

-- Proof
fmap f . fmap g
= \x -> fmap f (fmap g x)
= \x -> fmap f (case x of
    Nothing -> Nothing
    Just a  -> Just (f a) )
= \x -> case x of
    Nothing -> fmap f  Nothing
    Just a  -> fmap f (Just (g a))
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just (f (g a))
= \x -> case x of
    Nothing -> Nothing
    Just a  -> Just ((f . g) a)
= \x -> case x of
    Nothing -> fmap (f . g) Nothing
    Just a  -> fmap (f . g) (Just a)
= \x -> fmap (f . g) (case x of
    Nothing -> Nothing
    Just a  -> Just a )
= \x -> fmap (f . g) (case x of
    Nothing -> x
    Just a  -> x )
= \x -> fmap (f . g) (case x of
    _ -> x )
= \x -> fmap (f . g) x
= fmap (f . g)

```

Obviously I could have skipped a lot of those steps but I just wanted to spell out the complete proof. Proving these kinds of laws is difficult at first until you get the hang of them so it's a good idea to start slow and pedantic and then once you get better you can start combining steps and even do some in your head after a while for the simpler ones.