{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

{- | This module is the heart of multiwalk, providing generic instances for
   modifying and querying data types.
-}
module Control.MultiWalk.HasSub (
  HasSub (..),
  Spec (..),
  SubSpec (..),
  SelSpec (..),
  Carrier,
  ToSpec,
  ToSpecSel,
  All,
  AllMods,
  GSubTag,
) where

import Control.Applicative (liftA2)
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (..))
import GHC.Generics
import GHC.TypeLits

data Spec
  = SpecList [SubSpec]
  | SpecLeaf
  | -- | Modifiers (used for customizing constraints)
    SpecSelf
      Type

data SubSpec
  = SubSpec
      SelSpec
      -- ^ Constructor and field selectors
      Type
      -- ^ Modifiers (used for customizing constraints)
      Type
      -- ^ Carrier type, should be equal to Carrier of type above (to be aligned
      -- with the target's generic subtypes)

type family Carrier ctag a :: Type

data SelSpec
  = NoSel
  | ConsSel Symbol
  | FieldSel Symbol
  | ConsFieldSel Symbol Symbol

type ToSpec tag (a :: Type) = 'SubSpec 'NoSel a (Carrier tag a)
type ToSpecSel tag (s :: SelSpec) (a :: Type) = 'SubSpec s a (Carrier tag a)

class HasSub ctag tag (ls :: Spec) t where
  modSub ::
    forall c m.
    (Applicative m, AllMods c ls) =>
    Proxy c ->
    (forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)) ->
    t ->
    m t
  getSub ::
    forall c m.
    (Monoid m, AllMods c ls) =>
    Proxy c ->
    (forall s. c s => Proxy s -> Carrier ctag s -> m) ->
    t ->
    m

