{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Grisette.Experimental.GenSymConstrained
  ( -- * Symbolic value generation with errors
    GenSymConstrained (..),
    GenSymSimpleConstrained (..),
    genSymConstrained,
    genSymSimpleConstrained,
    derivedFreshConstrainedNoSpec,
    derivedSimpleFreshConstrainedNoSpec,
    derivedSimpleFreshConstrainedSameShape,

    -- * Some common GenSymConstrained specifications
    SOrdUpperBound (..),
    SOrdLowerBound (..),
    SOrdBound (..),
  )
where

import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError))
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import GHC.Generics
  ( Generic (Rep, from, to),
    K1 (K1),
    M1 (M1),
    U1 (U1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Core.Control.Monad.UnionM
  ( UnionM,
    liftToMonadUnion,
  )
import Grisette.Core.Data.Class.Bool (LogicalOp ((||~)))
import Grisette.Core.Data.Class.GenSym
  ( FreshIdent,
    GenSym (fresh),
    GenSymSimple (simpleFresh),
    ListSpec (ListSpec),
    MonadFresh,
    SimpleListSpec (SimpleListSpec),
    chooseFresh,
    chooseUnionFresh,
    runFreshT,
  )
import Grisette.Core.Data.Class.Mergeable (Mergeable, Mergeable1)
import Grisette.Core.Data.Class.SOrd (SOrd ((<~), (>=~)))
import Grisette.Core.Data.Class.SimpleMergeable
  ( UnionLike,
    merge,
    mrgIf,
    mrgSingle,
  )

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.Experimental
-- >>> import Grisette.IR.SymPrim
-- >>> :set -XOverloadedStrings
-- >>> :set -XTypeApplications

-- | Class of types in which symbolic values can be generated with some
-- specification.
--
-- See 'GenSym' for more details. The difference of this class is that it allows
-- constraints to be generated along with the generation of symbolic values.
class (Mergeable a) => GenSymConstrained spec a where
  -- | Generates a symbolic value with the given specification.
  --
  -- Constraint violations will throw an error in the monadic environment.
  --
  -- >>> runFreshT (freshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM (UnionM SymInteger)
  -- ExceptT <If (<= 1 a@0) (Left ()) (Right {a@0})>
  freshConstrained ::
    (MonadFresh m, MonadError e m, UnionLike m) =>
    e ->
    spec ->
    m (UnionM a)
  default freshConstrained ::
    (GenSymSimpleConstrained spec a) =>
    ( MonadFresh m,
      MonadError e m,
      UnionLike m
    ) =>
    e ->
    spec ->
    m (UnionM a)
  freshConstrained e
e spec
spec = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
spec

genSymConstrained :: forall spec a e. (GenSymConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM (UnionM a)
genSymConstrained :: forall spec a e.
(GenSymConstrained spec a, Mergeable e) =>
e -> spec -> FreshIdent -> ExceptT e UnionM (UnionM a)
genSymConstrained e
e spec
spec = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT (forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e spec
spec)

-- | Class of types in which symbolic values can be generated with some
-- specification.
--
-- See 'GenSymSimple' for more details. The difference of this class is that it allows
-- constraints to be generated along with the generation of symbolic values.
class (Mergeable a) => GenSymSimpleConstrained spec a where
  -- | Generates a symbolic value with the given specification.
  --
  -- Constraint violations will throw an error in the monadic environment.
  --
  -- >>> runFreshT (simpleFreshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM SymInteger
  -- ExceptT <If (<= 1 a@0) (Left ()) (Right a@0)>
  simpleFreshConstrained ::
    (MonadFresh m, MonadError e m, UnionLike m) =>
    e ->
    spec ->
    m a

genSymSimpleConstrained :: forall spec a e. (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM a
genSymSimpleConstrained :: forall spec a e.
(GenSymSimpleConstrained spec a, Mergeable e) =>
e -> spec -> FreshIdent -> ExceptT e UnionM a
genSymSimpleConstrained e
e spec
spec = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => FreshT m a -> FreshIdent -> m a
runFreshT (forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
spec)

instance {-# OVERLAPPABLE #-} (Mergeable a, GenSym spec a) => GenSymConstrained spec a where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
_ = forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh

instance {-# OVERLAPPABLE #-} (Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained spec a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
_ = forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh

-- | Exclusive bound, generates the values with the specification, then filters
-- out the ones that are greater than or equal to the bound
data SOrdUpperBound a spec = SOrdUpperBound a spec

instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdUpperBound a spec) a where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdUpperBound a spec -> m (UnionM a)
freshConstrained e
e (SOrdUpperBound a
u spec
spec) = do
    UnionM a
s <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
    a
v <- forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
s
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v

instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdUpperBound a spec) a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdUpperBound a spec -> m a
simpleFreshConstrained e
e (SOrdUpperBound a
u spec
spec) = do
    a
s <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
spec
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
s

-- | Inclusive bound, generates the values with the specification, then filters
-- out the ones that are less than the bound
data SOrdLowerBound a spec = SOrdLowerBound a spec

instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdLowerBound a spec) a where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdLowerBound a spec -> m (UnionM a)
freshConstrained e
e (SOrdLowerBound a
l spec
spec) = do
    UnionM a
s <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
    a
v <- forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
s
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v forall a. SOrd a => a -> a -> SymBool
<~ a
l) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v

instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdLowerBound a spec) a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdLowerBound a spec -> m a
simpleFreshConstrained e
e (SOrdLowerBound a
l spec
spec) = do
    a
s <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
spec
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s forall a. SOrd a => a -> a -> SymBool
<~ a
l) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
s

-- | Left-inclusive, right-exclusive bound, generates the values with the
-- specification, then filters out the ones that are out-of-bound
data SOrdBound a spec = SOrdBound a a spec

instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdBound a spec) a where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdBound a spec -> m (UnionM a)
freshConstrained e
e (SOrdBound a
l a
u spec
spec) = do
    UnionM a
s <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
spec
    a
v <- forall a (u :: * -> *).
(Mergeable a, MonadUnion u) =>
UnionM a -> u a
liftToMonadUnion UnionM a
s
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
v forall a. SOrd a => a -> a -> SymBool
<~ a
l forall b. LogicalOp b => b -> b -> b
||~ a
v forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
v

instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdBound a spec) a where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdBound a spec -> m a
simpleFreshConstrained e
e (SOrdBound a
l a
u spec
spec) = do
    a
