diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,19 @@
+Copyright Li-yao Xia (c) 2017-2020
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the “Software”), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,52 @@
+# Testable monad and mtl laws
+
+A library for testing implementations of *mtl* classes.
+
+*test-monad-laws* defines laws for monadic effects as QuickCheck
+properties.
+
+To use this library,
+[*quickcheck-higherorder*](https://hackage.haskell.org/package/quickcheck-higherorder)
+is also needed.
+
+Supported classes:
+
+- `mtl`: `MonadExcept`, `MonadReader`, `MonadState`, `MonadWriter`
+- `transformers`: `MonadTrans`
+- `transformers-base`: `MonadBase`
+- `monad-control`: `MonadTransControl`, `MonadBaseControl`
+
+This project also tests the effectiveness of these laws, by including some
+incorrect implementations, called *mutants*, and some invalid laws.
+
+Organization
+------------
+
+For every *mtl* class, for example `MonadReader`:
+
+- The most important module is `Test.Monad.Reader`, defining laws for the class.
+  Note that these laws are not official. But if your instance does not satisfy them,
+  now you know.
+- Mutants and bad laws are in `Test.Monad.Reader.Mutants`.
+- For convenience, all the good laws are gathered in a single list in
+  `Test.Monad.Reader.Checkers`.
+  It can easily be consumed by the library *tasty-quickcheck*.
+
+Related links and references
+----------------------------
+
+- [validity](https://github.com/NorfairKing/validity)
+- [checkers](https://hackage.haskell.org/package/checkers)
+- [quickcheck-classes](http://hackage.haskell.org/package/quickcheck-classes)
+- [hedgehog-classes](https://hackage.haskell.org/package/hedgehog-classes)
+- [ClassLaws](https://hackage.haskell.org/package/ClassLaws)
+- [test-invariant](https://hackage.haskell.org/package/test-invariant-0.4.5.0/docs/Test-Invariant.html)
+
+Papers with some relevant laws:
+
+- Just `do` it: Simple Monadic Equational Reasoning. Jeremy Gibbons, Ralf Hinze.
+- Proof abstraction for imperative languages. William L. Harrison.
+
+Hackage search terms:
+[laws](https://hackage.haskell.org/packages/search?terms=laws),
+[properties](https://hackage.haskell.org/packages/search?terms=properties).
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/src/Test/Monad/Base.hs b/src/Test/Monad/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Base.hs
@@ -0,0 +1,25 @@
+-- | Laws for 'MonadBase.
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Base where
+
+import Control.Monad.Base
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+import Test.Monad.Morph
+
+liftBase_return
+  :: forall m n a
+  .  MonadBase n m
+  => a -> Equation (m a)
+liftBase_return = returnHom @_ @m liftBase
+
+liftBase_bind
+  :: forall m n a b
+  .  MonadBase n m
+  => n a -> (a -> n b) -> Equation (m b)
+liftBase_bind = bindHom @_ @m liftBase
diff --git a/src/Test/Monad/Cont.hs b/src/Test/Monad/Cont.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Cont.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Test.Monad.Cont where
+
+import Control.Monad.Cont
+import Data.Void (absurd)
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+-- * 'MonadCont' laws
+
+-- Reference: https://mail.haskell.org/pipermail/libraries/2019-October/030041.html
+
+callCC_const :: forall m a. MonadCont m => m a -> Equation (m a)
+callCC_const m = callCC (const m) :=: m
+
+callCC_id :: forall m a. MonadCont m => a -> Equation (m a)
+callCC_id a = callCC ($ a) :=: pure a
+
+callCC_bind :: forall m a. MonadCont m => m a -> Equation (m a)
+callCC_bind m = callCC ((>>=) m) :=: m
+
+callCC_phantom ::
+  forall m a b.
+  MonadCont m =>
+  ((a -> m b) -> m a) ->
+  Equation (m a)
+callCC_phantom f = callCC f :=: callCC (f . (fmap . fmap) absurd)
+
+callCC_left_zero ::
+  forall m a b.
+  MonadCont m =>
+  ((a -> m b) -> m a) ->
+  ((a -> m b) -> b -> m a) ->
+  Equation (m a)
+callCC_left_zero f g = callCC (\k -> f k >>= (\a -> k a >>= g k)) :=: callCC f
diff --git a/src/Test/Monad/Cont/Checkers.hs b/src/Test/Monad/Cont/Checkers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Cont/Checkers.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Cont.Checkers where
+
+import Control.Monad.Cont
+import Control.Monad.State
+import Test.QuickCheck (Gen, Property)
+import Test.QuickCheck.HigherOrder (CoArbitrary, Constructible, TestEq, ok)
+
+import Test.Monad.Instances ()
+import Test.Monad.Cont
+-- import Test.Monad.Cont.Mutants
+
+checkCont ::
+  forall m a b.
+  ( MonadCont m
+  , TestEq (m a)
+  , CoArbitrary Gen b, CoArbitrary Gen (m b)
+  , Constructible a, Constructible (m a), Constructible (m b)
+  ) =>
+  [(String, Property)]
+checkCont =
+  [ ok "callCC-const"     (callCC_const @m @a)
+  , ok "callCC-id"        (callCC_id @m @a)
+  , ok "callCC-bind"      (callCC_bind @m @a)
+  , ok "callCC-phantom"   (callCC_phantom @m @a @b)
+  , ok "callCC-left-zero" (callCC_left_zero @m @a @b)
+  ]
+{-# NOINLINE checkCont #-}
+
+checkCont_ :: [(String, Property)]
+checkCont_ =
+     checkCont @(Cont Int) @Int @Int
+  ++ checkCont @(ContT Int (State Int)) @Int @Int
+  ++ checkCont @(ContT Int []) @Int @Int
+  ++ checkCont @(ContT Int (StateT Int [])) @Int @Int
diff --git a/src/Test/Monad/Control.hs b/src/Test/Monad/Control.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Control.hs
@@ -0,0 +1,63 @@
+-- | Laws for 'MonadTransControl' and 'MonadBaseControl'.
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Control where
+
+import Control.Monad.Base
+import Control.Monad.Trans
+import Control.Monad.Trans.Control
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+import Test.Monad.Morph
+
+-- * 'MonadState' laws
+
+liftControl :: forall t m a. (MonadTransControl t, Monad m) => m a -> t m a
+liftControl m = liftWith (\_ -> m)
+
+-- | Implied by 'liftWith_lift'.
+liftWith_return
+  :: forall t m a
+  .  (MonadTransControl t, Monad m, Monad (t m))
+  => a -> Equation (t m a)
+liftWith_return = returnHom @_ @(t m) liftControl
+
+-- | Implied by 'liftWith_lift'.
+liftWith_bind
+  :: forall t m a b
+  .  (MonadTransControl t, Monad m, Monad (t m))
+  => m a -> (a -> m b) -> Equation (t m b)
+liftWith_bind = bindHom @_ @(t m) liftControl
+
+-- | Implies 'liftWith_return' and 'liftWith_bind'.
+liftWith_lift
+  :: forall t m a
+  .  (MonadTransControl t, Monad m)
+  => m a -> Equation (t m a)
+liftWith_lift m = liftControl @t m :=: lift m
+
+liftWith_restoreT
+  :: forall t m a
+  .  (MonadTransControl t, Monad m, Monad (t m))
+  => t m a -> Equation (t m a)
+liftWith_restoreT t = (liftWith (\run -> run t) >>= restoreT . return) :=: t
+
+liftBaseControl :: forall m a n. MonadBaseControl n m => n a -> m a
+liftBaseControl n = liftBaseWith (\_ -> n)
+
+liftBaseWith_liftBase
+  :: forall m a n
+  .  MonadBaseControl n m
+  => n a -> Equation (m a)
+liftBaseWith_liftBase n = liftBaseControl @m n :=: liftBase n
+
+liftBaseWith_restoreM
+  :: forall m a n
+  .  MonadBaseControl n m
+  => m a -> Equation (m a)
+liftBaseWith_restoreM m = (liftBaseWith (\run -> run m) >>= restoreM) :=: m
diff --git a/src/Test/Monad/Control/Checkers.hs b/src/Test/Monad/Control/Checkers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Control/Checkers.hs
@@ -0,0 +1,117 @@
+-- {-# OPTIONS_GHC -ddump-
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Test.Monad.Control.Checkers where
+
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.Trans.Control (MonadTransControl, MonadBaseControl)
+import Data.Functor.Identity
+import Data.Kind (Type)
+import Data.Proxy (Proxy(Proxy))
+import Data.Typeable (Typeable, typeRep)
+import GHC.TypeLits
+import Test.QuickCheck (Property, pattern Fn)
+import Test.QuickCheck.HigherOrder
+
+import Test.Monad.Instances ()
+import Test.Monad.Control
+import Test.SmallList
+
+-- | All lists of length @n@ /or less/ with (possibly duplicate)
+-- elements from @xs@.
+type family Replicate (n :: Nat) (xs :: [k]) :: [[k]] where
+  Replicate 0 _ = '[ '[] ]
+  Replicate n xs = Extend' xs (Replicate (n - 1) xs)
+
+type Extend' xs ys = ys ++ Extend xs ys
+
+type family Extend (xs :: [k]) (ys :: [[k]]) :: [[k]] where
+  Extend '[] ys = '[]
+  Extend (x ': xs) ys = MapCons x ys ++ Extend xs ys
+
+type family MapCons (x :: k) (ys :: [[k]]) :: [[k]] where
+  MapCons x '[] = '[]
+  MapCons x (y ': ys) = (x ': y) ': MapCons x ys
+
+type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
+  '[] ++ ys = ys
+  (x ': xs) ++ ys = x ': xs ++ ys
+
+class TestControl (xs :: [[(Type -> Type) -> (Type -> Type)]]) (m :: Type -> Type) where
+  testControl :: [(String, [(String, Property)])]
+
+instance TestControl '[] m where
+  testControl = []
+
+instance
+  (  TestTransControl ts m, TestBaseControl ts m, TestControl tss m
+  ,  Typeable (StackT ts m)
+  )
+  => TestControl (ts ': tss) m where
+  testControl =
+    ( show (typeRep (Proxy @(StackT ts m)))
+    , testTransControl @ts @m ++ testBaseControl @ts @m
+    ) : testControl @tss @m
+
+type family StackT (ts :: [(Type -> Type) -> (Type -> Type)]) (m :: Type -> Type) :: Type -> Type where
+  StackT '[] m = m
+  StackT (t ': ts) m = t (StackT ts m)
+
+type Stack ts = StackT ts Identity
+
+class TestTransControl (ts :: [(Type -> Type) -> (Type -> Type)]) (m :: Type -> Type) where
+  testTransControl :: [(String, Property)]
+
+instance TestTransControl '[] m where
+  testTransControl = []
+
+instance
+  (  MonadTransControl t, Monad (StackT (t ': ts) m), Monad (StackT ts m)
+  ,  Constructible (StackT (t ': ts) m Int), Constructible (StackT ts m Int)
+  ,  TestEq (StackT (t ': ts) m Int))
+  => TestTransControl (t ': ts) m where
+  testTransControl =
+    [ ok "liftWith-return"   (liftWith_return @t @n @Int)
+    , ok "liftWith-bind"     (\m (Fn k) -> liftWith_bind @t @n @Int @Int m k)
+    , ok "liftWith-lift"     (liftWith_lift @t @n @Int)
+    , ok "liftWith-restoreT" (liftWith_restoreT @t @n @Int)
+    ] :: forall n. (n ~ StackT ts m) => [(String, Property)]
+  {-# NOINLINE testTransControl #-}
+
+class TestBaseControl (ts :: [(Type -> Type) -> (Type -> Type)]) (m :: Type -> Type) where
+  testBaseControl :: [(String, Property)]
+
+instance
+  (  MonadBaseControl m (StackT ts m)
+  ,  Constructible (StackT ts m Int), Constructible (m Int)
+  ,  TestEq (StackT ts m Int))
+  => TestBaseControl ts m where
+  testBaseControl =
+    [ ok "liftBaseWith-liftBase" (liftBaseWith_liftBase @n @Int)
+    , ok "liftBaseWith-restoreM" (liftBaseWith_restoreM @n @Int)
+    ] :: forall n. (n ~ StackT ts m) => [(String, Property)]
+  {-# NOINLINE testBaseControl #-}
+
+type StdTrans = '[ ReaderT Int, StateT Int, ExceptT Int ]
+
+type StdStacks = Replicate 2 StdTrans
+
+checkControl :: [(String, [(String, Property)])]
+checkControl =
+  testControl @StdStacks @Identity ++
+  testControl @StdStacks @SmallList
diff --git a/src/Test/Monad/Control/Mutants.hs b/src/Test/Monad/Control/Mutants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Control/Mutants.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.Monad.Control.Mutants where
+
+import Control.Monad.State
+import Control.Monad.Trans.Control
+
+import Test.Mutants
+
+mutantLiftWith
+  :: (Monad m, MonadTransControl t)
+  => (RunDefault (Mutant v t) t -> m a) -> Mutant v t m a
+mutantLiftWith = defaultLiftWith Mutant mutate
+
+mutantRestoreT :: (Monad m, MonadTransControl t) => m (StT t a) -> Mutant v t m a
+mutantRestoreT = defaultRestoreT Mutant
+
+-- | An general way to get 'MonadTransControl' wrong is to run the base
+-- computation twice when lifting...
+data LiftWithTwice
+
+-- | There should be no blanket @OVERLAPPABLE@ instance because of the type
+-- family.
+instance
+  MonadTransControl t => MonadTransControl (Mutant LiftWithTwice t) where
+  type StT (Mutant LiftWithTwice t) a = StT t a
+  restoreT = mutantRestoreT
+
+  liftWith f = mutantLiftWith (\run -> f run >> f run)
+
+data RunTwice
+
+instance
+  MonadTransControl t => MonadTransControl (Mutant RunTwice t) where
+  type StT (Mutant RunTwice t) a = StT t a
+  restoreT = mutantRestoreT
+
+  liftWith f = mutantLiftWith (\run -> f (\t -> run t >> run t))
+
+
+-- | ... or run it twice when restoring.
+data RestoreTwice
+
+instance
+  MonadTransControl t => MonadTransControl (Mutant RestoreTwice t) where
+  type StT (Mutant RestoreTwice t) a = StT t a
+  liftWith = mutantLiftWith
+
+  restoreT m = mutantRestoreT (m >> m)
+
+-- * State
+
+data LiftWithDropState
+
+instance MonadTransControl (Mutant LiftWithDropState (StateT s)) where
+  type StT (Mutant LiftWithDropState (StateT s)) a = StT (StateT s) a
+  restoreT = mutantRestoreT
+
+  liftWith f = Mutant . StateT $ \s ->
+    fmap
+      (\a -> (a, s))
+      (f (\(Mutant (StateT m)) ->
+        fmap
+          (\(a, _) -> (a, s))
+          (m s)))
+          -- Drop the state that should have been returned.
+
+data RestoreDropState
+
+instance MonadTransControl (Mutant RestoreDropState (StateT s)) where
+  type StT (Mutant RestoreDropState (StateT s)) a = StT (StateT s) a
+  liftWith = mutantLiftWith
+
+  restoreT m = Mutant . StateT $ \s -> fmap (\(a, _) -> (a, s)) m
+
diff --git a/src/Test/Monad/Except.hs b/src/Test/Monad/Except.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Except.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Except where
+
+import Control.Monad.Except
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+throwZero
+  :: forall m b a e
+  .  MonadError e m
+  => e -> (a -> m b) -> Equation (m b)
+throwZero e k = (throwError e >>= k) :=: throwError @_ @m e
+
+throw_catch
+  :: forall m a e
+  .  MonadError e m
+  => e -> (e -> m a) -> Equation (m a)
+throw_catch e h = catchError (throwError e) h :=: h e
+
+catch_throw
+  :: forall m a e
+  .  MonadError e m
+  => m a -> Equation (m a)
+catch_throw m = catchError m throwError :=: m
+
+catch_catch
+  :: forall m a e
+  .  MonadError e m
+  => m a -> (e -> m a) -> (e -> m a) -> Equation (m a)
+catch_catch m h1 h2 =
+  catchError (catchError m h1) h2
+  :=:
+  catchError m (\e -> catchError (h1 e) h2)
+
+catch_return
+  :: forall m a e
+  .  MonadError e m
+  => a -> (e -> m a) -> Equation (m a)
+catch_return a h = catchError (return a) h :=: return a
+
+-- Broken by @StateT s (Except e)@.
+catch_bind
+  :: forall m a b e
+  .  MonadError e m
+  => m a -> (a -> m b) -> (e -> m b) -> Equation (m b)
+catch_bind m k h =
+  catchError (m >>= k) h
+  :=:
+  (tryError m >>= either h (\a -> catchError (k a) h))
+
+-- TODO: remove
+tryError
+  :: forall m a e
+  .  MonadError e m
+  => m a -> m (Either e a)
+tryError m = catchError (fmap Right m) (pure . Left)
+
+-- | This should be a monad homomorphism.
+except :: forall m a e. MonadError e m => Either e a -> m a
+except = either throwError return
diff --git a/src/Test/Monad/Except/Checkers.hs b/src/Test/Monad/Except/Checkers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Except/Checkers.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Except.Checkers where
+
+import Control.Monad.Except
+import Control.Monad.State
+import Test.QuickCheck (Gen, Property)
+import Test.QuickCheck.HigherOrder (CoArbitrary, Constructible, TestEq, ok, ko)
+
+import Test.Monad.Instances ()
+import Test.Monad.Except
+import Test.Monad.Except.Mutants
+
+checkExcept
+  :: forall m a b e
+  .  ( MonadError e m
+     , CoArbitrary Gen b, CoArbitrary Gen e
+     , TestEq (m a)
+     , Constructible a, Constructible e, Constructible (m a), Constructible (m b))
+  => [(String, Property)]
+checkExcept =
+  [ ok "throwZero"    (throwZero @m @a @b)
+  , ok "throw-catch"  (throw_catch @m @a)
+  , ok "catch-throw"  (catch_throw @m @a)
+  , ok "catch-catch"  (catch_catch @m @a)  -- this takes one minute in test/prism-error?!
+  , ok "catch-return" (catch_return @m @a)
+  ]
+{-# NOINLINE checkExcept #-}
+
+checkExcept_ :: [(String, Property)]
+checkExcept_ =
+     checkExcept @(Either Int) @Int @Int
+  ++ checkExcept @(StateT Int (Either Int)) @Int @Int
+  ++ checkExcept @(ExceptT Int (State Int)) @Int @Int
+  ++ checkExcept @(StateT Int (ExceptT Int (State Int))) @Int @Int
+
+checkExcept' :: [(String, Property)]
+checkExcept' =
+  [ ok "catch-bind-e"      (catch_bind @(Except Int) @Int @Int)
+  , ko "catch-bind-se"     (catch_bind @(StateT Int (Either Int)) @Int @Int)
+  , ok "catch-bind-es"     (catch_bind @(ExceptT Int (State Int)) @Int @Int)
+  , ko "catch-bind-ses"    (catch_bind @(StateT Int (ExceptT Int (State Int))) @Int @Int)
+
+  , ko "bad-throwZero"     (bad_throwZero @(Except Int) @Int @Int)
+  , ko "bad-throw-catch"   (bad_throw_catch @(Except Int) @Int)
+  , ko "bad-catch-catch-1" (bad_catch_catch_1 @(Except Int) @Int)
+  , ko "bad-catch-catch-2" (bad_catch_catch_2 @(Except Int) @Int)
+  , ko "bad-catch-bind"    (bad_catch_bind @(Except Int) @Int @Int)
+
+  , ko "mut-1-throw-catch"       (throw_catch @(MutantExcept1 Int) @Int)
+  , ok "mut-1-bad-throw-catch"   (bad_throw_catch @(MutantExcept1 Int) @Int)
+  , ok "mut-1-bad-catch-catch-1" (bad_catch_catch_1 @(MutantExcept1 Int) @Int)
+  , ok "mut-1-bad-catch-catch-2" (bad_catch_catch_2 @(MutantExcept1 Int) @Int)
+  , ok "mut-1-bad-catch-bind"    (bad_catch_bind @(MutantExcept1 Int) @Int @Int)
+
+  , ko "mut-2-throw-catch" (throw_catch @(MutantExcept2 Int) @Int)
+  , ko "mut-2-catch-catch" (catch_catch @(MutantExcept2 Int) @Int)
+  , ko "mut-2-catch-bind"  (catch_bind @(MutantExcept2 Int) @Int @Int)
+  ]
+{-# NOINLINE checkExcept' #-}
diff --git a/src/Test/Monad/Except/Mutants.hs b/src/Test/Monad/Except/Mutants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Except/Mutants.hs
@@ -0,0 +1,108 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Test.Monad.Except.Mutants where
+
+import Control.Monad.Except
+import Control.Monad.State
+import Data.Functor.Identity
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+import Test.Mutants
+
+-- Notice the different type
+bad_throwZero
+  :: forall m b e
+  .  MonadError e m
+  => e -> (e -> m b) -> Equation (m b)
+bad_throwZero e k = (throwError e >>= k) :=: k e
+
+bad_throw_catch
+  :: forall m a e
+  .  MonadError e m
+  => e -> (e -> m a) -> Equation (m a)
+bad_throw_catch e h = catchError (throwError e) h :=: throwError e
+
+bad_catch_catch_1
+  :: forall m a e
+  .  MonadError e m
+  => m a -> (e -> m a) -> (e -> m a) -> Equation (m a)
+bad_catch_catch_1 m h1 h2 =
+  catchError (catchError m h1) h2
+  :=:
+  catchError m h1
+
+bad_catch_catch_2
+  :: forall m a e
+  .  MonadError e m
+  => m a -> (e -> m a) -> (e -> m a) -> Equation (m a)
+bad_catch_catch_2 m h1 h2 =
+  catchError (catchError m h1) h2
+  :=:
+  catchError m h2
+
+bad_catch_bind
+  :: forall m a b e
+  .  MonadError e m
+  => m a -> (a -> m b) -> (e -> m b) -> Equation (m b)
+bad_catch_bind m k h =
+  catchError (m >>= k) h
+  :=:
+  (m >>= \x -> catchError (k x) h)
+
+---
+
+data CatchDoesNothing
+
+-- | Fails:
+--
+-- > 'throw_catch'
+--
+-- Passes (wrongly):
+--
+-- > 'bad_throw_catch'
+-- > 'bad_catch_catch_1'
+-- > 'bad_catch_catch_2'
+-- > 'bad_catch_bind'
+--
+type MutantExcept1T e = Mutant CatchDoesNothing (ExceptT e)
+
+type MutantExcept1 e = MutantExcept1T e Identity
+
+instance {-# OVERLAPPING #-}
+  Monad m => MonadError e (MutantExcept1T e m) where
+  throwError e = Mutant (throwError e)
+  catchError m _ = m  -- "oops"
+
+data CatchTwice
+
+-- | Fails:
+--
+-- > 'throw_catch'
+-- > 'catch_catch'
+type MutantExcept2T e = Mutant CatchTwice (ExceptT e)
+
+type MutantExcept2 e = MutantExcept2T e Identity
+
+instance {-# OVERLAPPING #-}
+  Monad m => MonadError e (MutantExcept2T e m) where
+  throwError e = Mutant (throwError e)
+  catchError (Mutant m) h' = Mutant ((m `catchError` h) `catchError` h)  -- "oops"
+    where
+      h e = mutate (h' e)
+
+data Recoverable
+
+type MutantRStateT s = Mutant Recoverable (StateT s)
+
+instance {-# OVERLAPPING #-}
+  MonadError (e, s) m => MonadError e (MutantRStateT s m) where
+  throwError e = Mutant (do
+    s <- get
+    throwError (e, s))
+  catchError (Mutant m) h' = Mutant (m `catchError` h)
+    where
+      h (e, s) = StateT (\_ -> runStateT (mutate (h' e)) s)
diff --git a/src/Test/Monad/Instances.hs b/src/Test/Monad/Instances.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Instances.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE
+    FlexibleContexts,
+    FlexibleInstances,
+    MultiParamTypeClasses,
+    GeneralizedNewtypeDeriving,
+    StandaloneDeriving,
+    TypeFamilies,
+    UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.Monad.Instances where
+
+import Control.Monad.Cont
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.Writer
+import Test.QuickCheck (Gen)
+import Test.QuickCheck.HigherOrder (CoArbitrary(..), cogenEmbed, Constructible(..), TestEq(..))
+
+instance Constructible (r -> m a) => Constructible (ReaderT r m a) where
+  type Repr (ReaderT r m a) = Repr (r -> m a)
+  fromRepr = ReaderT . fromRepr
+
+instance (TestEq (r -> m a)) => TestEq (ReaderT r m a) where
+  ReaderT f =? ReaderT g = f =? g
+
+instance (CoArbitrary Gen (m r), Constructible a, Constructible (m r)) => Constructible (ContT r m a) where
+  type Repr (ContT r m a) = Repr ((a -> m r) -> m r)
+  fromRepr = ContT . fromRepr
+
+instance (TestEq ((a -> m r) -> m r)) => TestEq (ContT r m a) where
+  ContT f =? ContT g = f =? g
+
+instance (CoArbitrary Gen a, CoArbitrary Gen (m r), Constructible (m r)) => CoArbitrary Gen (ContT r m a) where
+  coarbitrary = cogenEmbed "runContT" runContT coarbitrary
+
+instance Constructible (m (Either e a)) => Constructible (ExceptT e m a) where
+  type Repr (ExceptT e m a) = Repr (m (Either e a))
+  fromRepr = ExceptT . fromRepr
+
+instance TestEq (m (Either e a)) => TestEq (ExceptT e m a) where
+  ExceptT m =? ExceptT n = m =? n
+
+instance Constructible (s -> m (a, s)) => Constructible (StateT s m a) where
+  type Repr (StateT s m a) = Repr (s -> m (a, s))
+  fromRepr = StateT . fromRepr
+
+instance TestEq (s -> m (a, s)) => TestEq (StateT s m a) where
+  StateT f =? StateT g = f =? g
+
+instance (Constructible s, CoArbitrary Gen (m (a, s))) => CoArbitrary Gen (StateT s m a) where
+  coarbitrary = cogenEmbed "runStateT" runStateT coarbitrary
+
+instance TestEq (m (a, w)) => TestEq (WriterT w m a) where
+  WriterT m =? WriterT n = m =? n
+
+instance Constructible (m (a, w)) => Constructible (WriterT w m a) where
+  type Repr (WriterT w m a) = Repr (m (a, w))
+  fromRepr = WriterT . fromRepr
diff --git a/src/Test/Monad/Morph.hs b/src/Test/Monad/Morph.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Morph.hs
@@ -0,0 +1,23 @@
+-- | Monad homomorphisms.
+
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Test.Monad.Morph where
+
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+-- | Natural transformation.
+type m ~> n = forall t. m t -> n t
+
+bindHom
+  :: forall m n a b
+  .  (Monad m, Monad n)
+  => (m ~> n) -> m a -> (a -> m b) -> Equation (n b)
+bindHom hom m k = hom (m >>= k) :=: (hom m >>= hom . k)
+
+returnHom
+  :: forall m n a
+  .  (Monad m, Monad n)
+  => (m ~> n) -> a -> Equation (n a)
+returnHom hom a = hom (return a) :=: return a
diff --git a/src/Test/Monad/Reader.hs b/src/Test/Monad/Reader.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Reader.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Reader where
+
+import Control.Monad.Reader
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+-- * Primary laws
+
+ask_ask
+  :: forall m r
+  .  MonadReader r m
+  => Equation (m r)
+ask_ask = (ask >> ask) :=: ask @r @m
+
+local_ask
+  :: forall m r
+  .  MonadReader r m
+  => (r -> r) -> Equation (m r)
+local_ask f = local f ask :=: fmap @m f ask
+
+-- Also:
+-- - 'local' and 'reader' should be monad homomorphisms.
+-- - 'ask' should have no effect.
+
+-- * Secondary laws
+
+local_local
+  :: forall m a r
+  .  MonadReader r m
+  => (r -> r) -> (r -> r) -> m a -> Equation (m a)
+local_local f g m = local f (local g m) :=: local (g . f) m
+
+local_id
+  :: forall m a r
+  .  MonadReader r m
+  => m a -> Equation (m a)
+local_id m = local id m :=: m
diff --git a/src/Test/Monad/Reader/Checkers.hs b/src/Test/Monad/Reader/Checkers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Reader/Checkers.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE
+    AllowAmbiguousTypes,
+    FlexibleContexts,
+    ScopedTypeVariables,
+    TypeApplications #-}
+
+module Test.Monad.Reader.Checkers where
+
+import Control.Monad.Reader
+import Control.Monad.State (StateT)
+import Test.QuickCheck (Gen, Property)
+import Test.QuickCheck.HigherOrder (CoArbitrary, Constructible, TestEq, ok, ko)
+
+import Test.Monad.Instances ()
+import Test.Monad.Morph
+import Test.Monad.Reader
+import Test.Monad.Reader.Mutants
+
+checkReader
+  :: forall m a b r
+  .  ( MonadReader r m
+     , CoArbitrary Gen b, CoArbitrary Gen r
+     , Constructible a, Constructible r, Constructible (m a), Constructible (m b)
+     , TestEq (m a), TestEq (m r))
+  => [(String, Property)]
+checkReader =
+  [ ok "ask-ask"         (ask_ask @m)
+  , ok "local-ask"       (local_ask @m)
+  , ok "local-local"     (local_local @m @a)
+  , ok "bindHom-local"   (\f -> bindHom @m @_ @b @a (local f))
+  , ok "returnHom-local" (\f -> returnHom @m @_ @a (local f))
+  ]
+{-# NOINLINE checkReader #-}
+
+checkReader_ :: [(String, Property)]
+checkReader_
+  =  checkReader @(Reader Int) @Int @Int
+  ++ checkReader @(StateT Int (Reader Int)) @Int @Int
+
+type Mutant1 = MutantReader LocalId Int
+type Mutant2 = MutantReaderT LocalRunsTwice Int []
+
+checkReader' :: [(String, Property)]
+checkReader' =
+  [ ok "mut-1-ask-ask"         (ask_ask @Mutant1)
+  , ko "mut-1-local-ask"       (local_ask @Mutant1)
+  , ok "mut-1-local-local"     (local_local @Mutant1 @Int)
+  , ok "mut-1-bindHom-local"   (\f -> bindHom @Mutant1 @_ @Int @Int (local f))
+  , ok "mut-1-returnHom-local" (\f -> returnHom @Mutant1 @_ @Int (local f))
+
+  , ok "mut-2-ask-ask"         (ask_ask @Mutant2)
+  , ok "mut-2-local-ask"       (local_ask @Mutant2)
+  , ko "mut-2-local-local"     (local_local @Mutant2 @Int)
+  , ko "mut-2-bindHom-local"   (\f -> bindHom @Mutant2 @_ @Int @Int (local f))
+  , ok "mut-2-returnHom-local" (\f -> returnHom @Mutant2 @_ @Int (local f))
+  ]
+{-# NOINLINE checkReader' #-}
diff --git a/src/Test/Monad/Reader/Mutants.hs b/src/Test/Monad/Reader/Mutants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Reader/Mutants.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Test.Monad.Reader.Mutants where
+
+import Control.Monad.Reader
+import Data.Functor.Identity
+
+import Test.Mutants
+
+data LocalId
+
+instance {-# OVERLAPPING #-}
+  Monad m => MonadReader r (Mutant LocalId (ReaderT r) m) where
+  ask = Mutant ask
+  local _ = id
+
+data LocalRunsTwice
+
+instance {-# OVERLAPPING #-}
+  Monad m => MonadReader r (Mutant LocalRunsTwice (ReaderT r) m) where
+  ask = Mutant ask
+  local f (Mutant m) = Mutant (local f (m >> m))
+
+type MutantReaderT v r = Mutant v (ReaderT r)
+type MutantReader v r = MutantReaderT v r Identity
diff --git a/src/Test/Monad/State.hs b/src/Test/Monad/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/State.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.State where
+
+import Control.Monad.State
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+-- * 'MonadState' laws
+
+get_get :: forall m s. MonadState s m => Equation (m s)
+get_get = (get >> get) :=: get @_ @m
+
+get_put :: forall m s. MonadState s m => Equation (m ())
+get_put = (get >>= put) :=: return @m ()
+
+put_get :: forall m s. MonadState s m => s -> Equation (m s)
+put_get s = (put s >> get) :=: (put s >> return @m s)
+
+put_put :: forall m s. MonadState s m => s -> s -> Equation (m ())
+put_put s1 s2 = (put s1 >> put s2) :=: put @_ @m s2
+
+-- | This is equivalent to 'state', which should be a monad homomorphism.
+state' :: forall m a s. MonadState s m => State s a -> m a
+state' = state . runState
diff --git a/src/Test/Monad/State/Checkers.hs b/src/Test/Monad/State/Checkers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/State/Checkers.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.State.Checkers where
+
+import Control.Monad.State
+import Test.QuickCheck (Property)
+import Test.QuickCheck.HigherOrder (Constructible, TestEq, ok, ko)
+
+import Test.Monad.Instances ()
+import Test.Monad.State
+import Test.Monad.State.Mutants
+
+checkState
+  :: forall m s
+  .  ( MonadState s m
+     , Constructible s, TestEq (m ()), TestEq (m s))
+  => [(String, Property)]
+checkState =
+  [ ok "get-get" (get_get @m)
+  , ok "get-put" (get_put @m)
+  , ok "put-get" (put_get @m)
+  , ok "put-put" (put_put @m)
+  ]
+
+checkState_ :: [(String, Property)]
+checkState_ = checkState @(State Int)
+
+checkState' :: [(String, Property)]
+checkState' =
+  [ ko "bad-get-put-get"     (bad_get_put_get @(State Int))
+  , ko "bad-put-put"         (bad_put_put     @(State Int))
+  , ko "mut-put-get"         (put_get         @(MutantState Int))
+  , ok "mut-bad-get-put-get" (bad_get_put_get @(MutantState Int))
+  , ok "mut-bad-put-put"     (bad_put_put     @(MutantState Int))
+  ]
+
diff --git a/src/Test/Monad/State/Mutants.hs b/src/Test/Monad/State/Mutants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/State/Mutants.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.State.Mutants where
+
+import Control.Monad.State
+import Data.Functor.Identity
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+import Test.Mutants
+
+bad_get_put_get :: forall m s. MonadState s m => s -> Equation (m s)
+bad_get_put_get s = (put s >> get) :=: (get >>= \s' -> put s >> return @m s')
+
+bad_put_put :: forall m s. MonadState s m => s -> s -> Equation (m ())
+bad_put_put s1 s2 = (put s1 >> put s2) :=: put @_ @m s1
+
+-- * 'StateT' mutant
+
+-- Can't get 'get' wrong.
+-- Only one way to get 'put' wrong.
+--
+-- Parametricity!
+
+data PutDoesNothing
+
+-- | Fails:
+--
+-- > 'put_get'
+--
+-- Passes (wrongly):
+--
+-- > 'bad_get_put_get'
+-- > 'bad_put_put'
+type MutantStateT s = Mutant PutDoesNothing (StateT s)
+
+type MutantState s = MutantStateT s Identity
+
+instance {-# OVERLAPPING #-}
+  Monad m => MonadState s (MutantStateT s m) where
+  get = Mutant get
+  put _s = Mutant $ StateT $ \s -> return ((), s)  -- "oops"
diff --git a/src/Test/Monad/Trans.hs b/src/Test/Monad/Trans.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Trans.hs
@@ -0,0 +1,24 @@
+-- | Laws for 'MonadTrans'.
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Trans where
+
+import Control.Monad.Trans
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+import Test.Monad.Morph
+
+lift_return
+  :: forall t m a
+  .  (MonadTrans t, Monad m, Monad (t m))
+  => a -> Equation (t m a)
+lift_return = returnHom @_ @(t m) lift
+
+lift_bind
+  :: forall t m a b
+  .  (MonadTrans t, Monad m, Monad (t m))
+  => m a -> (a -> m b) -> Equation (t m b)
+lift_bind = bindHom @_ @(t m) lift
diff --git a/src/Test/Monad/Trans/Mutants.hs b/src/Test/Monad/Trans/Mutants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Trans/Mutants.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Test.Monad.Trans.Mutants where
+
+import Control.Monad.Trans
+import Control.Monad.Trans.Maybe
+import Data.Functor (($>))
+
+import Test.Mutants
+
+-- | An general way to get 'MonadTrans' wrong is to run the base
+-- computation twice.
+data LiftTwice
+
+instance {-# OVERLAPPING #-}
+  MonadTrans t => MonadTrans (Mutant LiftTwice t) where
+  lift m = lift (m >> m)
+
+-- Other kinds of mistakes are difficult to make, by parametricity.
+
+-- State:
+-- lift :: m a -> (s -> m (a, s))
+
+-- Except:
+-- lift :: m a -> m (Either e a)
+
+-- Writer:
+-- lift :: m a -> m (w, a)
+
+-- Reader:
+-- lift :: m a -> (r -> m a)
+
+-- Maybe:
+-- lift :: m a -> m (Maybe a)
+
+-- | Forget the computation.
+data LiftMaybeNothing
+
+instance {-# OVERLAPPING #-}
+  MonadTrans (Mutant LiftMaybeNothing MaybeT) where
+  lift _ = Mutant . MaybeT $ return Nothing
+
+-- | Run the computation but forget the result.
+data LiftMaybeDiscard
+
+instance {-# OVERLAPPING #-}
+  MonadTrans (Mutant LiftMaybeDiscard MaybeT) where
+  lift m = Mutant . MaybeT $ m $> Nothing
diff --git a/src/Test/Monad/Writer.hs b/src/Test/Monad/Writer.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Writer.hs
@@ -0,0 +1,66 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Test.Monad.Writer where
+
+import Data.Functor (($>))
+import Control.Monad.Writer
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+tell_tell
+  :: forall m w
+  .  MonadWriter w m
+  => w -> w -> Equation (m ())
+tell_tell w1 w2 = (tell w1 >> tell w2) :=: tell (w1 <> w2)
+
+tell_mempty
+  :: forall m w
+  .  MonadWriter w m
+  => Equation (m ())
+tell_mempty = tell mempty :=: return ()
+
+listen_return
+  :: forall m a w
+  .  MonadWriter w m
+  => a -> Equation (m (a, w))
+listen_return a = listen (return a) :=: return (a, mempty)
+
+listen_bind
+  :: forall m a b w
+  .  MonadWriter w m
+  => m a -> (a -> m b) -> Equation (m (b, w))
+listen_bind m k =
+  listen (m >>= k) :=: do
+    (a, wa) <- listen m
+    (b, wb) <- listen (k a)
+    return (b, wa <> wb)
+
+listen_tell
+  :: forall m w
+  .  MonadWriter w m
+  => w -> Equation (m w)
+listen_tell w =
+  fmap snd (listen (tell w)) :=: (tell w >> return w)
+
+listen_listen
+  :: forall m a w
+  .  MonadWriter w m
+  => m a -> Equation (m ((a, w), w))
+listen_listen m = listen (listen m) :=: fmap (\(a, w) -> ((a, w), w)) (listen m)
+
+listen_pass
+  :: forall m a w
+  .  MonadWriter w m
+  => m (a, w -> w) -> Equation (m (a, w))
+listen_pass m =
+  listen (pass m) :=: pass (fmap (\((a, f), w) -> ((a, f w), f)) (listen m))
+
+pass_tell
+  :: forall m w
+  .  MonadWriter w m
+  => w -> (w -> w) -> Equation (m ())
+pass_tell w f =
+  pass (tell w $> ((), f)) :=: tell (f w)
+
+-- | This is equivalent to 'writer', which should be a monad homomorphism.
+writer' :: forall m a w. MonadWriter w m => Writer w a -> m a
+writer' = writer . runWriter
diff --git a/src/Test/Monad/Writer/Checkers.hs b/src/Test/Monad/Writer/Checkers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Writer/Checkers.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Monad.Writer.Checkers where
+
+import Control.Monad.Writer
+import Control.Monad.State (StateT)
+import Test.QuickCheck (Gen, Property)
+import Test.QuickCheck.HigherOrder (CoArbitrary, Constructible, TestEq, ok, ko)
+
+import Test.Monad.Instances ()
+import Test.Monad.Writer
+import Test.Monad.Writer.Mutants
+
+checkWriter
+  :: forall m a b w
+  .  ( MonadWriter w m
+     , CoArbitrary Gen b, CoArbitrary Gen w
+     , Constructible a, Constructible w, Constructible (m a), Constructible (m b)
+     , Constructible (m (a, w -> w))
+     , TestEq (m ()), TestEq (m (a, w)), TestEq (m w), TestEq (m ((a, w), w)) )
+  => [(String, Property)]
+checkWriter =
+  [ ok "tell-tell"     (tell_tell     @m)
+  , ok "tell-mempty"   (tell_mempty   @m)
+  , ok "listen-return" (listen_return @m @a)
+  , ok "listen-bind"   (listen_bind   @m @b @a)
+  , ok "listen-tell"   (listen_tell   @m)
+  , ok "listen-listen" (listen_listen @m @a)
+  , ok "listen-pass"   (listen_pass   @m @a)
+  , ok "pass-tell"     (pass_tell   @m)
+  ]
+{-# NOINLINE checkWriter #-}
+
+checkWriter_ :: [(String, Property)]
+checkWriter_
+  =  checkWriter @(Writer (Sum Int)) @Int @Int
+  ++ checkWriter @(StateT Int (Writer (Sum Int))) @Int @Int
+
+checkWriter' :: [(String, Property)]
+checkWriter' =
+  [ ko "bad-listen-tell" (bad_listen_tell @(Writer (Sum Int)))
+
+  , ko "mut-1-listen-tell" (listen_tell   @(MutantWriter TellDoesNothing (Sum Int)))
+
+  , ko "mut-2-listen-tell" (listen_tell   @(MutantWriter ListenDoesNothing (Sum Int)))
+  , ko "mut-2-listen-pass" (listen_pass   @(MutantWriter ListenDoesNothing (Sum Int)) @Int)
+
+  , ko "mut-3-listen-tell"     (listen_tell     @(MutantWriter ListenResets (Sum Int)))
+  , ko "mut-3-listen-listen"   (listen_listen   @(MutantWriter ListenResets (Sum Int)) @Int)
+  , ko "mut-3-listen-pass"     (listen_pass     @(MutantWriter ListenResets (Sum Int)) @Int)
+  , ok "mut-3-bad-listen-tell" (bad_listen_tell @(MutantWriter ListenResets (Sum Int)))
+
+  , ko "mut-4-listen-pass"   (listen_pass     @(MutantWriter PassDoesNothing (Sum Int)) @Int)
+  ]
+{-# NOINLINE checkWriter' #-}
diff --git a/src/Test/Monad/Writer/Mutants.hs b/src/Test/Monad/Writer/Mutants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Monad/Writer/Mutants.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Test.Monad.Writer.Mutants where
+
+import Control.Monad.Writer
+import Data.Functor.Identity
+import Test.QuickCheck.HigherOrder (Equation(..))
+
+import Test.Mutants
+
+bad_listen_tell
+  :: forall m w
+  .  MonadWriter w m
+  => w -> Equation (m w)
+bad_listen_tell w =
+  fmap snd (listen (tell w)) :=: return w
+
+type MutantWriter v w = Mutant v (WriterT w) Identity
+
+data TellDoesNothing
+
+instance {-# OVERLAPPING #-}
+  (Monad m, Monoid w)
+  => MonadWriter w (Mutant TellDoesNothing (WriterT w) m) where
+  tell _ = return ()
+  listen (Mutant m) = Mutant (listen m)
+  pass (Mutant m) = Mutant (pass m)
+
+data ListenDoesNothing
+
+instance {-# OVERLAPPING #-}
+  (Monad m, Monoid w)
+  => MonadWriter w (Mutant ListenDoesNothing (WriterT w) m) where
+  tell = Mutant . tell
+  listen m = fmap (\a -> (a, mempty)) m
+  pass (Mutant m) = Mutant (pass m)
+
+data ListenResets
+
+instance {-# OVERLAPPING #-}
+  (Monad m, Monoid w)
+  => MonadWriter w (Mutant ListenResets (WriterT w) m) where
+  tell = Mutant . tell
+  listen (Mutant (WriterT m)) = Mutant (WriterT (fmap (\(a, w) -> ((a, w), mempty)) m))
+  pass (Mutant m) = Mutant (pass m)
+
+data PassDoesNothing
+
+instance {-# OVERLAPPING #-}
+  (Monad m, Monoid w)
+  => MonadWriter w (Mutant PassDoesNothing (WriterT w) m) where
+  tell = Mutant . tell
+  listen (Mutant m) = Mutant (listen m)
+  pass = fmap fst
diff --git a/src/Test/Mutants.hs b/src/Test/Mutants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Mutants.hs
@@ -0,0 +1,54 @@
+-- | A manual mutation testing framework for monads and transformers.
+
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.Mutants where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.State
+import Control.Monad.Reader
+import Control.Monad.Except
+import Control.Monad.Writer
+import Data.Kind (Type)
+import Test.QuickCheck (Arbitrary)
+import Test.QuickCheck.HigherOrder (TestEq(..), Constructible(..))
+
+-- | The type @Mutant v t m a@ is isomorphic to @t m a@, and inherits
+-- various instances from it.
+--
+-- > class MyClass m where
+-- >   myMethod :: m ()
+-- >
+-- > deriving instance MyClass (t m) => MyClass (Mutant v t m)
+--
+-- The first parameter @v@ is phantom, and identifies a "mutation".
+--
+-- A new mutation can be declared as a datatype.
+--
+-- > data BugInMyClass
+--
+-- Use overlapping instances to "mutate" an implementation.
+--
+-- > instance {-# OVERLAPPING #-} MyClass (Mutant BugInMyClass t m) where
+-- >   myMethod = wrongMethod
+newtype Mutant v t (m :: Type -> Type) a = Mutant { mutate :: t m a }
+  deriving (
+    Eq, Ord, Show,
+    Functor, Applicative, Alternative, Monad, MonadPlus,
+    MonadState s, MonadReader r, MonadError e, MonadWriter w,
+    Arbitrary)
+
+deriving instance MonadTrans t => MonadTrans (Mutant v t)
+deriving instance TestEq (t m a) => TestEq (Mutant v t m a)
+
+instance Constructible (t m a) => Constructible (Mutant v t m a) where
+  type Repr (Mutant v t m a) = Repr (t m a)
+  fromRepr = Mutant . fromRepr
diff --git a/src/Test/SmallList.hs b/src/Test/SmallList.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/SmallList.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Test.SmallList where
+
+import Control.Monad.Base
+import Control.Monad.Trans.Control
+import Test.QuickCheck
+import Test.QuickCheck.HigherOrder (Constructible(..), TestEq(..))
+
+-- | Isomorphic to @[]@, but its arbitrary instance
+-- generates very small lists.
+newtype SmallList a = SmallList [a]
+  deriving (Eq, Ord, Show, Functor, Applicative, Monad)
+
+instance Arbitrary a => Arbitrary (SmallList a) where
+  arbitrary = sized $ \n -> do
+      k <- choose (0, logInt n)
+      SmallList <$> vectorOf k arbitrary
+    where
+      logInt n | n > 0 = 1 + logInt (n `div` 2)
+      logInt _ = 0
+  shrink (SmallList as) = fmap SmallList (shrink as)
+
+instance Constructible a => Constructible (SmallList a) where
+  type Repr (SmallList a) = SmallList (Repr a)
+  fromRepr = fmap fromRepr
+
+instance TestEq a => TestEq (SmallList a) where
+  SmallList as =? SmallList bs = as =? bs
+
+instance MonadBase SmallList SmallList where
+  liftBase = id
+
+instance MonadBaseControl SmallList SmallList where
+  type StM SmallList a = a
+  liftBaseWith f = f id
+  restoreM = return
diff --git a/test-monad-laws.cabal b/test-monad-laws.cabal
new file mode 100644
--- /dev/null
+++ b/test-monad-laws.cabal
@@ -0,0 +1,85 @@
+name:                test-monad-laws
+version:             0.0.0.0
+synopsis:
+  Laws for mtl classes as QuickCheck properties.
+description:         See README
+homepage:            https://github.com/Lysxia/test-monad-laws#readme
+license:             MIT
+license-file:        LICENSE
+author:              Li-yao Xia
+maintainer:          lysxia@gmail.com
+copyright:           2017-2020 Li-yao Xia
+category:            Test
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+
+library
+  hs-source-dirs:      src
+  exposed-modules:
+    Test.Monad.Base
+    Test.Monad.Control
+    Test.Monad.Control.Checkers
+    Test.Monad.Control.Mutants
+    Test.Monad.Cont
+    Test.Monad.Cont.Checkers
+    Test.Monad.Except
+    Test.Monad.Except.Checkers
+    Test.Monad.Except.Mutants
+    Test.Monad.Instances
+    Test.Monad.Reader
+    Test.Monad.Reader.Checkers
+    Test.Monad.Reader.Mutants
+    Test.Monad.State
+    Test.Monad.State.Checkers
+    Test.Monad.State.Mutants
+    Test.Monad.Writer
+    Test.Monad.Writer.Checkers
+    Test.Monad.Writer.Mutants
+    Test.Monad.Trans
+    Test.Monad.Trans.Mutants
+    Test.Monad.Morph
+    Test.Mutants
+    Test.SmallList
+  build-depends:
+    monad-control,
+    transformers,
+    transformers-base,
+    mtl,
+    QuickCheck >= 2.12,
+    quickcheck-higherorder,
+    base >= 4.9 && < 5
+  ghc-options:         -Wall -Wno-orphans
+  default-language:    Haskell2010
+
+test-suite test-monad-laws-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             test.hs
+  build-depends:
+    test-monad-laws,
+    QuickCheck,
+    tasty,
+    tasty-quickcheck >= 0.9.2,
+    base
+  default-language:    Haskell2010
+
+test-suite prism-error-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             prism-error.hs
+  build-depends:
+    test-monad-laws,
+    mtl,
+    QuickCheck,
+    quickcheck-higherorder,
+    tasty,
+    tasty-quickcheck >= 0.9.2,
+    base
+  default-language:    Haskell2010
+  if impl(ghc < 8.2)
+    buildable: False
+
+source-repository head
+  type:     git
+  location: https://github.com/Lysxia/test-monad-laws
diff --git a/test/prism-error.hs b/test/prism-error.hs
new file mode 100644
--- /dev/null
+++ b/test/prism-error.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+
+import Test.Tasty
+import Test.Tasty.QuickCheck
+
+import Test.Monad.Except.Checkers (checkExcept)
+import Test.SmallList (SmallList)
+import Test.QuickCheck.HigherOrder
+
+import Control.Monad.State
+import Control.Monad.Except
+
+newtype PrismErrorT f e m a = PrismErrorT { runPrismErrorT :: m a }
+  deriving (Functor, Applicative, Monad, Eq, Ord, Show, TestEq, Constructible)
+
+class Prism e f where
+  match :: e -> Either e f
+  build :: f -> e
+
+instance Prism (Either a b) a where
+  match (Left a) = Right a
+  match e = Left e
+  build = Left
+
+instance (MonadError e m, Prism e f) => MonadError f (PrismErrorT f e m) where
+  throwError f = PrismErrorT (throwError (build f))
+  catchError (PrismErrorT m) handleF = PrismErrorT (catchError m (\e ->
+    case match e of
+      Left e -> throwError e
+      Right f -> runPrismErrorT (handleF f)))
+
+trans :: forall m e f a. (MonadError e m, Prism e f)
+  => (forall n. MonadError f n => n a) -> m a
+trans g = runPrismErrorT g
+
+type M = PrismErrorT Int (Either Int Word) (ExceptT (Either Int Word) (StateT Int SmallList))
+
+main :: IO ()
+main = defaultMain . testProperties "PrismError" $ checkExcept @M @Int @Int
diff --git a/test/test.hs b/test/test.hs
new file mode 100644
--- /dev/null
+++ b/test/test.hs
@@ -0,0 +1,57 @@
+module Main where
+
+import Test.Tasty
+import Test.Tasty.QuickCheck
+
+import Test.Monad.Control.Checkers
+import Test.Monad.Cont.Checkers
+import Test.Monad.Except.Checkers
+import Test.Monad.Reader.Checkers
+import Test.Monad.State.Checkers
+import Test.Monad.Writer.Checkers
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Tests"
+  [ testsState
+  , testsCont
+  , testsExcept
+  , testsReader
+  , testsWriter
+  , testsControl
+  ]
+
+testsState :: TestTree
+testsState = testGroup "MonadState"
+  [ testProperties "Normal" checkState_
+  , testProperties "Mutant" checkState'
+  ]
+
+testsCont :: TestTree
+testsCont = testGroup "MonadCont"
+  [ testProperties "Normal" checkCont_
+  ]
+
+testsExcept :: TestTree
+testsExcept = testGroup "MonadExcept"
+  [ testProperties "Normal" checkExcept_
+  , testProperties "Mutant" checkExcept'
+  ]
+
+testsReader :: TestTree
+testsReader = testGroup "MonadReader"
+  [ testProperties "Normal" checkReader_
+  , testProperties "Mutant" checkReader'
+  ]
+
+testsWriter :: TestTree
+testsWriter = testGroup "MonadWriter"
+  [ testProperties "Normal" checkWriter_
+  , testProperties "Mutant" checkWriter'
+  ]
+
+testsControl :: TestTree
+testsControl = testGroup "Monad*Control"
+  [ testProperties name props | (name, props) <- checkControl ]