diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,17 @@
+## [0.6.0]
+
+* [Enhance `traversable` checks](https://github.com/haskell-checkers/checkers/pull/61)
+
+* [Remove redundant constraint from instance CoArbitrary Array](https://github.com/haskell-checkers/checkers/pull/65)
+
+[0.6.0]: https://github.com/haskell-checkers/checkers/compare/v0.5.7...v0.6.0
+
+## [0.5.7]
+
+* [Add `bifoldable` and `bifoldableBifunctor` tests](https://github.com/haskell-checkers/checkers/pull/62)
+
+* [Restore `verboseBatch` functionality](https://github.com/haskell-checkers/checkers/pull/59)
+
+* [Drop support for GHC < 8.2](https://github.com/haskell-checkers/checkers/pull/63)
+
+[0.5.7]: https://github.com/haskell-checkers/checkers/compare/v0.5.6...v0.5.7
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,2 @@
+**checkers** is a library for reusable QuickCheck properties, particularly for standard type classes (class laws and [class morphisms](http://conal.net/papers/type-class-morphisms)).
+Checkers also has lots of support for randomly generating data values (thanks to Thomas Davie).
diff --git a/checkers.cabal b/checkers.cabal
--- a/checkers.cabal
+++ b/checkers.cabal
@@ -1,6 +1,6 @@
 Name:                checkers
-Version:             0.3.1
-Cabal-Version:       >= 1.6
+Version:             0.6.0
+Cabal-Version:       >= 1.10
 Synopsis:            Check properties on standard classes and data structures.
 Category:            Testing
 Description:
@@ -10,25 +10,27 @@
   for common data types.
   .
   &#169; 2008-2013 by Conal Elliott; BSD3 license.
-  .
-  Contributions from: Thomas Davie.
-Author:              Conal Elliott 
+Author:              Conal Elliott
 Maintainer:          conal@conal.net
 Copyright:           (c) 2008-2013 by Conal Elliott
 License:             BSD3
 License-File:        COPYING
 Stability:           experimental
 build-type:          Simple
+tested-with:         GHC==9.2.1, GHC==9.0.2, GHC==8.10.7, GHC==8.8.4, GHC==8.6.5, GHC==8.4.4, GHC==8.2.2
+homepage:            https://github.com/haskell-checkers/checkers
+extra-source-files:  README.md CHANGELOG.md
 
 source-repository head
   type:     git
-  location: git://github.com/conal/checkers.git
+  location: git://github.com/haskell-checkers/checkers.git
 
 Library
   hs-Source-Dirs:      src
   Extensions:
-  Build-Depends:       base < 5, random, QuickCheck>=2.3, array >= 0.1
-  Exposed-Modules:     
+  Build-Depends:       base >= 4.10 && < 5, random, QuickCheck>=2.3, array >= 0.1, semigroupoids >= 5 && < 6
+
+  Exposed-Modules:
                        Test.QuickCheck.Utils
                        Test.QuickCheck.Checkers
                        Test.QuickCheck.Classes
@@ -45,4 +47,5 @@
                        Test.QuickCheck.Later
   Other-modules:
                        Control.Monad.Extensions
-  ghc-options:         -Wall
+  ghc-options:         -Wall -Wredundant-constraints
+  Default-Language:    Haskell2010
diff --git a/src/Control/Monad/Extensions.hs b/src/Control/Monad/Extensions.hs
--- a/src/Control/Monad/Extensions.hs
+++ b/src/Control/Monad/Extensions.hs
@@ -1,6 +1,6 @@
 module Control.Monad.Extensions (satisfiesM,if') where
 
-import Control.Applicative (Applicative,liftA3)
+import Control.Applicative (liftA3)
 
 satisfiesM :: Monad m => (a -> Bool) -> m a -> m a
 satisfiesM p x = x >>= if' p return (const (satisfiesM p x))
diff --git a/src/Test/QuickCheck/Checkers.hs b/src/Test/QuickCheck/Checkers.hs
--- a/src/Test/QuickCheck/Checkers.hs
+++ b/src/Test/QuickCheck/Checkers.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances
            , FlexibleContexts, TypeSynonymInstances, GeneralizedNewtypeDeriving
-           , UndecidableInstances, ScopedTypeVariables
+           , UndecidableInstances, ScopedTypeVariables, DefaultSignatures
+           , TypeOperators, CPP
   #-}
 {-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
 
@@ -9,10 +10,10 @@
 -- Module      :  Test.QuickCheck.Checkers
 -- Copyright   :  (c) Conal Elliott 2007,2008
 -- License     :  BSD3
--- 
+--
 -- Maintainer  :  conal@conal.net
 -- Stability   :  experimental
--- 
+--
 -- Some QuickCheck helpers
 ----------------------------------------------------------------------
 
@@ -21,7 +22,7 @@
   -- * Misc
     Test, TestBatch, unbatch, checkBatch, quickBatch, verboseBatch
   -- , probablisticPureCheck
-  , Unop, Binop, genR, inverseL, inverse
+  , Unop, Binop, genR, involution, inverseL, inverse
   , FracT, NumT, OrdT, T
   -- * Generalized equality
   , EqProp(..), eq
@@ -33,7 +34,7 @@
   -- * Model-based (semantics-based) testing
   , Model(..)
   , meq, meq1, meq2, meq3, meq4, meq5
-  , eqModels
+  , eqModels, denotationFor
   , Model1(..)
   -- * Some handy testing types
   -- , Positive, NonZero(..), NonNegative(..)
@@ -43,15 +44,29 @@
   , arbitrarySatisfying
   ) where
 
--- import Data.Function (on)
-import Data.Monoid
 import Data.Function (on)
 import Control.Applicative
 import Control.Arrow ((***),first)
 import qualified Control.Exception as Ex
 import Data.List (foldl')
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Monoid hiding (First, Last)
+
+import Data.Complex
+import Data.Proxy
+import Data.Ratio
+import Data.Functor.Identity
+
+#if __GLASGOW_HASKELL__ >= 800
+import Data.Functor.Compose
+import qualified Data.Functor.Product as F
+import qualified Data.Functor.Sum as F
+#endif
+import Data.Semigroup
+import GHC.Generics
 import System.Random
-import Test.QuickCheck
+import Test.QuickCheck hiding (generate)
+import Test.QuickCheck.Random (QCGen, newQCGen)
 -- import System.IO.Unsafe
 
 import Test.QuickCheck.Gen      (Gen (..)) -- for rand
@@ -83,17 +98,21 @@
 
 -- TODO: consider a tree structure so that flattening is unnecessary.
 
+type QuickCheckRunner = Args -> Property -> IO ()
+
 -- | Run a batch of tests.  See 'quickBatch' and 'verboseBatch'.
-checkBatch :: Args -> TestBatch -> IO ()
-checkBatch args (name,tests) =
+checkBatch' :: QuickCheckRunner -> Args -> TestBatch -> IO ()
+checkBatch' runner args (name,tests) =
   do putStrLn $ "\n" ++ name ++ ":"
      mapM_ pr tests
  where
    pr (s,p) = do putStr (padTo (width + 4) ("  "++s ++ ":"))
-                 Ex.catch (quickCheckWith args p) 
+                 Ex.catch (runner args p)
                           (print :: Ex.SomeException -> IO ())
    width    = foldl' max 0 (map (length.fst) tests)
 
+checkBatch :: Args -> TestBatch -> IO ()
+checkBatch = checkBatch' quickCheckWith
 
 padTo :: Int -> String -> String
 padTo n = take n . (++ repeat ' ')
@@ -101,18 +120,14 @@
 -- | Check a batch tersely.
 quickBatch :: TestBatch -> IO ()
 quickBatch = checkBatch quick'
- 
+
 -- | Check a batch verbosely.
 verboseBatch :: TestBatch -> IO ()
-verboseBatch = checkBatch verbose'
+verboseBatch = checkBatch' verboseCheckWith quick'
 
-quick', verbose' :: Args
+quick' :: Args
 quick'   = stdArgs { maxSuccess = 500 }
-verbose' = quick'
-           -- quick' { configEvery = \ n args -> show n ++ ":\n" ++ unlines args }
 
--- TODO: Restore verbose functionality.  How in QC2?
-
 {-
 
 -- TODO: change TestBatch to be hierarchical/recursive, rather than
@@ -149,11 +164,15 @@
 genR :: Random a => (a, a) -> Gen a
 genR (lo,hi) = fmap (fst . randomR (lo,hi)) rand
 
+-- | @f@ is its own inverse. See also 'inverse'.
+involution :: (Show a, Arbitrary a, EqProp a) =>
+              (a -> a) -> Property
+involution f = f `inverseL` f
 
 -- | @f@ is a left inverse of @g@.  See also 'inverse'.
 inverseL :: (EqProp b, Arbitrary b, Show b) =>
             (a -> b) -> (b -> a) -> Property
-f `inverseL` g = f . g =-= id 
+f `inverseL` g = f . g =-= id
 
 -- | @f@ is a left and right inverse of @g@.  See also 'inverseL'.
 inverse :: ( EqProp a, Arbitrary a, Show a
@@ -170,50 +189,107 @@
 
 -- | Types of values that can be tested for equality, perhaps through
 -- random sampling.
-class EqProp a where (=-=) :: a -> a -> Property
+class EqProp a where
+  (=-=) :: a -> a -> Property
+  default (=-=) :: (Generic a, GEqProp (Rep a)) => a -> a -> Property
+  (=-=) = geq `on` from
+  {-# INLINEABLE (=-=) #-}
 
+class GEqProp g where
+  geq :: g x -> g x -> Property
+
+instance GEqProp g => GEqProp (M1 _1 _2 g) where
+  geq = geq `on` unM1
+  {-# INLINEABLE geq #-}
+
+instance (GEqProp g1, GEqProp g2) => GEqProp (g1 :*: g2) where
+  geq (g1a :*: g1b) (g2a :*: g2b) = geq g1a g2a .&&. geq g1b g2b
+  {-# INLINEABLE geq #-}
+
+instance (GEqProp g1, GEqProp g2) => GEqProp (g1 :+: g2) where
+  geq (L1 g1) (L1 g2) = geq g1 g2
+  geq (R1 g1) (R1 g2) = geq g1 g2
+  geq _ _             = property False
+  {-# INLINEABLE geq #-}
+
+instance EqProp a => GEqProp (K1 _1 a) where
+  geq = (=-=) `on` unK1
+  {-# INLINEABLE geq #-}
+
+instance GEqProp U1 where
+  geq U1 U1 = property True
+  {-# INLINEABLE geq #-}
+
+instance GEqProp V1 where
+  geq _ _ = property True
+  {-# INLINEABLE geq #-}
+
 -- | For 'Eq' types as 'EqProp' types
 eq :: Eq a => a -> a -> Property
 a `eq` a' = property (a == a')
 
+
 -- Template: fill in with Eq types for a
 --   instance EqProp a where (=-=) = eq
 -- E.g.,
 
-instance EqProp Bool   where (=-=) = eq
-instance EqProp Char   where (=-=) = eq
-instance EqProp Int    where (=-=) = eq
-instance EqProp Float  where (=-=) = eq
-instance EqProp Double where (=-=) = eq
+instance EqProp ()
+instance EqProp Bool
+instance EqProp Char where (=-=) = eq
+instance EqProp Ordering
 
+-- Numeric
+instance EqProp Int     where (=-=) = eq
+instance EqProp Float   where (=-=) = eq
+instance EqProp Double  where (=-=) = eq
+instance EqProp Integer where (=-=) = eq
+instance Eq a => EqProp (Complex a) where (=-=) = eq
+instance Eq a => EqProp (Ratio a) where (=-=) = eq
+
+-- Semigroups
+instance EqProp a => EqProp (Min a)
+instance EqProp a => EqProp (Max a)
+instance EqProp a => EqProp (First a)
+instance EqProp a => EqProp (Last a)
+
+-- Monoids
+instance EqProp a => EqProp (Dual a)
+instance (Show a, Arbitrary a, EqProp a) => EqProp (Endo a)
+instance EqProp All
+instance EqProp Any
+instance EqProp a => EqProp (Sum a)
+instance EqProp a => EqProp (Product a)
+instance EqProp (f a) => EqProp (Alt f a)
+#if __GLASGOW_HASKELL__ >= 806
+instance EqProp (f a) => EqProp (Ap f a)
+#endif
+
 -- Lists
-instance EqProp a => EqProp [a] where
-    [] =-= [] = property True
-    x:xs =-= y:ys = x =-= y .&. xs =-= ys
-    _ =-= _ = property False
+instance EqProp a => EqProp [a]
+instance EqProp a => EqProp (NonEmpty a)
+instance EqProp a => EqProp (ZipList a)
 
 -- Maybe
-instance EqProp a => EqProp (Maybe a) where
-    Nothing =-= Nothing = property True
-    Just x =-= Just y = x =-= y
-    _ =-= _ = property False
+instance EqProp a => EqProp (Maybe a)
 
 -- Pairing
-instance (EqProp a, EqProp b) => EqProp (a,b) where
-  (a,b) =-= (a',b') = a =-= a' .&. b =-= b'
-
-instance (EqProp a, EqProp b, EqProp c) => EqProp (a,b,c) where
-  (a,b,c) =-=(a',b',c') = a =-= a' .&. b =-= b' .&. c =-= c'
-
-instance (EqProp a, EqProp b, EqProp c, EqProp d) => EqProp (a,b,c,d) where
-  (a,b,c,d) =-=(a',b',c',d') = a =-= a' .&. b =-= b' .&. c =-= c' .&. d =-= d'
+instance (EqProp a, EqProp b) => EqProp (a,b)
+instance (EqProp a, EqProp b, EqProp c) => EqProp (a,b,c)
+instance (EqProp a, EqProp b, EqProp c, EqProp d) => EqProp (a,b,c,d)
 
 -- Either
-instance (EqProp a, EqProp b) => EqProp (Either a b) where
-  (Left x)  =-=  (Left x') = x =-= x'
-  (Right x) =-= (Right x') = x =-= x'
-  _         =-=          _ = property False
+instance (EqProp a, EqProp b) => EqProp (Either a b)
 
+-- Functors
+#if __GLASGOW_HASKELL__ >= 800
+instance EqProp (f (g a)) => EqProp (Compose f g a)
+instance (EqProp (f a), EqProp (g a)) => EqProp (F.Sum f g a)
+instance (EqProp (f a), EqProp (g a)) => EqProp (F.Product f g a)
+#endif
+instance EqProp a => EqProp (Identity a)
+instance EqProp a => EqProp (Const a b)
+instance EqProp (Proxy a)
+
 -- Function equality
 instance (Show a, Arbitrary a, EqProp b) => EqProp (a -> b) where
   f =-= f' = property (liftA2 (=-=) f f')
@@ -225,6 +301,19 @@
 eqModels :: (Model a b, EqProp b) => a -> a -> Property
 eqModels = (=-=) `on` model
 
+
+-- | @f `'denotationFor'` g@ proves that @f@ is a model for @g@, ie that
+-- @'model' . g '=-=' f@.
+denotationFor
+    :: (Model b b', Arbitrary a, EqProp b', Show a)
+    => (a -> b')
+    -> (a -> b)
+    -> TestBatch
+denotationFor f g =
+  ( "denotation"
+  , [("eq", model . g =-= f)]
+  )
+
 -- Other types
 -- instance EqProp a => EqProp (S.Stream a) where (=-=) = eqModels
 
@@ -257,18 +346,13 @@
     forAll (gen a) $ \ b ->
       (a `rel` b) ==> (b `rel` a)
 
--- | Symmetric property: @a `rel` b && b `rel` a ==> a == b@.  Generate
--- @a@ randomly, but use @gen a@ to generate @b@.  @gen@ ought to satisfy
--- both @rel@ directions fairly often but not always.
+-- | Antisymmetric property: @(a `rel` b) && (a /= b) ==> not (b `rel` a)@.
+--
+-- @since 0.5.0
 antiSymmetric :: (Arbitrary a, Show a, Eq a) =>
-                 BinRel a -> (a -> Gen a) -> Property
-antiSymmetric rel gen =
-  property $ \ a ->
-    forAll (gen a) $ \ b ->
-      (a `rel` b) && (b `rel` a) ==> a == b
-
-
-
+                 BinRel a -> Property
+antiSymmetric rel =
+  property $ \ a b -> (a `rel` b) && (a /= b) ==> not (b `rel` a)
 
 -- | Has a given left identity, according to '(=-=)'
 leftId :: (Show a, Arbitrary a, EqProp a) => (i -> a -> a) -> i -> Property
@@ -363,11 +447,11 @@
 
 meq  :: (Model a b, EqProp b) => a -> b -> Property
 meq1 :: (Model a b, Model a1 b1, EqProp b) =>
-	(a1 -> a) -> (b1 -> b) -> a1 -> Property
+        (a1 -> a) -> (b1 -> b) -> a1 -> Property
 meq2 :: (Model a b, Model a1 b1, Model a2 b2, EqProp b) =>
-	(a1 -> a2 -> a) -> (b1 -> b2 -> b) -> a1 -> a2 -> Property
+        (a1 -> a2 -> a) -> (b1 -> b2 -> b) -> a1 -> a2 -> Property
 meq3 :: (Model a b, Model a1 b1, Model a2 b2, Model a3 b3, EqProp b) =>
-	(a1 -> a2 -> a3 -> a)
+        (a1 -> a2 -> a3 -> a)
      -> (b1 -> b2 -> b3 -> b)
      -> a1 -> a2 -> a3 -> Property
 meq4 :: ( Model a b, Model a1 b1, Model a2 b2
@@ -377,7 +461,7 @@
      -> a1 -> a2 -> a3 -> a4 -> Property
 meq5 :: ( Model a b, Model a1 b1, Model a2 b2, Model a3 b3
         , Model a4 b4, Model a5 b5, EqProp b) =>
-	(a1 -> a2 -> a3 -> a4 -> a5 -> a)
+        (a1 -> a2 -> a3 -> a4 -> a5 -> a)
      -> (b1 -> b2 -> b3 -> b4 -> b5 -> b)
      -> a1 -> a2 -> a3 -> a4 -> a5 -> Property
 
@@ -404,10 +488,13 @@
 instance Model Double Double where model = id
 instance Model String String where model = id
 
--- This next one requires UndecidableInstances
+-- These next two require UndecidableInstances
 instance (Model a b, Model a' b') => Model (a,a') (b,b') where
   model = model *** model
 
+instance Model b b' => Model (a -> b) (a -> b') where
+  model f = model . f
+
 -- instance Model (S.Stream a) (NonNegative Int -> a) where
 --   model s (NonNegative i) = s S.!! i
 
@@ -442,12 +529,13 @@
 
 -- | Generate n arbitrary values
 arbs :: Arbitrary a => Int -> IO [a]
-arbs n = fmap (\ rnd -> generate n rnd (vector n)) newStdGen
 
+arbs n = fmap (\ rnd -> generate n rnd (vector n)) newQCGen
+
 -- | Produce n values from a generator
 gens :: Int -> Gen a -> IO [a]
 gens n gen =
-  fmap (\ rnd -> generate 1000 rnd (sequence (replicate n gen))) newStdGen
+  fmap (\ rnd -> generate 1000 rnd (sequence (replicate n gen))) newQCGen
 
 -- The next two are from twanvl:
 
@@ -500,10 +588,10 @@
 
 -- TODO: are there QC2 replacements for these QC1 operations?
 
-rand :: Gen StdGen
+rand :: Gen QCGen
 rand = MkGen (\r _ -> r)
 
-generate :: Int -> StdGen -> Gen a -> a
+generate :: Int -> QCGen -> Gen a -> a
 generate n rnd (MkGen m) = m rnd' size
  where
   (size, rnd') = randomR (0, n) rnd
diff --git a/src/Test/QuickCheck/Classes.hs b/src/Test/QuickCheck/Classes.hs
--- a/src/Test/QuickCheck/Classes.hs
+++ b/src/Test/QuickCheck/Classes.hs
@@ -1,35 +1,47 @@
 {-# LANGUAGE ScopedTypeVariables, FlexibleContexts, KindSignatures
-           , Rank2Types, TypeOperators
+           , Rank2Types, TypeApplications, TypeOperators, CPP
   #-}
 
-{-# OPTIONS_GHC -Wall #-}
 ----------------------------------------------------------------------
 -- |
 -- Module      :  Test.QuickCheck.Classes
 -- Copyright   :  (c) Conal Elliott 2008
 -- License     :  BSD3
--- 
+--
 -- Maintainer  :  conal@conal.net
 -- Stability   :  experimental
--- 
+--
 -- Some QuickCheck properties for standard type classes
 ----------------------------------------------------------------------
 
 module Test.QuickCheck.Classes
   ( ordRel, ord, ordMorphism, semanticOrd
+  , semigroup
   , monoid, monoidMorphism, semanticMonoid
   , functor, functorMorphism, semanticFunctor, functorMonoid
+  , apply, applyMorphism, semanticApply
   , applicative, applicativeMorphism, semanticApplicative
+  , bind, bindMorphism, semanticBind, bindApply
   , monad, monadMorphism, semanticMonad, monadFunctor
-  , monadApplicative, arrow, arrowChoice, traversable
-  , monadPlus, monadOr
+  , monadApplicative, arrow, arrowChoice, foldable, foldableFunctor, bifoldable, bifoldableBifunctor, traversable
+  , monadPlus, monadOr, alt, alternative
   )
   where
 
-import Data.Monoid
-import Data.Foldable (foldMap)
-import Data.Traversable (Traversable (..), fmapDefault, foldMapDefault)
-import Control.Applicative
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifunctor hiding (first, second)
+import Data.Foldable (Foldable(..))
+import Data.Functor.Apply (Apply ((<.>)))
+import Data.Functor.Alt (Alt ((<!>)))
+import Data.Functor.Bind (Bind ((>>-)), apDefault)
+import qualified Data.Functor.Bind as B (Bind (join))
+import Data.Functor.Compose (Compose (..))
+import Data.Functor.Identity (Identity (..))
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Semigroup (Semigroup (..))
+import Data.Monoid (Endo(..), Dual(..), Sum(..), Product(..))
+import Data.Traversable (fmapDefault, foldMapDefault)
+import Control.Applicative (Alternative(..))
 import Control.Monad (MonadPlus (..), ap, join)
 import Control.Arrow (Arrow,ArrowChoice,first,second,left,right,(>>>),arr)
 import Test.QuickCheck
@@ -39,27 +51,47 @@
 import Test.QuickCheck.Instances.Char ()
 
 
--- | Total ordering.  @gen a@ ought to generate values @b@ satisfying @a
--- `rel` b@ fairly often.
-ordRel :: forall a. (Ord a, Show a, Arbitrary a, EqProp a) =>
+-- | Total ordering.
+--
+-- @gen a@ ought to generate values @b@ satisfying @a `rel` b@ fairly often.
+ordRel :: forall a. (Ord a, Show a, Arbitrary a) =>
           BinRel a -> (a -> Gen a) -> TestBatch
 ordRel rel gen =
   ( "ord"
   , [ ("reflexive"    , reflexive     rel    )
     , ("transitive"   , transitive    rel gen)
-    , ("antiSymmetric", antiSymmetric rel gen)
+    , ("antiSymmetric", antiSymmetric rel    )
     ]
   )
 
--- | Total ordering
-ord :: forall a. (Ord a, Show a, Arbitrary a, EqProp a) =>
+-- | 'Ord' laws.
+--
+-- @gen a@ ought to generate values @b@ satisfying @a `rel` b@ fairly often.
+ord :: forall a. (Ord a, Show a, Arbitrary a) =>
        (a -> Gen a) -> TestBatch
-ord = ordRel (<=)
-
-
+ord gen =
+    ( "Ord"
+    , [ ("Reflexivity of (<=)", reflexive le)
+      , ("Transitivity of (<=)", transitive le gen)
+      , ("Antisymmetry of (<=)", antiSymmetric le)
+      , ("x >= y = y <= x", p (\x y -> (x >= y) === (y <= x)))
+      , ("x < y = x <= y && x /= y", p (\x y -> (x < y) === (x <= y && x /= y)))
+      , ("x > y = y < x", p (\x y -> (x > y) === (y < x)))
+      , ("x < y = compare x y == LT", p (\x y -> (x < y) === (compare x y == LT)))
+      , ("x > y = compare x y == GT", p (\x y -> (x > y) === (compare x y == GT)))
+      , ("x == y = compare x y == EQ", p (\x y -> (x == y) === (compare x y == EQ)))
+      , ("min x y == if x <= y then x else y = True", p (\x y -> min x y === if x <= y then x else y))
+      , ("max x y == if x >= y then x else y = True", p (\x y -> max x y === if x >= y then x else y))
+      ]
+    )
+  where
+    le :: a -> a -> Bool
+    le = (<=)
+    p :: (a -> a -> Property) -> Property
+    p = property
 
 -- | 'Ord' morphism properties.  @h@ is an 'Ord' morphism iff:
--- 
+--
 -- >    a <= b = h a <= h b
 -- >
 -- >    h (a `min` b) = h a `min` h b
@@ -76,7 +108,7 @@
  where
    distrib  :: (forall c. Ord c => c -> c -> c) -> Property
    distrib  op = property $ \ u v -> h (u `op` v) =-= h u `op` h v
-   
+
    distrib' :: EqProp d => (forall c. Ord c => c -> c -> d) -> Property
    distrib' op = property $ \ u v -> u `op` v =-= h u `op` h v
 
@@ -102,9 +134,41 @@
                , [ ("left  identity", leftId  mappend (mempty :: a))
                  , ("right identity", rightId mappend (mempty :: a))
                  , ("associativity" , isAssoc (mappend :: Binop a))
+#if MIN_VERSION_base(4,11,0)
+                 , ("mappend = (<>)", property monoidSemigroupP)
+#endif
+                 , ("mconcat", property mconcatP)
                  ]
                )
+  where
+#if MIN_VERSION_base(4,11,0)
+    monoidSemigroupP :: a -> a -> Property
+    monoidSemigroupP x y = mappend x y =-= x <> y
+#endif
+    mconcatP :: [a] -> Property
+    mconcatP as = mconcat as =-= foldr mappend mempty as
 
+-- | Properties to check that the 'Semigroup' 'a' satisfies the semigroup
+-- properties.  The argument value is ignored and is present only for its
+-- type.
+--
+-- @since 0.5.0
+semigroup :: forall a n.
+             ( Semigroup a, Show a, Arbitrary a, EqProp a
+             , Integral n, Show n, Arbitrary n) =>
+             (a, n) -> TestBatch
+semigroup = const ( "semigroup"
+                  , [("associativity", isAssoc ((<>) :: Binop a))
+                    ,("sconcat", property sconcatP)
+                    ,("stimes", property stimesP)
+                    ]
+                  )
+  where
+    sconcatP :: a -> [a] -> Property
+    sconcatP a as = sconcat (a :| as) =-= foldr1 (<>) (a :| as)
+    stimesP :: Positive n -> a -> Property
+    stimesP (Positive n) a = stimes n a =-= foldr1 (<>) (replicate (fromIntegral n) a)
+
 -- | Monoid homomorphism properties.  See also 'homomorphism'.
 monoidMorphism :: (Monoid a, Monoid b, EqProp b, Show a, Arbitrary a) =>
                   (a -> b) -> TestBatch
@@ -127,7 +191,8 @@
   ( Functor m
   , Monoid (m a)
   , Monoid (m b)
-  , Arbitrary (a->b)
+  , CoArbitrary a
+  , Arbitrary b
   , Arbitrary (m a)
   , Show (m a)
   , EqProp (m b)) =>
@@ -143,7 +208,7 @@
     binopP :: (a->b) -> (m a) -> (m a) -> Property
     binopP f u v = (fmap f) (u `mappend` v) =-= (fmap f u) `mappend` (fmap f v)
 
--- <camio> There I have an attempt at doing this. I eventually implemented 
+-- <camio> There I have an attempt at doing this. I eventually implemented
 -- those semanticMorphisms as their own functions. I'm not too thrilled with
 -- that implementation, but it works.
 
@@ -153,7 +218,7 @@
 -- properties.
 functor :: forall m a b c.
            ( Functor m
-           , Arbitrary a, Arbitrary b, Arbitrary c
+           , Arbitrary b, Arbitrary c
            , CoArbitrary a, CoArbitrary b
            , Show (m a), Arbitrary (m a), EqProp (m a), EqProp (m c)) =>
            m (a,b,c) -> TestBatch
@@ -164,15 +229,15 @@
  where
    identityP :: Property
    composeP  :: (b -> c) -> (a -> b) -> Property
-   
+
    identityP = fmap id =-= (id :: m a -> m a)
    composeP g f = fmap g . fmap f =-= (fmap (g.f) :: m a -> m c)
 
 -- Note the similarity between 'functor' and 'monoidMorphism'.  The
 -- functor laws say that 'fmap' is a homomorphism w.r.t '(.)':
--- 
+--
 --   functor = const ("functor", homomorphism endoMonoidD endoMonoidD fmap)
--- 
+--
 -- However, I don't think the types can work out, since 'fmap' is used at
 -- three different types.
 
@@ -207,8 +272,66 @@
 semanticFunctor = const (functorMorphism (model1 :: forall b. f b -> g b))
 
 
--- | Properties to check that the 'Applicative' @m@ satisfies the monad
+-- | Properties to check that the 'Apply' @m@ satisfies the apply
 -- properties
+apply :: forall m a b c.
+         ( Apply m
+         , CoArbitrary a, Arbitrary b, CoArbitrary b
+         , Arbitrary c, Arbitrary (m a)
+         , Arbitrary (m (b -> c)), Show (m (b -> c))
+         , Arbitrary (m (a -> b)), Show (m (a -> b))
+         , Show (m a)
+         , EqProp (m c)
+         ) =>
+         m (a,b,c) -> TestBatch
+apply = const ( "apply"
+              , [ ("associativity", property associativityP)
+                , ("left"       , property leftP)
+                , ("right"      , property rightP)
+                ]
+              )
+ where
+   associativityP :: m (b -> c) -> m (a -> b) -> m a -> Property
+   rightP         :: (b -> c) -> m (a -> b) -> m a -> Property
+   leftP          :: (a -> b) -> m (b -> c) -> m a -> Property
+
+   associativityP u v w = ((.) <$> u <.> v <.> w) =-= (u <.> (v <.> w))
+   leftP f x y          = (x <.> (f <$> y)) =-= ((. f) <$> x <.> y)
+   rightP f x y         = (f <$> (x <.> y)) =-= ((f .) <$> x <.> y)
+
+
+-- | 'Apply' morphism properties
+applyMorphism :: forall f g.
+                 ( Apply f, Apply g
+                 , Show (f NumT), Arbitrary (f NumT)
+                 , EqProp (g T)
+                 , Show (f (NumT -> T))
+                 , Arbitrary (f (NumT -> T))
+                 ) =>
+                 (forall a. f a -> g a) -> TestBatch
+applyMorphism q =
+  ( "apply morphism"
+  , [ ("apply", property applyP)] )
+ where
+   applyP :: f (NumT->T) -> f NumT -> Property
+   applyP mf mx = q (mf <.> mx) =-= (q mf <.> q mx)
+
+
+-- | The semantic function ('model1') for @f@ is an 'applyMorphism'.
+semanticApply :: forall f g.
+                 ( Model1 f g
+                 , Apply f, Apply g
+                 , Arbitrary (f NumT), Arbitrary (f (NumT -> T))
+                 , EqProp (g T)
+                 , Show (f NumT), Show (f (NumT -> T))
+                 ) =>
+                 f () -> TestBatch
+semanticApply =
+  const (applyMorphism (model1 :: forall b. f b -> g b))
+
+
+-- | Properties to check that the 'Applicative' @m@ satisfies the applicative
+-- properties
 applicative :: forall m a b c.
                ( Applicative m
                , Arbitrary a, CoArbitrary a, Arbitrary b, Arbitrary (m a)
@@ -232,7 +355,7 @@
    homomorphismP :: (a -> b) -> a -> Property
    interchangeP  :: m (a -> b) -> a -> Property
    functorP      :: (a -> b) -> m a -> Property
-   
+
    identityP v        = (pure id <*> v) =-= v
    compositionP u v w = (pure (.) <*> u <*> v <*> w) =-= (u <*> (v <*> w))
    homomorphismP f x  = (pure f <*> pure x) =-= (pure (f x) :: m b)
@@ -255,7 +378,7 @@
  where
    pureP  :: NumT -> Property
    applyP :: f (NumT->T) -> f NumT -> Property
-   
+
    pureP a = q (pure a) =-= pure a
    applyP mf mx = q (mf <*> mx) =-= (q mf <*> q mx)
 
@@ -273,34 +396,115 @@
   const (applicativeMorphism (model1 :: forall b. f b -> g b))
 
 
+-- | Properties to check that the 'bind' @m@ satisfies the bind properties
+bind :: forall m a b c.
+        ( Bind m
+        , CoArbitrary a, CoArbitrary b
+        , Arbitrary (m a), EqProp (m a), Show (m a)
+        , Arbitrary (m b)
+        , Arbitrary (m c), EqProp (m c)
+        , Arbitrary (m (m (m a))), Show (m (m (m a)))
+        ) =>
+        m (a,b,c) -> TestBatch
+bind = const ( "bind laws"
+              , [ ("join associativity", property joinAssocP)
+                , ("bind associativity", property bindAssocP)
+                ]
+              )
+ where
+   bindAssocP :: m a -> (a -> m b) -> (b -> m c) -> Property
+   joinAssocP :: m (m (m a)) -> Property
+
+   bindAssocP m f g = ((m >>- f) >>- g) =-= (m >>- (\x -> f x >>- g))
+   joinAssocP mmma = B.join (B.join mmma) =-= B.join (fmap B.join mmma)
+
+bindApply :: forall m a b.
+             ( Bind m
+             , EqProp (m b)
+             , Show (m a), Arbitrary (m a)
+             , Show (m (a -> b)), Arbitrary (m (a -> b))) =>
+             m (a, b) -> TestBatch
+bindApply = const ( "bind apply"
+                  , [ ("ap", property apP) ]
+                  )
+ where
+   apP :: m (a -> b) -> m a -> Property
+   apP f x = (f <.> x) =-= (f `apDefault` x)
+
+-- | 'bind' morphism properties
+bindMorphism :: forall f g.
+                ( Bind f, Bind g
+                , Show (f NumT)
+                , Show (f (f (NumT -> T)))
+                , Arbitrary (f NumT), Arbitrary (f T)
+                , Arbitrary (f (f (NumT -> T)))
+                , EqProp (g T)
+                , EqProp (g (NumT -> T))
+                ) =>
+                (forall a. f a -> g a) -> TestBatch
+bindMorphism q =
+  ( "bind morphism"
+  , [ ("bind", property bindP), ("join", property joinP) ] )
+ where
+   bindP :: f NumT -> (NumT -> f T) -> Property
+   joinP :: f (f (NumT->T)) -> Property
+
+   bindP u k = q (u >>- k)  =-= (q u >>- q . k)
+   joinP uu  = q (B.join uu)  =-= B.join (fmap q (q uu))
+
+-- | The semantic function ('model1') for @f@ is a 'bindMorphism'.
+semanticBind :: forall f g.
+  ( Model1 f g
+  , Bind f, Bind g
+  , EqProp (g T)
+  , EqProp (g (NumT -> T))
+  , Arbitrary (f T) , Arbitrary (f NumT)
+  , Arbitrary (f (f (NumT -> T)))
+  , Show (f (f (NumT -> T)))
+  , Show (f NumT)
+  ) =>
+  f () -> TestBatch
+semanticBind = const (bindMorphism (model1 :: forall b. f b -> g b))
+
+
 -- | Properties to check that the 'Monad' @m@ satisfies the monad properties
 monad :: forall m a b c.
          ( Monad m
-         , Show a, Arbitrary a, CoArbitrary a, Arbitrary b, CoArbitrary b
+         , Show a, Arbitrary a, CoArbitrary a, CoArbitrary b
          , Arbitrary (m a), EqProp (m a), Show (m a)
          , Arbitrary (m b), EqProp (m b)
          , Arbitrary (m c), EqProp (m c)
+         , Show (m (a -> b)), Arbitrary (m (a -> b))
          ) =>
          m (a,b,c) -> TestBatch
 monad = const ( "monad laws"
               , [ ("left  identity", property leftP)
                 , ("right identity", property rightP)
                 , ("associativity" , property assocP)
+                , ("pure", property pureP)
+                , ("ap", property apP)
                 ]
               )
  where
    leftP  :: (a -> m b) -> a -> Property
    rightP :: m a -> Property
    assocP :: m a -> (a -> m b) -> (b -> m c) -> Property
-   
+   pureP :: a -> Property
+   apP :: m (a -> b) -> m a -> Property
+
    leftP f a    = (return a >>= f)  =-= f a
    rightP m     = (m >>= return)    =-=  m
    assocP m f g = ((m >>= f) >>= g) =-= (m >>= (\x -> f x >>= g))
+   pureP x = (pure x :: m a) =-= return x
+   apP f x = (f <*> x) =-= (f `ap` x)
 
 -- | Law for monads that are also instances of 'Functor'.
+--
+-- Note that instances that satisfy 'applicative' and 'monad'
+-- are implied to satisfy this property too.
 monadFunctor :: forall m a b.
-                ( Functor m, Monad m
-                , Arbitrary a, Arbitrary b, CoArbitrary a
+                ( Monad m
+                , Arbitrary b, CoArbitrary a
                 , Arbitrary (m a), Show (m a), EqProp (m b)) =>
                 m (a, b) -> TestBatch
 monadFunctor = const ( "monad functor"
@@ -309,8 +513,9 @@
    bindReturnP :: (a -> b) -> m a -> Property
    bindReturnP f xs = fmap f xs =-= (xs >>= return . f)
 
+-- | Note that 'monad' also contains these properties.
 monadApplicative :: forall m a b.
-                    ( Applicative m, Monad m
+                    ( Monad m
                     , EqProp (m a), EqProp (m b)
                     , Show a, Arbitrary a
                     , Show (m a), Arbitrary (m a)
@@ -332,12 +537,10 @@
 
 -- | 'Applicative' morphism properties
 monadMorphism :: forall f g.
-                 ( Monad f, Monad g, Functor g
+                 ( Monad f, Monad g
                  , Show (f NumT)
-                 , Show (f (NumT -> T))
                  , Show (f (f (NumT -> T)))
                  , Arbitrary (f NumT), Arbitrary (f T)
-                 , Arbitrary (f (NumT -> T))
                  , Arbitrary (f (f (NumT -> T)))
                  , EqProp (g NumT), EqProp (g T)
                  , EqProp (g (NumT -> T))
@@ -350,7 +553,7 @@
    returnP :: NumT -> Property
    bindP :: f NumT -> (NumT -> f T) -> Property
    joinP :: f (f (NumT->T)) -> Property
-   
+
    returnP a = q (return a) =-= return a
    bindP u k = q (u >>= k)  =-= (q u >>= q . k)
    joinP uu  = q (join uu)  =-= join (fmap q (q uu))
@@ -380,10 +583,8 @@
   , EqProp (g (NumT -> T))
   , Arbitrary (f T) , Arbitrary (f NumT)
   , Arbitrary (f (f (NumT -> T)))
-  , Arbitrary (f (NumT -> T))
   , Show (f (f (NumT -> T)))
-  , Show (f (NumT -> T)) , Show (f NumT)
-  , Functor g
+  , Show (f NumT)
   ) =>
   f () -> TestBatch
 semanticMonad = const (monadMorphism (model1 :: forall b. f b -> g b))
@@ -391,7 +592,7 @@
 -- | Laws for MonadPlus instances with left distribution.
 monadPlus :: forall m a b.
              ( MonadPlus m, Show (m a)
-             , Arbitrary a, CoArbitrary a, Arbitrary (m a), Arbitrary (m b)
+             , CoArbitrary a, Arbitrary (m a), Arbitrary (m b)
              , EqProp (m a), EqProp (m b)) =>
              m (a, b) -> TestBatch
 monadPlus = const ( "MonadPlus laws"
@@ -430,19 +631,36 @@
    leftZeroP k = (mzero >>= k) =-= mzero
    leftCatchP a b = return a `mplus` b =-= return a
 
+-- | Check Alt Semigroup law
+alt :: forall f a. ( Alt f, Arbitrary (f a)
+                   , EqProp (f a), Show (f a)) =>
+       f a -> TestBatch
+alt = const ( "Alt laws"
+            , [ ("associativity", isAssoc ((<!>) :: Binop (f a))) ] )
 
+
+-- | Check Alternative Monoid laws
+alternative :: forall f a. ( Alternative f, Arbitrary (f a)
+                           , EqProp (f a), Show (f a)) =>
+               f a -> TestBatch
+alternative = const ( "Alternative laws"
+                    , [ ("left identity", leftId (<|>) (empty :: f a))
+                      , ("right identity", rightId (<|>) (empty :: f a))
+                      , ("associativity", isAssoc ((<|>) :: Binop (f a)))
+                      ]
+                    )
+
+
 arrow :: forall a b c d e.
          ( Arrow a
          , Show (a d e), Show (a c d), Show (a b c)
-         , Show b, Show c, Show d, Show e
          , Arbitrary (a d e), Arbitrary (a c d), Arbitrary (a b c)
-         , Arbitrary b, Arbitrary c, Arbitrary d, Arbitrary e
+         , Arbitrary c, Arbitrary d, Arbitrary e
          , CoArbitrary b, CoArbitrary c, CoArbitrary d
          , EqProp (a b e), EqProp (a b d)
          , EqProp (a (b,d) c)
          , EqProp (a (b,d) (c,d)), EqProp (a (b,e) (d,e))
          , EqProp (a (b,d) (c,e))
-         , EqProp b, EqProp c, EqProp d, EqProp e
          ) =>
          a b (c,d,e) -> TestBatch
 arrow = const ("arrow laws"
@@ -460,21 +678,21 @@
   where
     assocP :: a b c -> a c d -> a d e -> Property
     assocP f g h = ((f >>> g) >>> h) =-= (f >>> (g >>> h))
-    
+
     arrDistributesP :: (b -> c) -> (c -> d) -> Property
     arrDistributesP f g = ((arr (f >>> g)) :: a b d) =-= (arr f >>> arr g)
-    
+
     firstAsFunP :: (b -> c) -> Property
     firstAsFunP f = (first (arr f) :: a (b,d) (c,d)) =-= arr (first f)
 
     firstKeepCompP :: a b c -> a c d -> Property
     firstKeepCompP f g =
       ((first (f >>> g)) :: (a (b,e) (d,e))) =-= (first f >>> first g)
- 
+
     firstIsFstP :: a b c -> Property
     firstIsFstP f = ((first f :: a (b,d) (c,d)) >>> arr fst)
                       =-= (arr fst >>> f)
-    
+
     secondMovesP :: (a b c) -> (d -> e) -> Property
     secondMovesP f g = (first f >>> second (arr g))
                          =-= ((second (arr g)) >>> first f)
@@ -483,7 +701,7 @@
                ( ArrowChoice a
                , Show (a b c)
                , Arbitrary (a b c)
-               , Arbitrary b, Arbitrary c, Arbitrary d, Arbitrary e
+               , Arbitrary c, Arbitrary e
                , CoArbitrary b, CoArbitrary d
                , EqProp (a (Either b d) (Either c e))
                , EqProp (a (Either b d) (Either c d))
@@ -503,20 +721,180 @@
     rightMovesP f g = (left f >>> right (arr g))
                         =-= ((right (arr g)) >>> left f)
 
-traversable :: forall f a b m.
-               ( Traversable f, Monoid m, Show (f a)
-               , Arbitrary (f a), Arbitrary b, Arbitrary a, Arbitrary m
-               , CoArbitrary a
-               , EqProp (f b), EqProp m) =>
-               f (a, b, m) -> TestBatch
-traversable = const ( "traversable"
-                    , [ ("fmap", property fmapP)
+traversable :: forall t a b c m f g.
+               ( Traversable t, Applicative f, Applicative g, Monoid m
+               , Arbitrary (t a), Arbitrary (t b), Arbitrary (f b), Arbitrary (g c)
+               , Arbitrary (t (f (g a)))
+               , Arbitrary m, Arbitrary b
+               , CoArbitrary a, CoArbitrary b
+               , Show (t a), Show (t b), Show (t (f (g a)))
+               , EqProp (t b), EqProp m, EqProp (f (g (t a))), EqProp (f (g (t c)))) => t (f a, g b, c, m)
+  -> TestBatch
+traversable = const ( "Traversable"
+                    , [ ("identity", property identityP)
+                      , ("composition", property compositionP)
+                      -- , ("naturality", property $ \(f :: f Int -> g Int) -> naturalityP f)
+                      , ("fmap", property fmapP)
                       , ("foldMap", property foldMapP)
+                      , ("sequenceA identity", property sequenceIdentityP)
+                      , ("sequenceA composition", property sequenceCompositionP)
+                      -- , ("sequenceA naturality", property $ \(f :: f a -> g a) -> sequenceNaturalityP f)
                       ]
                     )
  where
-   fmapP :: (a -> b) -> f a -> Property
-   foldMapP :: (a -> m) -> f a -> Property
+   identityP :: Property
+   identityP = traverse @t @_ @b Identity =-= Identity
 
+   compositionP :: (a -> f b) -> (b -> g c) -> Property
+   compositionP f g = traverse @t (Compose . fmap g . f) =-= Compose . fmap (traverse g) . traverse f
+
+   --FIXME: Does not compile due to rank2 type.
+   --naturalityP :: (forall x. (f x -> g x)) -> (a -> f b) -> Property
+   --naturalityP t f = t . traverse @t f =-= traverse (t . f)
+
+   fmapP :: (a -> b) -> t a -> Property
    fmapP f x = f `fmap` x =-= f `fmapDefault` x
-   foldMapP f x = f `foldMap` x =-= f `foldMapDefault` x
+
+   foldMapP :: (a -> m) -> t a -> Property
+   foldMapP f x = f `foldMap` x =-= (f `foldMapDefault` x :: m)
+
+   sequenceIdentityP :: Property
+   sequenceIdentityP = sequenceA @t @_ @b . fmap Identity =-= Identity
+
+   sequenceCompositionP :: Property
+   sequenceCompositionP = sequenceA @t @(Compose f g) @a . fmap Compose =-= Compose . fmap sequenceA . sequenceA
+
+   --FIXME: Does not compile due to rank2 type.
+   --sequenceNaturalityP :: (forall x. (f x -> g x)) -> Property
+   --sequenceNaturalityP t = t . sequenceA @t @_ @a =-= sequenceA . fmap t
+
+-- | Note that 'foldable' doesn't check the strictness of 'foldl'', `foldr'' and `foldMap''.
+--
+-- @since 0.4.13
+
+-- The (Arbitrary m) constraint is required with base >= 4.13, where we have an
+-- additional property for checking foldMap'.
+foldable :: forall t a b m n o.
+            ( Foldable t
+            , CoArbitrary a, CoArbitrary b
+            , Arbitrary a, Arbitrary b, Arbitrary m, Arbitrary o, Arbitrary (t a), Arbitrary (t m), Arbitrary (t n), Arbitrary (t o)
+            , Monoid m
+            , Num n
+            , Ord o
+            , EqProp m, EqProp n, EqProp b, EqProp o, EqProp a
+            , Show (t m), Show (t n), Show (t o), Show b, Show (t a), Show o) =>
+            t (a, b, m, n, o) -> TestBatch
+foldable = const ( "Foldable"
+                 , [ ("foldr and foldMap", property foldrFoldMapP)
+                   , ("foldl and foldMap", property foldlFoldMapP)
+                   , ("fold and foldMap", property foldFoldMapP)
+                   , ("length", property lengthP)
+#if MIN_VERSION_base(4,13,0)
+                   , ("foldMap'", property foldMap'P)
+#endif
+                   , ("foldr'", property foldr'P)
+                   , ("foldl'", property foldl'P)
+                   , ("foldr1", property foldr1P)
+                   , ("foldl1", property foldl1P)
+                   , ("toList", property toListP)
+                   , ("null", property nullP)
+                   , ("elem", property elemP)
+                   , ("maximum", property maximumP)
+                   , ("minimum", property minimumP)
+                   , ("sum", property sumP)
+                   , ("product", property productP)
+                   ]
+                 )
+  where
+    foldrFoldMapP :: (a -> b -> b) -> b -> t a -> Property
+    foldrFoldMapP f z t = foldr f z t =-= appEndo (foldMap (Endo . f) t ) z
+    foldlFoldMapP :: (b -> a -> b) -> b -> t a -> Property
+    foldlFoldMapP f z t = foldl f z t =-= appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z
+    foldFoldMapP :: t m -> Property
+    foldFoldMapP t = fold t =-= foldMap id t
+    lengthP :: t a -> Property
+    lengthP t = length t =-= (getSum . foldMap (Sum . const  1)) t
+#if MIN_VERSION_base(4,13,0)
+    -- TODO: Check strictness
+    foldMap'P :: (a -> m) -> t a -> Property
+    foldMap'P f t = foldMap' f t =-= foldl' (\acc a -> acc <> f a) mempty t
+#endif
+    sumP :: t n -> Property
+    sumP t = sum t =-= (getSum . foldMap Sum) t
+    productP :: t n -> Property
+    productP t = product t =-= (getProduct . foldMap Product) t
+    maximumP :: t o -> Property
+    maximumP t = not (null t) ==> maximum t =-= maximum (toList t)
+    minimumP :: t o -> Property
+    minimumP t = not (null t) ==> minimum t =-= minimum (toList t)
+    foldr1P :: (a -> a -> a) -> t a -> Property
+    foldr1P f t = not (null t) ==> foldr1 f t =-= foldr1 f (toList t)
+    foldl1P :: (a -> a -> a) -> t a -> Property
+    foldl1P f t = not (null t) ==> foldl1 f t =-= foldl1 f (toList t)
+    toListP :: t a -> Property
+    toListP t = toList t =-= foldr (:) [] t
+    nullP :: t a -> Property
+    nullP t = null t =-= foldr (const (const False)) True t
+    -- TODO: Check strictness
+    foldr'P :: (a -> b -> b) -> b -> t a -> Property
+    foldr'P f z t = foldr' f z t =-= foldr' f z (toList t)
+    -- TODO: Check strictness
+    foldl'P :: (b -> a -> b) -> b -> t a -> Property
+    foldl'P f z t = foldl' f z t =-= foldl' f z (toList t)
+    elemP :: o -> t o -> Property
+    elemP o t = elem o t =-= elem o (toList t)
+
+-- | @since 0.4.13
+foldableFunctor :: forall t a m.
+                   ( Functor t, Foldable t
+                   , CoArbitrary a
+                   , Arbitrary m, Arbitrary (t a)
+                   , EqProp m
+                   , Monoid m
+                   , Show (t a)) =>
+                   t (a, m) -> TestBatch
+foldableFunctor = const ( "Foldable Functor"
+                        , [ ("foldMap f = fold . fmap f", property foldMapP) ]
+                        )
+  where
+    foldMapP :: (a -> m) -> t a -> Property
+    foldMapP f t = foldMap f t =-= fold (fmap f t)
+
+-- | @since 0.5.7
+bifoldable :: forall p a b c m.
+               ( Bifoldable p, Monoid m
+               , Show (p a b), Show (p m m)
+               , Arbitrary (p a b), Arbitrary (p m m), Arbitrary m
+               , CoArbitrary a, CoArbitrary b
+               , EqProp m, EqProp c, CoArbitrary c, Arbitrary c, Show c) =>
+               p a (b, c, m)  -> TestBatch
+bifoldable = const ( "Bifoldable"
+                    , [ ("identity", property identityP)
+                      , ("bifoldMap f g ≡ bifoldr (mappend . f) (mappend . g) mempty", property bifoldMapBifoldrP)
+                      , ("bifoldr f g z t ≡ appEndo (bifoldMap (Endo . f) (Endo . g) t) z", property bifoldrBifoldMapP)
+                      ]
+                    )
+ where
+   identityP :: Property
+   identityP = bifold =-= (bifoldMap id id :: p m m -> m)
+
+   bifoldMapBifoldrP :: (a -> m) -> (b -> m) -> Property
+   bifoldMapBifoldrP f g = bifoldMap f g =-= (bifoldr (mappend . f) (mappend . g) mempty :: p a b -> m)
+
+   bifoldrBifoldMapP :: (a -> c -> c) -> (b -> c -> c) -> c -> p a b -> Property
+   bifoldrBifoldMapP f g z t = bifoldr f g z t =-= appEndo (bifoldMap (Endo . f) (Endo . g) t) z
+
+-- | @since 0.5.7
+bifoldableBifunctor :: forall p a b m.
+                       ( Bifoldable p, Bifunctor p, Monoid m
+                       , Show (p a b)
+                       , Arbitrary (p a b), Arbitrary m, CoArbitrary a, CoArbitrary b
+                       , EqProp m) =>
+                       p a (b, m) -> TestBatch
+bifoldableBifunctor = const ( "Bifoldable Bifunctor"
+                            , [ ("bifoldMap f g ≡  bifold . bimap f g", property bifoldBimapP) ]
+                            )
+  where
+    bifoldBimapP :: (a -> m) -> (b -> m) -> Property
+    bifoldBimapP f g = bifoldMap f g =-= (bifold . bimap f g :: p a b -> m)
+    
diff --git a/src/Test/QuickCheck/Instances.hs b/src/Test/QuickCheck/Instances.hs
--- a/src/Test/QuickCheck/Instances.hs
+++ b/src/Test/QuickCheck/Instances.hs
@@ -8,9 +8,9 @@
        ,module Test.QuickCheck.Instances.Ord
        ,module Test.QuickCheck.Instances.Tuple
        ) where
-       
+
 import Test.QuickCheck.Instances.Array ()
-import Test.QuickCheck.Instances.Char 
+import Test.QuickCheck.Instances.Char
 import Test.QuickCheck.Instances.Eq
 import Test.QuickCheck.Instances.List
 import Test.QuickCheck.Instances.Maybe
diff --git a/src/Test/QuickCheck/Instances/Array.hs b/src/Test/QuickCheck/Instances/Array.hs
--- a/src/Test/QuickCheck/Instances/Array.hs
+++ b/src/Test/QuickCheck/Instances/Array.hs
@@ -1,13 +1,14 @@
+{-# LANGUAGE CPP #-}
 {-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
+
 module Test.QuickCheck.Instances.Array where
 
 import Test.QuickCheck
-import Control.Applicative
 import Data.Array
 
 instance (Ix a, Integral a, Arbitrary b) => Arbitrary (Array a b) where
   arbitrary   =
-    (\x -> listArray (0,fromIntegral (length x - 1)) x) <$> arbitrary 
+    (\x -> listArray (0,fromIntegral (length x - 1)) x) <$> arbitrary
 
-instance (Ix a, Integral a, CoArbitrary b) => CoArbitrary (Array a b) where
+instance (CoArbitrary b) => CoArbitrary (Array a b) where
   coarbitrary = coarbitrary . elems
diff --git a/src/Test/QuickCheck/Instances/Eq.hs b/src/Test/QuickCheck/Instances/Eq.hs
--- a/src/Test/QuickCheck/Instances/Eq.hs
+++ b/src/Test/QuickCheck/Instances/Eq.hs
@@ -4,7 +4,7 @@
 import Test.QuickCheck.Checkers
 import Control.Monad.Extensions
 
-notEqualTo :: (Eq a,Arbitrary a) => a -> Gen a -> Gen a
+notEqualTo :: (Eq a) => a -> Gen a -> Gen a
 notEqualTo v = satisfiesM (/= v)
 
 notOneof :: (Eq a,Arbitrary a) => [a] -> Gen a
diff --git a/src/Test/QuickCheck/Instances/List.hs b/src/Test/QuickCheck/Instances/List.hs
--- a/src/Test/QuickCheck/Instances/List.hs
+++ b/src/Test/QuickCheck/Instances/List.hs
@@ -8,7 +8,7 @@
        ,decreasingInf,nonincreasingInf
        ) where
 
-import Test.QuickCheck
+import Test.QuickCheck hiding (infiniteList)
 import Test.QuickCheck.Instances.Num
 import Control.Applicative
 
diff --git a/src/Test/QuickCheck/Instances/Maybe.hs b/src/Test/QuickCheck/Instances/Maybe.hs
--- a/src/Test/QuickCheck/Instances/Maybe.hs
+++ b/src/Test/QuickCheck/Instances/Maybe.hs
@@ -1,7 +1,6 @@
 module Test.QuickCheck.Instances.Maybe (maybeGen) where
 
 import Test.QuickCheck
-import Control.Applicative
 
 maybeGen :: Gen a -> Gen (Maybe a)
 maybeGen x = oneof [pure Nothing
diff --git a/src/Test/QuickCheck/Instances/Num.hs b/src/Test/QuickCheck/Instances/Num.hs
--- a/src/Test/QuickCheck/Instances/Num.hs
+++ b/src/Test/QuickCheck/Instances/Num.hs
@@ -1,4 +1,4 @@
-module Test.QuickCheck.Instances.Num 
+module Test.QuickCheck.Instances.Num
        (nonNegative,nonPositive
        ,negative,positive
        ,nonZero,nonZero_
@@ -6,7 +6,6 @@
 
 import Test.QuickCheck
 import Control.Monad.Extensions
-import Control.Applicative
 
 nonNegative :: (Num a, Arbitrary a) => Gen a
 nonNegative = abs <$> arbitrary
@@ -20,7 +19,7 @@
 negative :: (Eq a, Num a, Arbitrary a) => Gen a
 negative = negate <$> positive
 
-nonZero :: (Eq a, Num a, Arbitrary a) => Gen a -> Gen a
+nonZero :: (Eq a, Num a) => Gen a -> Gen a
 nonZero g =
   sized (\s -> satisfiesM (/= 0) (if (s == 0) then (resize 1 g) else g))
 
diff --git a/src/Test/QuickCheck/Instances/Ord.hs b/src/Test/QuickCheck/Instances/Ord.hs
--- a/src/Test/QuickCheck/Instances/Ord.hs
+++ b/src/Test/QuickCheck/Instances/Ord.hs
@@ -3,8 +3,8 @@
 import Test.QuickCheck
 import Control.Monad.Extensions
 
-greaterThan :: (Ord a,Arbitrary a) => a -> Gen a -> Gen a
+greaterThan :: (Ord a) => a -> Gen a -> Gen a
 greaterThan v = satisfiesM (> v)
 
-lessThan :: (Ord a,Arbitrary a) => a -> Gen a -> Gen a
+lessThan :: (Ord a) => a -> Gen a -> Gen a
 lessThan v = satisfiesM (< v)
diff --git a/src/Test/QuickCheck/Later.hs b/src/Test/QuickCheck/Later.hs
--- a/src/Test/QuickCheck/Later.hs
+++ b/src/Test/QuickCheck/Later.hs
@@ -4,10 +4,10 @@
 -- Module      :  Data.Later
 -- Copyright   :  (c) David Sankel 2008
 -- License     :  BSD3
--- 
+--
 -- Maintainer  :  david@sankelsoftware.com
 -- Stability   :  experimental
--- 
+--
 -- Later. Allows for testing of functions that depend on the order of
 -- evaluation.
 --
@@ -45,7 +45,7 @@
            del t1 # del t2 =-= del t2 # del t1
 
 -- Note that we delay v by t1 and by t2 twice.
--- 
+--
 -- TODO: make sure CSE isn't kicking in.  Examine the core code.
 
 -- | Is the given function associative when restricted to the same value
@@ -75,7 +75,7 @@
 
 -- | A value that is never available.  Rerun of @hang@ from unamb, but
 -- replicated to avoid mutual dependency.
--- 
+--
 -- TODO: Remove when this module is moved into the unamb-test package.
 delayForever :: a
 delayForever = unsafePerformIO $ do _ <- forever (threadDelay maxBound)
diff --git a/src/Test/QuickCheck/Utils.hs b/src/Test/QuickCheck/Utils.hs
--- a/src/Test/QuickCheck/Utils.hs
+++ b/src/Test/QuickCheck/Utils.hs
@@ -1,9 +1,10 @@
+{-# OPTIONS_GHC -Wall #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Test.QuickCheck.Utils
 -- Copyright   :  (c) Andy Gill 2001
 -- License     :  BSD-style (see the file libraries/base/LICENSE)
--- 
+--
 -- Maintainer  :  libraries@haskell.org
 -- Stability   :  experimental
 -- Portability :  portable
@@ -25,29 +26,29 @@
 
 import Test.QuickCheck
 
-isAssociativeBy :: (Show a,Testable prop) 
-		=> (a -> a -> prop) -> Gen a -> (a -> a -> a) -> Property
-isAssociativeBy (===) src (#) = 
-     	forAll src $ \ a ->
-     	forAll src $ \ b ->
-     	forAll src $ \ c ->
-	((a # b) # c) === (a # (b # c))
+isAssociativeBy :: (Show a,Testable prop)
+                => (a -> a -> prop) -> Gen a -> (a -> a -> a) -> Property
+isAssociativeBy (=~=) src (#) =
+        forAll src $ \ a ->
+        forAll src $ \ b ->
+        forAll src $ \ c ->
+        ((a # b) # c) =~= (a # (b # c))
 
 isAssociative :: (Arbitrary a,Show a,Eq a) => (a -> a -> a) -> Property
 isAssociative = isAssociativeBy (==) arbitrary
 
-isCommutableBy :: (Show a,Testable prop) 
-	       => (b -> b -> prop) -> Gen a -> (a -> a -> b) -> Property
-isCommutableBy (===) src (#) =
-	forAll src $ \ a ->
-	forAll src $ \ b ->
-	(a # b) === (b # a)
+isCommutableBy :: (Show a,Testable prop)
+               => (b -> b -> prop) -> Gen a -> (a -> a -> b) -> Property
+isCommutableBy (=~=) src (#) =
+        forAll src $ \ a ->
+        forAll src $ \ b ->
+        (a # b) =~= (b # a)
 
 isCommutable :: (Arbitrary a,Show a,Eq b) => (a -> a -> b) -> Property
 isCommutable = isCommutableBy (==) arbitrary
 
-isTotalOrder :: (Arbitrary a,Show a,Ord a) => a -> a -> Property
-isTotalOrder x y = 
+isTotalOrder :: (Ord a) => a -> a -> Property
+isTotalOrder x y =
     classify (x > y)  "less than" $
     classify (x == y) "equals" $
     classify (x < y)  "greater than" $