diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,19 @@
+Copyright Li-yao Xia (c) 2020
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the “Software”), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,158 @@
+# Testable functions
+
+A representation of functions for property testing, featuring
+random generation, shrinking, and printing.
+
+This package implements the core functionality.
+Separate packages integrate it with existing testing frameworks.
+
+- QuickCheck: [quickcheck-higherorder](https://github.com/Lysxia/quickcheck-higherorder)
+
+- Hedgehog: [hedgehog-higherorder](https://github.com/Lysxia/hedgehog-higherorder)
+
+## Summary
+
+This package defines a type of *testable functions* `a :-> r`,
+representing functions `a -> r`.
+
+- To interpret a testable function into a function `a -> r`,
+  use `applyFun :: (a :-> r) -> a -> r`.
+
+- To pretty-print a testable function,
+  use `show :: Show r => (a :-> r) -> String`.
+
+- To shrink a testable function, given a shrinker for `r`,
+  use `shrinkFun :: (r -> [r]) -> (a :-> r) -> [a :-> r]`.
+
+- To randomly generate a testable function `a :-> r`,
+  apply a *cogenerator* of `a` to a generator of `r`.
+  Cogenerators can be defined using combinators from this library.
+
+### Cogenerators
+
+The type of cogenerators of `a` is `Co Gen a r`,
+where `Gen` is QuickCheck's monad of random generators
+and `r` is an abstract parameter (it's really `forall r. Co Gen a r`).
+
+That type `Co Gen a r` is literally defined as a type synonym of
+`Gen r -> Gen (a :-> r)`.
+Given both a cogenerator `c :: Co Gen a r`, and a generator `g :: Gen r`,
+we can construct the generator of testable functions `c g :: Gen (a :-> r)`.
+
+(Users can just think of `Co Gen` as a whole,
+even though the implementation defines a more general `Co`
+which may be applied to any monad.
+Similarly, the parameter `r` can be ignored most of the time;
+it matters to cogenerators of parameterized types.)
+
+There are several combinators to define cogenerators,
+covering the following scenarios.
+
+#### Newtypes and embeddings
+
+If we have a newtype `A` around some old type `B`, and we also have
+a cogenerator of `B`:
+
+```haskell
+newtype A = MkA { unA :: B }
+
+cogenB :: Co Gen B r
+```
+
+Then `cogenEmbed` transforms `cogenB` into a cogenerator of `A`:
+
+```haskell
+cogenEmbed "unA" unA cogenB :: Co Gen A r
+```
+
+This is actually not restricted to newtypes:
+any "embedding" function `A -> B` (here, `unA`) can be used to convert a
+`Co Gen B r` to a `Co Gen A r`.
+(Yes, there is a contravariant functor hiding there.)
+Note that `cogenEmbed` expects a name for that function as a `String`
+in its first argument, for pretty-printing.
+
+#### Generic data types
+
+To define a cogenerator of a type which is an instance of `Generic` (from
+`GHC.Generics`), use `cogenGeneric`. For example, consider this type:
+
+```haskell
+data Small a = Zero | One a | Two a a
+  deriving Generic
+```
+
+The function `cogenGeneric` takes a heterogeneous list of
+cogenerators, one for each constructor of the generic type.
+This is `cs` in the example below.
+
+The heterogeneous list is constructed using `(:+)` to append
+elements and `()` for the end of the list.
+
+For constructors with multiple fields,
+use `(.)` to compose cogenerators for individual fields.
+
+For nullary constructors, use `id` as the "nullary cogenerator".
+
+```haskell
+cogenSmall ::
+  forall a.
+  (forall r. Co Gen a r) ->
+  (forall r. Co Gen (Small a) r)
+cogenSmall cogenA = cogenGeneric cs where
+  cs
+    =  id                 -- Nullary cogenerator, for the constructor Zero
+    :+ cogenA             -- Cogenerator of a, for the constructor One
+    :+ (cogenA . cogenA)  -- A cogenerator of a, once for each field of the constructor Two
+    :+ ()                 -- End of the list
+```
+
+#### Functions
+
+To generate higher-order testable functions `(a -> b) :-> r`,
+we need a cogenerator of functions `a -> b`,
+which we can define using `cogenFun`.
+
+To a first approximation, the function `cogenFun` transforms
+a cogenerator of `b` into a cogenerator of `(a -> b)`, provided
+a way to generate, shrink, and show `a`.
+
+This is actually generalized further by allowing one to provide
+a way to generate, shrink, and show a *representation* `a0` of `a`,
+which can be equal to `a` in simple cases,
+but this generalization makes it possible to generate
+functions of arbitrarily high order.
+
+Hence, to construct a cogenerator of `a -> b`,
+the function `cogenFun` takes the following arguments, in this order:
+
+1. `Concrete a0`: a dictionary containing a shrinker and a pretty-printer of
+   representations `a0`;
+2. `Gen (Maybe a0)`: a random generator of `a0`, it must generate `Nothing`
+   once in a while (say with probability 1/5 if you have no clue);
+3. `a0 -> a`: a function from representations to actual values
+   (`id` in simple cases);
+4. `forall r. Co Gen b r`: a cogenerator of `b`.
+
+## References
+
+- [*Shrinking and showing functions*](https://dl.acm.org/citation.cfm?id=2364516),
+  by Koen Claessen, Haskell Symposium 2012.
+
+  This package extends that work with support for higher-order functions.
+
+  Other implementations based on that paper can be found in:
+
+  + [QuickCheck](https://hackage.haskell.org/package/QuickCheck-2.13.2); in
+    particular see the [`Fun`
+    type](https://hackage.haskell.org/package/QuickCheck-2.13.2/docs/Test-QuickCheck.html#g:14).
+
+  + [hedgehog-fn](https://hackage.haskell.org/package/hedgehog-fn).
+
+## Internal module policy
+
+Modules under `Test.Fun.Internal` are not subject to any versioning policy.
+Breaking changes may apply to them at any time.
+
+If something in those modules seems useful, please report it or create a pull
+request to export it from an external module.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/src/Test/Fun.hs b/src/Test/Fun.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Fun.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE TypeOperators #-}
+
+-- | Testable representation of (higher-order) functions.
+--
+-- See the README for an introduction.
+
+module Test.Fun
+  ( -- * Testable functions
+    (:->)()
+  , applyFun
+  , applyFun2
+  , applyFun3
+
+    -- * Shrink and show
+  , shrinkFun
+  , showsPrecFun
+  , indent
+  , ShowsPrec
+
+    -- * Cogenerators
+  , Co
+
+    -- ** Main combinators
+  , cogenEmbed
+  , cogenIntegral
+  , cogenIntegral'
+  , cogenFun
+  , Concrete(..)
+  , FunName
+  , TypeName
+
+    -- ** Generic cogenerators
+  , cogenGeneric
+  , (:+)(..)
+
+    -- ** Secondary combinators
+  , cogenList
+  , cogenConst
+  , cogenApply
+
+    -- ** @CoArbitrary@
+  , CoArbitrary(..)
+  , coarbitraryGeneric
+
+    -- ** Generic classes
+  , GCoGen()
+  , GCoArbitrary()
+  , GSumCo
+  ) where
+
+import Test.Fun.Internal.Types
+  ((:->), applyFun, applyFun2, applyFun3, Concrete(..), ShowsPrec, FunName, TypeName)
+import Test.Fun.Internal.CoGen
+import Test.Fun.Internal.Generic
+import Test.Fun.Internal.Pretty (showsPrecFun, indent)
+import Test.Fun.Internal.Shrink (shrinkFun)
+import Test.Fun.Internal.Orphan ()
diff --git a/src/Test/Fun/Internal/CoGen.hs b/src/Test/Fun/Internal/CoGen.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Fun/Internal/CoGen.hs
@@ -0,0 +1,180 @@
+{-# LANGUAGE TypeOperators #-}
+
+-- | Random generation of higher-order functions.
+--
+-- === Warning
+--
+-- This is an internal module: it is not subject to any versioning policy,
+-- breaking changes can happen at any time.
+-- It is made available only for debugging.
+-- Otherwise, use "Test.Fun".
+--
+-- If something here seems useful, please open an issue to export it from an
+-- external module.
+--
+-- === Fun fact
+--
+-- This module only uses an 'Applicative' constraint on the type of
+-- generators (which is really QuickCheck's @Gen@).
+
+module Test.Fun.Internal.CoGen where
+
+import Control.Applicative (liftA2, liftA3)
+
+import Test.Fun.Internal.Types
+
+-- * Cogenerators
+
+-- | A \"cogenerator\" of @a@ is a random generator of functions with domain @a@.
+-- They are parameterized by a generator in the codomain @r@.
+--
+-- More generally, we can make cogenerators to generate functions of arbitrary arities;
+-- @'Co' gen a r@ is only the type of unary cogenerators.
+--
+-- > gen r -> gen (a :-> r)         -- Co gen a r
+-- > gen r -> gen (a :-> b :-> r)
+-- > gen r -> gen (a :-> b :-> c :-> r)
+-- > gen r -> gen (a :-> b :-> c :-> d :-> r)
+-- >
+-- > -- etc.
+--
+-- === __More details__
+--
+-- Cogenerators can be composed using 'id' and @('.')@ (the usual combinators
+-- for functions).
+-- The arity of a cogenerator @f '.' g@ is the sum of the arities of @f@ and @g@.
+--
+-- @
+-- id  ::  forall r. gen r -> gen r  -- 0-ary cogenerator
+--
+-- -- (1-ary) . (1-ary) = (2-ary)
+-- (.) :: (forall r. gen r -> gen (a :-> r)) ->
+--        (forall r. gen r -> gen (b :-> r)) ->
+--        (forall r. gen r -> gen (a :-> b :-> r))
+--
+-- -- (2-ary) . (1-ary) = (3-ary)
+-- (.) :: (forall r. gen r -> gen (a :-> b :-> r)) ->
+--        (forall r. gen r -> gen (c :-> r)) ->
+--        (forall r. gen r -> gen (a :-> b :-> c :-> r))
+-- @
+--
+-- Note: the last type parameter @r@ should really be universally quantified
+-- (as in the above pseudo type signatures), but instead we use more specialized
+-- types to avoid making types higher-ranked.
+type Co gen a r = gen r -> gen (a :-> r)
+
+-- | Cogenerator for a type @a@ from a cogenerator for @b@,
+-- given an embedding function @(a -> b)@,
+-- and a name for that function (used for pretty-printing).
+--
+-- === __Example__
+--
+-- The common usage is to construct cogenerators for newtypes.
+--
+-- @
+-- -- Given some cogenerator of Fruit
+-- cogenFruit :: 'Co' Gen Fruit r
+--
+-- -- Wrap Fruit in a newtype
+-- newtype Apple = Apple { unApple :: Fruit }
+--
+-- cogenApple :: 'Co' Gen Apple r
+-- cogenApple = 'cogenEmbed' \"unApple\" cogenFruit
+-- @
+--
+-- If @cogenFruit@ generates a function that looks like:
+--
+-- > \y -> case y :: Fruit of { ... }
+--
+-- then @cogenApple@ will look like this,
+-- where @y@ is replaced with @unApple x@:
+--
+-- > \x -> case unApple x :: Fruit of { ... }
+--
+cogenEmbed :: Functor gen => FunName -> (a -> b) -> Co gen b r -> Co gen a r
+cogenEmbed fn f cog g = (ToShrink . Apply fn f) <$> cog g
+
+-- | Cogenerator for an integral type.
+-- The name of the type is used for pretty-printing.
+--
+-- === __Example__
+--
+-- @
+-- cogenInteger :: 'Co' Gen 'Integer' r
+-- cogenInteger = 'cogenIntegral' \"Integer\"
+--
+-- cogenInt :: 'Co' Gen 'Int' r
+-- cogenInt = 'cogenIntegral' \"Int\"
+--
+-- cogenWord :: 'Co' Gen 'Word' r
+-- cogenWord = 'cogenIntegral' \"Word\"
+-- @
+cogenIntegral :: (Applicative gen, Integral a) => TypeName -> Co gen a r
+cogenIntegral tn = cogenIntegral' tn toInteger
+
+-- | Variant of 'cogenIntegral' with an explicit conversion to 'Integer'.
+cogenIntegral' :: Applicative gen => TypeName -> (a -> Integer) -> Co gen a r
+cogenIntegral' tn f g = liftA2 (CaseInteger tn f) (genBin g) g
+
+genBin :: Applicative gen => gen r -> gen (Bin r)
+genBin g = BinToShrink <$> self where
+  self = liftA3 BinAlt (Just <$> g) self self
+
+-- | Extend a cogenerator of functions @(a -> b)@ (i.e., a generator of higher-order
+-- functions @((a -> b) -> r)@), applying the function to a given value @a@
+-- and inspecting the result with a cogenerator of @b@.
+--
+-- This is parameterized by a way to generate, shrink, and show values of
+-- type @a@ or, more generally, some representation @a0@ of values of type @a@.
+--
+-- === __Example__
+--
+-- @
+-- -- Assume Chips is some concrete type.
+-- concreteChips :: 'Concrete' Chips
+--
+-- -- Assume we have a cogenerator of Fish.
+-- cogenFish :: forall r. Gen r -> Gen (Fish ':->' r)
+--
+-- -- Then we can use cogenApply to construct this function
+-- -- to transform cogenerators of functions (Chips -> Fish).
+-- cogenX :: forall r.
+--   Chips ->
+--   Gen ((Chips -> Fish) ':->' r) ->
+--   Gen ((Chips -> Fish) ':->' r)
+-- cogenX = 'cogenApply' concreteChips 'id' '.' cogenFish
+--
+-- -- If we have some inputs...
+-- chips1, chips2, chips3 :: Chips
+--
+-- -- ... we can construct a cogenerator of functions by iterating cogenX.
+-- cogenF :: forall r. Gen r -> Gen ((Chips -> Fish) ':->' r)
+-- cogenF = cogenX chips1 '.' cogenX chips2 '.' cogenX chips3 '.' 'cogenConst'
+-- @
+cogenApply :: Functor gen =>
+  Concrete a0 {- ^ Shrink and show @a0@. -} ->
+  (a0 -> a)   {- ^ Reify to value @a@ (@id@ for simple data types). -} ->
+  a0          {- ^ Value to inspect.     -} ->
+  gen (b :-> (a -> b) :-> r) {- ^ Cogenerator of @b@ -} ->
+  gen ((a -> b) :-> r)
+cogenApply w fromRepr x gr = CoApply w x fromRepr <$> gr
+
+-- | The trivial cogenerator which generates a constant function.
+cogenConst :: Functor gen => Co gen a r
+cogenConst g = Const <$> g
+
+-- | Construct a cogenerator of functions @(a -> b)@ from a cogenerator of @b@,
+-- using @gen (Maybe a0)@ to generate random arguments until it returns
+-- @Nothing@.
+cogenFun :: Monad gen =>
+  Concrete a0    {- ^ Shrink and show @a0@.      -} ->
+  gen (Maybe a0) {- ^ Generate representations of argument values. -} ->
+  (a0 -> a)      {- ^ Interpret a representation @a0@ into a value @a@ (@id@ for simple data types). -} ->
+  Co gen b ((a -> b) :-> r) {- ^ Cogenerator of @b@. -} ->
+  Co gen (a -> b) r
+cogenFun w ga fromRepr cb gr = self where
+  self = do
+    ma <- ga
+    case ma of
+      Nothing -> cogenConst gr
+      Just a -> cogenApply w fromRepr a (cb self)
diff --git a/src/Test/Fun/Internal/Generic.hs b/src/Test/Fun/Internal/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Fun/Internal/Generic.hs
@@ -0,0 +1,324 @@
+{-# LANGUAGE
+    AllowAmbiguousTypes,
+    EmptyCase,
+    FlexibleContexts,
+    FlexibleInstances,
+    InstanceSigs,
+    MultiParamTypeClasses,
+    PolyKinds,
+    ScopedTypeVariables,
+    TypeApplications,
+    TypeFamilies,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Generic cogenerators
+--
+-- === Warning
+--
+-- This is an internal module: it is not subject to any versioning policy,
+-- breaking changes can happen at any time.
+-- It is made available only for debugging.
+-- Otherwise, use "Test.Fun".
+--
+-- If something here seems useful, please open an issue to export it from an
+-- external module.
+
+module Test.Fun.Internal.Generic where
+
+import Data.Functor.Identity (Identity(..))
+import Data.Kind (Type)
+import Data.Monoid (Sum(..))
+import Data.Proxy (Proxy(..))
+import Data.Typeable (Typeable, typeRep, typeRepTyCon, tyConName)
+import Data.Void (Void)
+import Data.Word (Word)
+import GHC.Generics
+
+import Test.Fun.Internal.Types
+import Test.Fun.Internal.CoGen
+
+-- * CoArbitrary
+
+-- | Implicit, default cogenerator.
+class Applicative gen => CoArbitrary gen a where
+  coarbitrary :: forall r. Co gen a r
+
+-- * Generics
+
+-- | Cogenerator for generic types, parameterized by a list of cogenerators,
+-- one for each constructor.
+--
+-- The list is constructed with @(':+')@ (pairs) and @()@.
+--
+-- === __Example__
+--
+-- @
+-- -- Cogenerator for lists, parameterized by a cogenerator for elements.
+-- 'cogenList' :: forall a. (forall r. 'Co' Gen a r) -> (forall r. 'Co' Gen [a] r)
+-- 'cogenList' coa = 'cogenGeneric' gs where
+--   -- gs :: GSumCo Gen [a] r  -- unfolds to --
+--   gs ::
+--     (gen r -> gen r)                 ':+'  -- Cogenerator for the empty list
+--     (gen r -> gen (a ':->' [a] ':->' r)) ':+'  -- Cogenerator for non-empty lists
+--     ()
+--   gs = id ':+' (coa '.' 'cogenList' coa) ':+' ()
+-- @
+cogenGeneric :: forall a r gen.
+  (Generic a, GCoGen a, Applicative gen) => GSumCo gen a r -> Co gen a r
+cogenGeneric gs g = ToShrink <$> (Case typename normalize <$> branches g <*> g) where
+  typename = shortTypeName @a
+  normalize = gnormalize . from
+  branches = genBranches @(Rep a) gs
+
+-- | Heterogeneous products as nested pairs. These products must be terminated by ().
+--
+-- > a :+ b :+ c :+ ()  -- the product of a, b, c
+data a :+ b = a :+ b
+
+infixr 2 :+  -- more than :-> to force parentheses
+
+-- | Cogenerator for lists.
+--
+-- === __Implementation note__
+--
+-- The cogenerator of @a@ is made monomorphic only to keep the type of
+-- 'cogenList' at rank 1. But really, don't pay attention to the last type
+-- argument of 'Co'.
+--
+-- @
+-- 'cogenList' :: ... => 'Co' gen a _ -> 'Co' gen [a] _
+-- @
+cogenList :: forall a r gen. Applicative gen => Co gen a ([a] :-> r) -> Co gen [a] r
+cogenList coa = self where
+  self = cogenGeneric @[a] (id :+ (coa . self) :+ ())
+
+-- * Internals
+
+-- ** Generic cogenerators
+
+-- The generic implementation is split in three parts:
+--
+-- - the type name, for printing;
+-- - simplifying the generic representation to forget details specific to GHC.Generics;
+-- - constructing the @case@ branches.
+
+-- | Class of types with generic cogenerators.
+class    (Typeable_ a, GNormalize (Rep a), GenBranches (Rep a)) => GCoGen a
+instance (Typeable_ a, GNormalize (Rep a), GenBranches (Rep a)) => GCoGen a
+
+-- *** Reify the name and arity of a type constructor
+
+shortTypeName :: forall a. Typeable_ a => TypeName
+shortTypeName = shortTypeName_ @_ @a ""
+
+class Typeable_ (a :: k) where
+  shortTypeName_ :: String -> String
+
+instance {-# OVERLAPPING #-} Typeable_ f => Typeable_ (f a) where
+  shortTypeName_ = shortTypeName_ @_ @f . (' ' :) . ('_' :)
+
+instance Typeable a => Typeable_ a where
+  shortTypeName_ = ((++) . tyConName . typeRepTyCon) (typeRep (Proxy @a))
+
+-- *** Type-level functions on generic representations
+
+-- | Convert a generic 'Rep' into a sum of products made of 'Either' and @(,)@,
+-- where products are nested to the left (i.e., @((((), a), b), c)@).
+type family Normalize (f :: Type -> Type) :: Type where
+  Normalize (M1 D c f) = Normalize f
+  Normalize (f :+: g) = Either (Normalize f) (Normalize g)
+  Normalize V1 = Void
+  Normalize (M1 C c f) = () >*> f
+
+-- | Convert a @(:*:)@ product into a left-nested @(,)@ product.
+type family (>*>) (s :: Type) (f :: Type -> Type) :: Type where
+  s >*> (f :*: g) = s >*> f >*> g
+  s >*> M1 S c (K1 R a) = (s, a)
+  s >*> U1 = s
+
+infixl 9 >*>
+
+-- | The list of cogenerators for a generic type, one for each constructor.
+type GSumCo gen a r = GSumCo_ gen (Rep a) r ()
+
+type family GSumCo_ (gen :: Type -> Type) (f :: Type -> Type) (r :: Type) (t :: Type) :: Type where
+  GSumCo_ gen (M1 D c f) r t = GSumCo_ gen f r t
+  GSumCo_ gen (f :+: g)  r t = GSumCo_ gen f r (GSumCo_ gen g r t)
+  GSumCo_ gen (M1 C c f) r t = (gen r -> gen (f >-> r)) :+ t
+  GSumCo_ gen V1 r t = t
+
+type family (>->) (f :: Type -> Type) (r :: Type) :: Type where
+  (f :*: g) >-> r = f >-> g >-> r
+  M1 S c (K1 R a) >-> r = a :-> r
+  U1 >-> r = r
+
+infixr 9 >->
+
+-- *** Simplify the generic representation
+
+-- Sums
+
+class GNormalize f where
+  gnormalize :: f p -> Normalize f
+
+instance GNormalize f => GNormalize (M1 D c f) where
+  gnormalize = gnormalize . unM1
+
+instance (GNormalize f, GNormalize g) => GNormalize (f :+: g) where
+  gnormalize (L1 x) = Left (gnormalize x)
+  gnormalize (R1 y) = Right (gnormalize y)
+
+instance GNormalize V1 where
+  gnormalize x = case x of {}
+
+instance GToList f => GNormalize (M1 C c f) where
+  gnormalize = gToList () . unM1
+
+-- Products
+
+class GToList f where
+  gToList :: y -> f p -> (y >*> f)
+
+instance (GToList f, GToList g) => GToList (f :*: g) where
+  gToList y (u :*: v) = (y `gToList` u) `gToList` v
+
+instance GToList (M1 S c (K1 R a)) where
+  gToList y (M1 (K1 a)) = (y, a)
+
+instance GToList U1 where
+  gToList y _ = y
+
+-- *** Construct the @case@ branches
+
+genBranches :: forall f r gen. (Applicative gen, GenBranches f) =>
+  GSumCo_ gen f r () -> gen r -> gen (Branches (Normalize f) r)
+genBranches gs g = genBranches_ @f g (\c () -> c) gs
+
+-- Sums
+
+class GenBranches f where
+  genBranches_ :: forall t r y gen. Applicative gen =>
+    gen r ->
+    (gen (Branches (Normalize f) r) -> t -> y) ->
+    GSumCo_ gen f r t -> y
+
+instance GenBranches f => GenBranches (M1 D c f) where
+  genBranches_ = genBranches_ @f
+
+instance (GenBranches f, GenBranches g) => GenBranches (f :+: g) where
+  genBranches_ gr k =
+    genBranches_ @f gr (\gf ->
+    genBranches_ @g gr (\gg ->
+    k (Alt <$> gf <*> gg)))
+
+instance (Constructor c, MkFields f) => GenBranches (M1 C c f) where
+  genBranches_ gr k (h :+ t) = k gh t where
+    gh = (Pat cn . mkFields @f . NoField) <$> h gr
+    cn = conName @c undefined
+
+instance GenBranches V1 where
+  genBranches_ _ k = k (pure Fail)
+
+-- Products
+
+class MkFields f where
+  mkFields :: Fields x (f >-> r) -> Fields (x >*> f) r
+
+instance (MkFields f, MkFields g) => MkFields (f :*: g) where
+  mkFields = mkFields @g . mkFields @f
+
+instance MkFields (M1 S c (K1 R a)) where
+  mkFields = Field
+
+instance MkFields U1 where
+  mkFields = id
+
+-- ** Generic @CoArbitrary@
+
+-- | Generic implementation of 'coarbitrary'.
+--
+-- @
+-- -- Assuming MyData is a data type whose fields are all instances of CoArbitrary.
+--
+-- instance CoArbitrary MyData where
+--   coarbitrary = coarbitraryGeneric
+-- @
+coarbitraryGeneric :: forall a r gen. (Generic a, GCoArbitrary gen a) => Co gen a r
+coarbitraryGeneric = cogenGeneric (gsumCoarb @gen @(Rep a) (Proxy @r) ())
+
+-- | Constraint for 'coarbitraryGeneric'.
+class    (GCoGen a, Applicative gen, GSumCoArb gen (Rep a)) => GCoArbitrary gen a
+instance (GCoGen a, Applicative gen, GSumCoArb gen (Rep a)) => GCoArbitrary gen a
+
+-- Sums
+
+class GSumCoArb gen f where
+  gsumCoarb :: forall r t. Proxy r -> t -> GSumCo_ gen f r t
+
+instance GSumCoArb gen f => GSumCoArb gen (M1 D c f) where
+  gsumCoarb = gsumCoarb @gen @f
+
+instance (GSumCoArb gen f, GSumCoArb gen g) => GSumCoArb gen (f :+: g) where
+  gsumCoarb p = gsumCoarb @gen @f p . gsumCoarb @gen @g p
+
+instance GSumCoArb gen V1 where
+  gsumCoarb _ = id
+
+instance GProdCoArb gen f => GSumCoArb gen (M1 C c f) where
+  gsumCoarb _ t = gprodCoarb @gen @f :+ t
+
+-- Products
+
+class GProdCoArb gen f where
+  gprodCoarb :: gen r -> gen (f >-> r)
+
+instance (GProdCoArb gen f, GProdCoArb gen g) => GProdCoArb gen (f :*: g) where
+  gprodCoarb = gprodCoarb @gen @f . gprodCoarb @gen @g
+
+instance CoArbitrary gen a => GProdCoArb gen (M1 S c (K1 R a)) where
+  gprodCoarb = coarbitrary
+
+instance GProdCoArb gen U1 where
+  gprodCoarb = id
+
+-- Instances
+
+instance Applicative gen => CoArbitrary gen () where
+  coarbitrary g = Const <$> g
+
+instance Applicative gen => CoArbitrary gen Void where
+  coarbitrary _ = pure (Absurd id)
+
+instance Applicative gen => CoArbitrary gen Integer where
+  coarbitrary = cogenIntegral "Integer"
+
+instance Applicative gen => CoArbitrary gen Int where
+  coarbitrary = cogenIntegral "Int"
+
+instance Applicative gen => CoArbitrary gen Word where
+  coarbitrary = cogenIntegral "Word"
+
+instance Applicative gen => CoArbitrary gen Bool where
+  coarbitrary = coarbitraryGeneric
+
+instance Applicative gen => CoArbitrary gen Ordering where
+  coarbitrary = coarbitraryGeneric
+
+instance CoArbitrary gen a => CoArbitrary gen [a] where
+  coarbitrary = coarbitraryGeneric
+
+instance CoArbitrary gen a => CoArbitrary gen (Maybe a) where
+  coarbitrary = coarbitraryGeneric
+
+instance (CoArbitrary gen a, CoArbitrary gen b) => CoArbitrary gen (a, b) where
+  coarbitrary = coarbitraryGeneric
+
+instance (CoArbitrary gen a, CoArbitrary gen b) => CoArbitrary gen (Either a b) where
+  coarbitrary = coarbitraryGeneric
+
+instance CoArbitrary gen a => CoArbitrary gen (Identity a) where
+  coarbitrary = cogenEmbed "runIdentity" runIdentity coarbitrary
+
+instance CoArbitrary gen a => CoArbitrary gen (Sum a) where
+  coarbitrary = cogenEmbed "getSum" getSum coarbitrary
diff --git a/src/Test/Fun/Internal/Orphan.hs b/src/Test/Fun/Internal/Orphan.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Fun/Internal/Orphan.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- | Show for @(':->')@.
+--
+-- === Warning
+--
+-- This is an internal module: it is not subject to any versioning policy,
+-- breaking changes can happen at any time.
+-- It is made available only for debugging.
+-- Otherwise, use "Test.Fun".
+--
+-- If something here seems useful, please open an issue to export it from an
+-- external module.
+
+module Test.Fun.Internal.Orphan where
+
+import Test.Fun.Internal.Types ((:->))
+import Test.Fun.Internal.Pretty (showsPrecFun)
+
+-- | Pretty-printed 'Show' instance.
+instance Show r => Show (a :-> r) where
+  showsPrec = showsPrecFun showsPrec
diff --git a/src/Test/Fun/Internal/Pretty.hs b/src/Test/Fun/Internal/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Fun/Internal/Pretty.hs
@@ -0,0 +1,273 @@
+{-# LANGUAGE
+    BangPatterns,
+    GADTs,
+    ScopedTypeVariables,
+    TypeOperators #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- | Pretty printing of function representations.
+--
+-- === Warning
+--
+-- This is an internal module: it is not subject to any versioning policy,
+-- breaking changes can happen at any time.
+-- It is made available only for debugging.
+-- Otherwise, use "Test.Fun".
+--
+-- If something here seems useful, please open an issue to export it from an
+-- external module.
+
+module Test.Fun.Internal.Pretty where
+
+import Data.Bits (setBit)
+import Control.Applicative (liftA2)
+import Data.List (sortBy)
+import Data.Ord (comparing)
+import Data.Semigroup (Semigroup((<>)))
+
+import Test.Fun.Internal.Types
+  ((:->)(..), Branches(..), Fields(..), Bin(..), ConName, FunName, TypeName, Concrete(..), ShowsPrec)
+
+-- * Interface
+
+-- | Prettify function representation.
+showsPrecFun :: forall a r. ShowsPrec r -> ShowsPrec (a :-> r)
+showsPrecFun showsPrec_ _ h = s 0 where
+  s = sparens 0 ("\\" ~% sVar defVar % " -> " ~% unExpr_ (tFun (tShow_ showsPrec_) h defCtx))
+
+-- | Break up lines after braces and indent.
+--
+-- === __Example__
+--
+-- Input:
+--
+-- > \x -> case x :: Either _ _ of { Left x1 -> case x1 of { Left x2 -> () ; Right x2 -> case x2 of {} } ; Right x1 -> () }
+--
+-- Output:
+--
+-- > \x -> case x :: Either _ _ of {
+-- >   Left x1 -> case x1 of {
+-- >     Left x2 -> () ;
+-- >     Right x2 -> case x2 of {} } ;
+-- >   Right x1 -> () }
+indent :: String -> String
+indent = go 0 where
+  go !n ('{' : '}' : xs) = '{' : '}' : go n xs
+  go n ('{' : xs) = '{' : '\n' : replicate (n + 2) ' ' ++ go (n + 2) (dropWhile (== ' ') xs)
+  go n (';' : xs) = ';' : '\n' : replicate n ' ' ++ go n (dropWhile (== ' ') xs)
+  go n ('}' : xs) = '}' : go (n - 2) xs
+  go n (c : xs) = c : go n xs
+  go _ [] = []
+
+prettyFun :: forall a r. (r -> C Expr) -> (a :-> r) -> String
+prettyFun prettyR h = unExpr_ (tFun prettyR h defCtx) ""
+
+-- * Implementation
+
+-- ** Strings
+
+type DString = String -> String
+type PrecDString = Int -> DString
+
+sid :: DString
+sid = id
+
+sstring :: String -> DString
+sstring = (++)
+
+(%) :: DString -> DString -> DString
+(%) = (.)
+
+(~%) :: String -> DString -> DString
+(~%) = (%) . sstring
+
+infixr 1 %, ~%
+
+sparens :: Int -> DString -> PrecDString
+sparens d0 s d = if d > d0 then "(" ~% s % ")" ~% sid else s
+
+-- ** Pretty-printed expressions
+
+newtype Expr = Expr { unExpr :: PrecDString }
+
+type Pattern = Expr
+
+unExpr_ :: Expr -> DString
+unExpr_ e = unExpr e 0
+
+data Var = Var String !Int
+
+-- Context mapping variables to expressions.
+data Ctx = (Var, Expr) :. Ctx
+
+infixr 1 :.
+
+defVar :: Var
+defVar = Var "a" 0
+
+defCtx :: Ctx
+defCtx = addVar [defVar] badCtx
+
+badCtx :: Ctx
+badCtx = addVar [Var "unknown" 0] badCtx
+
+-- | Type of values under some context
+type C a = Ctx -> a
+
+-- ** Basic expression constructors
+
+-- Naming convention:
+-- - s for strings,
+-- - e for expressions (Expr),
+-- - t for terms (C Expr, expression under some context).
+
+eWild :: Pattern
+eWild = Expr (\_ -> sstring "_")
+
+eConst :: String -> Expr
+eConst s = Expr (\_ -> sstring s)
+
+tConst :: String -> C Expr
+tConst s _ = eConst s
+
+eInt :: Integer -> Expr
+eInt n = Expr (\_ -> show n ~% sid)
+
+eApp :: Expr -> Expr -> Expr
+eApp f x = Expr (sparens 10 (unExpr f 10 % " " ~% unExpr x 11))
+
+tShow :: Show a => a -> C Expr
+tShow = tShow_ showsPrec
+
+tShow_ :: ShowsPrec a -> a -> C Expr
+tShow_ showsPrec_ a _ = Expr (flip showsPrec_ a)
+
+sVar :: Var -> DString
+sVar (Var s i) = s ~% show i ~% sid
+
+eVar :: Var -> Expr
+eVar v = Expr (\_ -> sVar v)
+
+addVar :: [Var] -> Ctx -> Ctx
+addVar [] vs = vs
+addVar (v : ps) vs = (v, eVar v) :. addVar ps vs
+
+-- ** Main implementation
+
+-- | Pretty-print a function representation.
+tFun :: forall a r. (r -> C Expr) -> (a :-> r) -> C Expr
+tFun prettyR = go where
+  go :: forall b. (b :-> r) -> C Expr
+  go (Absurd _) = tAbsurd
+  go (Const r) = \(_ :. vs) -> prettyR r vs
+  go (CoApply c a _ h) = tCoApply c a (tFun go h)
+  go (Apply fn _ h) = tApply fn (go h)
+  go (Case tn _ b r) = tCase tn (appendIf (partialBranches b) (tBranches prettyR b) (bWild (prettyR r)))
+  go (CaseInteger tn _ b r) = tCase tn (tBin prettyR b <> bEllipsis b <> bWild (prettyR r))
+  go (ToShrink _) = tConst "[...]"
+
+tApply :: FunName -> C Expr -> C Expr
+tApply f y ((v, t) :. vs) =
+  y ((v, eApp (eConst f) t) :. vs)
+
+tCoApply :: Concrete w -> w -> C Expr -> C Expr
+tCoApply c a y ((v, t) :. vs) =
+  y ((nextVar v, eApp t (eConst (showsPrecC c 11 a ""))) :. (v, t) :. vs)
+
+tAbsurd :: C Expr
+tAbsurd ((_, t) :. _) = Expr (\_ -> "case " ~% unExpr_ t % " of {}" ~% sid)
+
+appendIf :: Semigroup m => Bool -> m -> m -> m
+appendIf True = (<>)
+appendIf False = const
+
+-- | @True@ if there is a @Fail@ branch.
+partialBranches :: Branches x r -> Bool
+partialBranches Fail = True
+partialBranches (Pat _ _) = False
+partialBranches (Alt b1 b2) = partialBranches b1 || partialBranches b2
+
+-- The patterns are parameterized by a fresh variable.
+type CBranches = Var -> C [EBranch]
+
+data EBranch
+  = EBranch Pattern Expr
+  | EBranchEllipsis
+
+bEllipsis :: Bin r -> CBranches
+bEllipsis b _ _
+  | ellidedBin b = [EBranchEllipsis]
+  | otherwise = []
+
+bWild :: C Expr -> CBranches
+bWild e _ vs = [EBranch eWild (e vs)]
+
+tCase :: TypeName -> CBranches -> C Expr
+tCase tn bs ((v, t) :. vs) = Expr (\_ ->
+    "case " ~% unExpr_ t % " :: " ~% tn ~% " of { "
+      ~% sBranches (bs v vs)
+      % " }" ~% sid)
+  where
+    renderBranch (EBranch p e) = unExpr_ p % " -> " ~% unExpr_ e
+    renderBranch EBranchEllipsis = "[...]" ~% sid
+    sBranches [] = sid
+    sBranches (b0 : bs_) =
+      renderBranch b0 %
+      foldr (\b ebs -> " ; " ~% renderBranch b % ebs) sid bs_
+
+tBranches :: forall x r. (r -> C Expr) -> Branches x r -> CBranches
+tBranches prettyR = go where
+  go :: forall y. Branches y r -> CBranches
+  go Fail = \_ _ -> []
+  go (Alt b1 b2) = (liftA2 . liftA2) (++) (go b1) (go b2)
+  go (Pat cn d) = tFields prettyR d cn []
+
+tFields :: forall x r. (r -> C Expr) -> Fields x r -> ConName -> [Var] -> CBranches
+tFields prettyR = go where
+  go :: forall y. Fields y r -> ConName -> [Var] -> CBranches
+  go (NoField h) cn ps _ vs = [EBranch (mkPattern cn ps) (prettyR h (addVar ps vs))]
+  go (Field d) cn ps v vs = tFields (tFun prettyR) d cn (v' : ps) v' vs where
+    v' = nextVar v
+
+nextVar :: Var -> Var
+nextVar (Var s i) = Var s (i + 1)
+
+mkPattern :: ConName -> [Var] -> Pattern
+mkPattern cn vs = Expr (\_ -> cn ~% foldr (\v s -> " " ~% sVar v % s) sid vs)
+
+tBin :: (r -> C Expr) -> Bin r -> CBranches
+tBin prettyR b _ vs =
+  fmap (\(n, e) -> EBranch (eInt n) e)
+    (sortBy (comparing fst) (tBin' prettyR b vs))
+
+data Sign = Pos | Neg
+
+resign :: Sign -> Integer -> Integer
+resign Pos x = x
+resign Neg x = - x
+
+tBin' :: (r -> C Expr) -> Bin r -> C [(Integer, Expr)]
+tBin' prettyR b vs = go_ b where
+  go_ (BinToShrink _) = []
+  go_ BinEmpty = []
+  go_ (BinAlt r_ b0 b1) = tr ++ tb01 where
+    tr = case r_ of
+      Nothing -> []
+      Just r -> [(0, prettyR r vs)]
+    tb01 = (go Pos 0 0 b0 . go Neg 0 0 b1) []
+
+  go _ !_ !_ (BinToShrink _) k = k
+  go _ _ _ BinEmpty k = k
+  go z i n (BinAlt r_ b0 b1) k = tr ++ tb01 where
+    i' = i + 1
+    n' = setBit n i
+    tr = case r_ of
+      Nothing -> []
+      Just r -> [(resign z n', prettyR r vs)]
+    tb01 = (go z i' n b0 . go z i' n' b1) k
+
+ellidedBin :: Bin r -> Bool
+ellidedBin (BinToShrink _) = True
+ellidedBin BinEmpty = False
+ellidedBin (BinAlt _ b0 b1) = ellidedBin b0 && ellidedBin b1
diff --git a/src/Test/Fun/Internal/Shrink.hs b/src/Test/Fun/Internal/Shrink.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Fun/Internal/Shrink.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE GADTs, ScopedTypeVariables, TypeOperators #-}
+
+-- | Shrinker for representation of functions.
+--
+-- === Warning
+--
+-- This is an internal module: it is not subject to any versioning policy,
+-- breaking changes can happen at any time.
+-- It is made available only for debugging.
+-- Otherwise, use "Test.Fun".
+--
+-- If something here seems useful, please open an issue to export it from an
+-- external module.
+
+module Test.Fun.Internal.Shrink where
+
+import Control.Applicative ((<|>))
+
+import Test.Fun.Internal.Types
+
+-- | Simplify function.
+shrinkFun :: forall a r. (r -> [r]) -> (a :-> r) -> [a :-> r]
+shrinkFun shrinkR = go where
+  go :: forall b. (b :-> r) -> [b :-> r]
+  go (ToShrink h) = go h ++ [h]
+  go (Absurd _) = []
+  go (Const r) = fmap Const (shrinkR r)
+  go (CoApply c a f h) = fmap (coapply c a f) (shrinkFun go h) ++ fmap (\a' -> CoApply c a' f h) (shrinkC c a)
+  go (Apply fn f h) = apply fn f <$> go h
+  go (Case tn f b r)
+    =  maybeConst (firstBranches Just b)
+    ++ fmap (\b' -> case_ tn f b' r) (shrinkBranches shrinkR b)
+    ++ fmap (\r' -> Case tn f b r') (shrinkR r)
+  go (CaseInteger tn f b r)
+    =  maybeConst (firstBin Just b)
+    ++ fmap (\b' -> caseInteger tn f b' r) (shrinkBin shrinkR b)
+    ++ fmap (\r' -> CaseInteger tn f b r') (shrinkR r)
+
+  maybeConst (Just r) = [Const r]
+  maybeConst Nothing = []
+
+shrinkBranches :: forall x r. (r -> [r]) -> Branches x r -> [Branches x r]
+shrinkBranches shrinkR = go where
+  go :: forall y. Branches y r -> [Branches y r]
+  go Fail = []
+  go (Alt b1 b2) = Fail : fmap (\b1' -> alt b1' b2) (go b1) ++ fmap (alt b1) (go b2)
+  go (Pat cn d) = Fail : fmap (Pat cn) (shrinkFields shrinkR d)
+
+shrinkFields :: forall x r. (r -> [r]) -> Fields x r -> [Fields x r]
+shrinkFields shrinkR = go where
+  go :: forall y. Fields y r -> [Fields y r]
+  go (NoField r) = fmap NoField (shrinkR r)
+  go (Field h) = fmap Field (shrinkFields (shrinkFun shrinkR) h)
+
+shrinkBin :: forall r. (r -> [r]) -> Bin r -> [Bin r]
+shrinkBin shrinkR = go where
+  go BinEmpty = []
+  go (BinAlt r b0 b1) =
+    BinEmpty
+      :  fmap (\r' -> BinAlt r' b0 b1) (shrinkMaybe shrinkR r)
+      ++ fmap (\b0' -> BinAlt r b0' b1) (go b0)
+      ++ [b0]
+      ++ fmap (\b1' -> BinAlt r b0 b1') (go b1)
+      ++ [b1]
+  go (BinToShrink b) = go b' ++ [b'] where b' = binToShrink b
+
+binToShrink :: forall r. Bin r -> Bin r
+binToShrink BinEmpty = BinEmpty
+binToShrink (BinAlt r b0 b1) = BinAlt r (BinToShrink b0) (BinToShrink b1)
+binToShrink (BinToShrink b) = b  -- Should not happen, but no problem if it does.
+
+shrinkMaybe :: (r -> [r]) -> Maybe r -> [Maybe r]
+shrinkMaybe _ Nothing = []
+shrinkMaybe shrinkR (Just r) = Nothing : fmap Just (shrinkR r)
+
+-- Try to find some value in the image of a given function @(a :-> r)@,
+-- but don't try too hard. Stop at 'ToShrink' nodes because these
+-- trees can be big/infinite.
+
+firstFun :: forall a r t. (r -> Maybe t) -> (a :-> r) -> Maybe t
+firstFun firstR h0 = case h0 of
+  ToShrink _ -> Nothing
+  Absurd _ -> Nothing
+  Const r -> firstR r
+  CoApply _ _ _ h -> firstFun (firstFun firstR) h
+  Apply _ _ h -> firstFun firstR h
+  Case _ _ b _ -> firstBranches firstR b
+  CaseInteger _ _ b _ -> firstBin firstR b
+
+firstBranches :: forall x r t. (r -> Maybe t) -> Branches x r -> Maybe t
+firstBranches firstR h = case h of
+  Alt b1 b2 -> firstBranches firstR b1 <|> firstBranches firstR b2
+  Fail -> Nothing
+  Pat _ d -> firstField firstR d
+
+firstField :: forall x r t. (r -> Maybe t) -> Fields x r -> Maybe t
+firstField firstR d = case d of
+  NoField h -> firstR h
+  Field d' -> firstField (firstFun firstR) d'
+
+firstBin :: forall r t. (r -> Maybe t) -> Bin r -> Maybe t
+firstBin firstR h = case h of
+  BinEmpty -> Nothing
+  BinAlt (Just r) _ _ -> firstR r
+  BinAlt Nothing l r -> firstBin firstR l <|> firstBin firstR r
+  BinToShrink _ -> Nothing
diff --git a/src/Test/Fun/Internal/Types.hs b/src/Test/Fun/Internal/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Fun/Internal/Types.hs
@@ -0,0 +1,306 @@
+{-# LANGUAGE
+    DeriveFunctor,
+    DeriveFoldable,
+    DeriveTraversable,
+    EmptyCase,
+    GADTs,
+    ScopedTypeVariables,
+    TypeOperators #-}
+
+-- | Representation of (higher-order) functions.
+--
+-- === Warning
+--
+-- This is an internal module: it is not subject to any versioning policy,
+-- breaking changes can happen at any time.
+-- It is made available only for debugging.
+-- Otherwise, use "Test.Fun".
+--
+-- If something here seems useful, please open an issue to export it from an
+-- external module.
+
+module Test.Fun.Internal.Types where
+
+import Data.Maybe (fromMaybe)
+import Data.Void (Void)
+import Data.Monoid ((<>))
+
+-- | Name of a function.
+type FunName = String
+
+-- | Name of a type.
+type TypeName = String
+
+-- | Name of a constructor.
+type ConName = String
+
+-- | The type of 'Text.Show.showsPrec'.
+type ShowsPrec r = Int -> r -> String -> String
+
+-- | Dictionary with shrinker and printer.
+-- Used as part of the representation of higher-order functions with @(':->')@.
+data Concrete r = Concrete
+  { shrinkC :: r -> [r]
+  , showsPrecC :: ShowsPrec r
+  }
+
+-- | Trivial shrinker and default printer.
+hardConcrete :: Show r => Concrete r
+hardConcrete = Concrete (\_ -> []) showsPrec
+
+infixr 1 :->
+
+-- | Testable representation of functions @(a -> r)@.
+--
+-- This representation supports random generation, shrinking, and printing,
+-- for property testing with QuickCheck or Hedgehog.
+--
+-- Higher-order functions can be represented.
+data a :-> r where
+  -- | Constant function, ignore the argument.
+  Const :: r -> a :-> r
+
+  -- | Apply the argument @(a -> b)@ to a value @a@, stored in some representation @w@,
+  -- and describe what to do with the result @b@ in another function.
+  CoApply :: Concrete w -> w -> (w -> a) -> (b :-> (a -> b) :-> r) -> (a -> b) :-> r
+
+  -- | Apply some function to the argument @a@.
+  Apply :: FunName -> (a -> b) -> (b :-> r) -> (a :-> r)
+
+  -- | Pattern-match on the argument (in some ADT).
+  -- The branches may be incomplete, in which case a default value @r@ is used.
+  Case :: TypeName -> (a -> x) -> Branches x r -> r -> (a :-> r)
+
+  -- | Pattern-match on the argument (of some integral type).
+  CaseInteger :: TypeName -> (a -> Integer) -> Bin r -> r -> (a :-> r)
+
+  -- | There is no value for the argument, so we're done.
+  Absurd :: (a -> Void) -> a :-> r
+
+  -- | Marker for truncating infinite representations.
+  ToShrink :: (a :-> r) -> a :-> r
+
+-- | Representation of the branches of a 'Case'.
+data Branches x r where
+  Fail :: Branches x r
+  Alt :: !(Branches x r) -> !(Branches y r) -> Branches (Either x y) r
+  Pat :: ConName -> !(Fields x r) -> Branches x r
+
+-- | Representation of one branch of a 'Case'.
+data Fields x r where
+  NoField :: r -> Fields () r
+  Field :: !(Fields x (y :-> r)) -> Fields (x, y) r
+
+-- | Representation of branches of a 'CaseInteger'.
+data Bin r
+  = BinEmpty
+  | BinAlt (Maybe r) (Bin r) (Bin r)
+  | BinToShrink (Bin r)
+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+-- Smart constructors to enforce some invariants
+
+coapply :: Concrete w -> w -> (w -> a) -> (b :-> (a -> b) :-> r) -> (a -> b) :-> r
+coapply _ _ _ (Const h) = h
+coapply c w f h = CoApply c w f h
+
+apply :: FunName -> (a -> b) -> (b :-> r) -> (a :-> r)
+apply _ _ (Const r) = Const r
+apply fn f h = Apply fn f h
+
+case_ :: TypeName -> (a -> x) -> Branches x r -> r -> (a :-> r)
+case_ _ _ Fail r = Const r
+case_ tn f b r = Case tn f b r
+
+caseInteger :: TypeName -> (a -> Integer) -> Bin r -> r -> (a :-> r)
+caseInteger _ _ BinEmpty r = Const r
+caseInteger tn f b r = CaseInteger tn f b r
+
+alt :: Branches x r -> Branches y r -> Branches (Either x y) r
+alt Fail Fail = Fail
+alt b1 b2 = Alt b1 b2
+
+binAlt :: r -> Bin r -> Bin r -> Bin r
+binAlt = BinAlt . Just
+
+--
+
+-- | Evaluate a representation into the function it represents.
+applyFun :: (a :-> r) -> a -> r
+applyFun (Const r) _ = r
+applyFun (CoApply _ w f h) x = applyFun (applyFun h (x (f w))) x
+applyFun (Apply _ f h) x = applyFun h (f x)
+applyFun (Case _ f b r) x = applyBranches r b (f x)
+applyFun (CaseInteger _ f b r) x = applyBin r b (f x)
+applyFun (Absurd f) x = case f x of {}
+applyFun (ToShrink h) x = applyFun h x
+
+-- | Apply a binary function representation.
+applyFun2 :: (a :-> b :-> r) -> a -> b -> r
+applyFun2 h x y = h `applyFun` x `applyFun` y
+
+-- | Apply a ternary function representation.
+applyFun3 :: (a :-> b :-> c :-> r) -> a -> b -> c -> r
+applyFun3 h x y z = h `applyFun` x `applyFun` y `applyFun` z
+
+applyBranches :: r -> Branches x r -> x -> r
+applyBranches r Fail _ = r
+applyBranches r (Alt b1 _) (Left  x) = applyBranches r b1 x
+applyBranches r (Alt _ b2) (Right y) = applyBranches r b2 y
+applyBranches _ (Pat _ d) x = applyFields d x
+
+applyFields :: Fields x r -> x -> r
+applyFields (NoField h) _ = h
+applyFields (Field h) (x, y) = applyFun (applyFields h x) y
+
+applyBin :: r -> Bin r -> Integer -> r
+applyBin r BinEmpty _ = r
+applyBin r (BinAlt r0 b0 b1) x = case compare x 0 of
+  EQ -> fromMaybe r r0
+  GT -> applyBin' r b0 x
+  LT -> applyBin' r b1 (- x)
+applyBin r (BinToShrink b) x = applyBin r b x
+
+applyBin' :: r -> Bin r -> Integer -> r
+applyBin' r BinEmpty _ = r
+applyBin' r (BinAlt r0 b0 b1) x
+  | x == 1 = fromMaybe r r0
+  | x `mod` 2 == 0 = applyBin' r b0 (x `div` 2)
+  | otherwise      = applyBin' r b1 (x `div` 2)
+applyBin' r (BinToShrink b) x = applyBin' r b x
+
+--
+
+-- | Remove 'ToShrink' nodes from evaluating a given argument @a@.
+clearFun :: (r -> r) -> a -> (a :-> r) -> (a :-> r)
+clearFun clearR x h0 = case h0 of
+  ToShrink h -> clearFun clearR x h
+  Const r -> Const (clearR r)
+  Absurd f -> Absurd f
+  CoApply c w f h -> CoApply c w f (clearFun (clearFun clearR x) (x (f w)) h)
+  Apply fn f h -> Apply fn f (clearFun clearR (f x) h)
+  Case tn f b r -> case clearBranches clearR b (f x) of
+    Nothing -> Case tn f b (clearR r)
+    Just b' -> Case tn f b' r
+  CaseInteger tn f b r -> case clearBin clearR b (f x) of
+    Nothing -> CaseInteger tn f b (clearR r)
+    Just b' -> CaseInteger tn f b' r
+
+clearBranches :: forall x r. (r -> r) -> Branches x r -> x -> Maybe (Branches x r)
+clearBranches clearR = go where
+  go :: forall z. Branches z r -> z -> Maybe (Branches z r)
+  go Fail _ = Nothing
+  go (Alt b1 b2) (Left y) = (\b1' -> Alt b1' b2) <$> go b1 y
+  go (Alt b1 b2) (Right y) = Alt b1 <$> go b2 y
+  go (Pat cn d) x = Just (Pat cn (clearFields clearR d x))
+
+clearFields :: (r -> r) -> Fields x r -> x -> Fields x r
+clearFields clearR d0 w = case d0 of
+  NoField r -> NoField (clearR r)
+  Field d | (x, y) <- w -> Field (clearFields (clearFun clearR y) d x)
+
+clearBin :: (r -> r) -> Bin r -> Integer -> Maybe (Bin r)
+clearBin clearR b' x = case b' of
+  BinEmpty -> Nothing
+  BinAlt r0 b0 b1 -> case compare x 0 of
+    EQ -> case r0 of
+      Just r -> Just (BinAlt (Just (clearR r)) b0 b1)
+      Nothing -> Nothing
+    GT -> clearBin' clearR (x - 1) b0
+    LT -> clearBin' clearR (- x - 1) b1
+  BinToShrink b -> clearBin clearR b x
+
+clearBin' :: (r -> r) -> Integer -> Bin r -> Maybe (Bin r)
+clearBin' clearR = go where
+  go _ BinEmpty = Nothing
+  go x (BinAlt r0 b0 b1)
+    | x == 0 = case r0 of
+      Just r -> Just (BinAlt (Just (clearR r)) b0 b1)
+      Nothing -> Nothing
+    | x `mod` 2 == 0 = (\b0' -> BinAlt r0 b0' b1) <$> go (x `div` 2) b0
+    | otherwise = BinAlt r0 b0 <$> go (x `div` 2) b1
+  go x (BinToShrink b) = go x b
+
+--
+
+instance Functor ((:->) a) where
+  fmap g h0 = case h0 of
+    Const r -> Const (g r)
+    Apply fn f h -> Apply fn f (fmap g h)
+    CoApply c w f h -> CoApply c w f (fmap (fmap g) h)
+    Case tn f b r -> Case tn f (fmap g b) (g r)
+    CaseInteger tn f b r -> CaseInteger tn f (fmap g b) (g r)
+    Absurd f -> Absurd f
+    ToShrink h -> ToShrink (fmap g h)
+
+instance Functor (Branches x) where
+  fmap g b = case b of
+    Fail -> Fail
+    Alt b1 b2 -> Alt (fmap g b1) (fmap g b2)
+    Pat cn d -> Pat cn (fmap g d)
+
+instance Functor (Fields x) where
+  fmap g d = case d of
+    NoField h -> NoField (g h)
+    Field h -> Field (fmap (fmap g) h)
+
+instance Foldable ((:->) a) where
+  foldMap foldR h0 = case h0 of
+    Const r -> foldR r
+    Apply _ _ h -> foldMap foldR h
+    CoApply _ _ _ h -> foldMap (foldMap foldR) h
+    Case _ _ b r -> foldMap foldR b <> foldR r
+    CaseInteger _ _ b r -> foldMap foldR b <> foldR r
+    Absurd _ -> mempty
+    ToShrink h -> foldMap foldR h
+
+instance Foldable (Branches x) where
+  foldMap foldR b = case b of
+    Fail -> mempty
+    Alt b1 b2 -> foldMap foldR b1 <> foldMap foldR b2
+    Pat _ d -> foldMap foldR d
+
+instance Foldable (Fields x) where
+  foldMap foldR d = case d of
+    NoField h -> foldR h
+    Field h -> foldMap (foldMap foldR) h
+
+instance Traversable ((:->) a) where
+  traverse traverseR h0 = case h0 of
+    Const r -> Const <$> traverseR r
+    Apply fn f h -> Apply fn f <$> traverse traverseR h
+    CoApply c w f h -> CoApply c w f <$> traverse (traverse traverseR) h
+    Case tn f b r -> Case tn f <$> traverse traverseR b <*> traverseR r
+    CaseInteger tn f b r -> CaseInteger tn f <$> traverse traverseR b <*> traverseR r
+    Absurd f -> pure (Absurd f)
+    ToShrink h -> ToShrink <$> traverse traverseR h
+
+instance Traversable (Branches x) where
+  traverse traverseR b = case b of
+    Fail -> pure Fail
+    Alt b1 b2 -> Alt <$> traverse traverseR b1 <*> traverse traverseR b2
+    Pat cn d -> Pat cn <$> traverse traverseR d
+
+instance Traversable (Fields x) where
+  traverse traverseR d = case d of
+    NoField h -> NoField <$> traverseR h
+    Field h -> Field <$> traverse (traverse traverseR) h
+
+truncateFun :: Int -> (r -> t) -> t -> (a :-> r) -> (a :-> t)
+truncateFun 0 _ s _ = Const s
+truncateFun n truncateR r h0 = case h0 of
+  Const s -> Const (truncateR s)
+  Apply fn f h -> Apply fn f (truncateFun (n-1) truncateR r h)
+  CoApply c w f h -> CoApply c w f (truncateFun (n-1) (truncateFun (n-1) truncateR r) (Const r) h)
+  Case tn f b s -> Case tn f (fmap truncateR b) (truncateR s)
+  CaseInteger tn f b s -> CaseInteger tn f (truncateBin (n-1) truncateR b) (truncateR s)
+  Absurd f -> Absurd f
+  ToShrink h -> truncateFun (n-1) truncateR r h
+
+truncateBin :: Int -> (r -> s) -> Bin r -> Bin s
+truncateBin 0 _ _ = BinEmpty
+truncateBin n truncateR d = case d of
+    BinEmpty -> BinEmpty
+    BinAlt r d0 d1 -> BinAlt (fmap truncateR r) (go d0) (go d1)
+    BinToShrink d' -> go d'
+  where go = truncateBin (n-1) truncateR
diff --git a/test-fun.cabal b/test-fun.cabal
new file mode 100644
--- /dev/null
+++ b/test-fun.cabal
@@ -0,0 +1,48 @@
+name:                test-fun
+version:             0.1.0.0
+synopsis: Testable functions
+description:
+  Generate, shrink, and show functions for testing higher-order properties.
+  See README.
+homepage:            https://github.com/Lysxia/test-fun#readme
+license:             MIT
+license-file:        LICENSE
+author:              Li-yao Xia
+maintainer:          lysxia@gmail.com
+copyright:           2020 Li-yao Xia
+category:            Testing
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+tested-with:         GHC == 8.0.2 || == 8.2.2 || == 8.4.4 || == 8.6.5 || == 8.8.2
+
+library
+  hs-source-dirs:      src
+  exposed-modules:
+    Test.Fun
+    Test.Fun.Internal.CoGen
+    Test.Fun.Internal.Generic
+    Test.Fun.Internal.Orphan
+    Test.Fun.Internal.Pretty
+    Test.Fun.Internal.Shrink
+    Test.Fun.Internal.Types
+  build-depends:
+    base >= 4.9 && < 5
+  ghc-options: -Wall
+  default-language:    Haskell2010
+
+test-suite simple-test
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: test.hs
+  build-depends:
+    test-fun,
+    tasty,
+    tasty-hunit,
+    base
+  ghc-options: -Wall
+  default-language: Haskell2010
+
+source-repository head
+  type:     git
+  location: https://github.com/Lysxia/test-fun
diff --git a/test/test.hs b/test/test.hs
new file mode 100644
--- /dev/null
+++ b/test/test.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE
+    DeriveGeneric,
+    RankNTypes,
+    TypeApplications,
+    TypeOperators #-}
+
+module Main where
+
+import Data.Foldable (for_)
+import GHC.Generics (Generic)
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Test.Fun.Internal.CoGen (Co)
+import Test.Fun.Internal.Generic ((:+)(..), cogenGeneric)
+import Test.Fun.Internal.Pretty
+import Test.Fun.Internal.Types
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "tests"
+  [ testFunctionPretty
+  , testFunctionApply
+  ]
+
+prettyFun_ :: (a :-> String) -> String
+prettyFun_ = prettyFun tConst
+
+testFunctionPretty :: TestTree
+testFunctionPretty = testGroup "pretty"
+  [ testCase "case"
+      $ "case a0 :: Either _ _ of { Left a1 -> 0 ; Right a1 -> case a1 of {} }"
+      @=? prettyFun_
+        (Case "Either _ _" id
+          (Alt
+            (Pat "Left" (Field (NoField (Const "0"))))
+            (Pat "Right" (Field (NoField (Absurd id))))) "0")
+  , testCase "coapply"
+      $ "case a0 0 of {}"
+      @=? prettyFun_ (CoApply hardConcrete (0 :: Int) id (Absurd id))
+  , testCase "apply"
+      $ "case f a0 of {}"
+      @=? prettyFun_ (Apply "f" id (Absurd id))
+  , testCase "case-Integer"
+      $ "case a0 :: Integer of { -1 -> -1 ; 0 -> 0 ; 1 -> 1 ; _ -> 2 }"
+      @=? prettyFun_
+        (CaseInteger "Integer" id
+          (binAlt "0" (binAlt "1" z z) (binAlt "-1" z z)) "2")
+  , testCase "case-Integer-big"
+      $ "case a0 :: Integer of { "
+        ++ concat [ m ++ " -> " ++ m ++ " ; " | n <- [-7 .. 7 :: Int], let m = show n ]
+        ++ "_ -> 22 }"
+      @=? prettyFun_ bigFun
+  ]
+
+testFunctionApply :: TestTree
+testFunctionApply = testCase "apply" $ do
+  for_ ([-7 .. 7]) $ \i -> do
+    show i @=? applyFun bigFun i
+
+bigFun :: Integer :-> String
+bigFun = CaseInteger "Integer" id
+  (binAlt "0"
+    (binAlt "1"
+      (binAlt "2" (binAlt "4" z z) (binAlt "6" z z))
+      (binAlt "3" (binAlt "5" z z) (binAlt "7" z z)))
+    (binAlt "-1"
+      (binAlt "-2" (binAlt "-4" z z) (binAlt "-6" z z))
+      (binAlt "-3" (binAlt "-5" z z) (binAlt "-7" z z)))) "22"
+
+z :: Bin r
+z = BinEmpty
+
+-- Examples
+
+data These a b = This a | That b | Those a b
+  deriving Generic
+
+cogenThese ::
+  forall a b gen.
+  Applicative gen =>
+  (forall r. Co gen a r) ->
+  (forall r. Co gen b r) ->
+  (forall r. Co gen (These a b) r)
+cogenThese cogenA cogenB = cogenGeneric cs where
+  cs = cogenA :+ cogenB :+ (cogenA . cogenB) :+ ()
+
+data Small a = Zero | One a | Two a a
+  deriving Generic
+
+cogenSmall ::
+  forall a gen.
+  Applicative gen =>
+  (forall r. Co gen a r) ->
+  (forall r. Co gen (Small a) r)
+cogenSmall cogenA = cogenGeneric cs where
+  cs = id :+ cogenA :+ (cogenA . cogenA) :+ ()