s <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
spec
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
s forall a. SOrd a => a -> a -> SymBool
<~ a
l forall b. LogicalOp b => b -> b -> b
||~ a
s forall a. SOrd a => a -> a -> SymBool
>=~ a
u) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e) (forall (m :: * -> *) a. Monad m => a -> m a
return ())
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
s

instance GenSymConstrained (SOrdBound Integer ()) Integer where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SOrdBound Integer () -> m (UnionM Integer)
freshConstrained e
_ (SOrdBound Integer
l Integer
r ()
_) = forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[a] -> m (UnionM a)
chooseFresh [Integer
l .. Integer
r forall a. Num a => a -> a -> a
- Integer
1]

-- Either
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b
  ) =>
  GenSymConstrained (Either aspec bspec) (Either a b)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Either aspec bspec -> m (UnionM (Either a b))
freshConstrained e
e (Left aspec
aspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e aspec
aspec
  freshConstrained e
e (Right bspec
bspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e bspec
bspec

instance
  ( GenSymSimpleConstrained a a,
    GenSymSimpleConstrained b b
  ) =>
  GenSymSimpleConstrained (Either a b) (Either a b)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Either a b -> m (Either a b)
simpleFreshConstrained = forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, UnionLike m) =>
e -> a -> m a
derivedSimpleFreshConstrainedSameShape

instance
  (GenSymConstrained () a, Mergeable a, GenSymConstrained () b, Mergeable b) =>
  GenSymConstrained () (Either a b)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> () -> m (UnionM (Either a b))
freshConstrained = forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, UnionLike m) =>
e -> () -> m (UnionM a)
derivedFreshConstrainedNoSpec

