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

    module Hedgehog.Classes.MonadZip (monadZipLaws) where

    import Control.Arrow (Arrow(..))
    import Control.Monad.Zip (MonadZip(mzip))

    import Hedgehog
    import Hedgehog.Classes.Common

    -- | Tests the following 'MonadZip' laws:
    --
    -- [__Naturality__]: @'fmap' (f '***' g) ('mzip' ma mb)@ ≡ @'mzip' ('fmap' f ma) ('fmap' g mb)@
    monadZipLaws ::
      ( MonadZip f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Laws
    monadZipLaws :: forall (f :: * -> *).
    (MonadZip f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Laws
    monadZipLaws forall x. Gen x -> Gen (f x)
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "Monad"
      [ (String
    "Naturality", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadZipProp f
    monadZipNaturality GenT Identity x -> GenT Identity (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      ]

    type MonadZipProp f =
      ( MonadZip f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property

    monadZipNaturality :: forall f. MonadZipProp f
    monadZipNaturality :: forall (f :: * -> *). MonadZipProp f
    monadZipNaturality 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' <- Gen LinearEquation -> PropertyT IO LinearEquation
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquation
    genLinearEquation
      g' <- forAll genLinearEquation
      let f = LinearEquation -> Integer -> Integer
    runLinearEquation LinearEquation
    f'
          g = LinearEquation -> Integer -> Integer
    runLinearEquation LinearEquation
    g'
      ma <- forAll $ fgen genSmallInteger
      mb <- forAll $ fgen genSmallInteger
      let lhs = ((Integer, Integer) -> (Integer, Integer))
    -> f (Integer, Integer) -> 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 (Integer -> Integer
    f (Integer -> Integer)
    -> (Integer -> Integer) -> (Integer, Integer) -> (Integer, Integer)
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** Integer -> Integer
    g) (f Integer -> f Integer -> f (Integer, Integer)
    forall a b. f a -> f b -> f (a, b)
    forall (m :: * -> *) a b. MonadZip m => m a -> m b -> m (a, b)
    mzip f Integer
    ma f Integer
    mb)
      let rhs = f Integer -> f Integer -> f (Integer, Integer)
    forall a b. f a -> f b -> f (a, b)
    forall (m :: * -> *) a b. MonadZip m => m a -> m b -> m (a, b)
    mzip ((Integer -> Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Integer -> Integer
    f f Integer
    ma) ((Integer -> Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Integer -> Integer
    g f Integer
    mb)
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Naturality", lawContextTcName :: String
    lawContextTcName = String
    "MonadZip"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "(fmap (f *** g) (mzip ma mb)" String -> String -> String
    `congruency` String
    "mzip (fmap f ma) (fmap g mb)"
            , lawContextReduced :: String
    lawContextReduced = f (Integer, Integer) -> f (Integer, Integer) -> String
    forall a. Show a => a -> a -> String
    reduced f (Integer, Integer)
    lhs f (Integer, Integer)
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showF :: String
    showF = LinearEquation -> String
    forall a. Show a => a -> String
    show LinearEquation
    f'; showG :: String
    showG = LinearEquation -> String
    forall a. Show a => a -> String
    show LinearEquation
    g'; showMA :: String
    showMA = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    ma; showMB :: String
    showMB = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    mb;
                in [String] -> String
    lawWhere
                  [ String
    "fmap (f *** g) (mzip ma mb)" String -> String -> String
    `congruency` String
    "mzip (fmap f ma) (fmap g mb), where"
                  , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                  , String
    "g = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showG
                  , String
    "ma = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showMA
                  , String
    "mb = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showMB
                  ]
            }
      heqCtx1 lhs rhs ctx