instance (Carrier tag s ~ t) => HasSub tag ctag ('SpecSelf s) t where
  modSub :: forall (c :: * -> Constraint) (m :: * -> *).
(Applicative m, AllMods c ('SpecSelf s)) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier tag s -> m (Carrier tag s))
-> t
-> m t
modSub Proxy c
_ forall s. c s => Proxy s -> Carrier tag s -> m (Carrier tag s)
f = forall s. c s => Proxy s -> Carrier tag s -> m (Carrier tag s)
f (forall {k} (t :: k). Proxy t
Proxy @s)
  getSub :: forall (c :: * -> Constraint) m.
(Monoid m, AllMods c ('SpecSelf s)) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier tag s -> m) -> t -> m
getSub Proxy c
_ forall s. c s => Proxy s -> Carrier tag s -> m
f = forall s. c s => Proxy s -> Carrier tag s -> m
f (forall {k} (t :: k). Proxy t
Proxy @s)

instance HasSub tag ctag 'SpecLeaf t where
  modSub :: forall (c :: * -> Constraint) (m :: * -> *).
(Applicative m, AllMods c 'SpecLeaf) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier tag s -> m (Carrier tag s))
-> t
-> m t
modSub Proxy c
_ forall s. c s => Proxy s -> Carrier tag s -> m (Carrier tag s)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  getSub :: forall (c :: * -> Constraint) m.
(Monoid m, AllMods c 'SpecLeaf) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier tag s -> m) -> t -> m
getSub Proxy c
_ forall s. c s => Proxy s -> Carrier tag s -> m
_ = forall a. Monoid a => a
mempty

data GSubTag

instance (Generic t, HasSub' ctag (l : ls) 'Nothing 'Nothing (Rep t)) => HasSub ctag GSubTag ('SpecList (l : ls)) t where
  modSub :: forall (c :: * -> Constraint) (m :: * -> *).
(Applicative m, AllMods c ('SpecList (l : ls))) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t
-> m t
modSub Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @(l : ls) @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from
  getSub :: forall (c :: * -> Constraint) m.
(Monoid m, AllMods c ('SpecList (l : ls))) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t -> m
getSub Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @(l : ls) @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from

-- Generic code

type family All (p :: k -> Constraint) (as :: [k]) :: Constraint where
  All p '[] = ()
  All p (a ': as) = (p a, All p as)

type family SpecMods (s :: SubSpec) :: Type where
  SpecMods ('SubSpec _ t _) = t

type family AllMods (p :: Type -> Constraint) (as :: Spec) :: Constraint where
  AllMods p ('SpecList ls) = AllMods' p ls
  AllMods p ('SpecSelf t) = p t
  AllMods p 'SpecLeaf = ()

type family AllMods' (p :: Type -> Constraint) (as :: [SubSpec]) :: Constraint where
  AllMods' p '[] = ()
  AllMods' p (a ': as) = (p (SpecMods a), AllMods' p as)

class HasSub' ctag (ls :: [SubSpec]) (cname :: Maybe Symbol) (sname :: Maybe Symbol) (t :: Type -> Type) where
  modSub' ::
    forall c m p.
    (Applicative m, AllMods' c ls) =>
    Proxy c ->
    (forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)) ->
    t p ->
    m (t p)
  getSub' ::
    forall c m p.
    (Monoid m, AllMods' c ls) =>
    Proxy c ->
    (forall s. c s => Proxy s -> Carrier ctag s -> m) ->
    t p ->
    m

instance
  Carrier ctag t1 ~ t2 =>
  HasSub' ctag ('SubSpec 'NoSel t1 t2 : ls) _a _b (K1 _c t2)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c ('SubSpec 'NoSel t1 t2 : ls)) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> K1 _c t2 p
-> m (K1 _c t2 p)
modSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (K1 t2
x) = 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 s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c ('SubSpec 'NoSel t1 t2 : ls)) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> K1 _c t2 p
-> m
getSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m
f (K1 t2
x) = forall s. c s => Proxy s -> Carrier ctag s -> m
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x

instance
  Carrier ctag t1 ~ t2 =>
  HasSub' ctag ('SubSpec ('FieldSel s) t1 t2 : ls) _a ('Just s) (K1 _c t2)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c ('SubSpec ('FieldSel s) t1 t2 : ls)) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> K1 _c t2 p
-> m (K1 _c t2 p)
modSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (K1 t2
x) = 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 s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c ('SubSpec ('FieldSel s) t1 t2 : ls)) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> K1 _c t2 p
-> m
getSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m
f (K1 t2
x) = forall s. c s => Proxy s -> Carrier ctag s -> m
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x

instance
  Carrier ctag t1 ~ t2 =>
  HasSub' ctag ('SubSpec ('ConsSel s) t1 t2 : ls) ('Just s) _b (K1 _c t2)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c ('SubSpec ('ConsSel s) t1 t2 : ls)) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> K1 _c t2 p
-> m (K1 _c t2 p)
modSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (K1 t2
x) = 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 s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c ('SubSpec ('ConsSel s) t1 t2 : ls)) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> K1 _c t2 p
-> m
getSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m
f (K1 t2
x) = forall s. c s => Proxy s -> Carrier ctag s -> m
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x

instance
  Carrier ctag t1 ~ t2 =>
  HasSub' ctag ('SubSpec ('ConsFieldSel s1 s2) t1 t2 : ls) ('Just s1) ('Just s2) (K1 _c t2)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m,
 AllMods' c ('SubSpec ('ConsFieldSel s1 s2) t1 t2 : ls)) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> K1 _c t2 p
-> m (K1 _c t2 p)
modSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (K1 t2
x) = 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 s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m,
 AllMods' c ('SubSpec ('ConsFieldSel s1 s2) t1 t2 : ls)) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> K1 _c t2 p
-> m
getSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m
f (K1 t2
x) = forall s. c s => Proxy s -> Carrier ctag s -> m
f (forall {k} (t :: k). Proxy t
Proxy @t1) t2
x

instance {-# OVERLAPPABLE #-} HasSub' ctag ls a b (K1 j s) => HasSub' ctag (l : ls) a b (K1 j s) where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c (l : ls)) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> K1 j s p
-> m (K1 j s p)
modSub' = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @ls @a @b
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c (l : ls)) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> K1 j s p
-> m
getSub' = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @ls @a @b

instance HasSub' ctag '[] _a _b (K1 _c _d) where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c '[]) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> K1 _c _d p
-> m (K1 _c _d p)
modSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c '[]) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> K1 _c _d p
-> m
getSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m
_ = forall a. Monoid a => a
mempty

instance
  ( HasSub' ctag s a 'Nothing x
  , HasSub' ctag s a 'Nothing y
  ) =>
  HasSub' ctag s a 'Nothing (x :*: y)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c s) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> (:*:) x y p
-> m ((:*:) x y p)
modSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (x p
x :*: y p
y) = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @s @a @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f x p
x) (forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @s @a @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f y p
y)
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c s) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> (:*:) x y p
-> m
getSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f (x p
x :*: y p
y) = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @s @a @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f x p
x forall a. Semigroup a => a -> a -> a
<> forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @s @a @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f y p
y

instance HasSub' ctag _a _b _c U1 where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c _a) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> U1 p
-> m (U1 p)
modSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c _a) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> U1 p -> m
getSub' Proxy c
_ forall s. c s => Proxy s -> Carrier ctag s -> m
_ = forall a. Monoid a => a
mempty

instance
  ( HasSub' ctag s 'Nothing 'Nothing x
  , HasSub' ctag s 'Nothing 'Nothing y
  ) =>
  HasSub' ctag s 'Nothing 'Nothing (x :+: y)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c s) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> (:+:) x y p
-> m ((:+:) x y p)
modSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (L1 x p
x) = 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 ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @s @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f x p
x
  modSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (R1 y p
x) = 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 ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @s @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f y p
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c s) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> (:+:) x y p
-> m
getSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f (L1 x p
x) = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @s @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f x p
x
  getSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f (R1 y p
x) = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @s @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f y p
x

instance
  HasSub' ctag ls a s x =>
  HasSub' ctag ls a 'Nothing (S1 ('MetaSel s _a _b _c) x)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> S1 ('MetaSel s _a _b _c) x p
-> m (S1 ('MetaSel s _a _b _c) x p)
modSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (M1 x p
x) = 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 ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @ls @a @s Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f x p
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> S1 ('MetaSel s _a _b _c) x p
-> m
getSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f (M1 x p
x) = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @ls @a @s Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f x p
x

instance
  HasSub' ctag ls ('Just s) 'Nothing x =>
  HasSub' ctag ls 'Nothing 'Nothing (C1 ('MetaCons s _a _b) x)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> C1 ('MetaCons s _a _b) x p
-> m (C1 ('MetaCons s _a _b) x p)
modSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (M1 x p
x) = 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 ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @ls @('Just s) @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f x p
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> C1 ('MetaCons s _a _b) x p
-> m
getSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f (M1 x p
x) = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @ls @('Just s) @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f x p
x

instance
  HasSub' ctag ls 'Nothing 'Nothing x =>
  HasSub' ctag ls 'Nothing 'Nothing (D1 _a x)
  where
  modSub' :: forall (c :: * -> Constraint) (m :: * -> *) p.
(Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> D1 _a x p
-> m (D1 _a x p)
modSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f (M1 x p
x) = 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 ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint)
       (m :: * -> *) p.
(HasSub' ctag ls cname sname t, Applicative m, AllMods' c ls) =>
Proxy c
-> (forall s.
    c s =>
    Proxy s -> Carrier ctag s -> m (Carrier ctag s))
-> t p
-> m (t p)
modSub' @ctag @ls @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m (Carrier ctag s)
f x p
x
  getSub' :: forall (c :: * -> Constraint) m p.
(Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m)
-> D1 _a x p
-> m
getSub' Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f (M1 x p
x) = forall ctag (ls :: [SubSpec]) (cname :: Maybe Symbol)
       (sname :: Maybe Symbol) (t :: * -> *) (c :: * -> Constraint) m p.
(HasSub' ctag ls cname sname t, Monoid m, AllMods' c ls) =>
Proxy c
-> (forall s. c s => Proxy s -> Carrier ctag s -> m) -> t p -> m
getSub' @ctag @ls @'Nothing @'Nothing Proxy c
p forall s. c s => Proxy s -> Carrier ctag s -> m
f x p
x