-- Maybe
instance
  (GenSymConstrained aspec a, Mergeable a) =>
  GenSymConstrained (Maybe aspec) (Maybe a)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Maybe aspec -> m (UnionM (Maybe a))
freshConstrained e
_ Maybe aspec
Nothing = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a. Maybe a
Nothing
  freshConstrained e
e (Just aspec
aspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e aspec
aspec

instance
  (GenSymSimpleConstrained aspec a) =>
  GenSymSimpleConstrained (Maybe aspec) (Maybe a)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Maybe aspec -> m (Maybe a)
simpleFreshConstrained e
_ Maybe aspec
Nothing = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a. Maybe a
Nothing
  simpleFreshConstrained e
e (Just aspec
aspec) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec

instance (GenSymConstrained aspec a, Mergeable a) => GenSymConstrained aspec (Maybe a) where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> aspec -> m (UnionM (Maybe a))
freshConstrained e
e aspec
aspec = do
    UnionM a
a :: UnionM a <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e aspec
aspec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh [forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing, forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnionM a
a]

-- List
instance
  (GenSymConstrained () a, Mergeable a) =>
  GenSymConstrained Integer [a]
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m (UnionM [a])
freshConstrained e
e Integer
v = do
    [UnionM a]
l <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m [UnionM a]
gl e
e Integer
v
    let xs :: [[UnionM a]]
xs = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
    where
      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Integer -> m [UnionM a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m [UnionM a]
gl e
e1 Integer
v1
        | Integer
v1 forall a. Ord a => a -> a -> Bool
<= Integer
0 = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle []
        | Bool
otherwise = do
            UnionM a
l <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e1 ()
            [UnionM a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Integer -> m [UnionM a]
gl e
e1 (Integer
v1 forall a. Num a => a -> a -> a
- Integer
1)
            forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r

instance
  (GenSymConstrained spec a, Mergeable a) =>
  GenSymConstrained (ListSpec spec) [a]
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> ListSpec spec -> m (UnionM [a])
freshConstrained e
e (ListSpec Int
minLen Int
maxLen spec
subSpec) =
    if Int
minLen forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
maxLen forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
minLen forall a. Ord a => a -> a -> Bool
>= Int
maxLen
      then forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Int
minLen, Int
maxLen)
      else do
        [UnionM a]
l <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e Int
maxLen
        let xs :: [[UnionM a]]
xs = forall a. Int -> [a] -> [a]
drop Int
minLen forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr (:) [] [UnionM a]
l
        forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Mergeable a, MonadFresh m) =>
[UnionM a] -> m (UnionM a)
chooseUnionFresh forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[UnionM a]]
xs
    where
      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 Int
currLen
        | Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do
            UnionM a
l <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e1 spec
subSpec
            [UnionM a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r

instance
  (GenSymConstrained a a, Mergeable a) =>
  GenSymConstrained [a] [a]
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> [a] -> m (UnionM [a])
freshConstrained e
e [a]
l = do
    [UnionM a]
r :: [UnionM a] <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e) [a]
l
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [UnionM a]
r

instance
  (GenSymSimpleConstrained a a) =>
  GenSymSimpleConstrained [a] [a]
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> [a] -> m [a]
simpleFreshConstrained = forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, UnionLike m) =>
e -> a -> m a
derivedSimpleFreshConstrainedSameShape

instance
  (GenSymConstrained spec a, Mergeable a) =>
  GenSymConstrained (SimpleListSpec spec) [a]
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SimpleListSpec spec -> m (UnionM [a])
freshConstrained e
e (SimpleListSpec Int
len spec
subSpec) =
    if Int
