    {-# LANGUAGE CPP #-}
    {-# LANGUAGE BangPatterns, TypeFamilies, ScopedTypeVariables #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE DefaultSignatures #-}
    {-# LANGUAGE Safe #-}
    -- | Bottoms are ignored for this entire module:
    -- only fully-defined inhabitants are considered inhabitants.
    module Data.Universe.Class
      ( Universe(..)
      , Finite(..)
      ) where

    import Data.Universe.Helpers

    import Control.Applicative (Const (..))
    import Control.Monad (liftM2, liftM3, liftM4, liftM5)
    import Control.Monad.Trans.Identity (IdentityT (..))
    import Control.Monad.Trans.Reader (ReaderT (..))
    import Data.Functor.Compose (Compose (..))
    import Data.Functor.Identity (Identity (..))
    import Data.Functor.Product (Product (..))
    import Data.Functor.Sum (Sum (..))
    import Data.Int (Int, Int8, Int16, Int32, Int64)
    import Data.List (genericLength)
    import Data.List.NonEmpty (NonEmpty (..))
    import Data.Map ((!), fromList)
    import Data.Proxy (Proxy (..))
    import Data.Ratio (Ratio, numerator, denominator, (%))
    import Data.Tagged (Tagged (..), retag)
    import Data.Void (Void)
    import Data.Word  (Word, Word8, Word16, Word32, Word64)
    import GHC.Real (Ratio (..))
    import Numeric.Natural (Natural)

    import qualified Data.Monoid as Mon
    import qualified Data.Semigroup as Semi
    import qualified Data.Set as Set
    import qualified Data.Map as Map

    #if MIN_VERSION_base(4,18,0)
    import Data.Tuple (Solo (MkSolo))
    #elif MIN_VERSION_base(4,16,0)
    import Data.Tuple (Solo (Solo))
    #define MkSolo Solo
    #elif MIN_VERSION_base(4,15,0)
    import GHC.Tuple (Solo (Solo))
    #define MkSolo Solo
    #else
    import Data.Tuple.Solo (Solo (MkSolo))
    #endif

    -- $setup
    -- >>> import Data.List
    -- >>> import Data.Universe.Helpers
    --
    -- -- Show (a -> b) instance (in universe-reverse-instances, but cannot depend on it here).
    -- >>> instance (Finite a, Show a, Show b) => Show (a -> b) where showsPrec n f = showsPrec n [(a, f a) | a <- universeF]

    -- | Creating an instance of this class is a declaration that your type is
    -- recursively enumerable (and that 'universe' is that enumeration). In
    -- particular, you promise that any finite inhabitant has a finite index in
    -- 'universe', and that no inhabitant appears at two different finite indices.
    --
    -- Well-behaved instance should produce elements lazily.
    --
    -- /Laws:/
    --
    -- @
    -- 'elem' x 'universe'                    -- any inhabitant has a finite index
    -- let pfx = 'take' n 'universe'          -- any finite prefix of universe has unique elements
    -- in 'length' pfx = 'length' (nub pfx)
    -- @
    class Universe a where
      universe :: [a]
      default universe :: (Enum a, Bounded a) => [a]
      universe = [a]
    forall a. (Bounded a, Enum a) => [a]
    universeDef

    -- | Creating an instance of this class is a declaration that your 'universe'
    -- eventually ends. Minimal definition: no methods defined. By default,
    -- @universeF = universe@, but for some types (like 'Either') the 'universeF'
    -- method may have a more intuitive ordering.
    --
    -- /Laws:/
    --
    -- @
    -- 'elem' x 'universeF'                       -- any inhabitant has a finite index
    -- 'length' ('filter' (== x) 'universeF') == 1  -- should terminate
    -- (\xs -> 'cardinality' xs == 'genericLength' xs) 'universeF'
    -- @
    --
    -- /Note:/ @'elemIndex' x 'universe' == 'elemIndex' x 'universeF'@
    -- may not hold for all types, though the laws imply that `universe`
    -- is a permutation of `universeF`.
    --
    -- >>> elemIndex (Left True :: Either Bool Bool) universe
    -- Just 2
    --
    -- >>> elemIndex (Left True :: Either Bool Bool) universeF
    -- Just 1
    --
    class Universe a => Finite a where
      universeF :: [a]
      universeF = [a]
    forall a. Universe a => [a]
    universe

      cardinality :: Tagged a Natural
      cardinality = Natural -> Tagged a Natural
    forall {k} (s :: k) b. b -> Tagged s b
    Tagged ([a] -> Natural
    forall i a. Num i => [a] -> i
    genericLength ([a]
    forall a. Finite a => [a]
    universeF :: [a]))

    -------------------------------------------------------------------------------
    -- Base
    -------------------------------------------------------------------------------

    instance Universe ()       where universe :: [()]
    universe = [()]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Bool     where universe :: [Bool]
    universe = [Bool]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Char     where universe :: [Char]
    universe = [Char]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Ordering where universe :: [Ordering]
    universe = [Ordering]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Integer  where universe :: [Integer]
    universe = [Integer
    0, -Integer
    1..] [Integer] -> [Integer] -> [Integer]
    forall a. [a] -> [a] -> [a]
    +++ [Integer
    1..]
    instance Universe Natural  where universe :: [Natural]
    universe = [Natural
    0..]
    instance Universe Int      where universe :: [Int]
    universe = [Int]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Int8     where universe :: [Int8]
    universe = [Int8]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Int16    where universe :: [Int16]
    universe = [Int16]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Int32    where universe :: [Int32]
    universe = [Int32]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Int64    where universe :: [Int64]
    universe = [Int64]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Word     where universe :: [Word]
    universe = [Word]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Word8    where universe :: [Word8]
    universe = [Word8]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Word16   where universe :: [Word16]
    universe = [Word16]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Word32   where universe :: [Word32]
    universe = [Word32]
    forall a. (Bounded a, Enum a) => [a]
    universeDef
    instance Universe Word64   where universe :: [Word64]
    universe = [Word64]
    forall a. (Bounded a, Enum a) => [a]
    universeDef

    instance (Universe a, Universe b) => Universe (Either a b) where universe :: [Either a b]
    universe = (a -> Either a b) -> [a] -> [Either a b]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Either a b
    forall a b. a -> Either a b
    Left [a]
    forall a. Universe a => [a]
    universe [Either a b] -> [Either a b] -> [Either a b]
    forall a. [a] -> [a] -> [a]
    +++ (b -> Either a b) -> [b] -> [Either a b]
    forall a b. (a -> b) -> [a] -> [b]
    map b -> Either a b
    forall a b. b -> Either a b
    Right [b]
    forall a. Universe a => [a]
    universe
    instance  Universe a              => Universe (Maybe  a  ) where universe :: [Maybe a]
    universe = Maybe a
    forall a. Maybe a
    Nothing Maybe a -> [Maybe a] -> [Maybe a]
    forall a. a -> [a] -> [a]
    : (a -> Maybe a) -> [a] -> [Maybe a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Maybe a
    forall a. a -> Maybe a
    Just [a]
    forall a. Universe a => [a]
    universe

    instance (Universe a, Universe b) => Universe (a, b) where universe :: [(a, b)]
    universe = [a]
    forall a. Universe a => [a]
    universe [a] -> [b] -> [(a, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [b]
    forall a. Universe a => [a]
    universe
    instance (Universe a, Universe b, Universe c) => Universe (a, b, c) where universe :: [(a, b, c)]
    universe = [(a
    a,b
    b,c
    c) | ((a
    a,b
    b),c
    c) <- [a]
    forall a. Universe a => [a]
    universe [a] -> [b] -> [(a, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [b]
    forall a. Universe a => [a]
    universe [(a, b)] -> [c] -> [((a, b), c)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [c]
    forall a. Universe a => [a]
    universe]
    instance (Universe a, Universe b, Universe c, Universe d) => Universe (a, b, c, d) where universe :: [(a, b, c, d)]
    universe = [(a
    a,b
    b,c
    c,d
    d) | (((a
    a,b
    b),c
    c),d
    d) <- [a]
    forall a. Universe a => [a]
    universe [a] -> [b] -> [(a, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [b]
    forall a. Universe a => [a]
    universe [(a, b)] -> [c] -> [((a, b), c)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [c]
    forall a. Universe a => [a]
    universe [((a, b), c)] -> [d] -> [(((a, b), c), d)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [d]
    forall a. Universe a => [a]
    universe]
    instance (Universe a, Universe b, Universe c, Universe d, Universe e) => Universe (a, b, c, d, e) where universe :: [(a, b, c, d, e)]
    universe = [(a
    a,b
    b,c
    c,d
    d,e
    e) | ((((a
    a,b
    b),c
    c),d
    d),e
    e) <- [a]
    forall a. Universe a => [a]
    universe [a] -> [b] -> [(a, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [b]
    forall a. Universe a => [a]
    universe [(a, b)] -> [c] -> [((a, b), c)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [c]
    forall a. Universe a => [a]
    universe [((a, b), c)] -> [d] -> [(((a, b), c), d)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [d]
    forall a. Universe a => [a]
    universe [(((a, b), c), d)] -> [e] -> [((((a, b), c), d), e)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [e]
    forall a. Universe a => [a]
    universe]

    instance Universe a => Universe [a] where
      universe :: [[a]]
    universe = [[[a]]] -> [[a]]
    forall a. [[a]] -> [a]
    diagonal ([[[a]]] -> [[a]]) -> [[[a]]] -> [[a]]
    forall a b. (a -> b) -> a -> b
    $ [[]] [[a]] -> [[[a]]] -> [[[a]]]
    forall a. a -> [a] -> [a]
    : [[a
    ha -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    t | [a]
    t <- [[a]]
    forall a. Universe a => [a]
    universe] | a
    h <- [a]
    forall a. Universe a => [a]
    universe]

    instance Universe a => Universe (NonEmpty a) where
      universe :: [NonEmpty a]
    universe = [[NonEmpty a]] -> [NonEmpty a]
    forall a. [[a]] -> [a]
    diagonal [[a
    h a -> [a] -> NonEmpty a
    forall a. a -> [a] -> NonEmpty a
    :| [a]
    t | [a]
    t <- [[a]]
    forall a. Universe a => [a]
    universe] | a
    h <- [a]
    forall a. Universe a => [a]
    universe]

    instance Universe Mon.All where universe :: [All]
    universe = (Bool -> All) -> [Bool] -> [All]
    forall a b. (a -> b) -> [a] -> [b]
    map Bool -> All
    Mon.All [Bool]
    forall a. Universe a => [a]
    universe
    instance Universe Mon.Any where universe :: [Any]
    universe = (Bool -> Any) -> [Bool] -> [Any]
    forall a b. (a -> b) -> [a] -> [b]
    map Bool -> Any
    Mon.Any [Bool]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Mon.Sum     a) where universe :: [Sum a]
    universe = (a -> Sum a) -> [a] -> [Sum a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Sum a
    forall a. a -> Sum a
    Mon.Sum     [a]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Mon.Product a) where universe :: [Product a]
    universe = (a -> Product a) -> [a] -> [Product a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Product a
    forall a. a -> Product a
    Mon.Product [a]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Mon.Dual    a) where universe :: [Dual a]
    universe = (a -> Dual a) -> [a] -> [Dual a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Dual a
    forall a. a -> Dual a
    Mon.Dual    [a]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Mon.First   a) where universe :: [First a]
    universe = (Maybe a -> First a) -> [Maybe a] -> [First a]
    forall a b. (a -> b) -> [a] -> [b]
    map Maybe a -> First a
    forall a. Maybe a -> First a
    Mon.First   [Maybe a]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Mon.Last    a) where universe :: [Last a]
    universe = (Maybe a -> Last a) -> [Maybe a] -> [Last a]
    forall a b. (a -> b) -> [a] -> [b]
    map Maybe a -> Last a
    forall a. Maybe a -> Last a
    Mon.Last    [Maybe a]
    forall a. Universe a => [a]
    universe

    -------------------------------------------------------------------------------
    -- Semi
    -------------------------------------------------------------------------------

    instance Universe a => Universe (Semi.Max   a) where universe :: [Max a]
    universe = (a -> Max a) -> [a] -> [Max a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Max a
    forall a. a -> Max a
    Semi.Max   [a]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Semi.Min   a) where universe :: [Min a]
    universe = (a -> Min a) -> [a] -> [Min a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Min a
    forall a. a -> Min a
    Semi.Min   [a]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Semi.First a) where universe :: [First a]
    universe = (a -> First a) -> [a] -> [First a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> First a
    forall a. a -> First a
    Semi.First [a]
    forall a. Universe a => [a]
    universe
    instance Universe a => Universe (Semi.Last  a) where universe :: [Last a]
    universe = (a -> Last a) -> [a] -> [Last a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Last a
    forall a. a -> Last a
    Semi.Last  [a]
    forall a. Universe a => [a]
    universe

    -------------------------------------------------------------------------------
    -- Rational
    -------------------------------------------------------------------------------

    -- see http://mathlesstraveled.com/2008/01/07/recounting-the-rationals-part-ii-fractions-grow-on-trees/
    --
    -- also, Brent Yorgey writes:
    --
    -- positiveRationals2 :: [Ratio Integer]
    -- positiveRationals2 = iterate' next 1
    --   where
    --     next x = let (n,y) = properFraction x in recip (fromInteger n + 1 - y)
    --     iterate' f x = let x' = f x in x' `seq` (x : iterate' f x')
    --
    -- But this turns out to be substantially slower.
    --
    -- We used to use
    --
    --    positiveRationals =
    --      1 : map lChild positiveRationals +++ map rChild positiveRationals
    --
    -- where lChild and rChild produced the left and right child of each fraction,
    -- respectively. Aside from building unnecessary thunks (thanks to the lazy
    -- map), this had the problem of calculating each sum at least four times:
    -- once for a denominator, a second time for the following numerator, and then two
    -- more times on the other side of the Calkin-Wilf tree. That doesn't
    -- sound too bad, since in practice the integers will be small. But taking each
    -- sum allocates a constructor to wrap the result, and that's not
    -- free. We can avoid the problem with very little additional effort by
    -- interleaving manually. Negative rationals, unfortunately, don't get the
    -- full benefit of sharing here, but we can still share their denominators.

    infixr 5 :<
    data Stream a = !a :< Stream a

    -- All the rational numbers on the left side of the Calkin-Wilf tree,
    -- in breadth-first order.
    leftSideStream :: Integral a => Stream (Ratio a)
    leftSideStream :: forall a. Integral a => Stream (Ratio a)
    leftSideStream = a
    1 a -> a -> Ratio a
    forall a. a -> a -> Ratio a
    :% a
    2 Ratio a -> Stream (Ratio a) -> Stream (Ratio a)
    forall a. a -> Stream a -> Stream a
    :< Stream (Ratio a) -> Stream (Ratio a)
    forall {a}. Num a => Stream (Ratio a) -> Stream (Ratio a)
    go Stream (Ratio a)
    forall a. Integral a => Stream (Ratio a)
    leftSideStream
      where
          go :: Stream (Ratio a) -> Stream (Ratio a)
    go (Ratio a
    x :< Stream (Ratio a)
    xs) = Ratio a
    lChild Ratio a -> Stream (Ratio a) -> Stream (Ratio a)
    forall a. a -> Stream a -> Stream a
    :< Ratio a
    rChild Ratio a -> Stream (Ratio a) -> Stream (Ratio a)
    forall a. a -> Stream a -> Stream a
    :< Stream (Ratio a) -> Stream (Ratio a)
    go Stream (Ratio a)
    xs
            where
              nd :: a
    nd = Ratio a -> a
    forall a. Ratio a -> a
    numerator Ratio a
    x a -> a -> a
    forall a. Num a => a -> a -> a
    + Ratio a -> a
    forall a. Ratio a -> a
    denominator Ratio a
    x
              !lChild :: Ratio a
    lChild = Ratio a -> a
    forall a. Ratio a -> a
    numerator Ratio a
    x a -> a -> Ratio a
    forall a. a -> a -> Ratio a
    :% a
    nd
              !rChild :: Ratio a
    rChild = a
    nd a -> a -> Ratio a
    forall a. a -> a -> Ratio a
    :% Ratio a -> a
    forall a. Ratio a -> a
    denominator Ratio a
    x

    instance RationalUniverse a => Universe (Ratio a) where
      universe :: [Ratio a]
    universe = [Ratio a]
    forall a. RationalUniverse a => [Ratio a]
    rationalUniverse

    class RationalUniverse a where
      rationalUniverse :: [Ratio a]

    instance RationalUniverse Integer where
        -- Why force the negations and reciprocals? This is more expensive if we
        -- ignore most of the result: it allocates four words (generally) for a
        -- negative element rather than two words for a thunk that will evaluate to
        -- one. But it's presumably more common to use the elements in a universe
        -- than to leap over them, so we optimize for the former case. We
        -- interleave manually to avoid allocating four intermediate lists.
        rationalUniverse :: [Ratio Integer]
    rationalUniverse = Ratio Integer
    0 Ratio Integer -> [Ratio Integer] -> [Ratio Integer]
    forall a. a -> [a] -> [a]
    : Ratio Integer
    1 Ratio Integer -> [Ratio Integer] -> [Ratio Integer]
    forall a. a -> [a] -> [a]
    : (-Ratio Integer
    1) Ratio Integer -> [Ratio Integer] -> [Ratio Integer]
    forall a. a -> [a] -> [a]
    : Stream (Ratio Integer) -> [Ratio Integer]
    forall {a}. Integral a => Stream (Ratio a) -> [Ratio a]
    go Stream (Ratio Integer)
    forall a. Integral a => Stream (Ratio a)
    leftSideStream
          where
            go :: Stream (Ratio a) -> [Ratio a]
    go (x :: Ratio a
    x@(a
    xn :% a
    xd) :< Stream (Ratio a)
    xs) =
              let !nx :: Ratio a
    nx = -Ratio a
    x
                  !rx :: Ratio a
    rx = a
    xd a -> a -> Ratio a
    forall a. a -> a -> Ratio a
    :% a
    xn
                  !nrx :: Ratio a
    nrx = -Ratio a
    rx
              in Ratio a
    x Ratio a -> [Ratio a] -> [Ratio a]
    forall a. a -> [a] -> [a]
    : Ratio a
    rx Ratio a -> [Ratio a] -> [Ratio a]
    forall a. a -> [a] -> [a]
    : Ratio a
    nx Ratio a -> [Ratio a] -> [Ratio a]
    forall a. a -> [a] -> [a]
    : Ratio a
    nrx Ratio a -> [Ratio a] -> [Ratio a]
    forall a. a -> [a] -> [a]
    : Stream (Ratio a) -> [Ratio a]
    go Stream (Ratio a)
    xs

    instance RationalUniverse Natural where
        rationalUniverse :: [Ratio Natural]
    rationalUniverse = Ratio Natural
    0 Ratio Natural -> [Ratio Natural] -> [Ratio Natural]
    forall a. a -> [a] -> [a]
    : Ratio Natural
    1 Ratio Natural -> [Ratio Natural] -> [Ratio Natural]
    forall a. a -> [a] -> [a]
    : Stream (Ratio Natural) -> [Ratio Natural]
    forall {a}. Stream (Ratio a) -> [Ratio a]
    go Stream (Ratio Natural)
    forall a. Integral a => Stream (Ratio a)
    leftSideStream
          where
            go :: Stream (Ratio a) -> [Ratio a]
    go (x :: Ratio a
    x@(a
    xn :% a
    xd) :< Stream (Ratio a)
    xs) =
              let !rx :: Ratio a
    rx = a
    xd a -> a -> Ratio a
    forall a. a -> a -> Ratio a
    :% a
    xn
              in Ratio a
    x Ratio a -> [Ratio a] -> [Ratio a]
    forall a. a -> [a] -> [a]
    : Ratio a
    rx Ratio a -> [Ratio a] -> [Ratio a]
    forall a. a -> [a] -> [a]
    : Stream (Ratio a) -> [Ratio a]
    go Stream (Ratio a)
    xs

    -------------------------------------------------------------------------------
    --
    -------------------------------------------------------------------------------

    -- |
    -- >>> mapM_ print (universe :: [Bool -> Bool])
    -- [(False,False),(True,False)]
    -- [(False,False),(True,True)]
    -- [(False,True),(True,False)]
    -- [(False,True),(True,True)]
    --
    instance (Finite a, Ord a, Universe b) => Universe (a -> b) where
      -- could change the Ord constraint to an Eq one, but come on, how many finite
      -- types can't be ordered?
      universe :: [a -> b]
    universe = ([b] -> a -> b) -> [[b]] -> [a -> b]
    forall a b. (a -> b) -> [a] -> [b]
    map [b] -> a -> b
    tableToFunction [[b]]
    tables where
        tables :: [[b]]
    tables          = [[b]] -> [[b]]
    forall a. [[a]] -> [[a]]
    choices [[b]
    forall a. Universe a => [a]
    universe | a
    _ <- [a]
    monoUniverse]
        tableToFunction :: [b] -> a -> b
    tableToFunction = Map a b -> a -> b
    forall k a. Ord k => Map k a -> k -> a
    (!) (Map a b -> a -> b) -> ([b] -> Map a b) -> [b] -> a -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(a, b)] -> Map a b
    forall k a. Ord k => [(k, a)] -> Map k a
    fromList ([(a, b)] -> Map a b) -> ([b] -> [(a, b)]) -> [b] -> Map a b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> [b] -> [(a, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [a]
    monoUniverse
        monoUniverse :: [a]
    monoUniverse    = [a]
    forall a. Finite a => [a]
    universeF

    instance Finite ()       where cardinality :: Tagged () Natural
    cardinality = Tagged () Natural
    1
    instance Finite Bool     where cardinality :: Tagged Bool Natural
    cardinality = Tagged Bool Natural
    2
    instance Finite Char     where cardinality :: Tagged Char Natural
    cardinality = Tagged Char Natural
    1114112
    instance Finite Ordering where cardinality :: Tagged Ordering Natural
    cardinality = Tagged Ordering Natural
    3
    instance Finite Int      where cardinality :: Tagged Int Natural
    cardinality = Int -> Tagged Int Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    forall a. Bounded a => a
    maxBound :: Int) Tagged Int Natural -> Tagged Int Natural -> Tagged Int Natural
    forall a. Num a => a -> a -> a
    - Int -> Tagged Int Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int
    forall a. Bounded a => a
    minBound :: Int) Tagged Int Natural -> Tagged Int Natural -> Tagged Int Natural
    forall a. Num a => a -> a -> a
    + Tagged Int Natural
    1
    instance Finite Int8     where cardinality :: Tagged Int8 Natural
    cardinality = Tagged Int8 Natural
    2Tagged Int8 Natural -> Integer -> Tagged Int8 Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    8
    instance Finite Int16    where cardinality :: Tagged Int16 Natural
    cardinality = Tagged Int16 Natural
    2Tagged Int16 Natural -> Integer -> Tagged Int16 Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    16
    instance Finite Int32    where cardinality :: Tagged Int32 Natural
    cardinality = Tagged Int32 Natural
    2Tagged Int32 Natural -> Integer -> Tagged Int32 Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    32
    instance Finite Int64    where cardinality :: Tagged Int64 Natural
    cardinality = Tagged Int64 Natural
    2Tagged Int64 Natural -> Integer -> Tagged Int64 Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    64
    instance Finite Word     where cardinality :: Tagged Word Natural
    cardinality = Word -> Tagged Word Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word
    forall a. Bounded a => a
    maxBound :: Word) Tagged Word Natural -> Tagged Word Natural -> Tagged Word Natural
    forall a. Num a => a -> a -> a
    - Word -> Tagged Word Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word
    forall a. Bounded a => a
    minBound :: Word) Tagged Word Natural -> Tagged Word Natural -> Tagged Word Natural
    forall a. Num a => a -> a -> a
    + Tagged Word Natural
    1
    instance Finite Word8    where cardinality :: Tagged Word8 Natural
    cardinality = Natural -> Tagged Word8 Natural
    forall {k} (s :: k) b. b -> Tagged s b
    Tagged (Natural -> Tagged Word8 Natural)
    -> Natural -> Tagged Word8 Natural
    forall a b. (a -> b) -> a -> b
    $ Natural
    2Natural -> Integer -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    8
    instance Finite Word16   where cardinality :: Tagged Word16 Natural
    cardinality = Natural -> Tagged Word16 Natural
    forall {k} (s :: k) b. b -> Tagged s b
    Tagged (Natural -> Tagged Word16 Natural)
    -> Natural -> Tagged Word16 Natural
    forall a b. (a -> b) -> a -> b
    $ Natural
    2Natural -> Integer -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    16
    instance Finite Word32   where cardinality :: Tagged Word32 Natural
    cardinality = Natural -> Tagged Word32 Natural
    forall {k} (s :: k) b. b -> Tagged s b
    Tagged (Natural -> Tagged Word32 Natural)
    -> Natural -> Tagged Word32 Natural
    forall a b. (a -> b) -> a -> b
    $ Natural
    2Natural -> Integer -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    32
    instance Finite Word64   where cardinality :: Tagged Word64 Natural
    cardinality = Natural -> Tagged Word64 Natural
    forall {k} (s :: k) b. b -> Tagged s b
    Tagged (Natural -> Tagged Word64 Natural)
    -> Natural -> Tagged Word64 Natural
    forall a b. (a -> b) -> a -> b
    $ Natural
    2Natural -> Integer -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    64

    instance  Finite a            => Finite (Maybe  a  ) where
        cardinality :: Tagged (Maybe a) Natural
    cardinality = (Natural -> Natural)
    -> Tagged (Maybe a) Natural -> Tagged (Maybe a) Natural
    forall a b. (a -> b) -> Tagged (Maybe a) a -> Tagged (Maybe a) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Natural -> Natural
    forall a. Enum a => a -> a
    succ (Tagged a Natural -> Tagged (Maybe a) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))
    instance (Finite a, Finite b) => Finite (Either a b) where
      universeF :: [Either a b]
    universeF = (a -> Either a b) -> [a] -> [Either a b]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Either a b
    forall a b. a -> Either a b
    Left [a]
    forall a. Universe a => [a]
    universe [Either a b] -> [Either a b] -> [Either a b]
    forall a. [a] -> [a] -> [a]
    ++ (b -> Either a b) -> [b] -> [Either a b]
    forall a b. (a -> b) -> [a] -> [b]
    map b -> Either a b
    forall a b. b -> Either a b
    Right [b]
    forall a. Universe a => [a]
    universe
      cardinality :: Tagged (Either a b) Natural
    cardinality = (Natural -> Natural -> Natural)
    -> Tagged (Either a b) Natural
    -> Tagged (Either a b) Natural
    -> Tagged (Either a b) Natural
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (\Natural
    a Natural
    b -> Natural
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    + Natural
    b)
        (Tagged a Natural -> Tagged (Either a b) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))
        (Tagged b Natural -> Tagged (Either a b) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged b Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged b Natural))

    instance (Finite a, Finite b) => Finite (a, b) where
      universeF :: [(a, b)]
    universeF = (a -> b -> (a, b)) -> [a] -> [b] -> [(a, b)]
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (,) [a]
    forall a. Finite a => [a]
    universeF [b]
    forall a. Finite a => [a]
    universeF
      cardinality :: Tagged (a, b) Natural
    cardinality = (Natural -> Natural -> Natural)
    -> Tagged (a, b) Natural
    -> Tagged (a, b) Natural
    -> Tagged (a, b) Natural
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (\Natural
    a Natural
    b -> Natural
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    b)
        (Tagged a Natural -> Tagged (a, b) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))
        (Tagged b Natural -> Tagged (a, b) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged b Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged b Natural))

    instance (Finite a, Finite b, Finite c) => Finite (a, b, c) where
      universeF :: [(a, b, c)]
    universeF = (a -> b -> c -> (a, b, c)) -> [a] -> [b] -> [c] -> [(a, b, c)]
    forall (m :: * -> *) a1 a2 a3 r.
    Monad m =>
    (a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
    liftM3 (,,) [a]
    forall a. Finite a => [a]
    universeF [b]
    forall a. Finite a => [a]
    universeF [c]
    forall a. Finite a => [a]
    universeF
      cardinality :: Tagged (a, b, c) Natural
    cardinality = (Natural -> Natural -> Natural -> Natural)
    -> Tagged (a, b, c) Natural
    -> Tagged (a, b, c) Natural
    -> Tagged (a, b, c) Natural
    -> Tagged (a, b, c) Natural
    forall (m :: * -> *) a1 a2 a3 r.
    Monad m =>
    (a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
    liftM3 (\Natural
    a Natural
    b Natural
    c -> Natural
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    b Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    c)
        (Tagged a Natural -> Tagged (a, b, c) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))
        (Tagged b Natural -> Tagged (a, b, c) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged b Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged b Natural))
        (Tagged c Natural -> Tagged (a, b, c) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged c Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged c Natural))

    instance (Finite a, Finite b, Finite c, Finite d) => Finite (a, b, c, d) where
      universeF :: [(a, b, c, d)]
    universeF = (a -> b -> c -> d -> (a, b, c, d))
    -> [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
    forall (m :: * -> *) a1 a2 a3 a4 r.
    Monad m =>
    (a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
    liftM4 (,,,) [a]
    forall a. Finite a => [a]
    universeF [b]
    forall a. Finite a => [a]
    universeF [c]
    forall a. Finite a => [a]
    universeF [d]
    forall a. Finite a => [a]
    universeF
      cardinality :: Tagged (a, b, c, d) Natural
    cardinality = (Natural -> Natural -> Natural -> Natural -> Natural)
    -> Tagged (a, b, c, d) Natural
    -> Tagged (a, b, c, d) Natural
    -> Tagged (a, b, c, d) Natural
    -> Tagged (a, b, c, d) Natural
    -> Tagged (a, b, c, d) Natural
    forall (m :: * -> *) a1 a2 a3 a4 r.
    Monad m =>
    (a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
    liftM4 (\Natural
    a Natural
    b Natural
    c Natural
    d -> Natural
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    b Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    c Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    d)
        (Tagged a Natural -> Tagged (a, b, c, d) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))
        (Tagged b Natural -> Tagged (a, b, c, d) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged b Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged b Natural))
        (Tagged c Natural -> Tagged (a, b, c, d) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged c Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged c Natural))
        (Tagged d Natural -> Tagged (a, b, c, d) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged d Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged d Natural))

    instance (Finite a, Finite b, Finite c, Finite d, Finite e) => Finite (a, b, c, d, e) where
      universeF :: [(a, b, c, d, e)]
    universeF = (a -> b -> c -> d -> e -> (a, b, c, d, e))
    -> [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
    forall (m :: * -> *) a1 a2 a3 a4 a5 r.
    Monad m =>
    (a1 -> a2 -> a3 -> a4 -> a5 -> r)
    -> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
    liftM5 (,,,,) [a]
    forall a. Finite a => [a]
    universeF [b]
    forall a. Finite a => [a]
    universeF [c]
    forall a. Finite a => [a]
    universeF [d]
    forall a. Finite a => [a]
    universeF [e]
    forall a. Finite a => [a]
    universeF
      cardinality :: Tagged (a, b, c, d, e) Natural
    cardinality = (Natural -> Natural -> Natural -> Natural -> Natural -> Natural)
    -> Tagged (a, b, c, d, e) Natural
    -> Tagged (a, b, c, d, e) Natural
    -> Tagged (a, b, c, d, e) Natural
    -> Tagged (a, b, c, d, e) Natural
    -> Tagged (a, b, c, d, e) Natural
    -> Tagged (a, b, c, d, e) Natural
    forall (m :: * -> *) a1 a2 a3 a4 a5 r.
    Monad m =>
    (a1 -> a2 -> a3 -> a4 -> a5 -> r)
    -> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
    liftM5 (\Natural
    a Natural
    b Natural
    c Natural
    d Natural
    e -> Natural
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    b Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    c Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    d Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    e)
        (Tagged a Natural -> Tagged (a, b, c, d, e) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))
        (Tagged b Natural -> Tagged (a, b, c, d, e) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged b Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged b Natural))
        (Tagged c Natural -> Tagged (a, b, c, d, e) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged c Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged c Natural))
        (Tagged d Natural -> Tagged (a, b, c, d, e) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged d Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged d Natural))
        (Tagged e Natural -> Tagged (a, b, c, d, e) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged e Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged e Natural))

    instance Finite Mon.All where universeF :: [All]
    universeF = (Bool -> All) -> [Bool] -> [All]
    forall a b. (a -> b) -> [a] -> [b]
    map Bool -> All
    Mon.All [Bool]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged All Natural
    cardinality = Tagged All Natural
    2
    instance Finite Mon.Any where universeF :: [Any]
    universeF = (Bool -> Any) -> [Bool] -> [Any]
    forall a b. (a -> b) -> [a] -> [b]
    map Bool -> Any
    Mon.Any [Bool]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged Any Natural
    cardinality = Tagged Any Natural
    2
    instance Finite a => Finite (Mon.Sum     a) where universeF :: [Sum a]
    universeF = (a -> Sum a) -> [a] -> [Sum a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Sum a
    forall a. a -> Sum a
    Mon.Sum     [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Sum a) Natural
    cardinality = (a -> Sum a) -> Tagged a Natural -> Tagged (Sum a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Sum a
    forall a. a -> Sum a
    Mon.Sum     Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance Finite a => Finite (Mon.Product a) where universeF :: [Product a]
    universeF = (a -> Product a) -> [a] -> [Product a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Product a
    forall a. a -> Product a
    Mon.Product [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Product a) Natural
    cardinality = (a -> Product a) -> Tagged a Natural -> Tagged (Product a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Product a
    forall a. a -> Product a
    Mon.Product Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance Finite a => Finite (Mon.Dual    a) where universeF :: [Dual a]
    universeF = (a -> Dual a) -> [a] -> [Dual a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Dual a
    forall a. a -> Dual a
    Mon.Dual    [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Dual a) Natural
    cardinality = (a -> Dual a) -> Tagged a Natural -> Tagged (Dual a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Dual a
    forall a. a -> Dual a
    Mon.Dual    Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance Finite a => Finite (Mon.First   a) where universeF :: [First a]
    universeF = (Maybe a -> First a) -> [Maybe a] -> [First a]
    forall a b. (a -> b) -> [a] -> [b]
    map Maybe a -> First a
    forall a. Maybe a -> First a
    Mon.First   [Maybe a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (First a) Natural
    cardinality = (Maybe a -> First a)
    -> Tagged (Maybe a) Natural -> Tagged (First a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith Maybe a -> First a
    forall a. Maybe a -> First a
    Mon.First   Tagged (Maybe a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance Finite a => Finite (Mon.Last    a) where universeF :: [Last a]
    universeF = (Maybe a -> Last a) -> [Maybe a] -> [Last a]
    forall a b. (a -> b) -> [a] -> [b]
    map Maybe a -> Last a
    forall a. Maybe a -> Last a
    Mon.Last    [Maybe a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Last a) Natural
    cardinality = (Maybe a -> Last a)
    -> Tagged (Maybe a) Natural -> Tagged (Last a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith Maybe a -> Last a
    forall a. Maybe a -> Last a
    Mon.Last    Tagged (Maybe a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality

    instance Finite a => Finite (Semi.Max   a) where universeF :: [Max a]
    universeF = (a -> Max a) -> [a] -> [Max a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Max a
    forall a. a -> Max a
    Semi.Max   [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Max a) Natural
    cardinality = (a -> Max a) -> Tagged a Natural -> Tagged (Max a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Max a
    forall a. a -> Max a
    Semi.Max   Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance Finite a => Finite (Semi.Min   a) where universeF :: [Min a]
    universeF = (a -> Min a) -> [a] -> [Min a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Min a
    forall a. a -> Min a
    Semi.Min   [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Min a) Natural
    cardinality = (a -> Min a) -> Tagged a Natural -> Tagged (Min a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Min a
    forall a. a -> Min a
    Semi.Min   Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance Finite a => Finite (Semi.First a) where universeF :: [First a]
    universeF = (a -> First a) -> [a] -> [First a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> First a
    forall a. a -> First a
    Semi.First [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (First a) Natural
    cardinality = (a -> First a) -> Tagged a Natural -> Tagged (First a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> First a
    forall a. a -> First a
    Semi.First Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance Finite a => Finite (Semi.Last  a) where universeF :: [Last a]
    universeF = (a -> Last a) -> [a] -> [Last a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Last a
    forall a. a -> Last a
    Semi.Last  [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Last a) Natural
    cardinality = (a -> Last a) -> Tagged a Natural -> Tagged (Last a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Last a
    forall a. a -> Last a
    Semi.Last  Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality

    -- |
    -- >>> mapM_ print (universeF :: [Bool -> Bool])
    -- [(False,False),(True,False)]
    -- [(False,False),(True,True)]
    -- [(False,True),(True,False)]
    -- [(False,True),(True,True)]
    --
    -- >>> cardinality :: Tagged (Bool -> Ordering) Natural
    -- Tagged 9
    --
    -- >>> cardinality :: Tagged (Ordering -> Bool) Natural
    -- Tagged 8
    --
    instance (Ord a, Finite a, Finite b) => Finite (a -> b) where
      universeF :: [a -> b]
    universeF = ([b] -> a -> b) -> [[b]] -> [a -> b]
    forall a b. (a -> b) -> [a] -> [b]
    map [b] -> a -> b
    tableToFunction [[b]]
    tables where
        tables :: [[b]]
    tables          = [[b]] -> [[b]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [[b]
    forall a. Finite a => [a]
    universeF | a
    _ <- [a]
    monoUniverse]
        tableToFunction :: [b] -> a -> b
    tableToFunction = Map a b -> a -> b
    forall k a. Ord k => Map k a -> k -> a
    (!) (Map a b -> a -> b) -> ([b] -> Map a b) -> [b] -> a -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(a, b)] -> Map a b
    forall k a. Ord k => [(k, a)] -> Map k a
    fromList ([(a, b)] -> Map a b) -> ([b] -> [(a, b)]) -> [b] -> Map a b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> [b] -> [(a, b)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [a]
    monoUniverse
        monoUniverse :: [a]
    monoUniverse    = [a]
    forall a. Finite a => [a]
    universeF
      cardinality :: Tagged (a -> b) Natural
    cardinality = (Natural -> Natural -> Natural)
    -> Tagged (a -> b) Natural
    -> Tagged (a -> b) Natural
    -> Tagged (a -> b) Natural
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Natural -> Natural -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    (^)
        (Tagged b Natural -> Tagged (a -> b) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged b Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged b Natural))
        (Tagged a Natural -> Tagged (a -> b) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))

    -- to add when somebody asks for it: instance (Eq a, Finite a) => Finite (Endo a) (+Universe)

    -------------------------------------------------------------------------------
    -- void
    -------------------------------------------------------------------------------

    instance Universe Void where universe :: [Void]
    universe = []
    instance Finite Void where cardinality :: Tagged Void Natural
    cardinality = Tagged Void Natural
    0

    -------------------------------------------------------------------------------
    -- tagged
    -------------------------------------------------------------------------------

    instance Universe (Proxy a) where universe :: [Proxy a]
    universe = [Proxy a
    forall {k} (t :: k). Proxy t
    Proxy]
    instance Finite (Proxy a) where cardinality :: Tagged (Proxy a) Natural
    cardinality = Tagged (Proxy a) Natural
    1

    instance Universe a => Universe (Tagged b a) where universe :: [Tagged b a]
    universe = (a -> Tagged b a) -> [a] -> [Tagged b a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Tagged b a
    forall {k} (s :: k) b. b -> Tagged s b
    Tagged [a]
    forall a. Universe a => [a]
    universe
    instance Finite a => Finite (Tagged b a) where cardinality :: Tagged (Tagged b a) Natural
    cardinality = (a -> Tagged b a)
    -> Tagged a Natural -> Tagged (Tagged b a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Tagged b a
    forall {k} (s :: k) b. b -> Tagged s b
    Tagged Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality

    -------------------------------------------------------------------------------
    -- containers
    -------------------------------------------------------------------------------

    -- |
    -- >>> import qualified Data.Set as Set
    -- >>> mapM_ print (universe :: [Set.Set Bool])
    -- fromList []
    -- fromList [False]
    -- fromList [True]
    -- fromList [False,True]
    --
    instance (Ord a, Universe a) => Universe (Set.Set a) where
        universe :: [Set a]
    universe = Set a
    forall a. Set a
    Set.empty Set a -> [Set a] -> [Set a]
    forall a. a -> [a] -> [a]
    : [a] -> [Set a]
    forall {a}. Ord a => [a] -> [Set a]
    go [a]
    forall a. Universe a => [a]
    universe
          where
            go :: [a] -> [Set a]
    go []     = []
            go (a
    x:[a]
    xs) = a -> Set a
    forall a. a -> Set a
    Set.singleton a
    x Set a -> [Set a] -> [Set a]
    forall a. a -> [a] -> [a]
    : [Set a] -> [Set a]
    inter ([a] -> [Set a]
    go [a]
    xs)
              where
                -- Probably more efficient than using (+++)
                inter :: [Set a] -> [Set a]
    inter []     = []
                inter (Set a
    y:[Set a]
    ys) = Set a
    y Set a -> [Set a] -> [Set a]
    forall a. a -> [a] -> [a]
    : a -> Set a -> Set a
    forall a. Ord a => a -> Set a -> Set a
    Set.insert a
    x Set a
    y Set a -> [Set a] -> [Set a]
    forall a. a -> [a] -> [a]
    : [Set a] -> [Set a]
    inter [Set a]
    ys

    instance (Ord a, Finite a) => Finite (Set.Set a) where
        cardinality :: Tagged (Set a) Natural
    cardinality = Tagged a Natural -> Tagged (Set a) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag ((Natural -> Natural) -> Tagged a Natural -> Tagged a Natural
    forall a b. (a -> b) -> Tagged a a -> Tagged a b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Natural
    2 Natural -> Natural -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^) (Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged a Natural))

    -- |
    -- >>> import qualified Data.Map as Map
    -- >>> mapM_ print (universe :: [Map.Map Bool Bool])
    -- fromList []
    -- fromList [(True,False)]
    -- fromList [(False,False)]
    -- fromList [(True,True)]
    -- fromList [(False,False),(True,False)]
    -- fromList [(False,True)]
    -- fromList [(False,False),(True,True)]
    -- fromList [(False,True),(True,False)]
    -- fromList [(False,True),(True,True)]
    --
    --
    instance (Ord k, Finite k, Universe v) => Universe (Map.Map k v) where
      universe :: [Map k v]
    universe = ([Maybe v] -> Map k v) -> [[Maybe v]] -> [Map k v]
    forall a b. (a -> b) -> [a] -> [b]
    map [Maybe v] -> Map k v
    tableToFunction [[Maybe v]]
    tables where
        tables :: [[Maybe v]]
    tables          = [[Maybe v]] -> [[Maybe v]]
    forall a. [[a]] -> [[a]]
    choices [[Maybe v]
    forall a. Universe a => [a]
    universe | k
    _ <- [k]
    monoUniverse]
        tableToFunction :: [Maybe v] -> Map k v
    tableToFunction = [(k, Maybe v)] -> Map k v
    forall {k} {a}. Ord k => [(k, Maybe a)] -> Map k a
    fromList' ([(k, Maybe v)] -> Map k v)
    -> ([Maybe v] -> [(k, Maybe v)]) -> [Maybe v] -> Map k v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [k] -> [Maybe v] -> [(k, Maybe v)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [k]
    monoUniverse
        monoUniverse :: [k]
    monoUniverse    = [k]
    forall a. Finite a => [a]
    universeF
        fromList' :: [(k, Maybe a)] -> Map k a
    fromList' [(k, Maybe a)]
    xs = [(k, a)] -> Map k a
    forall k a. Ord k => [(k, a)] -> Map k a
    fromList [ (k
    k,a
    v) | (k
    k, Just a
    v) <- [(k, Maybe a)]
    xs ]

    instance (Ord k, Finite k, Finite v) => Finite (Map.Map k v) where
      universeF :: [Map k v]
    universeF = ([Maybe v] -> Map k v) -> [[Maybe v]] -> [Map k v]
    forall a b. (a -> b) -> [a] -> [b]
    map [Maybe v] -> Map k v
    tableToFunction [[Maybe v]]
    tables where
        tables :: [[Maybe v]]
    tables          = [[Maybe v]] -> [[Maybe v]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [[Maybe v]
    forall a. Finite a => [a]
    universeF | k
    _ <- [k]
    monoUniverse]
        tableToFunction :: [Maybe v] -> Map k v
    tableToFunction = [(k, Maybe v)] -> Map k v
    forall {k} {a}. Ord k => [(k, Maybe a)] -> Map k a
    fromList' ([(k, Maybe v)] -> Map k v)
    -> ([Maybe v] -> [(k, Maybe v)]) -> [Maybe v] -> Map k v
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [k] -> [Maybe v] -> [(k, Maybe v)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [k]
    monoUniverse
        monoUniverse :: [k]
    monoUniverse    = [k]
    forall a. Finite a => [a]
    universeF
        fromList' :: [(k, Maybe a)] -> Map k a
    fromList' [(k, Maybe a)]
    xs = [(k, a)] -> Map k a
    forall k a. Ord k => [(k, a)] -> Map k a
    fromList [ (k
    k,a
    v) | (k
    k, Just a
    v) <- [(k, Maybe a)]
    xs ]

      cardinality :: Tagged (Map k v) Natural
    cardinality = (Natural -> Natural -> Natural)
    -> Tagged (Map k v) Natural
    -> Tagged (Map k v) Natural
    -> Tagged (Map k v) Natural
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (\Natural
    b Natural
    a -> (Natural
    1 Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    + Natural
    b) Natural -> Natural -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Natural
    a)
        (Tagged v Natural -> Tagged (Map k v) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged v Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged v Natural))
        (Tagged k Natural -> Tagged (Map k v) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged k Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged k Natural))

    -------------------------------------------------------------------------------
    -- transformers
    -------------------------------------------------------------------------------

    instance  Universe  a => Universe (Const a b) where universe :: [Const a b]
    universe  = (a -> Const a b) -> [a] -> [Const a b]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Const a b
    forall {k} a (b :: k). a -> Const a b
    Const [a]
    forall a. Universe a => [a]
    universe
    instance  Finite    a => Finite   (Const a b) where universeF :: [Const a b]
    universeF = (a -> Const a b) -> [a] -> [Const a b]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Const a b
    forall {k} a (b :: k). a -> Const a b
    Const [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Const a b) Natural
    cardinality = (a -> Const a b) -> Tagged a Natural -> Tagged (Const a b) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Const a b
    forall {k} a (b :: k). a -> Const a b
    Const Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality

    instance  Universe    a                    => Universe (Identity    a) where universe :: [Identity a]
    universe  = (a -> Identity a) -> [a] -> [Identity a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Identity a
    forall a. a -> Identity a
    Identity  [a]
    forall a. Universe a => [a]
    universe
    instance  Universe (f a)                   => Universe (IdentityT f a) where universe :: [IdentityT f a]
    universe  = (f a -> IdentityT f a) -> [f a] -> [IdentityT f a]
    forall a b. (a -> b) -> [a] -> [b]
    map f a -> IdentityT f a
    forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
    IdentityT [f a]
    forall a. Universe a => [a]
    universe
    instance (Finite e, Ord e, Universe (m a)) => Universe (ReaderT e m a) where universe :: [ReaderT e m a]
    universe  = ((e -> m a) -> ReaderT e m a) -> [e -> m a] -> [ReaderT e m a]
    forall a b. (a -> b) -> [a] -> [b]
    map (e -> m a) -> ReaderT e m a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT   [e -> m a]
    forall a. Universe a => [a]
    universe
    instance  Universe (f (g a))               => Universe (Compose f g a) where universe :: [Compose f g a]
    universe  = (f (g a) -> Compose f g a) -> [f (g a)] -> [Compose f g a]
    forall a b. (a -> b) -> [a] -> [b]
    map f (g a) -> Compose f g a
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose   [f (g a)]
    forall a. Universe a => [a]
    universe
    instance (Universe (f a), Universe (g a))  => Universe (Product f g a) where universe :: [Product f g a]
    universe  = [f a -> g a -> Product f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f a
    f g a
    g | (f a
    f, g a
    g) <- [f a]
    forall a. Universe a => [a]
    universe [f a] -> [g a] -> [(f a, g a)]
    forall a b. [a] -> [b] -> [(a, b)]
    +*+ [g a]
    forall a. Universe a => [a]
    universe]
    instance (Universe (f a), Universe (g a))  => Universe (Sum     f g a) where universe :: [Sum f g a]
    universe  = (f a -> Sum f g a) -> [f a] -> [Sum f g a]
    forall a b. (a -> b) -> [a] -> [b]
    map f a -> Sum f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL [f a]
    forall a. Universe a => [a]
    universe [Sum f g a] -> [Sum f g a] -> [Sum f g a]
    forall a. [a] -> [a] -> [a]
    +++ (g a -> Sum f g a) -> [g a] -> [Sum f g a]
    forall a b. (a -> b) -> [a] -> [b]
    map g a -> Sum f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
    InR [g a]
    forall a. Universe a => [a]
    universe

    instance  Finite       a                   => Finite   (Identity    a) where universeF :: [Identity a]
    universeF = (a -> Identity a) -> [a] -> [Identity a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Identity a
    forall a. a -> Identity a
    Identity  [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Identity a) Natural
    cardinality = (a -> Identity a)
    -> Tagged a Natural -> Tagged (Identity a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Identity a
    forall a. a -> Identity a
    Identity  Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance  Finite    (f a)                  => Finite   (IdentityT f a) where universeF :: [IdentityT f a]
    universeF = (f a -> IdentityT f a) -> [f a] -> [IdentityT f a]
    forall a b. (a -> b) -> [a] -> [b]
    map f a -> IdentityT f a
    forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
    IdentityT [f a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (IdentityT f a) Natural
    cardinality = (f a -> IdentityT f a)
    -> Tagged (f a) Natural -> Tagged (IdentityT f a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith f a -> IdentityT f a
    forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
    IdentityT Tagged (f a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance (Finite e, Ord e, Finite   (m a)) => Finite   (ReaderT e m a) where universeF :: [ReaderT e m a]
    universeF = ((e -> m a) -> ReaderT e m a) -> [e -> m a] -> [ReaderT e m a]
    forall a b. (a -> b) -> [a] -> [b]
    map (e -> m a) -> ReaderT e m a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT   [e -> m a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (ReaderT e m a) Natural
    cardinality = ((e -> m a) -> ReaderT e m a)
    -> Tagged (e -> m a) Natural -> Tagged (ReaderT e m a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith (e -> m a) -> ReaderT e m a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT   Tagged (e -> m a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance  Finite (f (g a))                 => Finite   (Compose f g a) where universeF :: [Compose f g a]
    universeF = (f (g a) -> Compose f g a) -> [f (g a)] -> [Compose f g a]
    forall a b. (a -> b) -> [a] -> [b]
    map f (g a) -> Compose f g a
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose   [f (g a)]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Compose f g a) Natural
    cardinality = (f (g a) -> Compose f g a)
    -> Tagged (f (g a)) Natural -> Tagged (Compose f g a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith f (g a) -> Compose f g a
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose   Tagged (f (g a)) Natural
    forall a. Finite a => Tagged a Natural
    cardinality
    instance (Finite (f a), Finite (g a))      => Finite   (Product f g a) where
      universeF :: [Product f g a]
    universeF = (f a -> g a -> Product f g a) -> [f a] -> [g a] -> [Product f g a]
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 f a -> g a -> Product f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair [f a]
    forall a. Finite a => [a]
    universeF [g a]
    forall a. Finite a => [a]
    universeF
      cardinality :: Tagged (Product f g a) Natural
    cardinality = (Natural -> Natural -> Natural)
    -> Tagged (Product f g a) Natural
    -> Tagged (Product f g a) Natural
    -> Tagged (Product f g a) Natural
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    (*)
        (Tagged (f a) Natural -> Tagged (Product f g a) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged (f a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged (f a) Natural))
        (Tagged (g a) Natural -> Tagged (Product f g a) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged (g a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged (g a) Natural))
    instance (Finite (f a), Finite (g a))      => Finite   (Sum f g a) where
      universeF :: [Sum f g a]
    universeF =  (f a -> Sum f g a) -> [f a] -> [Sum f g a]
    forall a b. (a -> b) -> [a] -> [b]
    map f a -> Sum f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL [f a]
    forall a. Universe a => [a]
    universe [Sum f g a] -> [Sum f g a] -> [Sum f g a]
    forall a. [a] -> [a] -> [a]
    ++ (g a -> Sum f g a) -> [g a] -> [Sum f g a]
    forall a b. (a -> b) -> [a] -> [b]
    map g a -> Sum f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
    InR [g a]
    forall a. Universe a => [a]
    universe
      cardinality :: Tagged (Sum f g a) Natural
    cardinality = (Natural -> Natural -> Natural)
    -> Tagged (Sum f g a) Natural
    -> Tagged (Sum f g a) Natural
    -> Tagged (Sum f g a) Natural
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    (+)
        (Tagged (f a) Natural -> Tagged (Sum f g a) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged (f a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged (f a) Natural))
        (Tagged (g a) Natural -> Tagged (Sum f g a) Natural
    forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
    retag (Tagged (g a) Natural
    forall a. Finite a => Tagged a Natural
    cardinality :: Tagged (g a) Natural))

    -------------------------------------------------------------------------------
    -- OneTuple
    -------------------------------------------------------------------------------

    -- @since 1.1.3
    instance  Universe a => Universe (Solo a) where universe :: [Solo a]
    universe  = (a -> Solo a) -> [a] -> [Solo a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Solo a
    forall a. a -> Solo a
    MkSolo [a]
    forall a. Universe a => [a]
    universe

    -- @since 1.1.3
    instance  Finite   a => Finite   (Solo a) where universeF :: [Solo a]
    universeF = (a -> Solo a) -> [a] -> [Solo a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Solo a
    forall a. a -> Solo a
    MkSolo [a]
    forall a. Finite a => [a]
    universeF; cardinality :: Tagged (Solo a) Natural
    cardinality = (a -> Solo a) -> Tagged a Natural -> Tagged (Solo a) Natural
    forall a b x. (a -> b) -> Tagged a x -> Tagged b x
    retagWith a -> Solo a
    forall a. a -> Solo a
    MkSolo Tagged a Natural
    forall a. Finite a => Tagged a Natural
    cardinality