diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,21 @@
+https://github.com/Lysxia/generic-random/blob/master/changelog.md
+
+# 1.0.0.0
+
+- Make the main module `Generic.Random`
+- Rework generic base case generation
+  + You can explicitly provide a trivial generator (e.g., returning a
+    nullary constructor) using `withBaseCase`
+  + Generically derive `BaseCaseSearch` and let `BaseCase` find small
+    values, no depth parameter must be specified anymore
+- Add `genericArbitrarySingle`, `genericArbitraryRec`, `genericArbitraryU'`
+- Deprecate `weights`
+- Fixed bug with `genericArbitrary'` not dividing the size parameter
+
 # 0.5.0.0
 
 - Turn off dependency on boltzmann-samplers by default
-- Add genericArbitraryU, genericArbitraryU0 and genericArbitraryU1
+- Add `genericArbitraryU`, `genericArbitraryU0` and `genericArbitraryU1`
 - Compatible with GHC 7.8.4 and GHC 7.10.3
 
 # 0.4.1.0
@@ -17,5 +31,5 @@
 # 0.3.0.0
 
 - Support GHC 7.10.3
-- Replace TypeApplications with ad-hoc data types in
-  genericArbitraryFrequency'/genericArbitrary'
+- Replace `TypeApplications` with ad-hoc data types in
+  `genericArbitraryFrequency'`/`genericArbitrary'`
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,20 +1,23 @@
 Generic random generators [![Hackage](https://img.shields.io/hackage/v/generic-random.svg)](https://hackage.haskell.org/package/generic-random) [![Build Status](https://travis-ci.org/Lysxia/generic-random.svg)](https://travis-ci.org/Lysxia/generic-random)
 =========================
 
-Say goodbye to `Constructor <$> arbitrary <*> arbitrary <*> arbitrary`-boilerplate.
+Derive simple random generators for [QuickCheck](https://hackage.haskell.org/package/QuickCheck) using generics.
 
+Example
+-------
+
 ```haskell
     {-# LANGUAGE DeriveGeneric #-}
 
-    import GHC.Generics ( Generic )
+    import GHC.Generics (Generic)
     import Test.QuickCheck
-    import Generic.Random.Generic
+    import Generic.Random
 
     data Tree a = Leaf | Node (Tree a) a (Tree a)
       deriving (Show, Generic)
 
     instance Arbitrary a => Arbitrary (Tree a) where
-      arbitrary = genericArbitrary' Z uniform
+      arbitrary = genericArbitraryRec uniform `withBaseCase` return Leaf
 
     -- Equivalent to
     -- > arbitrary =
@@ -24,14 +27,18 @@
     -- >     else
     -- >       oneof
     -- >         [ return Leaf
-    -- >         , Node <$> arbitrary <*> arbitrary <*> arbitrary
+    -- >         , resize (n `div` 3) $
+    -- >             Node <$> arbitrary <*> arbitrary <*> arbitrary
     -- >         ]
 
     main = sample (arbitrary :: Gen (Tree ()))
 ```
 
-- User-specified distribution of constructors, with a compile-time check that
-  weights have been specified for all constructors.
-- A simple (optional) strategy to ensure termination: `Test.QuickCheck.Gen`'s
-  size parameter decreases at every recursive `genericArbitrary'` call; when it
-  reaches zero, sample directly from a finite set of finite values.
+Features
+--------
+
+- User-specified distribution of constructors.
+- A simple (optional) strategy to ensure termination for recursive types:
+  using `genericArbitrary'`, `Test.QuickCheck.Gen`'s size parameter decreases
+  at every recursive call; when it reaches zero, sample directly from a
+  trivially terminating generator.
diff --git a/generic-random.cabal b/generic-random.cabal
--- a/generic-random.cabal
+++ b/generic-random.cabal
@@ -1,5 +1,5 @@
 name:                generic-random
-version:             0.5.0.0
+version:             1.0.0.0
 synopsis:            Generic random generators
 description:         Please see the README.
 homepage:            http://github.com/lysxia/generic-random
@@ -12,31 +12,32 @@
 build-type:          Simple
 extra-source-files:  README.md CHANGELOG.md
 cabal-version:       >=1.10
-tested-with:         GHC == 8.0.1
-
-flag boltzmann
-  Description:
-    Dependency on boltzmann-samplers for backwards compatibility.
-  Manual:  False
-  Default: False
+tested-with:         GHC == 8.0.1, GHC == 8.2.1
 
 library
   hs-source-dirs:      src
   exposed-modules:
+    Generic.Random
     Generic.Random.Generic
+    Generic.Random.Internal.BaseCase
     Generic.Random.Internal.Generic
+    Generic.Random.Tutorial
   build-depends:
-    base >= 4.7 && < 4.10,
+    base >= 4.7 && < 4.11,
     QuickCheck
-  if flag(boltzmann)
-    exposed-modules:
-      Generic.Random.Boltzmann
-      Generic.Random.Data
-    build-depends:
-      boltzmann-samplers <= 0.2
   default-language:    Haskell2010
   ghc-options: -Wall -fno-warn-name-shadowing
 
 source-repository head
   type:     git
   location: https://github.com/lysxia/generic-random
+
+test-suite unit
+  Hs-source-dirs:  test
+  Main-is:         Unit.hs
+  Build-depends:
+      base,
+      QuickCheck,
+      generic-random
+  Type: exitcode-stdio-1.0
+  Default-language: Haskell2010
diff --git a/src/Generic/Random.hs b/src/Generic/Random.hs
new file mode 100644
--- /dev/null
+++ b/src/Generic/Random.hs
@@ -0,0 +1,32 @@
+-- | Simple "GHC.Generics"-based 'arbitrary' generators.
+--
+-- For more information:
+--
+-- - "Generic.Random.Tutorial"
+-- - https://byorgey.wordpress.com/2016/09/20/the-generic-random-library-part-1-simple-generic-arbitrary-instances/
+
+module Generic.Random
+  (
+    -- * Arbitrary implementations
+    genericArbitrary
+  , genericArbitraryU
+  , genericArbitrarySingle
+  , genericArbitrary'
+  , genericArbitraryU'
+  , genericArbitraryRec
+
+    -- * Specifying finite distributions
+  , Weights
+  , W
+  , (%)
+  , uniform
+
+    -- * Base cases for recursive types
+  , withBaseCase
+  , BaseCase (..)
+
+  , weights
+  ) where
+
+import Generic.Random.Internal.BaseCase
+import Generic.Random.Internal.Generic
diff --git a/src/Generic/Random/Boltzmann.hs b/src/Generic/Random/Boltzmann.hs
deleted file mode 100644
--- a/src/Generic/Random/Boltzmann.hs
+++ /dev/null
@@ -1,7 +0,0 @@
-
-module Generic.Random.Boltzmann
-  {-# DEPRECATED "Directly use \"Boltzmann.Species\" from @boltzmann-samplers@ instead." #-}
-  ( module Boltzmann.Species
-  ) where
-
-import Boltzmann.Species
diff --git a/src/Generic/Random/Data.hs b/src/Generic/Random/Data.hs
deleted file mode 100644
--- a/src/Generic/Random/Data.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-module Generic.Random.Data
-  {-# DEPRECATED "Directly use \"Boltzmann.Data\" from @boltzmann-samplers@ instead." #-}
-  ( module Boltzmann.Data
-  ) where
-
-import Boltzmann.Data
diff --git a/src/Generic/Random/Generic.hs b/src/Generic/Random/Generic.hs
--- a/src/Generic/Random/Generic.hs
+++ b/src/Generic/Random/Generic.hs
@@ -1,213 +1,5 @@
--- | Simple 'GHC.Generics'-based 'arbitrary' generators.
---
--- Here is an example. Define your type.
---
--- @
--- data Tree a = Leaf a | Node (Tree a) (Tree a)
---   deriving Generic
--- @
---
--- Pick an 'arbitrary' implementation.
---
--- @
--- instance Arbitrary a => Arbitrary (Tree a) where
---   arbitrary = 'genericArbitrary' ('weights' (9 '%' 8 '%' ()))
--- @
---
--- @arbitrary :: 'Gen' (Tree a)@ picks a @Leaf@ with probability 9\/17, or a
--- @Node@ with probability 8\/17, and recursively fills their fields with
--- @arbitrary@.
---
--- == Distribution of constructors
---
--- The distribution of constructors can be specified using 'weights' applied to
--- a special list of /weights/ in the same order as the data type definition.
--- This assigns to each constructor a probability proportional to its weight;
--- in other words, @p_C = weight_C / sumOfWeights@.
---
--- The list of weights is built up with the @('%')@ operator as a cons, and using
--- the unit @()@ as the empty list, in the order corresponding to the data type
--- definition. The uniform distribution can be obtained with 'uniform'.
---
--- === Example
---
--- For @Tree@, 'genericArbitrary' produces code equivalent to the following:
---
--- @
--- 'genericArbitrary' :: Arbitrary a => 'Weights' (Tree a) -> Gen (Tree a)
--- 'genericArbitrary' ('weighted' (x '%' y '%' ())) =
---   frequency
---     [ (x, Leaf \<$\> arbitrary)
---     , (y, Node \<$\> arbitrary \<*\> arbitrary)
---     ]
--- @
---
--- === Uniform distribution
---
--- You can specify the uniform distribution (all weights equal) with 'uniform'.
--- 'genericArbitraryU' is available as a shorthand for
--- @'genericArbitrary' 'uniform'@.
---
--- Note that for many types, a uniform distribution tends to produce big
--- values. For instance for @Tree a@, generated values are finite but the
--- __average__ number of @Leaf@ and @Node@ constructors is __infinite__.
---
--- === Checked weights
---
--- /GHC 8.0.1 and above only./
---
--- The weights actually have type @'W' \"ConstructorName\"@ (just a newtype
--- around 'Int'), so that you can annotate a weight with its corresponding
--- constructor, and it will be checked that you got the order right.
---
--- This will type-check.
---
--- @
--- 'weighted' ((x :: 'W' \"Leaf\") '%' (y :: 'W' \"Node\") '%' ()) :: 'Weights' (Tree a)
--- 'weighted' (x '%' (y :: 'W' \"Node\") '%' ()) :: 'Weights' (Tree a)
--- @
---
--- This will not: the first requires an order of constructors different from
--- the definition of the @Tree@ type; the second doesn't have the right number
--- of weights.
---
--- @
--- 'weighted' ((x :: 'W' \"Node\") '%' y '%' ()) :: 'Weights' (Tree a)
--- 'weighted' (x '%' y '%' z '%' ()) :: 'Weights' (Tree a)
--- @
---
--- == Ensuring termination
---
--- As was just mentioned, one must be careful with recursive types
--- to avoid producing extremely large values.
---
--- The alternative 'genericArbitrary'' implements a simple strategy to keep
--- values at reasonable sizes: the size parameter of 'Gen' is divided among the
--- fields of the chosen constructor. When it reaches zero, the generator
--- selects a finite term whenever it can find any of the given type.  This
--- generally ensures that the number of constructors remains close to the
--- initial size parameter passed to 'Gen'.
---
--- A natural number @n@ determines the maximum /depth/ of terms that can be
--- used to end recursion.
--- It is encoded using @'Z' :: 'Z'@ and @'S' :: n -> 'S' n@.
---
--- @
--- 'genericArbitrary'' n ('weights' (...))
--- @
---
--- With @n = 'Z'@, the generator looks for a simple nullary constructor.  If none
--- exist at the current type, as is the case for our @Tree@ type, it carries on
--- as in 'genericArbitrary'.
---
--- @
--- 'genericArbitrary'' 'Z' :: Arbitrary a => 'Weights' (Tree a) -> Gen (Tree a)
--- 'genericArbitrary'' 'Z' ('weights' (x '%' y '%' ())) =
---   frequency
---     [ (x, Leaf \<$\> arbitrary)
---     , (y, scale (\`div\` 2) $ Node \<$\> arbitrary \<*\> arbitrary)
---     -- 2 because Node is 2-ary.
---     ]
--- @
---
--- Here is another example with nullary constructors:
---
--- @
--- data Tree' = Leaf1 | Leaf2 | Node3 Tree' Tree' Tree'
---   deriving Generic
---
--- instance Arbitrary Tree' where
---   arbitrary = 'genericArbitrary'' 'Z' ('weights' (1 '%' 2 '%' 3 '%' ()))
--- @
---
--- Here, @'genericArbitrary'' 'Z'@ is equivalent to:
---
--- @
--- 'genericArbitrary'' 'Z' :: 'Weights' Tree' -> Gen Tree'
--- 'genericArbitrary'' 'Z' ('weights' (x '%' y '%' z '%' ())) =
---   sized $ \n ->
---     if n == 0 then
---       -- If the size parameter is zero, the non-nullary alternative is discarded.
---       frequency $
---         [ (x, return Leaf1)
---         , (y, return Leaf2)
---         ]
---     else
---       frequency $
---         [ (x, return Leaf1)
---         , (y, return Leaf2)
---         , (z, resize (n \`div\` 3) node)  -- 3 because Node3 is 3-ary
---         ]
---   where
---     node = Node3 \<$\> arbitrary \<*\> arbitrary \<*\> arbitrary
--- @
---
--- To increase the chances of termination when no nullary constructor is directly
--- available, such as in @Tree@, we can pass a larger depth @n@. The effectiveness
--- of this parameter depends on the concrete type the generator is used for.
---
--- For instance, if we want to generate a value of type @Tree ()@, there is a
--- value of depth 1 (represented by @'S' 'Z'@) that we can use to end
--- recursion: @Leaf ()@.
---
--- @
--- 'genericArbitrary'' ('S' 'Z') :: 'Weights' (Tree ()) -> Gen (Tree ())
--- 'genericArbitrary'' ('S' 'Z') ('weights' (x '%' y '%' ())) =
---   sized $ \n ->
---     if n == 0 then
---       return (Leaf ())
---     else
---       frequency
---         [ (x, Leaf \<$\> arbitrary)
---         , (y, scale (\`div\` 2) $ Node \<$\> arbitrary \<*\> arbitrary)
---         ]
--- @
---
--- Because the argument of @Tree@ must be inspected in order to discover
--- values of type @Tree ()@, we incur some extra constraints if we want
--- polymorphism.
---
--- @UndecidableInstances@ is also required.
---
--- @
--- instance (Arbitrary a, Generic a, 'ListBaseCases' 'Z' (Rep a))
---   => Arbitrary (Tree a) where
---   arbitrary = 'genericArbitrary'' ('S' 'Z') ('weights' (1 '%' 2 '%' ()))
--- @
---
--- A synonym is provided for brevity.
---
--- @
--- instance (Arbitrary a, 'BaseCases'' Z a) => Arbitrary (Tree a) where
---   arbitrary = 'genericArbitrary'' ('S' 'Z') ('weights' (1 '%' 2 '%' ()))
--- @
-
-
-module Generic.Random.Generic
-  (
-    -- * Arbitrary implementations
-    genericArbitrary
-  , genericArbitraryU
-  , genericArbitrary'
-  , genericArbitraryU0
-  , genericArbitraryU1
-
-    -- * Specifying finite distributions
-  , Weights
-  , W
-  , weights
-  , (%)
-  , uniform
-
-    -- * Type-level natural numbers
-    -- $nat
-  , Z (..)
-  , S (..)
+-- | Reexport of "Generic.Random", for backwards-compatibility.
 
-    -- * Generic classes for finite values
-  , BaseCases'
-  , BaseCases
-  , ListBaseCases
-  ) where
+module Generic.Random.Generic ( module Generic.Random ) where
 
-import Generic.Random.Internal.Generic
+import Generic.Random
diff --git a/src/Generic/Random/Internal/BaseCase.hs b/src/Generic/Random/Internal/BaseCase.hs
new file mode 100644
--- /dev/null
+++ b/src/Generic/Random/Internal/BaseCase.hs
@@ -0,0 +1,320 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+#if __GLASGOW_HASKELL__ < 710
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+
+module Generic.Random.Internal.BaseCase where
+
+import Control.Applicative
+#if __GLASGOW_HASKELL__ >= 800
+import Data.Proxy
+#endif
+#if __GLASGOW_HASKELL__ < 710
+import Data.Word
+#endif
+import GHC.Generics
+import GHC.TypeLits
+import Test.QuickCheck
+
+import Generic.Random.Internal.Generic
+
+-- | Decrease size to ensure termination for
+-- recursive types, looking for base cases once the size reaches 0.
+--
+-- > genericArbitrary' (17 % 19 % 23 % ()) :: Gen a
+genericArbitrary'
+  :: (Generic a, GA Sized (Rep a), BaseCase a)
+  => Weights a  -- ^ List of weights for every constructor
+  -> Gen a
+genericArbitrary' w = genericArbitraryRec w `withBaseCase` baseCase
+
+-- | Equivalent to @'genericArbitrary'' 'uniform'@.
+--
+-- > genericArbitraryU :: Gen a
+genericArbitraryU'
+  :: (Generic a, GA Sized (Rep a), BaseCase a, UniformWeight_ (Rep a))
+  => Gen a
+genericArbitraryU' = genericArbitrary' uniform
+
+-- | Run the first generator if the size is positive.
+-- Run the second if the size is zero.
+--
+-- > defaultGen `withBaseCase` baseCaseGen
+withBaseCase :: Gen a -> Gen a -> Gen a
+withBaseCase def bc = sized $ \sz ->
+  if sz > 0 then def else bc
+
+
+-- | Find a base case of type @a@ with maximum depth @z@,
+-- recursively using 'BaseCaseSearch' instances to search deeper levels.
+--
+-- @y@ is the depth of a base case, if found.
+--
+-- @e@ is the original type the search started with, that @a@ appears in.
+-- It is used for error reporting.
+class BaseCaseSearch (a :: *) (z :: Nat) (y :: Maybe Nat) (e :: *) where
+  baseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy a
+
+
+instance {-# OVERLAPPABLE #-} GBaseCaseSearch a z y e => BaseCaseSearch a z y e where
+  baseCaseSearch = gBaseCaseSearch
+
+
+instance (y ~ 'Just 0) => BaseCaseSearch Char z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch Int z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch Integer z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch Float z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch Double z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch Word z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch () z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch Bool z y e where
+  baseCaseSearch _ _ = arbitrary
+
+instance (y ~ 'Just 0) => BaseCaseSearch [a] z y e where
+  baseCaseSearch _ _ = return []
+
+instance (y ~ 'Just 0) => BaseCaseSearch Ordering z y e where
+  baseCaseSearch _ _ = arbitrary
+
+-- Either and (,) use Generics
+
+
+class BaseCaseSearching_ a z y where
+  baseCaseSearching_ :: proxy y -> proxy2 '(z, a) -> IfM y Gen Proxy a -> Gen a
+
+instance BaseCaseSearching_ a z ('Just m) where
+  baseCaseSearching_ _ _ = id
+
+instance BaseCaseSearching a (z + 1) => BaseCaseSearching_ a z 'Nothing where
+  baseCaseSearching_ _ _ _ = baseCaseSearching (Proxy :: Proxy '(z + 1, a))
+
+-- | Progressively increase the depth bound for 'BaseCaseSearch'.
+class BaseCaseSearching a z where
+  baseCaseSearching :: proxy '(z, a) -> Gen a
+
+instance (BaseCaseSearch a z y a, BaseCaseSearching_ a z y) => BaseCaseSearching a z where
+  baseCaseSearching z = baseCaseSearching_ y z (baseCaseSearch y z)
+    where
+      y = Proxy :: Proxy y
+
+-- | Custom instances can override the default behavior.
+class BaseCase a where
+  -- | Generator of base cases.
+  baseCase :: Gen a
+
+-- | Overlappable
+instance {-# OVERLAPPABLE #-} BaseCaseSearching a 0 => BaseCase a where
+  baseCase = baseCaseSearching (Proxy :: Proxy '(0, a))
+
+
+type family IfM (b :: Maybe t) (c :: k) (d :: k) :: k
+type instance IfM ('Just t) c d = c
+type instance IfM 'Nothing c d = d
+
+type (==) m n = IsEQ (CmpNat m n)
+
+type family IsEQ (e :: Ordering) :: Bool
+type instance IsEQ 'EQ = 'True
+type instance IsEQ 'GT = 'False
+type instance IsEQ 'LT = 'False
+
+type family (||?) (b :: Maybe Nat) (c :: Maybe Nat) :: Maybe Nat
+type instance 'Just m ||? 'Just n = 'Just (Min m n)
+type instance m ||? 'Nothing = m
+type instance 'Nothing ||? n = n
+
+type family (&&?) (b :: Maybe Nat) (c :: Maybe Nat) :: Maybe Nat
+type instance 'Just m &&? 'Just n = 'Just (Max m n)
+type instance m &&? 'Nothing = 'Nothing
+type instance 'Nothing &&? n = 'Nothing
+
+type Max m n = MaxOf (CmpNat m n) m n
+
+type family MaxOf (e :: Ordering) (m :: k) (n :: k) :: k
+type instance MaxOf 'GT m n = m
+type instance MaxOf 'EQ m n = m
+type instance MaxOf 'LT m n = n
+
+type Min m n = MinOf (CmpNat m n) m n
+
+type family MinOf (e :: Ordering) (m :: k) (n :: k) :: k
+type instance MinOf 'GT m n = n
+type instance MinOf 'EQ m n = n
+type instance MinOf 'LT m n = m
+
+class Alternative (IfM y Weighted Proxy)
+  => GBCS (f :: k -> *) (z :: Nat) (y :: Maybe Nat) (e :: *) where
+  gbcs :: prox y -> proxy '(z, e) -> IfM y Weighted Proxy (f p)
+
+instance GBCS f z y e => GBCS (M1 i c f) z y e where
+  gbcs y z = fmap M1 (gbcs y z)
+
+instance
+  ( GBCSSum f g z e yf yg
+  , GBCS f z yf e
+  , GBCS g z yg e
+  , y ~ (yf ||? yg)
+  ) => GBCS (f :+: g) z y e where
+  gbcs _ z = gbcsSum (Proxy :: Proxy '(yf, yg)) z
+    (gbcs (Proxy :: Proxy yf) z)
+    (gbcs (Proxy :: Proxy yg) z)
+
+class Alternative (IfM (yf ||? yg) Weighted Proxy) => GBCSSum f g z e yf yg where
+  gbcsSum
+    :: prox '(yf, yg)
+    -> proxy '(z, e)
+    -> IfM yf Weighted Proxy (f p)
+    -> IfM yg Weighted Proxy (g p)
+    -> IfM (yf ||? yg) Weighted Proxy ((f :+: g) p)
+
+instance GBCSSum f g z e 'Nothing 'Nothing where
+  gbcsSum _ _ _ _ = Proxy
+
+instance GBCSSum f g z e ('Just m) 'Nothing where
+  gbcsSum _ _ f _ = fmap L1 f
+
+instance GBCSSum f g z e 'Nothing ('Just n) where
+  gbcsSum _ _ _ g = fmap R1 g
+
+instance GBCSSumCompare f g z e (CmpNat m n)
+  => GBCSSum f g z e ('Just m) ('Just n) where
+  gbcsSum _ = gbcsSumCompare (Proxy :: Proxy (CmpNat m n))
+
+class GBCSSumCompare f g z e o where
+  gbcsSumCompare
+    :: proxy0 o
+    -> proxy '(z, e)
+    -> Weighted (f p)
+    -> Weighted (g p)
+    -> Weighted ((f :+: g) p)
+
+instance GBCSSumCompare f g z e 'EQ where
+  gbcsSumCompare _ _ f g = fmap L1 f <|> fmap R1 g
+
+instance GBCSSumCompare f g z e 'LT where
+  gbcsSumCompare _ _ f _ = fmap L1 f
+
+instance GBCSSumCompare f g z e 'GT where
+  gbcsSumCompare _ _ _ g = fmap R1 g
+
+instance
+  ( GBCSProduct f g z e yf yg
+  , GBCS f z yf e
+  , GBCS g z yg e
+  , y ~ (yf &&? yg)
+  ) => GBCS (f :*: g) z y e where
+  gbcs _ z = gbcsProduct (Proxy :: Proxy '(yf, yg)) z
+    (gbcs (Proxy :: Proxy yf) z)
+    (gbcs (Proxy :: Proxy yg) z)
+
+class Alternative (IfM (yf &&? yg) Weighted Proxy) => GBCSProduct f g z e yf yg where
+  gbcsProduct
+    :: prox '(yf, yg)
+    -> proxy '(z, e)
+    -> IfM yf Weighted Proxy (f p)
+    -> IfM yg Weighted Proxy (g p)
+    -> IfM (yf &&? yg) Weighted Proxy ((f :*: g) p)
+
+instance {-# OVERLAPPABLE #-} ((yf &&? yg) ~ 'Nothing) => GBCSProduct f g z e yf yg where
+  gbcsProduct _ _ _ _ = Proxy
+
+instance GBCSProduct f g z e ('Just m) ('Just n) where
+  gbcsProduct _ _ f g = liftA2 (:*:) f g
+
+class IsMaybe b where
+  ifMmap :: proxy b -> (c a -> c' a') -> (d a -> d' a') -> IfM b c d a -> IfM b c' d' a'
+  ifM :: proxy b -> c a -> d a -> IfM b c d a
+
+instance IsMaybe ('Just t) where
+  ifMmap _ f _ a = f a
+  ifM _ f _ = f
+
+instance IsMaybe 'Nothing where
+  ifMmap _ _ g a = g a
+  ifM _ _ g = g
+
+instance {-# OVERLAPPABLE #-}
+  ( BaseCaseSearch c (z - 1) y e
+  , (z == 0) ~ 'False
+  , Alternative (IfM y Weighted Proxy)
+  , IsMaybe y
+  ) => GBCS (K1 i c) z y e where
+  gbcs y _ =
+    fmap K1
+      (ifMmap y
+        liftGen
+        (id :: Proxy c -> Proxy c)
+        (baseCaseSearch y (Proxy :: Proxy '(z - 1, e))))
+
+instance (y ~ 'Nothing) => GBCS (K1 i c) 0 y e where
+  gbcs _ _ = empty
+
+instance (y ~ 'Just 0) => GBCS U1 z y e where
+  gbcs _ _ = pure U1
+
+#if __GLASGOW_HASKELL__ >= 800
+instance {-# INCOHERENT #-}
+  ( TypeError
+      (     'Text "Unrecognized Rep: "
+      ':<>: 'ShowType f
+      ':$$: 'Text "Possible causes:"
+      ':$$: 'Text "    Missing ("
+      ':<>: 'ShowType (BaseCase e)
+      ':<>: 'Text ") constraint"
+      ':$$: 'Text "    Missing Generic instance"
+    )
+  , Alternative (IfM y Weighted Proxy)
+  ) => GBCS f z y e where
+  gbcs = error "Type error"
+#endif
+
+class GBaseCaseSearch a z y e where
+  gBaseCaseSearch :: prox y -> proxy '(z, e) -> IfM y Gen Proxy a
+
+instance (Generic a, GBCS (Rep a) z y e, IsMaybe y)
+  => GBaseCaseSearch a z y e where
+  gBaseCaseSearch y z = ifMmap y
+    (\(Weighted (Just (g, n))) -> choose (0, n-1) >>= fmap to . g)
+    (\Proxy -> Proxy)
+    (gbcs y z)
+
+#if __GLASGOW_HASKELL__ < 800
+data Proxy a = Proxy
+
+instance Functor Proxy where
+  fmap _ _ = Proxy
+
+instance Applicative Proxy where
+  pure _ = Proxy
+  _ <*> _ = Proxy
+
+instance Alternative Proxy where
+  empty = Proxy
+  _ <|> _ = Proxy
+#endif
diff --git a/src/Generic/Random/Internal/Generic.hs b/src/Generic/Random/Internal/Generic.hs
--- a/src/Generic/Random/Internal/Generic.hs
+++ b/src/Generic/Random/Internal/Generic.hs
@@ -1,70 +1,76 @@
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+#if __GLASGOW_HASKELL__ < 710
+{-# LANGUAGE OverlappingInstances #-}
+#endif
 
 module Generic.Random.Internal.Generic where
 
 import Control.Applicative
-import Data.Coerce
 import Data.Proxy
+#if __GLASGOW_HASKELL__ >= 800
+import GHC.Generics hiding (S)
+#else
 import GHC.Generics hiding (S, Arity)
+#endif
 import GHC.TypeLits
 import Test.QuickCheck
 
 -- * Random generators
 
 -- | Pick a constructor with a given distribution, and fill its fields
--- recursively.
+-- with recursive calls to 'arbitrary'.
+--
+-- === Example
+--
+-- > genericArbitrary (2 % 3 % 5 % ()) :: Gen a
+--
+-- Picks the first constructor with probability @2/10@,
+-- the second with probability @3/10@, the third with probability @5/10@.
 genericArbitrary
-  :: forall a
-  .  (Generic a, GA Unsized (Rep a))
+  :: (Generic a, GA Unsized (Rep a))
   => Weights a  -- ^ List of weights for every constructor
   -> Gen a
-genericArbitrary (Weights w n) = (unGen' . fmap to) (ga w n :: Gen' Unsized (Rep a p))
+genericArbitrary (Weights w n) = fmap to (ga (Proxy :: Proxy Unsized) w n)
 
--- | Shorthand for @'genericArbitrary' 'uniform'@.
+-- | Pick every constructor with equal probability.
+-- Equivalent to @'genericArbitrary' 'uniform'@.
+--
+-- > genericArbitraryU :: Gen a
 genericArbitraryU
-  :: forall a
-  .  (Generic a, GA Unsized (Rep a), UniformWeight (Weights_ (Rep a)))
+  :: (Generic a, GA Unsized (Rep a), UniformWeight_ (Rep a))
   => Gen a
 genericArbitraryU = genericArbitrary uniform
 
--- | Like 'genericArbitrary'', with decreasing size to ensure termination for
--- recursive types, looking for base cases once the size reaches 0.
-genericArbitrary'
-  :: forall n a
-  . (Generic a, GA (Sized n) (Rep a))
-  => n
-  -> Weights a  -- ^ List of weights for every constructor
-  -> Gen a
-genericArbitrary' _ (Weights w n) =
-  (unGen' . fmap to) (ga w n :: Gen' (Sized n) (Rep a p))
-
--- | Shorthand for @'genericArbitrary'' 'Z' 'uniform'@, using nullary
--- constructors as the base cases.
-genericArbitraryU0
-  :: forall n a
-  . (Generic a, GA (Sized Z) (Rep a), UniformWeight (Weights_ (Rep a)))
+-- | 'arbitrary' for types with one constructor.
+-- Equivalent to 'genericArbitraryU', with a stricter type.
+--
+-- > genericArbitrarySingle :: Gen a
+genericArbitrarySingle
+  :: (Generic a, GA Unsized (Rep a), Weights_ (Rep a) ~ L c0)
   => Gen a
-genericArbitraryU0 = genericArbitrary' Z uniform
+genericArbitrarySingle = genericArbitraryU
 
--- | Shorthand for @'genericArbitrary'' ('S' 'Z') 'uniform'@, using nullary
--- constructors and constructors whose fields are all nullary as base cases.
-genericArbitraryU1
-  :: forall n a
-  . (Generic a, GA (Sized (S Z)) (Rep a), UniformWeight (Weights_ (Rep a)))
-  => Gen a
-genericArbitraryU1 = genericArbitrary' (S Z) uniform
+-- | Decrease size at every recursive call, but don't do anything different
+-- at size 0.
+--
+-- > genericArbitraryRec (7 % 11 % 13 % ()) :: Gen a
+genericArbitraryRec
+  :: forall a
+  . (Generic a, GA Sized (Rep a))
+  => Weights a  -- ^ List of weights for every constructor
+  -> Gen a
+genericArbitraryRec (Weights w n) =
+  fmap to (ga (Proxy :: Proxy Sized) w n :: Gen (Rep a p))
 
 -- * Internal
 
@@ -74,7 +80,7 @@
 #if __GLASGOW_HASKELL__ >= 800
   Weights_ (M1 C ('MetaCons c _i _j) _f) = L c
 #else
-  Weights_ (M1 C _c _f) = ()
+  Weights_ (M1 C _c _f) = L ""
 #endif
 
 data a :| b = N a Int b
@@ -86,14 +92,14 @@
 -- Two ways of constructing them.
 --
 -- @
--- 'weights' (x1 '%' x2 '%' ... '%' xn '%' ()) :: 'Weights' a
+-- (x1 '%' x2 '%' ... '%' xn '%' ()) :: 'Weights' a
 -- 'uniform' :: 'Weights' a
 -- @
 --
--- Using @weights@, there must be exactly as many weights as
+-- Using @('%')@, there must be exactly as many weights as
 -- there are constructors.
 --
--- 'uniform' is equivalent to @'weights' (1 '%' ... '%' 1 '%' ())@
+-- 'uniform' is equivalent to @(1 '%' ... '%' 1 '%' ())@
 -- (automatically fills out the right number of 1s).
 data Weights a = Weights (Weights_ (Rep a)) Int
 
@@ -101,16 +107,17 @@
 -- constructor for additional compile-time checking.
 --
 -- @
--- 'weights' ((9 :: 'W' \"Leaf\") '%' (8 :: 'W' \"Node\") '%' ())
+-- ((9 :: 'W' \"Leaf\") '%' (8 :: 'W' \"Node\") '%' ())
 -- @
 newtype W (c :: Symbol) = W Int deriving Num
 
+{-# DEPRECATED weights "Can be omitted" #-}
 -- | A smart constructor to specify a custom distribution.
 weights :: (Weights_ (Rep a), Int, ()) -> Weights a
 weights (w, n, ()) = Weights w n
 
 -- | Uniform distribution.
-uniform :: UniformWeight (Weights_ (Rep a)) => Weights a
+uniform :: UniformWeight_ (Rep a) => Weights a
 uniform =
   let (w, n) = uniformWeight
   in Weights w n
@@ -119,27 +126,45 @@
   First (a :| _b) = First a
   First (L c) = c
 
+type family First' w where
+  First' (Weights a) = First (Weights_ (Rep a))
+  First' (a, Int, r) = First a
+
+type family Prec' w where
+  Prec' (Weights a) = Prec (Weights_ (Rep a)) ()
+  Prec' (a, Int, r) = Prec a r
+
+class WeightBuilder' w where
+
+  -- | A binary constructor for building up trees of weights.
+  (%) :: W (First' w) -> Prec' w -> w
+
+instance WeightBuilder (Weights_ (Rep a)) => WeightBuilder' (Weights a) where
+  w % prec = weights (w %. prec)
+
+instance WeightBuilder a => WeightBuilder' (a, Int, r) where
+  (%) = (%.)
+
 class WeightBuilder a where
   type Prec a r
 
-  -- | A binary constructor for building up trees of weights.
-  (%) :: W (First a) -> Prec a r -> (a, Int, r)
+  (%.) :: W (First a) -> Prec a r -> (a, Int, r)
 
 infixr 1 %
 
 instance WeightBuilder a => WeightBuilder (a :| b) where
   type Prec (a :| b) r = Prec a (b, Int, r)
-  m % prec =
+  m %. prec =
     let (a, n, (b, p, r)) = m % prec
     in (N a n b, n + p, r)
 
 instance WeightBuilder (L c) where
   type Prec (L c) r = r
-  W m % prec = (L, m, prec)
+  W m %. prec = (L, m, prec)
 
 instance WeightBuilder () where
   type Prec () r = r
-  W m % prec = ((), m, prec)
+  W m %. prec = ((), m, prec)
 
 class UniformWeight a where
   uniformWeight :: (a, Int)
@@ -158,96 +183,89 @@
 instance UniformWeight () where
   uniformWeight = ((), 1)
 
-newtype Gen' sized a = Gen' { unGen' :: Gen a }
-  deriving (Functor, Applicative, Monad)
+class UniformWeight (Weights_ f) => UniformWeight_ f
+instance UniformWeight (Weights_ f) => UniformWeight_ f
 
-data Sized n
+data Sized
 data Unsized
 
-sized' :: (Int -> Gen' sized a) -> Gen' sized a
-sized' g = Gen' . sized $ \sz -> unGen' (g sz)
-
 -- | Generic Arbitrary
 class GA sized f where
-  ga :: Weights_ f -> Int -> Gen' sized (f p)
+  ga :: proxy sized -> Weights_ f -> Int -> Gen (f p)
 
 instance GA sized f => GA sized (M1 D c f) where
-  ga w n = fmap M1 (ga w n)
-
-instance GAProduct f => GA Unsized (M1 C c f) where
-  ga _ _ = (Gen' . fmap M1) gaProduct
-
-instance (GAProduct f, KnownNat (Arity f)) => GA (Sized n) (M1 C c f) where
-  ga _ _ = Gen' (sized $ \n -> resize (n `div` arity) gaProduct)
-    where
-      arity = fromInteger (natVal (Proxy :: Proxy (Arity f)))
-
-instance (GASum (Sized n) f, GASum (Sized n) g, BaseCases n f, BaseCases n g)
-  => GA (Sized n) (f :+: g) where
-  ga w n = sized' $ \sz ->
-    case unTagged (baseCases w n :: Tagged n (Weighted ((f :+: g) p))) of
-      Weighted (Just (bc, n)) | sz == 0 -> Gen' (choose (0, n - 1) >>= bc)
-      _ -> gaSum' w n
+  ga z w n = fmap M1 (ga z w n)
 
-instance (GASum Unsized f, GASum Unsized g) => GA Unsized (f :+: g) where
+instance (GASum sized f, GASum sized g) => GA sized (f :+: g) where
   ga = gaSum'
 
-gArbitrarySingle
-  :: forall sized f p c0
-  .  (GA sized f, Weights_ f ~ L c0)
-  => Gen' sized (f p)
-gArbitrarySingle = ga L 0
+instance GAProduct sized f => GA sized (M1 C c f) where
+  ga z _ _ = fmap M1 (gaProduct z)
 
-gaSum' :: GASum sized f => Weights_ f -> Int -> Gen' sized (f p)
-gaSum' w n = do
-  i <- Gen' $ choose (0, n-1)
-  gaSum i w
+#if __GLASGOW_HASKELL__ >= 800
+instance {-# INCOHERENT #-}
+  TypeError
+    (     'Text "Unrecognized Rep: "
+    ':<>: 'ShowType f
+    ':$$: 'Text "Possible cause: missing Generic instance"
+    )
+  => GA sized f where
+  ga = error "Type error"
+#endif
 
+gaSum' :: GASum sized f => proxy sized -> Weights_ f -> Int -> Gen (f p)
+gaSum' z w n = do
+  i <- choose (0, n-1)
+  gaSum z i w
+
 class GASum sized f where
-  gaSum :: Int -> Weights_ f -> Gen' sized (f p)
+  gaSum :: proxy sized -> Int -> Weights_ f -> Gen (f p)
 
 instance (GASum sized f, GASum sized g) => GASum sized (f :+: g) where
-  gaSum i (N a n b)
-    | i < n = fmap L1 (gaSum i a)
-    | otherwise = fmap R1 (gaSum (i - n) b)
+  gaSum z i (N a n b)
+    | i < n = fmap L1 (gaSum z i a)
+    | otherwise = fmap R1 (gaSum z (i - n) b)
 
-instance GAProduct f => GASum sized (M1 i c f) where
-  gaSum _ _ = Gen' gaProduct
+instance GAProduct sized f => GASum sized (M1 i c f) where
+  gaSum z _ _ = fmap M1 (gaProduct z)
 
 
-class GAProduct f where
-  gaProduct :: Gen (f p)
+class GAProduct sized f where
+  gaProduct :: proxy sized -> Gen (f p)
 
-instance GAProduct U1 where
-  gaProduct = pure U1
+instance GAProduct' f => GAProduct Unsized f where
+  gaProduct _ = gaProduct'
 
-instance Arbitrary c => GAProduct (K1 i c) where
-  gaProduct = fmap K1 arbitrary
+instance (GAProduct' f, KnownNat (Arity f)) => GAProduct Sized f where
+  gaProduct _ = sized $ \n -> resize (n `div` arity) gaProduct'
+    where
+      arity = fromInteger (natVal (Proxy :: Proxy (Arity f)))
 
-instance GAProduct f => GAProduct (M1 i c f) where
-  gaProduct = fmap M1 gaProduct
+instance {-# OVERLAPPING #-} GAProduct Sized U1 where
+  gaProduct _ = pure U1
 
-instance (GAProduct f, GAProduct g) => GAProduct (f :*: g) where
-  gaProduct = liftA2 (:*:) gaProduct gaProduct
 
-type family Arity f :: Nat where
-  Arity (f :*: g) = Arity f + Arity g
-  Arity (M1 _i _c _f) = 1
+class GAProduct' f where
+  gaProduct' :: Gen (f p)
 
+instance GAProduct' U1 where
+  gaProduct' = pure U1
 
-newtype Tagged a b = Tagged { unTagged :: b }
-  deriving Functor
+instance Arbitrary c => GAProduct' (K1 i c) where
+  gaProduct' = fmap K1 arbitrary
 
--- $nat
--- Use the 'Z' and 'S' data types to define the depths of values used
--- by 'genericArbitrary'' to make generators terminate.
+instance (GAProduct' f, GAProduct' g) => GAProduct' (f :*: g) where
+  gaProduct' = liftA2 (:*:) gaProduct' gaProduct'
 
--- | Zero
-data Z = Z
+instance GAProduct' f => GAProduct' (M1 i c f) where
+  gaProduct' = fmap M1 gaProduct'
 
--- | Successor
-data S n = S n
 
+type family Arity f :: Nat where
+  Arity (f :*: g) = Arity f + Arity g
+  Arity (M1 _i _c _f) = 1
+
+
 newtype Weighted a = Weighted (Maybe (Int -> Gen a, Int))
   deriving Functor
 
@@ -273,62 +291,6 @@
           b (i - m)
     , m + n )
 
-class BaseCases n f where
-  baseCases :: Weights_ f -> Int -> Tagged n (Weighted (f p))
-
-instance (BaseCases n f, BaseCases n g) => BaseCases n (f :+: g) where
-  baseCases (N a m b) n =
-    concat
-      ((fmap . fmap) L1 (baseCases a m))
-      ((fmap . fmap) R1 (baseCases b (n - m)))
-    where
-      concat :: Alternative u => Tagged n (u a) -> Tagged n (u a) -> Tagged n (u a)
-      concat (Tagged a) (Tagged b) = Tagged (a <|> b)
-
-instance ListBaseCases n f => BaseCases n (M1 i c f) where
-  baseCases _ n = fmap reweigh listBaseCases
-    where
-      reweigh :: Weighted a -> Weighted a
-      reweigh (Weighted h) = Weighted (fmap (\(g, _) -> (g, n)) h)
-
--- | A @ListBaseCases n ('Rep' a)@ constraint basically provides the list of
--- values of type @a@ with depth at most @n@.
-class ListBaseCases n f where
-  listBaseCases :: Alternative u => Tagged n (u (f p))
-
--- | For convenience.
-type BaseCases' n a = (Generic a, ListBaseCases n (Rep a))
-
-instance ListBaseCases n U1 where
-  listBaseCases = Tagged (pure U1)
-
-instance ListBaseCases n f => ListBaseCases n (M1 i c f) where
-  listBaseCases = (fmap . fmap) M1 listBaseCases
-
-instance ListBaseCases Z (K1 i c) where
-  listBaseCases = Tagged empty
-
-instance (Generic c, ListBaseCases n (Rep c)) => ListBaseCases (S n) (K1 i c) where
-  listBaseCases = (retag . (fmap . fmap) (K1 . to)) listBaseCases
-    where
-      retag :: Tagged n a -> Tagged (S n) a
-      retag = coerce
-
-instance (ListBaseCases n f, ListBaseCases n g) => ListBaseCases n (f :+: g) where
-  listBaseCases =
-    concat
-      ((fmap . fmap) L1 listBaseCases)
-      ((fmap . fmap) R1 listBaseCases)
-    where
-      concat :: Alternative u => Tagged n (u a) -> Tagged n (u a) -> Tagged n (u a)
-      concat (Tagged a) (Tagged b) = Tagged (a <|> b)
+liftGen :: Gen a -> Weighted a
+liftGen g = Weighted (Just (\_ -> g, 1))
 
-instance (ListBaseCases n f, ListBaseCases n g) => ListBaseCases n (f :*: g) where
-  listBaseCases = liftedP listBaseCases listBaseCases
-    where
-      liftedP
-        :: Applicative u
-        => Tagged n (u (f p))
-        -> Tagged n (u (g p))
-        -> Tagged n (u ((f :*: g) p))
-      liftedP (Tagged f) (Tagged g) = Tagged (liftA2 (:*:) f g)
diff --git a/src/Generic/Random/Tutorial.hs b/src/Generic/Random/Tutorial.hs
new file mode 100644
--- /dev/null
+++ b/src/Generic/Random/Tutorial.hs
@@ -0,0 +1,183 @@
+-- | Generic implementations of
+-- [QuickCheck](https://hackage.haskell.org/package/QuickCheck)'s
+-- @arbitrary@.
+--
+-- == Example
+--
+-- Define your type.
+--
+-- @
+-- data Tree a = Leaf a | Node (Tree a) (Tree a)
+--   deriving 'Generic'
+-- @
+--
+-- Pick an 'arbitrary' implementation, specifying the required distribution of
+-- data constructors.
+--
+-- @
+-- instance Arbitrary a => Arbitrary (Tree a) where
+--   arbitrary = 'genericArbitrary' (8 '%' 9 '%' ())
+-- @
+--
+-- @arbitrary :: 'Gen' (Tree a)@ picks a @Leaf@ with probability 9\/17, or a
+-- @Node@ with probability 8\/17, and recursively fills their fields with
+-- @arbitrary@.
+--
+-- For @Tree@, 'genericArbitrary' produces code equivalent to the following:
+--
+-- @
+-- 'genericArbitrary' :: Arbitrary a => 'Weights' (Tree a) -> Gen (Tree a)
+-- 'genericArbitrary' (x '%' y '%' ()) =
+--   frequency
+--     [ (x, Leaf \<$\> arbitrary)
+--     , (y, Node \<$\> arbitrary \<*\> arbitrary)
+--     ]
+-- @
+--
+-- == Distribution of constructors
+--
+-- The distribution of constructors can be specified as
+-- a special list of /weights/ in the same order as the data type definition.
+-- This assigns to each constructor a probability proportional to its weight;
+-- in other words, @p_C = weight_C / sumOfWeights@.
+--
+-- The list of weights is built up with the @('%')@ operator as a cons, and using
+-- the unit @()@ as the empty list, in the order corresponding to the data type
+-- definition. The uniform distribution can be obtained with 'uniform'.
+--
+-- === Uniform distribution
+--
+-- You can specify the uniform distribution (all weights equal) with 'uniform'.
+-- ('genericArbitraryU' is available as a shorthand for
+-- @'genericArbitrary' 'uniform'@.)
+--
+-- Note that for many recursive types, a uniform distribution tends to produce
+-- big or even infinite values.
+--
+-- === Typed weights
+--
+-- /GHC 8.0.1 and above only (base ≥ 4.9)./
+--
+-- The weights actually have type @'W' \"ConstructorName\"@ (just a newtype
+-- around 'Int'), so that you can annotate a weight with its corresponding
+-- constructor, and it will be checked that you got the order right.
+--
+-- This will type-check.
+--
+-- @
+-- ((x :: 'W' \"Leaf\") '%' (y :: 'W' \"Node\") '%' ()) :: 'Weights' (Tree a)
+-- (x '%' (y :: 'W' \"Node\") '%' ()) :: 'Weights' (Tree a)
+-- @
+--
+-- This will not: the first requires an order of constructors different from
+-- the definition of the @Tree@ type; the second doesn't have the right number
+-- of weights.
+--
+-- @
+-- ((x :: 'W' \"Node\") '%' y '%' ()) :: 'Weights' (Tree a)
+-- (x '%' y '%' z '%' ()) :: 'Weights' (Tree a)
+-- @
+--
+-- == Ensuring termination
+--
+-- As mentioned earlier, one must be careful with recursive types
+-- to avoid producing extremely large values.
+--
+-- The alternative generator 'genericArbitrary'' implements a simple strategy to keep
+-- values at reasonable sizes: the size parameter of 'Gen' is divided among the
+-- fields of the chosen constructor. When it reaches zero, the generator
+-- selects a small term of the given type. This generally ensures that the
+-- number of constructors remains close to the initial size parameter passed to
+-- 'Gen'.
+--
+-- @
+-- 'genericArbitrary'' (x1 '%' ... '%' xn '%' ())
+-- @
+--
+-- Here is an example with nullary constructors:
+--
+-- @
+-- data Bush = Leaf1 | Leaf2 | Node3 Bush Bush Bush
+--   deriving Generic
+--
+-- instance Arbitrary Bush where
+--   arbitrary = 'genericArbitrary'' (1 '%' 2 '%' 3 '%' ())
+-- @
+--
+-- Here, 'genericArbitrary'' is equivalent to:
+--
+-- @
+-- 'genericArbitrary'' :: 'Weights' Bush -> Gen Bush
+-- 'genericArbitrary'' (x '%' y '%' z '%' ()) =
+--   sized $ \\n ->
+--     if n == 0 then
+--       -- If the size parameter is zero, only nullary alternatives are kept.
+--       elements [Leaf1, Leaf2]
+--     else
+--       frequency
+--         [ (x, return Leaf1)
+--         , (y, return Leaf2)
+--         , (z, resize (n \`div\` 3) node)  -- 3 because Node3 is 3-ary
+--         ]
+--   where
+--     node = Node3 \<$\> arbitrary \<*\> arbitrary \<*\> arbitrary
+-- @
+--
+-- If we want to generate a value of type @Tree ()@, there is a
+-- value of depth 1 that we can use to end recursion: @Leaf ()@.
+--
+-- @
+-- 'genericArbitrary'' :: 'Weights' (Tree ()) -> Gen (Tree ())
+-- 'genericArbitrary'' (x '%' y '%' ()) =
+--   sized $ \\n ->
+--     if n == 0 then
+--       return (Leaf ())
+--     else
+--       frequency
+--         [ (x, Leaf \<$\> arbitrary)
+--         , (y, resize (n \`div\` 2) $ Node \<$\> arbitrary \<*\> arbitrary)
+--         ]
+-- @
+--
+-- Because the argument of @Tree@ must be inspected in order to discover
+-- values of type @Tree ()@, we incur some extra constraints if we want
+-- polymorphism.
+--
+-- @
+-- {-\# LANGUAGE FlexibleContexts, UndecidableInstances \#-}
+--
+-- instance (Arbitrary a, BaseCase (Tree a))
+--   => Arbitrary (Tree a) where
+--   arbitrary = 'genericArbitrary'' (1 '%' 2 '%' ())
+-- @
+--
+-- By default, the 'BaseCase' type class looks for all values of minimal depth
+-- (constructors have depth @1 + max(0, depths of fields)@).
+--
+-- This can easily be overriden by declaring a specialized 'BaseCase' instance,
+-- such as this one:
+--
+-- @
+-- instance Arbitrary a => 'BaseCase' (Tree a) where
+--   'baseCase' = oneof [leaf, simpleNode]
+--     where
+--       leaf = Leaf \<$\> arbitrary
+--       simpleNode = Node \<$\> leaf \<*\> leaf
+-- @
+--
+-- An alternative base case can also be specified directly in the `arbitrary`
+-- definition with the 'withBaseCase' combinator.
+--
+-- 'genericArbitraryRec' is a variant of 'genericArbitrary'' with no base case.
+--
+-- @
+-- instance Arbitrary Bush where
+--   arbitrary =
+--     'genericArbitraryRec' (1 '%' 2 '%' 3 '%' ())
+--       \`withBaseCase\` return Leaf1
+-- @
+
+module Generic.Random.Tutorial () where
+
+import GHC.Generics
+import Generic.Random
diff --git a/test/Unit.hs b/test/Unit.hs
new file mode 100644
--- /dev/null
+++ b/test/Unit.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+#if __GLASGOW_HASKELL__ < 710
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+
+import GHC.Generics
+import Test.QuickCheck
+
+import Generic.Random.Generic
+
+newtype T a = W a deriving (Generic, Show)
+
+instance (Arbitrary a, BaseCase (T a)) => Arbitrary (T a) where
+  arbitrary = genericArbitrary' uniform
+
+f :: Gen (T (T Int))
+f = arbitrary
+
+main :: IO ()
+main = sample' f >>= force
+  where
+    force [] = return ()
+    force (x : xs) = x `seq` force xs