len forall a. Ord a => a -> a -> Bool
< Int
0
      then forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
len
      else do
        forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e Int
len
    where
      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 Int
currLen
        | Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle []
        | Bool
otherwise = do
            UnionM a
l <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e1 spec
subSpec
            [UnionM a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [UnionM a]
gl e
e1 (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
            forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ UnionM a
l forall a. a -> [a] -> [a]
: [UnionM a]
r

instance
  (GenSymSimpleConstrained spec a) =>
  GenSymSimpleConstrained (SimpleListSpec spec) [a]
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> SimpleListSpec spec -> m [a]
simpleFreshConstrained e
e (SimpleListSpec Int
len spec
subSpec) =
    if Int
len forall a. Ord a => a -> a -> Bool
< Int
0
      then forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Bad lengths: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
len
      else do
        forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [a]
gl e
e Int
len
    where
      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [a]
      gl :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [a]
gl e
e1 Int
currLen
        | Int
currLen forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle []
        | Bool
otherwise = do
            a
l <- forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e1 spec
subSpec
            [a]
r <- forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> Int -> m [a]
gl e
e1 (Int
currLen forall a. Num a => a -> a -> a
- Int
1)
            forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ a
l forall a. a -> [a] -> [a]
: [a]
r

-- (,)
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b
  ) =>
  GenSymConstrained (aspec, bspec) (a, b)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec) -> m (UnionM (a, b))
freshConstrained e
err (aspec
aspec, bspec
bspec) = do
    UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
    UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx)

instance
  ( GenSymSimpleConstrained aspec a,
    GenSymSimpleConstrained bspec b
  ) =>
  GenSymSimpleConstrained (aspec, bspec) (a, b)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec) -> m (a, b)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec) = do
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
      (,)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec

-- (,,)
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b,
    GenSymConstrained cspec c,
    Mergeable c
  ) =>
  GenSymConstrained (aspec, bspec, cspec) (a, b, c)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec) -> m (UnionM (a, b, c))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec) = do
    UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
    UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
    UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx)

instance
  ( GenSymSimpleConstrained aspec a,
    GenSymSimpleConstrained bspec b,
    GenSymSimpleConstrained cspec c
  ) =>
  GenSymSimpleConstrained (aspec, bspec, cspec) (a, b, c)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec) -> m (a, b, c)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec) = do
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
      (,,)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec

-- (,,,)
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b,
    GenSymConstrained cspec c,
    Mergeable c,
    GenSymConstrained dspec d,
    Mergeable d
  ) =>
  GenSymConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec, dspec) -> m (UnionM (a, b, c, d))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
    UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
    UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
    UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
    UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx)

instance
  ( GenSymSimpleConstrained aspec a,
    GenSymSimpleConstrained bspec b,
    GenSymSimpleConstrained cspec c,
    GenSymSimpleConstrained dspec d
  ) =>
  GenSymSimpleConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec, dspec) -> m (a, b, c, d)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec) = do
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
      (,,,)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec

-- (,,,,)
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b,
    GenSymConstrained cspec c,
    Mergeable c,
    GenSymConstrained dspec d,
    Mergeable d,
    GenSymConstrained espec e,
    Mergeable e
  ) =>
  GenSymConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec)
-> m (UnionM (a, b, c, d, e))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
    UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
    UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
    UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
    UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
    UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex)

instance
  ( GenSymSimpleConstrained aspec a,
    GenSymSimpleConstrained bspec b,
    GenSymSimpleConstrained cspec c,
    GenSymSimpleConstrained dspec d,
    GenSymSimpleConstrained espec e
  ) =>
  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (aspec, bspec, cspec, dspec, espec) -> m (a, b, c, d, e)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec) = do
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
      (,,,,)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec

