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

    module Hedgehog.Classes.MonadIO (monadIOLaws) where

    import Control.Monad.IO.Class (MonadIO(..))

    import Hedgehog
    import Hedgehog.Classes.Common

    -- | Tests the following 'MonadIO' laws:
    --
    -- [__Return__]: @'liftIO' '.' 'return'@ ≡ @'return'@
    -- [__Lift__]: @'liftIO' (m '>>=' f)@ ≡ @'liftIO' m '>>=' ('liftIO' '.' f)@
    monadIOLaws ::
      ( MonadIO f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Laws
    monadIOLaws :: forall (f :: * -> *).
    (MonadIO f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Laws
    monadIOLaws forall x. Gen x -> Gen (f x)
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "MonadIO"
      [ (String
    "Return", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadIOProp f
    monadIOReturn Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Lift", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadIOProp f
    monadIOLift Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      ]

    type MonadIOProp f =
      ( MonadIO f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property

    monadIOReturn :: forall f. MonadIOProp f
    monadIOReturn :: forall (f :: * -> *). MonadIOProp f
    monadIOReturn 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
      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 = IO Integer -> f Integer
    forall a. IO a -> f a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Integer -> IO Integer
    forall a. a -> IO 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 (m :: * -> *) a. Monad m => a -> m a
    return 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
    "MonadIO"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "liftIO . return" String -> String -> String
    `congruency` String
    "return"
            , 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
    "liftIO . return $ x" String -> String -> String
    `congruency` String
    "return 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

    monadIOLift :: forall f. MonadIOProp f
    monadIOLift :: forall (f :: * -> *). MonadIOProp f
    monadIOLift 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
      IO Integer
    m <- (IO Integer -> String)
    -> Gen (IO Integer) -> PropertyT IO (IO Integer)
    forall (m :: * -> *) a.
    (Monad m, HasCallStack) =>
    (a -> String) -> Gen a -> PropertyT m a
    forAllWith IO Integer -> String
    forall a. Show a => IO a -> String
    showIO (Gen (IO Integer) -> PropertyT IO (IO Integer))
    -> Gen (IO Integer) -> PropertyT IO (IO Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (IO Integer)
    forall a. Gen a -> Gen (IO a)
    genIO Gen Integer
    genSmallInteger
      LinearEquation
    f' <- Gen LinearEquation -> PropertyT IO LinearEquation
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquation
    genLinearEquation
      let f :: Integer -> IO Integer
    f = Integer -> IO Integer
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> IO Integer)
    -> (Integer -> Integer) -> Integer -> IO Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LinearEquation -> Integer -> Integer
    runLinearEquation LinearEquation
    f'
      let lhs :: f Integer
    lhs = IO Integer -> f Integer
    forall a. IO a -> f a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Integer
    m IO Integer -> (Integer -> IO Integer) -> IO Integer
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Integer -> IO Integer
    f) :: f Integer
      let rhs :: f Integer
    rhs = IO Integer -> f Integer
    forall a. IO a -> f a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO 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
    >>= (IO Integer -> f Integer
    forall a. IO a -> f a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Integer -> f Integer)
    -> (Integer -> IO Integer) -> Integer -> f Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> IO Integer
    f) :: 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
    "Lift", lawContextTcName :: String
    lawContextTcName = String
    "MonadIO"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "liftIO (m >>= f)" String -> String -> String
    `congruency` String
    "liftIO m >>= (liftIO . 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 showM :: String
    showM = IO Integer -> String
    forall a. Show a => IO a -> String
    showIO IO Integer
    m
                    showF :: String
    showF = LinearEquation -> String
    forall a. Show a => a -> String
    show LinearEquation
    f'
                in [String] -> String
    lawWhere
                  [ String
    "liftIO (m >>= f)" String -> String -> String
    `congruency` String
    "liftIO m >>= (liftIO . f), where"
                  , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                  , 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