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

    module Hedgehog.Classes.Monad (monadLaws) where

    import Control.Monad (ap)

    import Hedgehog
    import Hedgehog.Classes.Common

    -- | Tests the following 'Monad' laws:
    --
    -- [__Left Identity__]: @'return' a '>>=' k@ ≡ @k a@
    -- [__Right Identity__]: @m '>>=' 'return'@ ≡ @m@
    -- [__Associativity__]: @m '>>=' (\\x -> k x '>>=' h)@ ≡ @(m '>>=' k) '>>=' h@
    -- [__Return__]: @'return'@ ≡ @'pure'@
    -- [__Ap__]: @'ap' f x@ ≡ @f '<*>' x@
    monadLaws ::
      ( Monad f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Laws
    monadLaws :: forall (f :: * -> *).
    (Monad f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Laws
    monadLaws forall x. Gen x -> Gen (f x)
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "Monad"
      [ (String
    "Left Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadProp f
    monadLeftIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Right Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadProp f
    monadRightIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Associativity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadProp f
    monadAssociativity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Return", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadProp f
    monadReturn Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Ap", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadProp f
    monadAp Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      ]

    type MonadProp f =
      ( Monad f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property

    monadLeftIdentity :: forall f. MonadProp f
    monadLeftIdentity :: forall (f :: * -> *). MonadProp f
    monadLeftIdentity forall x. Gen x -> Gen (f x)
    _ = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      LinearEquationM f
    k' :: LinearEquationM f <- Gen (LinearEquationM f) -> PropertyT IO (LinearEquationM f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen (LinearEquationM f)
    forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
    genLinearEquationM
      Integer
    a <- Gen Integer -> PropertyT IO Integer
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen Integer -> PropertyT IO Integer)
    -> Gen Integer -> PropertyT IO Integer
    forall a b. (a -> b) -> a -> b
    $ Gen Integer
    genSmallInteger
      let k :: Integer -> f Integer
    k = LinearEquationM f -> Integer -> f Integer
    forall (m :: * -> *).
    Functor m =>
    LinearEquationM m -> Integer -> m Integer
    runLinearEquationM LinearEquationM f
    k'

      let lhs :: f Integer
    lhs = Integer -> f Integer
    forall a. a -> f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    a f Integer -> (Integer -> f Integer) -> f Integer
    forall a b. f a -> (a -> f b) -> f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Integer -> f Integer
    k
      let rhs :: f Integer
    rhs = Integer -> f Integer
    k Integer
    a
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Left Identity", lawContextTcName :: String
    lawContextTcName = String
    "Monad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "return a >>= k" String -> String -> String
    `congruency` String
    "k a"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showK :: String
    showK = LinearEquationM f -> String
    forall a. Show a => a -> String
    show LinearEquationM f
    k'
                    showA :: String
    showA = Integer -> String
    forall a. Show a => a -> String
    show Integer
    a
                in [String] -> String
    lawWhere
                  [ String
    "return a >>= k" String -> String -> String
    `congruency` String
    "k a, where"
                  , String
    "k = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showK
                  , String
    "a = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                  ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a (f :: * -> *).
    (MonadTest m, HasCallStack, Eq a, Show a,
     forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
    f a -> f a -> Context -> m ()
    heqCtx1 f Integer
    lhs f Integer
    rhs Context
    ctx

    monadRightIdentity :: forall f. MonadProp f
    monadRightIdentity :: forall (f :: * -> *). MonadProp f
    monadRightIdentity 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
      f Integer
    m <- 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
    lhs = f Integer
    m f Integer -> (Integer -> f Integer) -> f Integer
    forall a b. f a -> (a -> f b) -> f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Integer -> f Integer
    forall a. a -> f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      let rhs :: f Integer
    rhs = f Integer
    m
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Right Identity", lawContextTcName :: String
    lawContextTcName = String
    "Monad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "m >>= return" String -> String -> String
    `congruency` String
    "m"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showM :: String
    showM = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    m
                in [String] -> String
    lawWhere
                  [ String
    "m >>= return" String -> String -> String
    `congruency` String
    "m, where"
                  , String
    "m = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showM
                  ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a (f :: * -> *).
    (MonadTest m, HasCallStack, Eq a, Show a,
     forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
    f a -> f a -> Context -> m ()
    heqCtx1 f Integer
    lhs f Integer
    rhs Context
    ctx

    monadAssociativity :: forall f. MonadProp f
    monadAssociativity :: forall (f :: * -> *). MonadProp f
    monadAssociativity 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
      f Integer
    m <- 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
      LinearEquationM f
    k' :: LinearEquationM f <- Gen (LinearEquationM f) -> PropertyT IO (LinearEquationM f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen (LinearEquationM f)
    forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
    genLinearEquationM
      LinearEquationM f
    h' :: LinearEquationM f <- Gen (LinearEquationM f) -> PropertyT IO (LinearEquationM f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen (LinearEquationM f)
    forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
    genLinearEquationM
      let k :: Integer -> f Integer
    k = LinearEquationM f -> Integer -> f Integer
    forall (m :: * -> *).
    Functor m =>
    LinearEquationM m -> Integer -> m Integer
    runLinearEquationM LinearEquationM f
    k'
          h :: Integer -> f Integer
    h = LinearEquationM f -> Integer -> f Integer
    forall (m :: * -> *).
    Functor m =>
    LinearEquationM m -> Integer -> m Integer
    runLinearEquationM LinearEquationM f
    h'
      let lhs :: f Integer
    lhs = f Integer
    m f Integer -> (Integer -> f Integer) -> f Integer
    forall a b. f a -> (a -> f b) -> f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (\Integer
    x -> Integer -> f Integer
    k Integer
    x f Integer -> (Integer -> f Integer) -> f Integer
    forall a b. f a -> (a -> f b) -> f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Integer -> f Integer
    h)
      let rhs :: f Integer
    rhs = (f Integer
    m f Integer -> (Integer -> f Integer) -> f Integer
    forall a b. f a -> (a -> f b) -> f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Integer -> f Integer
    k) f Integer -> (Integer -> f Integer) -> f Integer
    forall a b. f a -> (a -> f b) -> f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Integer -> f Integer
    h
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Associativity", lawContextTcName :: String
    lawContextTcName = String
    "Monad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "m >>= (\\x -> k x >>= h)" String -> String -> String
    `congruency` String
    "(m >>= k) >>= h"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showM :: String
    showM = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    m
                    showK :: String
    showK = LinearEquationM f -> String
    forall a. Show a => a -> String
    show LinearEquationM f
    k'
                    showH :: String
    showH = LinearEquationM f -> String
    forall a. Show a => a -> String
    show LinearEquationM f
    h'
                in [String] -> String
    lawWhere
                  [ String
    "m >>= (\\x -> k x >>= h)" String -> String -> String
    `congruency` String
    "(m >>= k) >>= h, where"
                  , String
    "m = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showM
                  , String
    "k = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showK
                  , String
    "h = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showH
                  ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a (f :: * -> *).
    (MonadTest m, HasCallStack, Eq a, Show a,
     forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
    f a -> f a -> Context -> m ()
    heqCtx1 f Integer
    lhs f Integer
    rhs Context
    ctx

    monadReturn :: forall f. MonadProp f
    monadReturn :: forall (f :: * -> *). MonadProp f
    monadReturn forall x. Gen x -> Gen (f x)
    _ = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      Integer
    x <- Gen Integer -> PropertyT IO Integer
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen Integer
    genSmallInteger
      let lhs :: f Integer
    lhs = Integer -> f Integer
    forall a. a -> f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    x
      let rhs :: f Integer
    rhs = Integer -> f Integer
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Integer
    x :: f Integer
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Return", lawContextTcName :: String
    lawContextTcName = String
    "Monad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "return" String -> String -> String
    `congruency` String
    "pure"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showX :: String
    showX = Integer -> String
    forall a. Show a => a -> String
    show Integer
    x
                in [String] -> String
    lawWhere
                  [ String
    "return x" String -> String -> String
    `congruency` String
    "pure x, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a (f :: * -> *).
    (MonadTest m, HasCallStack, Eq a, Show a,
     forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
    f a -> f a -> Context -> m ()
    heqCtx1 f Integer
    lhs f Integer
    rhs Context
    ctx

    monadAp :: forall f. MonadProp f
    monadAp :: forall (f :: * -> *). MonadProp f
    monadAp forall x. Gen x -> Gen (f x)
    _ = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f QuadraticEquation
    f' :: f QuadraticEquation <- Gen (f QuadraticEquation) -> PropertyT IO (f QuadraticEquation)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f QuadraticEquation) -> PropertyT IO (f QuadraticEquation))
    -> Gen (f QuadraticEquation) -> PropertyT IO (f QuadraticEquation)
    forall a b. (a -> b) -> a -> b
    $ QuadraticEquation -> f QuadraticEquation
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QuadraticEquation -> f QuadraticEquation)
    -> GenT Identity QuadraticEquation -> Gen (f QuadraticEquation)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GenT Identity QuadraticEquation
    genQuadraticEquation
      f Integer
    x :: f Integer <- 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
    $ Integer -> f Integer
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> f Integer) -> Gen Integer -> Gen (f Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Gen Integer
    genSmallInteger
      let f :: f (Integer -> Integer)
    f = (QuadraticEquation -> Integer -> Integer)
    -> f QuadraticEquation -> f (Integer -> Integer)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap QuadraticEquation -> Integer -> Integer
    runQuadraticEquation f QuadraticEquation
    f'

      let lhs :: f Integer
    lhs = f (Integer -> Integer) -> f Integer -> f Integer
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap f (Integer -> Integer)
    f f Integer
    x
      let rhs :: f Integer
    rhs = f (Integer -> Integer)
    f f (Integer -> Integer) -> f Integer -> f Integer
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Ap", lawContextTcName :: String
    lawContextTcName = String
    "Monad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "ap f" String -> String -> String
    `congruency` String
    "f <*>"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showX :: String
    showX = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                    showF :: String
    showF = f QuadraticEquation -> String
    forall a. Show a => a -> String
    show f QuadraticEquation
    f'
                in [String] -> String
    lawWhere
                  [ String
    "ap f x" String -> String -> String
    `congruency` String
    "f <*> x, where"
                  , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a (f :: * -> *).
    (MonadTest m, HasCallStack, Eq a, Show a,
     forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
    f a -> f a -> Context -> m ()
    heqCtx1 f Integer
    lhs f Integer
    rhs Context
    ctx