-- (,,,,,)
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b,
    GenSymConstrained cspec c,
    Mergeable c,
    GenSymConstrained dspec d,
    Mergeable d,
    GenSymConstrained espec e,
    Mergeable e,
    GenSymConstrained fspec f,
    Mergeable f
  ) =>
  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec)
-> m (UnionM (a, b, c, d, e, f))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
    UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
    UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
    UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
    UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
    UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
    UnionM f
f1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err fspec
fspec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      f
fx <- UnionM f
f1
      forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx)

instance
  ( GenSymSimpleConstrained aspec a,
    GenSymSimpleConstrained bspec b,
    GenSymSimpleConstrained cspec c,
    GenSymSimpleConstrained dspec d,
    GenSymSimpleConstrained espec e,
    GenSymSimpleConstrained fspec f
  ) =>
  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec)
-> m (a, b, c, d, e, f)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec) = do
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
      (,,,,,)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e fspec
fspec

-- (,,,,,,)
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b,
    GenSymConstrained cspec c,
    Mergeable c,
    GenSymConstrained dspec d,
    Mergeable d,
    GenSymConstrained espec e,
    Mergeable e,
    GenSymConstrained fspec f,
    Mergeable f,
    GenSymConstrained gspec g,
    Mergeable g
  ) =>
  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (UnionM (a, b, c, d, e, f, g))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
    UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
    UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
    UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
    UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
    UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
    UnionM f
f1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err fspec
fspec
    UnionM g
g1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err gspec
gspec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      f
fx <- UnionM f
f1
      g
gx <- UnionM g
g1
      forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx)

instance
  ( GenSymSimpleConstrained aspec a,
    GenSymSimpleConstrained bspec b,
    GenSymSimpleConstrained cspec c,
    GenSymSimpleConstrained dspec d,
    GenSymSimpleConstrained espec e,
    GenSymSimpleConstrained fspec f,
    GenSymSimpleConstrained gspec g
  ) =>
  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec)
-> m (a, b, c, d, e, f, g)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec) = do
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
      (,,,,,,)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e fspec
fspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e gspec
gspec

-- (,,,,,,,)
instance
  ( GenSymConstrained aspec a,
    Mergeable a,
    GenSymConstrained bspec b,
    Mergeable b,
    GenSymConstrained cspec c,
    Mergeable c,
    GenSymConstrained dspec d,
    Mergeable d,
    GenSymConstrained espec e,
    Mergeable e,
    GenSymConstrained fspec f,
    Mergeable f,
    GenSymConstrained gspec g,
    Mergeable g,
    GenSymConstrained hspec h,
    Mergeable h
  ) =>
  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (UnionM (a, b, c, d, e, f, g, h))
freshConstrained e
err (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
    UnionM a
a1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err aspec
aspec
    UnionM b
b1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err bspec
bspec
    UnionM c
c1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err cspec
cspec
    UnionM d
d1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err dspec
dspec
    UnionM e
e1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err espec
espec
    UnionM f
f1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err fspec
fspec
    UnionM g
g1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err gspec
gspec
    UnionM h
h1 <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
err hspec
hspec
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ do
      a
ax <- UnionM a
a1
      b
bx <- UnionM b
b1
      c
cx <- UnionM c
c1
      d
dx <- UnionM d
d1
      e
ex <- UnionM e
e1
      f
fx <- UnionM f
f1
      g
gx <- UnionM g
g1
      h
hx <- UnionM h
h1
      forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
ax, b
bx, c
cx, d
dx, e
ex, f
fx, g
gx, h
hx)

instance
  ( GenSymSimpleConstrained aspec a,
    GenSymSimpleConstrained bspec b,
    GenSymSimpleConstrained cspec c,
    GenSymSimpleConstrained dspec d,
    GenSymSimpleConstrained espec e,
    GenSymSimpleConstrained fspec f,
    GenSymSimpleConstrained gspec g,
    GenSymSimpleConstrained hspec h
  ) =>
  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e
