    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE QuantifiedConstraints #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE LambdaCase #-}

    module Hedgehog.Classes.Foldable (foldableLaws) where

    import Hedgehog
    import Hedgehog.Classes.Common

    import Control.Monad.IO.Class (MonadIO(..))
    import Control.Exception (ErrorCall(..), try, evaluate)
    import Data.Monoid (Sum(..), Endo(..), Dual(..))
    import qualified Data.Foldable as Foldable

    -- | Tests the following 'Foldable' laws:
    --
    -- [__Fold__]: @'Foldable.fold' ≡ 'Foldable.foldMap' 'id'@
    -- [__FoldMap__]: @'Foldable.foldMap' f ≡ 'Foldable.foldr' ('mappend' '.' f) 'mempty'@
    -- [__Foldr__]: @'Foldable.foldr' f z t ≡ 'appEndo' ('Foldable.foldMap' ('Endo' '.' f) t) z@
    -- [__Foldr'__]: @'Foldable.foldr'' f z0 t ≡ 'Foldable.foldl' f' 'id' t z0, where f' k x z = k '$!' f x z@
    -- [__Foldl__]: @'Foldable.foldl' f z t ≡ 'appEndo' ('getDual' ('Foldable.foldMap' ('Dual' '.' 'Endo' '.' 'flip' f) t)) z@
    -- [__Foldl'__]: @'Foldable.foldl'' f z0 xs ≡ 'Foldable.foldr' f' 'id' xs z0, where f' x k z = k '$!' f z x@
    -- [__Foldl1__]: @'Foldable.foldl1' f t ≡ let (x:xs) = 'Foldable.toList' t in 'foldl' f x xs@
    -- [__Foldr1__]: @'Foldable.foldr1' f t ≡ let (xs,x)@ = @unsnoc ('Foldable.toList' t) in 'foldr' f x xs@
    -- [__ToList__]: @'Foldable.toList' ≡ 'Foldable.foldr' (:) []@
    -- [__Null__]: @'Foldable.null' ≡ 'Foldable.foldr' ('const' ('const' 'False')) 'True'@
    -- [__Length__]: @'Foldable.length' ≡ 'getSum' '.' 'Foldable.foldMap' ('const' ('Sum' 1))@
    --
    -- This additionally tests that the user's implementations of 'Foldable.foldr'' and 'Foldable.foldl'' are strict in their accumulators.
    foldableLaws ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Laws
    foldableLaws :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Laws
    foldableLaws forall x. Gen x -> Gen (f x)
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "Foldable"
      [ (String
    "fold", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFold Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "foldMap", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldMap Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "foldr", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "foldr'", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr' Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "foldl", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "foldl'", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl' Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "foldl1", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl1 Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "foldr1", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr1 Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "toList", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableToList Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "null", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableNull Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "length", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableLength Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      ]

    foldableFold ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFold :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFold forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      a <- Gen (f [Integer]) -> PropertyT IO (f [Integer])
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f [Integer]) -> PropertyT IO (f [Integer]))
    -> Gen (f [Integer]) -> PropertyT IO (f [Integer])
    forall a b. (a -> b) -> a -> b
    $ Gen [Integer] -> Gen (f [Integer])
    forall x. Gen x -> Gen (f x)
    fgen (Gen [Integer] -> Gen (f [Integer]))
    -> Gen [Integer] -> Gen (f [Integer])
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen [Integer]
    forall a. Gen a -> Gen [a]
    genVerySmallList Gen Integer
    genSmallInteger
      let lhs = f [Integer] -> [Integer]
    forall m. Monoid m => f m -> m
    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
    Foldable.fold f [Integer]
    a
      let rhs = ([Integer] -> [Integer]) -> f [Integer] -> [Integer]
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    Foldable.foldMap [Integer] -> [Integer]
    forall a. a -> a
    id f [Integer]
    a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Fold"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "fold" String -> String -> String
    `congruency` String
    "foldMap id"
            , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showA :: String
    showA = f [Integer] -> String
    forall a. Show a => a -> String
    show f [Integer]
    a
                in [String] -> String
    lawWhere
                  [ String
    "fold a" String -> String -> String
    `congruency` String
    "foldMap id a, where"
                  , String
    "a = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                  ]
            , lawContextReduced :: String
    lawContextReduced = [Integer] -> [Integer] -> String
    forall a. Show a => a -> a -> String
    reduced [Integer]
    lhs [Integer]
    rhs
            }

      heqCtx lhs rhs ctx

    foldableFoldMap ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldMap :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldMap forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      a <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      e <- forAll genQuadraticEquation
      let f = (Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    :[]) (Integer -> [Integer])
    -> (Integer -> Integer) -> Integer -> [Integer]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QuadraticEquation -> Integer -> Integer
    runQuadraticEquation QuadraticEquation
    e
      let lhs = (Integer -> [Integer]) -> f Integer -> [Integer]
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    Foldable.foldMap Integer -> [Integer]
    f f Integer
    a
      let rhs = (Integer -> [Integer] -> [Integer])
    -> [Integer] -> f Integer -> [Integer]
    forall a b. (a -> b -> b) -> b -> f a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Foldable.foldr ([Integer] -> [Integer] -> [Integer]
    forall a. Monoid a => a -> a -> a
    mappend ([Integer] -> [Integer] -> [Integer])
    -> (Integer -> [Integer]) -> Integer -> [Integer] -> [Integer]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> [Integer]
    f) [Integer]
    forall a. Monoid a => a
    mempty f Integer
    a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "FoldMap"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "foldMap f" String -> String -> String
    `congruency` String
    "foldr (mappend . f) mempty"
            , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showA :: String
    showA = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    a
                    showF :: String
    showF = String
    "(:[]) $ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QuadraticEquation -> String
    forall a. Show a => a -> String
    show QuadraticEquation
    e
                in [String] -> String
    lawWhere
                  [ String
    "foldMap f a" String -> String -> String
    `congruency` String
    "foldr (mappend . f) mempty  a, where"
                  , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                  , String
    "a = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                  ]
            , lawContextReduced :: String
    lawContextReduced = [Integer] -> [Integer] -> String
    forall a. Show a => a -> a -> String
    reduced [Integer]
    lhs [Integer]
    rhs
            }
      heqCtx lhs rhs ctx

    foldableFoldr ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      e <- Gen LinearEquationTwo -> PropertyT IO LinearEquationTwo
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquationTwo
    genLinearEquationTwo
      z <- forAll genSmallInteger
      t <- forAll $ fgen genSmallInteger
      let f = LinearEquationTwo -> Integer -> Integer -> Integer
    runLinearEquationTwo LinearEquationTwo
    e
      let lhs = (Integer -> Integer -> Integer) -> Integer -> f Integer -> Integer
    forall a b. (a -> b -> b) -> b -> f a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Foldable.foldr Integer -> Integer -> Integer
    f Integer
    z f Integer
    t
      let rhs = Endo Integer -> Integer -> Integer
    forall a. Endo a -> a -> a
    appEndo ((Integer -> Endo Integer) -> f Integer -> Endo Integer
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    Foldable.foldMap ((Integer -> Integer) -> Endo Integer
    forall a. (a -> a) -> Endo a
    Endo ((Integer -> Integer) -> Endo Integer)
    -> (Integer -> Integer -> Integer) -> Integer -> Endo Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> Integer
    f) f Integer
    t) Integer
    z
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Foldr"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "foldr f z t" String -> String -> String
    `congruency` String
    "appEndo (foldMap (Endo . f) t) z"
            , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showT :: String
    showT = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    t
                    showF :: String
    showF = LinearEquationTwo -> String
    forall a. Show a => a -> String
    show LinearEquationTwo
    e
                    showZ :: String
    showZ = Integer -> String
    forall a. Show a => a -> String
    show Integer
    z
                in [String] -> String
    lawWhere
                  [ String
    "foldr f z t" String -> String -> String
    `congruency` String
    "appEndo (foldMap (Endo . f) t) z"
                  , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                  , String
    "z = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showZ
                  , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                  ]
            , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
            }
      heqCtx lhs rhs ctx

    foldableFoldl ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      e <- Gen LinearEquationTwo -> PropertyT IO LinearEquationTwo
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquationTwo
    genLinearEquationTwo
      z <- forAll genSmallInteger
      t <- forAll $ fgen genSmallInteger
      let f = LinearEquationTwo -> Integer -> Integer -> Integer
    runLinearEquationTwo LinearEquationTwo
    e
      let lhs = (Integer -> Integer -> Integer) -> Integer -> f Integer -> Integer
    forall b a. (b -> a -> b) -> b -> f a -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    Foldable.foldl Integer -> Integer -> Integer
    f Integer
    z f Integer
    t
      let rhs = Endo Integer -> Integer -> Integer
    forall a. Endo a -> a -> a
    appEndo (Dual (Endo Integer) -> Endo Integer
    forall a. Dual a -> a
    getDual ((Integer -> Dual (Endo Integer))
    -> f Integer -> Dual (Endo Integer)
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    Foldable.foldMap (Endo Integer -> Dual (Endo Integer)
    forall a. a -> Dual a
    Dual (Endo Integer -> Dual (Endo Integer))
    -> (Integer -> Endo Integer) -> Integer -> Dual (Endo Integer)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Integer -> Integer) -> Endo Integer
    forall a. (a -> a) -> Endo a
    Endo ((Integer -> Integer) -> Endo Integer)
    -> (Integer -> Integer -> Integer) -> Integer -> Endo Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Integer -> Integer -> Integer
    f) f Integer
    t)) Integer
    z
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Foldl"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "foldl f z t" String -> String -> String
    `congruency` String
    "appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z"
            , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showT :: String
    showT = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    t
                    showF :: String
    showF = LinearEquationTwo -> String
    forall a. Show a => a -> String
    show LinearEquationTwo
    e
                    showZ :: String
    showZ = Integer -> String
    forall a. Show a => a -> String
    show Integer
    z
                in [String] -> String
    lawWhere
                  [ String
    "foldl f z t" String -> String -> String
    `congruency` String
    "appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z"
                  , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                  , String
    "z = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showZ
                  , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                  ]
            , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
            }
      heqCtx lhs rhs ctx

    ctxNotStrict :: String -> Context
    ctxNotStrict :: String -> Context
    ctxNotStrict String
    str = String -> Context
    Context (String -> Context) -> String -> Context
    forall a b. (a -> b) -> a -> b
    $ String
    "Your implementation of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    str String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not strict."

    foldableFoldr' ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr' :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr' forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      xs <- Gen (f (Bottom Integer)) -> PropertyT IO (f (Bottom Integer))
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f (Bottom Integer)) -> PropertyT IO (f (Bottom Integer)))
    -> Gen (f (Bottom Integer)) -> PropertyT IO (f (Bottom Integer))
    forall a b. (a -> b) -> a -> b
    $ Gen (Bottom Integer) -> Gen (f (Bottom Integer))
    forall x. Gen x -> Gen (f x)
    fgen (Gen Integer -> Gen (Bottom Integer)
    forall a. Gen a -> Gen (Bottom a)
    genBottom Gen Integer
    genSmallInteger)
      let f :: Bottom Integer -> Integer -> Integer
          f Bottom Integer
    a Integer
    b = case Bottom Integer
    a of
            Bottom Integer
    BottomUndefined -> String -> Integer
    forall a. HasCallStack => String -> a
    error String
    "foldableFoldr': your foldr' is not strict!"
            BottomValue Integer
    v -> if Integer -> Bool
    forall a. Integral a => a -> Bool
    even Integer
    v then Integer
    v else Integer
    b
      z0 <- forAll genSmallInteger
      (rhs, ctx1) <- liftIO $ do
        let f' Integer -> b
    k Bottom Integer
    x Integer
    z = Integer -> b
    k (Integer -> b) -> Integer -> b
    forall a b. (a -> b) -> a -> b
    $! Bottom Integer -> Integer -> Integer
    f Bottom Integer
    x Integer
    z
        e <- try (evaluate (Foldable.foldl f' id xs z0))
        case e of
          Left (ErrorCall
    _ :: ErrorCall) -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Integer
    forall a. Maybe a
    Nothing, String -> Context
    ctxNotStrict String
    "foldr'")
          Right Integer
    i -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    i, Context
    NoContext)
      (lhs, ctx2) <- liftIO $ do
        e <- try (evaluate (Foldable.foldr' f z0 xs))
        case e of
          Left (ErrorCall
    _ :: ErrorCall) -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Integer
    forall a. Maybe a
    Nothing, String -> Context
    ctxNotStrict String
    "foldr'")
          Right Integer
    i -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    i, Context
    NoContext)
      let ctx = case Context
    ctx1 of
            Context
    NoContext -> case Context
    ctx2 of
              Context
    NoContext -> LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
                { lawContextLawName :: String
    lawContextLawName = String
    "Foldr'"
                , lawContextLawBody :: String
    lawContextLawBody = String
    "foldr' f z0 t" String -> String -> String
    `congruency` String
    "foldl f' id t z0, where f' k x z = k $! f x z"
                , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
                , lawContextTcProp :: String
    lawContextTcProp =
                    let showT :: String
    showT = f (Bottom Integer) -> String
    forall a. Show a => a -> String
    show f (Bottom Integer)
    xs
                        showF :: String
    showF = String
    "\\a b -> case a of\n  BottomUndefined -> error \"foldableFoldr': not strict\"\n  BottomValue v -> if even v then v else b"
                        showZ :: String
    showZ = Integer -> String
    forall a. Show a => a -> String
    show Integer
    z0
                    in [String] -> String
    lawWhere
                      [ String
    "foldr' f z0 t" String -> String -> String
    `congruency` String
    "foldl f' id t z0, where f' k x z = k $! f x z"
                      , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                      , String
    "z0 = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showZ
                      , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                      ]
                , lawContextReduced :: String
    lawContextReduced = Maybe Integer -> Maybe Integer -> String
    forall a. Show a => a -> a -> String
    reduced Maybe Integer
    lhs Maybe Integer
    rhs
                }
              Context
    c2 -> Context
    c2
            Context
    c1 -> Context
    c1
      heqCtx lhs rhs ctx

    foldableFoldl' ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl' :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl' forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      xs <- Gen (f (Bottom Integer)) -> PropertyT IO (f (Bottom Integer))
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f (Bottom Integer)) -> PropertyT IO (f (Bottom Integer)))
    -> Gen (f (Bottom Integer)) -> PropertyT IO (f (Bottom Integer))
    forall a b. (a -> b) -> a -> b
    $ Gen (Bottom Integer) -> Gen (f (Bottom Integer))
    forall x. Gen x -> Gen (f x)
    fgen (Gen Integer -> Gen (Bottom Integer)
    forall a. Gen a -> Gen (Bottom a)
    genBottom Gen Integer
    genSmallInteger)
      let f :: Integer -> Bottom Integer -> Integer
          f Integer
    a Bottom Integer
    b = case Bottom Integer
    b of
            Bottom Integer
    BottomUndefined -> String -> Integer
    forall a. HasCallStack => String -> a
    error String
    "foldableFoldl': your foldl' is not strict!"
            BottomValue Integer
    v -> if Integer -> Bool
    forall a. Integral a => a -> Bool
    even Integer
    v then Integer
    a else Integer
    v
      let z0 = Integer
    0
      (rhs,ctx1) <- liftIO $ do
        let f' Bottom Integer
    x Integer -> b
    k Integer
    z = Integer -> b
    k (Integer -> b) -> Integer -> b
    forall a b. (a -> b) -> a -> b
    $! Integer -> Bottom Integer -> Integer
    f Integer
    z Bottom Integer
    x
        e <- try (evaluate (Foldable.foldr f' id xs z0))
        case e of
          Left (ErrorCall
    _ :: ErrorCall) -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Integer
    forall a. Maybe a
    Nothing, String -> Context
    ctxNotStrict String
    "foldl'")
          Right Integer
    i -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    i, Context
    NoContext)
      (lhs,ctx2) <- liftIO $ do
        e <- try (evaluate (Foldable.foldl' f z0 xs))
        case e of
          Left (ErrorCall
    _ :: ErrorCall) -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Integer
    forall a. Maybe a
    Nothing, String -> Context
    ctxNotStrict String
    "foldl'")
          Right Integer
    i -> (Maybe Integer, Context) -> IO (Maybe Integer, Context)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    i, Context
    NoContext)
      let ctx = case Context
    ctx1 of
            Context
    NoContext -> case Context
    ctx2 of
              Context
    NoContext -> LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
                { lawContextLawName :: String
    lawContextLawName = String
    "Foldl'"
                , lawContextLawBody :: String
    lawContextLawBody = String
    "foldl' f z0 xs" String -> String -> String
    `congruency` String
    "foldr f' id xs z0, where f' x k z = k $! f z x"
                , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
                , lawContextTcProp :: String
    lawContextTcProp =
                    let showT :: String
    showT = f (Bottom Integer) -> String
    forall a. Show a => a -> String
    show f (Bottom Integer)
    xs
                        showF :: String
    showF = String
    "\\a b -> case a of\n  BottomUndefined -> error \"foldableFoldr': not strict\"\n  BottomValue v -> if even v then v else b"
                        showZ :: String
    showZ = Integer -> String
    forall a. Show a => a -> String
    show Integer
    z0
                    in [String] -> String
    lawWhere
                      [ String
    "foldl' f z0 xs" String -> String -> String
    `congruency` String
    "foldr f' id xs z0, where f' x k z = k $! f z x"
                      , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                      , String
    "z0 = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showZ
                      , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                      ]
                , lawContextReduced :: String
    lawContextReduced = Maybe Integer -> Maybe Integer -> String
    forall a. Show a => a -> a -> String
    reduced Maybe Integer
    lhs Maybe Integer
    rhs
                }
              Context
    c2 -> Context
    c2
            Context
    c1 -> Context
    c1
      heqCtx lhs rhs ctx

    foldableFoldl1 ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl1 :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldl1 forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      e <- Gen LinearEquationTwo -> PropertyT IO LinearEquationTwo
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquationTwo
    genLinearEquationTwo
      t <- forAll $ fgen genSmallInteger
      case compatToList t of
        [] -> PropertyT IO ()
    forall (m :: * -> *). MonadTest m => m ()
    success
        (Integer
    x:[Integer]
    xs) ->
          let f :: Integer -> Integer -> Integer
    f = LinearEquationTwo -> Integer -> Integer -> Integer
    runLinearEquationTwo LinearEquationTwo
    e
              lhs :: Integer
    lhs = (Integer -> Integer -> Integer) -> f Integer -> Integer
    forall a. (a -> a -> a) -> f a -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    Foldable.foldl1 Integer -> Integer -> Integer
    f f Integer
    t
              rhs :: Integer
    rhs = (Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    Foldable.foldl Integer -> Integer -> Integer
    f Integer
    x [Integer]
    xs
              ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
                { lawContextLawName :: String
    lawContextLawName = String
    "Foldl1"
                , lawContextLawBody :: String
    lawContextLawBody = String
    "foldl1 f t" String -> String -> String
    `congruency` String
    "let (x:xs) = toList t in foldl f x xs"
                , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
                , lawContextTcProp :: String
    lawContextTcProp =
                    let showF :: String
    showF = LinearEquationTwo -> String
    forall a. Show a => a -> String
    show LinearEquationTwo
    e
                        showT :: String
    showT = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    t
                        showX :: String
    showX = Integer -> String
    forall a. Show a => a -> String
    show Integer
    x
                        showXS :: String
    showXS = [Integer] -> String
    forall a. Show a => a -> String
    show [Integer]
    xs
                    in [String] -> String
    lawWhere
                      [ String
    "foldl1 f t" String -> String -> String
    `congruency` String
    "let (x:xs) = toList t in foldl f x xs, where"
                      , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                      , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                      , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                      , String
    "xs = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showXS
                      ]
                , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
                }
          in Integer -> Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx Integer
    lhs Integer
    rhs Context
    ctx

    foldableFoldr1 ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr1 :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableFoldr1 forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      e <- Gen LinearEquationTwo -> PropertyT IO LinearEquationTwo
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquationTwo
    genLinearEquationTwo
      t <- forAll $ fgen genSmallInteger
      case unsnoc (compatToList t) of
        Maybe ([Integer], Integer)
    Nothing -> PropertyT IO ()
    forall (m :: * -> *). MonadTest m => m ()
    success
        Just ([Integer]
    xs, Integer
    x) ->
          let f :: Integer -> Integer -> Integer
    f = LinearEquationTwo -> Integer -> Integer -> Integer
    runLinearEquationTwo LinearEquationTwo
    e
              lhs :: Integer
    lhs = (Integer -> Integer -> Integer) -> f Integer -> Integer
    forall a. (a -> a -> a) -> f a -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    Foldable.foldr1 Integer -> Integer -> Integer
    f f Integer
    t
              rhs :: Integer
    rhs = (Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Foldable.foldr Integer -> Integer -> Integer
    f Integer
    x [Integer]
    xs
              ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
                { lawContextLawName :: String
    lawContextLawName = String
    "Foldr1"
                , lawContextLawBody :: String
    lawContextLawBody = String
    "foldr1 f t" String -> String -> String
    `congruency` String
    "let (xs, x) = unsnoc (toList t) in foldr f x xs"
                , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
                , lawContextTcProp :: String
    lawContextTcProp =
                    let showF :: String
    showF = LinearEquationTwo -> String
    forall a. Show a => a -> String
    show LinearEquationTwo
    e
                        showT :: String
    showT = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    t
                        showX :: String
    showX = Integer -> String
    forall a. Show a => a -> String
    show Integer
    x
                        showXS :: String
    showXS = [Integer] -> String
    forall a. Show a => a -> String
    show [Integer]
    xs
                    in [String] -> String
    lawWhere
                      [ String
    "foldr1 f t" String -> String -> String
    `congruency` String
    "let (xs, x) = unsnoc (toList t) in foldr f x xs, where"
                      , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                      , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                      , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                      , String
    "xs = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showXS
                      ]
                , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
                }
          in Integer -> Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx Integer
    lhs Integer
    rhs Context
    ctx

    foldableToList ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableToList :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableToList forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      t <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs = f Integer -> [Integer]
    forall a. f a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Foldable.toList f Integer
    t
      let rhs = (Integer -> [Integer] -> [Integer])
    -> [Integer] -> f Integer -> [Integer]
    forall a b. (a -> b -> b) -> b -> f a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Foldable.foldr (:) [] f Integer
    t
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "ToList"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "toList" String -> String -> String
    `congruency` String
    "foldr (:) []"
            , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showT :: String
    showT = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    t
                in [String] -> String
    lawWhere
                  [ String
    "toList t" String -> String -> String
    `congruency` String
    "foldr (:) [] t, where"
                  , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                  ]
            , lawContextReduced :: String
    lawContextReduced = [Integer] -> [Integer] -> String
    forall a. Show a => a -> a -> String
    reduced [Integer]
    lhs [Integer]
    rhs
            }
      heqCtx lhs rhs ctx

    foldableNull ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableNull :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableNull forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      t <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs = f Integer -> Bool
    forall a. f a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Foldable.null f Integer
    t
      let rhs = (Integer -> Bool -> Bool) -> Bool -> f Integer -> Bool
    forall a b. (a -> b -> b) -> b -> f a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    Foldable.foldr ((Bool -> Bool) -> Integer -> Bool -> Bool
    forall a b. a -> b -> a
    const (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    False)) Bool
    True f Integer
    t
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Null"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "null" String -> String -> String
    `congruency` String
    "foldr (const (const False)) True"
            , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showT :: String
    showT = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    t
                in [String] -> String
    lawWhere
                  [ String
    "null t" String -> String -> String
    `congruency` String
    "foldr (const (const False)) True t, where"
                  , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                  ]
            , lawContextReduced :: String
    lawContextReduced = Bool -> Bool -> String
    forall a. Show a => a -> a -> String
    reduced Bool
    lhs Bool
    rhs
            }
      heqCtx lhs rhs ctx

    foldableLength ::
      ( Foldable f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    foldableLength :: forall (f :: * -> *).
    (Foldable f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    foldableLength forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      t <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs = f Integer -> Int
    forall a. f a -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    Foldable.length f Integer
    t
      let rhs = Sum Int -> Int
    forall a. Sum a -> a
    getSum ((Integer -> Sum Int) -> f Integer -> Sum Int
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    Foldable.foldMap (Sum Int -> Integer -> Sum Int
    forall a b. a -> b -> a
    const (Int -> Sum Int
    forall a. a -> Sum a
    Sum Int
    1)) f Integer
    t)
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Length"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "length" String -> String -> String
    `congruency` String
    "getSum . foldMap (const (Sum 1))"
            , lawContextTcName :: String
    lawContextTcName = String
    "Foldable"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showT :: String
    showT = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    t
                in [String] -> String
    lawWhere
                  [ String
    "length t" String -> String -> String
    `congruency` String
    "getSum . foldMap (const (Sum 1)) $ t, where"
                  , String
    "t = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showT
                  ]
            , lawContextReduced :: String
    lawContextReduced = Int -> Int -> String
    forall a. Show a => a -> a -> String
    reduced Int
    lhs Int
    rhs
            }
      heqCtx lhs rhs ctx

    unsnoc :: [a] -> Maybe ([a], a)
    unsnoc :: forall a. [a] -> Maybe ([a], a)
    unsnoc = \case
      [] -> Maybe ([a], a)
    forall a. Maybe a
    Nothing
      [a
    x] -> ([a], a) -> Maybe ([a], a)
    forall a. a -> Maybe a
    Just ([], a
    x)
      (a
    x:a
    y:[a]
    xs) -> (([a], a) -> ([a], a)) -> Maybe ([a], a) -> Maybe ([a], a)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\([a]
    bs,a
    b) -> (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    bs,a
    b)) ([a] -> Maybe ([a], a)
    forall a. [a] -> Maybe ([a], a)
    unsnoc (a
    y a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    xs))

    compatToList :: Foldable f => f a -> [a]
    compatToList :: forall (f :: * -> *) a. Foldable f => f a -> [a]
    compatToList = (a -> [a]) -> f a -> [a]
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    Foldable.foldMap (\a
    x -> [a
    x])