{-# LANGUAGE AllowAmbiguousTypes, UndecidableInstances #-}

module StreamPatch.HFunctorList where

import Data.Vinyl
import Data.Vinyl.TypeLevel ( RDelete, RIndex )
import Control.Applicative  ( liftA2 )
import GHC.Generics         ( Generic, Rep )
import Foreign.Storable     ( Storable )

import Optics

import Data.Aeson

instance ( ToJSON (Flap a r), Generic (Rec (Flap a) rs)
         , GToJSON' Value Zero (Rep (Rec (Flap a) rs))
         , GToJSON' Encoding Zero (Rep (Rec (Flap a) rs))
         ) => ToJSON (Rec (Flap a) (r ': rs))

-- | A list of functors parametric over a "shared" 'a', where each functor
--   stores a single value 'f a'.
--
-- Just a wrapper on top of Vinyl with some types swap around.
newtype HFunctorList fs a = HFunctorList { forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList :: Rec (Flap a) fs }
    deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (fs :: [k -> *]) (a :: k) x.
Rep (HFunctorList fs a) x -> HFunctorList fs a
forall k (fs :: [k -> *]) (a :: k) x.
HFunctorList fs a -> Rep (HFunctorList fs a) x
$cto :: forall k (fs :: [k -> *]) (a :: k) x.
Rep (HFunctorList fs a) x -> HFunctorList fs a
$cfrom :: forall k (fs :: [k -> *]) (a :: k) x.
HFunctorList fs a -> Rep (HFunctorList fs a) x
Generic)

deriving via (Rec (Flap a) fs) instance ToJSON (Rec (Flap a) fs) => ToJSON (HFunctorList fs a)

deriving instance (ReifyConstraint Show (Flap a) fs, RMap fs, RecordToList fs) => Show (HFunctorList fs a)
deriving instance Eq        (Rec (Flap a) fs) => Eq        (HFunctorList fs a)
deriving instance Ord       (Rec (Flap a) fs) => Ord       (HFunctorList fs a)

-- Right. I only partly get this. As I understand, I'm leveraging deriving via
-- to generate the instance bodies, since they look the same as Rec but with a
-- set functor. So I just have to assure it that you can make it Storable in the
-- same way, given that @Flap a@ is storable (which is handled similarly at its
-- own definition).
deriving via (Rec (Flap a) '[])       instance Storable (HFunctorList '[] a)
deriving via (Rec (Flap a) (f ': fs)) instance (Storable (f a), Storable (Rec (Flap a) fs)) => Storable (HFunctorList (f ': fs) a)

-- It appears we can't do the same for 'Functor' etc., because the @a@ type
-- variable isn't bound, but must be for us to say what type to derive via. I
-- wonder if there is a workaround, but I can't figure it out.
instance Functor (HFunctorList '[]) where
  fmap :: forall a b. (a -> b) -> HFunctorList '[] a -> HFunctorList '[] b
fmap a -> b
_ (HFunctorList Rec (Flap a) '[]
RNil) = forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList forall {u} (a :: u -> *). Rec a '[]
RNil
instance (Functor r, Functor (HFunctorList rs)) => Functor (HFunctorList (r ': rs)) where
  fmap :: forall a b.
(a -> b) -> HFunctorList (r : rs) a -> HFunctorList (r : rs) b
fmap a -> b
f (HFunctorList (Flap r a
r :& Rec (Flap a) rs
rs)) =
    forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList (forall {k} (a :: k) (f :: k -> *). f a -> Flap a f
Flap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f r a
r) forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList Rec (Flap a) rs
rs)))

instance Applicative (HFunctorList '[]) where
  pure :: forall a. a -> HFunctorList '[] a
pure a
_ = forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList forall {u} (a :: u -> *). Rec a '[]
RNil
  HFunctorList Rec (Flap (a -> b)) '[]
RNil <*> :: forall a b.
HFunctorList '[] (a -> b)
-> HFunctorList '[] a -> HFunctorList '[] b
<*> HFunctorList Rec (Flap a) '[]
RNil = forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList forall {u} (a :: u -> *). Rec a '[]
RNil
instance (Applicative r, Applicative (HFunctorList rs)) => Applicative (HFunctorList (r ': rs)) where
  pure :: forall a. a -> HFunctorList (r : rs) a
pure a
a = forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList (forall {k} (a :: k) (f :: k -> *). f a -> Flap a f
Flap (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a) forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a))
  HFunctorList (Flap r (a -> b)
f :& Rec (Flap (a -> b)) rs
fs) <*> :: forall a b.
HFunctorList (r : rs) (a -> b)
-> HFunctorList (r : rs) a -> HFunctorList (r : rs) b
<*> HFunctorList (Flap r a
a :& Rec (Flap a) rs
as) =
    forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList (forall {k} (a :: k) (f :: k -> *). f a -> Flap a f
Flap (r (a -> b)
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> r a
a) forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList (forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList Rec (Flap (a -> b)) rs
fs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList Rec (Flap a) rs
as))

instance Foldable (HFunctorList '[]) where
  foldr :: forall a b. (a -> b -> b) -> b -> HFunctorList '[] a -> b
foldr a -> b -> b
_ b
z (HFunctorList Rec (Flap a) '[]
RNil) = b
z
instance (Foldable r, Foldable (HFunctorList rs)) => Foldable (HFunctorList (r ': rs)) where
    -- only foldmap because foldr is harder looool
    foldMap :: forall m a. Monoid m => (a -> m) -> HFunctorList (r : rs) a -> m
foldMap a -> m
f (HFunctorList (Flap r a
r :& Rec (Flap a) rs
rs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f r a
r forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList Rec (Flap a) rs
rs)

-- this took me ages because I'm stupid T_T
instance Traversable (HFunctorList '[]) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HFunctorList '[] a -> f (HFunctorList '[] b)
traverse a -> f b
_ (HFunctorList Rec (Flap a) '[]
RNil) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList forall {u} (a :: u -> *). Rec a '[]
RNil)
instance (Traversable r, Traversable (HFunctorList rs)) => Traversable (HFunctorList (r ': rs)) where
  traverse
      :: forall f a b. Applicative f
      => (a -> f b)
      -> (HFunctorList (r ': rs)) a
      -> f (HFunctorList (r ': rs) b)
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> HFunctorList (r : rs) a -> f (HFunctorList (r : rs) b)
traverse a -> f b
f (HFunctorList (Flap (r a
r :: r a) :& Rec (Flap a) rs
rs)) =
      forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Rec (Flap b) (r : rs))
rBoth
    where
      rBoth :: f (Rec (Flap b) (r ': rs))
      rBoth :: f (Rec (Flap b) (r : rs))
rBoth = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) f (Flap b r)
rHead f (Rec (Flap b) rs)
rTail
      rHead :: f (Flap b r)
      rHead :: f (Flap b r)
rHead = forall {k} (a :: k) (f :: k -> *). f a -> Flap a f
Flap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f r a
r
      rTail :: f (Rec (Flap b) rs)
      rTail :: f (Rec (Flap b) rs)
rTail = forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f (forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList Rec (Flap a) rs
rs)

-- | Flipped apply: a single value at 'f a', but with "flipped" type arguments.
--   Very useless - has no Functor nor Contravariant nor HFunctor instance.
newtype Flap a f = Flap { forall {k} (a :: k) (f :: k -> *). Flap a f -> f a
getFlap :: f a }
    deriving stock   (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (a :: k) (f :: k -> *) x. Rep (Flap a f) x -> Flap a f
forall k (a :: k) (f :: k -> *) x. Flap a f -> Rep (Flap a f) x
$cto :: forall k (a :: k) (f :: k -> *) x. Rep (Flap a f) x -> Flap a f
$cfrom :: forall k (a :: k) (f :: k -> *) x. Flap a f -> Rep (Flap a f) x
Generic, Int -> Flap a f -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k) (f :: k -> *).
Show (f a) =>
Int -> Flap a f -> ShowS
forall k (a :: k) (f :: k -> *). Show (f a) => [Flap a f] -> ShowS
forall k (a :: k) (f :: k -> *). Show (f a) => Flap a f -> String
showList :: [Flap a f] -> ShowS
$cshowList :: forall k (a :: k) (f :: k -> *). Show (f a) => [Flap a f] -> ShowS
show :: Flap a f -> String
$cshow :: forall k (a :: k) (f :: k -> *). Show (f a) => Flap a f -> String
showsPrec :: Int -> Flap a f -> ShowS
$cshowsPrec :: forall k (a :: k) (f :: k -> *).
Show (f a) =>
Int -> Flap a f -> ShowS
Show, Flap a f -> Flap a f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k) (f :: k -> *).
Eq (f a) =>
Flap a f -> Flap a f -> Bool
/= :: Flap a f -> Flap a f -> Bool
$c/= :: forall k (a :: k) (f :: k -> *).
Eq (f a) =>
Flap a f -> Flap a f -> Bool
== :: Flap a f -> Flap a f -> Bool
$c== :: forall k (a :: k) (f :: k -> *).
Eq (f a) =>
Flap a f -> Flap a f -> Bool
Eq, Flap a f -> Flap a f -> Bool
Flap a f -> Flap a f -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {k} {a :: k} {f :: k -> *}. Ord (f a) => Eq (Flap a f)
forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Bool
forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Ordering
forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Flap a f
min :: Flap a f -> Flap a f -> Flap a f
$cmin :: forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Flap a f
max :: Flap a f -> Flap a f -> Flap a f
$cmax :: forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Flap a f
>= :: Flap a f -> Flap a f -> Bool
$c>= :: forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Bool
> :: Flap a f -> Flap a f -> Bool
$c> :: forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Bool
<= :: Flap a f -> Flap a f -> Bool
$c<= :: forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Bool
< :: Flap a f -> Flap a f -> Bool
$c< :: forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Bool
compare :: Flap a f -> Flap a f -> Ordering
$ccompare :: forall k (a :: k) (f :: k -> *).
Ord (f a) =>
Flap a f -> Flap a f -> Ordering
Ord)
    deriving Ptr (Flap a f) -> IO (Flap a f)
Ptr (Flap a f) -> Int -> IO (Flap a f)
Ptr (Flap a f) -> Int -> Flap a f -> IO ()
Ptr (Flap a f) -> Flap a f -> IO ()
Flap a f -> Int
forall b. Ptr b -> Int -> IO (Flap a f)
forall b. Ptr b -> Int -> Flap a f -> IO ()
forall a.
(a -> Int)
-> (a -> Int)
-> (Ptr a -> Int -> IO a)
-> (Ptr a -> Int -> a -> IO ())
-> (forall b. Ptr b -> Int -> IO a)
-> (forall b. Ptr b -> Int -> a -> IO ())
-> (Ptr a -> IO a)
-> (Ptr a -> a -> IO ())
-> Storable a
forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> IO (Flap a f)
forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> Int -> IO (Flap a f)
forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> Int -> Flap a f -> IO ()
forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> Flap a f -> IO ()
forall k (f :: k -> *) (a :: k). Storable (f a) => Flap a f -> Int
forall k (f :: k -> *) (a :: k) b.
Storable (f a) =>
Ptr b -> Int -> IO (Flap a f)
forall k (f :: k -> *) (a :: k) b.
Storable (f a) =>
Ptr b -> Int -> Flap a f -> IO ()
poke :: Ptr (Flap a f) -> Flap a f -> IO ()
$cpoke :: forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> Flap a f -> IO ()
peek :: Ptr (Flap a f) -> IO (Flap a f)
$cpeek :: forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> IO (Flap a f)
pokeByteOff :: forall b. Ptr b -> Int -> Flap a f -> IO ()
$cpokeByteOff :: forall k (f :: k -> *) (a :: k) b.
Storable (f a) =>
Ptr b -> Int -> Flap a f -> IO ()
peekByteOff :: forall b. Ptr b -> Int -> IO (Flap a f)
$cpeekByteOff :: forall k (f :: k -> *) (a :: k) b.
Storable (f a) =>
Ptr b -> Int -> IO (Flap a f)
pokeElemOff :: Ptr (Flap a f) -> Int -> Flap a f -> IO ()
$cpokeElemOff :: forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> Int -> Flap a f -> IO ()
peekElemOff :: Ptr (Flap a f) -> Int -> IO (Flap a f)
$cpeekElemOff :: forall k (f :: k -> *) (a :: k).
Storable (f a) =>
Ptr (Flap a f) -> Int -> IO (Flap a f)
alignment :: Flap a f -> Int
$calignment :: forall k (f :: k -> *) (a :: k). Storable (f a) => Flap a f -> Int
sizeOf :: Flap a f -> Int
$csizeOf :: forall k (f :: k -> *) (a :: k). Storable (f a) => Flap a f -> Int
Storable via (f a)
    deriving ([Flap a f] -> Encoding
[Flap a f] -> Value
Flap a f -> Encoding
Flap a f -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
forall k (f :: k -> *) (a :: k).
ToJSON (f a) =>
[Flap a f] -> Encoding
forall k (f :: k -> *) (a :: k).
ToJSON (f a) =>
[Flap a f] -> Value
forall k (f :: k -> *) (a :: k).
ToJSON (f a) =>
Flap a f -> Encoding
forall k (f :: k -> *) (a :: k). ToJSON (f a) => Flap a f -> Value
toEncodingList :: [Flap a f] -> Encoding
$ctoEncodingList :: forall k (f :: k -> *) (a :: k).
ToJSON (f a) =>
[Flap a f] -> Encoding
toJSONList :: [Flap a f] -> Value
$ctoJSONList :: forall k (f :: k -> *) (a :: k).
ToJSON (f a) =>
[Flap a f] -> Value
toEncoding :: Flap a f -> Encoding
$ctoEncoding :: forall k (f :: k -> *) (a :: k).
ToJSON (f a) =>
Flap a f -> Encoding
toJSON :: Flap a f -> Value
$ctoJSON :: forall k (f :: k -> *) (a :: k). ToJSON (f a) => Flap a f -> Value
ToJSON, Value -> Parser [Flap a f]
Value -> Parser (Flap a f)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
forall k (f :: k -> *) (a :: k).
FromJSON (f a) =>
Value -> Parser [Flap a f]
forall k (f :: k -> *) (a :: k).
FromJSON (f a) =>
Value -> Parser (Flap a f)
parseJSONList :: Value -> Parser [Flap a f]
$cparseJSONList :: forall k (f :: k -> *) (a :: k).
FromJSON (f a) =>
Value -> Parser [Flap a f]
parseJSON :: Value -> Parser (Flap a f)
$cparseJSON :: forall k (f :: k -> *) (a :: k).
FromJSON (f a) =>
Value -> Parser (Flap a f)
FromJSON) via (f a)

--------------------------------------------------------------------------------

-- | Get the value at a type in an HFunctorList.
hflGet
    :: forall f fs a i
    .  RElem f fs i
    => HFunctorList fs a
    -> f a
hflGet :: forall {k} (f :: k -> *) (fs :: [k -> *]) (a :: k) (i :: Nat).
RElem f fs i =>
HFunctorList fs a -> f a
hflGet = forall {k} (a :: k) (f :: k -> *). Flap a f -> f a
getFlap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList

-- | Put a value at a type in an HFunctorList.
hflPut
    :: forall f f' fs fs' a
    .  RecElem Rec f f' fs fs' (RIndex f fs)
    => f' a
    -> HFunctorList fs a
    -> HFunctorList fs' a
hflPut :: forall {k} (f :: k -> *) (f' :: k -> *) (fs :: [k -> *])
       (fs' :: [k -> *]) (a :: k).
RecElem Rec f f' fs fs' (RIndex f fs) =>
f' a -> HFunctorList fs a -> HFunctorList fs' a
hflPut f' a
x = forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (r :: k) (r' :: k) (rs :: [k]) (rs' :: [k])
       (record :: (k -> *) -> [k] -> *) (f :: k -> *).
(RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f) =>
f r' -> record f rs -> record f rs'
rput' @_ @f (forall {k} (a :: k) (f :: k -> *). f a -> Flap a f
Flap f' a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList

-- | Get a lens to the value at a type in an HFunctorList.
hflLens
    :: forall f f' fs fs' a s t
    .  ( RecElem Rec f f' fs fs' (RIndex f fs)
       , RElem f fs (RIndex f fs)
       , s ~ HFunctorList fs  a
       , t ~ HFunctorList fs' a )
    => Lens s t (f a) (f' a)
hflLens :: forall {k} (f :: k -> *) (f' :: k -> *) (fs :: [k -> *])
       (fs' :: [k -> *]) (a :: k) s t.
(RecElem Rec f f' fs fs' (RIndex f fs), RElem f fs (RIndex f fs),
 s ~ HFunctorList fs a, t ~ HFunctorList fs' a) =>
Lens s t (f a) (f' a)
hflLens = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall {k} (f :: k -> *) (fs :: [k -> *]) (a :: k) (i :: Nat).
RElem f fs i =>
HFunctorList fs a -> f a
hflGet (\s
hfl f' a
x -> forall {k} (f :: k -> *) (f' :: k -> *) (fs :: [k -> *])
       (fs' :: [k -> *]) (a :: k).
RecElem Rec f f' fs fs' (RIndex f fs) =>
f' a -> HFunctorList fs a -> HFunctorList fs' a
hflPut @f f' a
x s
hfl)

-- | Use the value at a type in an HFunctorList, and remove it from the list.
hflStrip
    :: forall f fs a fs' b i is
    .  ( RElem f fs i
       , fs' ~ RDelete f fs
       , RSubset fs' fs is )
    => (f a -> b)
    -> HFunctorList fs a
    -> (b, HFunctorList fs' a)
hflStrip :: forall {k} (f :: k -> *) (fs :: [k -> *]) (a :: k)
       (fs' :: [k -> *]) b (i :: Nat) (is :: [Nat]).
(RElem f fs i, fs' ~ RDelete f fs, RSubset fs' fs is) =>
(f a -> b) -> HFunctorList fs a -> (b, HFunctorList fs' a)
hflStrip f a -> b
f HFunctorList fs a
hfl =
    let hfl' :: HFunctorList fs' a
hfl' = forall {k} (fs :: [k -> *]) (a :: k).
Rec (Flap a) fs -> HFunctorList fs a
HFunctorList forall a b. (a -> b) -> a -> b
$ forall {k1} {k2} (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast forall a b. (a -> b) -> a -> b
$ forall {k} (fs :: [k -> *]) (a :: k).
HFunctorList fs a -> Rec (Flap a) fs
getHFunctorList HFunctorList fs a
hfl
     in (f a -> b
f (forall {k} (f :: k -> *) (fs :: [k -> *]) (a :: k) (i :: Nat).
RElem f fs i =>
HFunctorList fs a -> f a
hflGet HFunctorList fs a
hfl), HFunctorList fs' a
hfl')