-> (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec)
-> m (a, b, c, d, e, f, g, h)
simpleFreshConstrained e
e (aspec
aspec, bspec
bspec, cspec
cspec, dspec
dspec, espec
espec, fspec
fspec, gspec
gspec, hspec
hspec) = do
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$
      (,,,,,,,)
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e aspec
aspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e bspec
bspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e cspec
cspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e dspec
dspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e espec
espec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e fspec
fspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e gspec
gspec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e hspec
hspec

-- MaybeT
instance
  {-# OVERLAPPABLE #-}
  ( GenSymConstrained spec (m (Maybe a)),
    Mergeable1 m,
    Mergeable a
  ) =>
  GenSymConstrained spec (MaybeT m a)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (UnionM (MaybeT m a))
freshConstrained e
e spec
v = do
    UnionM (m (Maybe a))
x <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e spec
v
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ UnionM (m (Maybe a))
x

instance
  {-# OVERLAPPABLE #-}
  ( GenSymSimpleConstrained spec (m (Maybe a)),
    Mergeable1 m,
    Mergeable a
  ) =>
  GenSymSimpleConstrained spec (MaybeT m a)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (MaybeT m a)
simpleFreshConstrained e
e spec
v = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),
    Mergeable1 m,
    Mergeable a
  ) =>
  GenSymSimpleConstrained (MaybeT m a) (MaybeT m a)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> MaybeT m a -> m (MaybeT m a)
simpleFreshConstrained e
e (MaybeT m (Maybe a)
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e m (Maybe a)
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),
    Mergeable1 m,
    Mergeable a
  ) =>
  GenSymConstrained (MaybeT m a) (MaybeT m a)

-- ExceptT
instance
  {-# OVERLAPPABLE #-}
  ( GenSymConstrained spec (m (Either a b)),
    Mergeable1 m,
    Mergeable a,
    Mergeable b
  ) =>
  GenSymConstrained spec (ExceptT a m b)
  where
  freshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (UnionM (ExceptT a m b))
freshConstrained e
e spec
v = do
    UnionM (m (Either a b))
x <- forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e spec
v
    forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ UnionM (m (Either a b))
x

instance
  {-# OVERLAPPABLE #-}
  ( GenSymSimpleConstrained spec (m (Either a b)),
    Mergeable1 m,
    Mergeable a,
    Mergeable b
  ) =>
  GenSymSimpleConstrained spec (ExceptT a m b)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> spec -> m (ExceptT a m b)
simpleFreshConstrained e
e spec
v = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e spec
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),
    Mergeable1 m,
    Mergeable e,
    Mergeable a
  ) =>
  GenSymSimpleConstrained (ExceptT e m a) (ExceptT e m a)
  where
  simpleFreshConstrained :: forall (m :: * -> *) e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> ExceptT e m a -> m (ExceptT e m a)
simpleFreshConstrained e
e (ExceptT m (Either e a)
v) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e m (Either e a)
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),
    Mergeable1 m,
    Mergeable e,
    Mergeable a
  ) =>
  GenSymConstrained (ExceptT e m a) (ExceptT e m a)

-- Deriving

class GenSymConstrainedNoSpec a where
  freshConstrainedNoSpec ::
    ( MonadFresh m,
      MonadError e m,
      UnionLike m
    ) =>
    e ->
    m (UnionM (a c))

instance GenSymConstrainedNoSpec U1 where
  freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM (U1 c))
freshConstrainedNoSpec e
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall k (p :: k). U1 p
U1

instance (GenSymConstrained () c) => GenSymConstrainedNoSpec (K1 i c) where
  freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM (K1 i c c))
freshConstrainedNoSpec e
e = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m (UnionM a)
freshConstrained e
e ()

instance (GenSymConstrainedNoSpec a) => GenSymConstrainedNoSpec (M1 i c a) where
  freshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM (M1 i c a c))
freshConstrainedNoSpec e
e = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e

instance
  ( GenSymConstrainedNoSpec a,
    GenSymConstrainedNoSpec b,
    forall x. Mergeable (a x),
    forall x. Mergeable (b x)
  ) =>
  GenSymConstrainedNoSpec (a :+: b)
  where
  freshConstrainedNoSpec ::
    forall m c e.
    ( MonadFresh m,
      MonadError e m,
      UnionLike m
    ) =>
    e ->
    m (UnionM ((a :+: b) c))
  freshConstrainedNoSpec :: forall (m :: * -> *) c e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM ((:+:) a b c))
freshConstrainedNoSpec e
e = do
    SymBool
cond :: bool <- forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh ()
    UnionM (a c)
l :: UnionM (a c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
    UnionM (b c)
r :: UnionM (b c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 UnionM (a c)
l) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 UnionM (b c)
r)

instance
  (GenSymConstrainedNoSpec a, GenSymConstrainedNoSpec b) =>
  GenSymConstrainedNoSpec (a :*: b)
  where
  freshConstrainedNoSpec ::
    forall m c e.
    ( MonadFresh m,
      MonadError e m,
      UnionLike m
    ) =>
    e ->
    m (UnionM ((a :*: b) c))
  freshConstrainedNoSpec :: forall (m :: * -> *) c e.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (UnionM ((:*:) a b c))
freshConstrainedNoSpec e
e = do
    UnionM (a c)
l :: UnionM (a c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
    UnionM (b c)
r :: UnionM (b c) <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
      a c
l1 <- UnionM (a c)
l
      b c
r1 <- UnionM (b c)
r
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l1 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r1

-- | We cannot provide DerivingVia style derivation for 'GenSymConstrained', while you can
-- use this 'freshConstrained' implementation to implement 'GenSymConstrained' for your own types.
--
-- This 'freshConstrained' implementation is for the types that does not need any specification.
-- It will generate product types by generating each fields with @()@ as specification,
-- and generate all possible values for a sum type.
--
-- __Note:__ __Never__ use on recursive types.
derivedFreshConstrainedNoSpec ::
  forall a m e.
  ( Generic a,
    GenSymConstrainedNoSpec (Rep a),
    Mergeable a,
    MonadFresh m,
    MonadError e m,
    UnionLike m
  ) =>
  e ->
  () ->
  m (UnionM a)
derivedFreshConstrainedNoSpec :: forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, UnionLike m) =>
e -> () -> m (UnionM a)
derivedFreshConstrainedNoSpec e
e ()
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (UnionM (a c))
freshConstrainedNoSpec e
e

class GenSymSimpleConstrainedNoSpec a where
  simpleFreshConstrainedNoSpec ::
    ( MonadFresh m,
      MonadError e m,
      UnionLike m
    ) =>
    e ->
    m (a c)

instance GenSymSimpleConstrainedNoSpec U1 where
  simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (U1 c)
simpleFreshConstrainedNoSpec e
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall k (p :: k). U1 p
U1

instance (GenSymSimpleConstrained () c) => GenSymSimpleConstrainedNoSpec (K1 i c) where
  simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (K1 i c c)
simpleFreshConstrainedNoSpec e
e = forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e ()

instance (GenSymSimpleConstrainedNoSpec a) => GenSymSimpleConstrainedNoSpec (M1 i c a) where
  simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m (M1 i c a c)
simpleFreshConstrainedNoSpec e
e = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e

instance
  (GenSymSimpleConstrainedNoSpec a, GenSymSimpleConstrainedNoSpec b) =>
  GenSymSimpleConstrainedNoSpec (a :*: b)
  where
  simpleFreshConstrainedNoSpec :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> m ((:*:) a b c)
simpleFreshConstrainedNoSpec e
e = do
    a c
l :: a c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e
    b c
r :: b c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r

-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while
-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo
-- your own types.
--
-- This 'simpleFreshConstrained' implementation is for the types that does not need any specification.
-- It will generate product types by generating each fields with '()' as specification.
-- It will not work on sum types.
--
-- __Note:__ __Never__ use on recursive types.
derivedSimpleFreshConstrainedNoSpec ::
  forall a m e.
  ( Generic a,
    GenSymSimpleConstrainedNoSpec (Rep a),
    MonadFresh m,
    MonadError e m,
    UnionLike m,
    Mergeable a
  ) =>
  e ->
  () ->
  m a
derivedSimpleFreshConstrainedNoSpec :: forall a (m :: * -> *) e.
(Generic a, GenSymSimpleConstrainedNoSpec (Rep a), MonadFresh m,
 MonadError e m, UnionLike m, Mergeable a) =>
e -> () -> m a
derivedSimpleFreshConstrainedNoSpec e
e ()
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) (m :: * -> *) e c.
(GenSymSimpleConstrainedNoSpec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> m (a c)
simpleFreshConstrainedNoSpec e
e

class GenSymConstrainedSameShape a where
  simpleFreshConstrainedSameShape ::
    ( MonadFresh m,
      MonadError e m,
      UnionLike m
    ) =>
    e ->
    a c ->
    m (a c)

instance GenSymConstrainedSameShape U1 where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> U1 c -> m (U1 c)
simpleFreshConstrainedSameShape e
_ U1 c
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall k (p :: k). U1 p
U1

instance (GenSymSimpleConstrained c c) => GenSymConstrainedSameShape (K1 i c) where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> K1 i c c -> m (K1 i c c)
simpleFreshConstrainedSameShape e
e (K1 c
c) = forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *) e.
(GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> spec -> m a
simpleFreshConstrained e
e c
c

instance (GenSymConstrainedSameShape a) => GenSymConstrainedSameShape (M1 i c a) where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> M1 i c a c -> m (M1 i c a c)
simpleFreshConstrainedSameShape e
e (M1 a c
a) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a

instance
  (GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>
  GenSymConstrainedSameShape (a :+: b)
  where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (:+:) a b c -> m ((:+:) a b c)
simpleFreshConstrainedSameShape e
e (L1 a c
a) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a
  simpleFreshConstrainedSameShape e
e (R1 b c
a) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e b c
a

instance
  (GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>
  GenSymConstrainedSameShape (a :*: b)
  where
  simpleFreshConstrainedSameShape :: forall (m :: * -> *) e c.
(MonadFresh m, MonadError e m, UnionLike m) =>
e -> (:*:) a b c -> m ((:*:) a b c)
simpleFreshConstrainedSameShape e
e (a c
a :*: b c
b) = do
    a c
l :: a c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e a c
a
    b c
r :: b c <- forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e b c
b
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a c
l forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b c
r

-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while
-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo
-- your own types.
--
-- This 'simpleFreshConstrained' implementation is for the types that can be generated with
-- a reference value of the same type.
--
-- For sum types, it will generate the result with the same data constructor.
-- For product types, it will generate the result by generating each field with
-- the corresponding reference value.
--
-- __Note:__ __Can__ be used on recursive types.
derivedSimpleFreshConstrainedSameShape ::
  ( Generic a,
    GenSymConstrainedSameShape (Rep a),
    Mergeable a,
    MonadFresh m,
    MonadError e m,
    UnionLike m
  ) =>
  e ->
  a ->
  m a
derivedSimpleFreshConstrainedSameShape :: forall a (m :: * -> *) e.
(Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a,
 MonadFresh m, MonadError e m, UnionLike m) =>
e -> a -> m a
derivedSimpleFreshConstrainedSameShape e
e a
a = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall a b. (a -> b) -> a -> b
$ (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) (m :: * -> *) e c.
(GenSymConstrainedSameShape a, MonadFresh m, MonadError e m,
 UnionLike m) =>
e -> a c -> m (a c)
simpleFreshConstrainedSameShape e
e (forall a x. Generic a => a -> Rep a x
from a
a)